I'm a new user to `finmap.v`

and the use of `key`

is not immediate for me. Typically, for proving the equality between `f @ A`

and `A`

when `f `

in injective, should one try to use `card_imfset`

or rewrite and go through `card_imset`

? Why does `card_imfset`

use `key`

?

```
card_imfset
: forall (key : unit) (T T' : choiceType) (f : T -> T') (p : finmempred T),
injective f -> #|` imfset key f p| = size (enum_finmem p)
card_imset
: forall (aT rT : finType) (f : aT -> rT) (D : {pred aT}),
injective f -> #|[set f x | x in D]| = #|D|
```

The `key`

is an opaque element of type `unit`

in order to prevent Coq to diverge during some unification/conversion tests in failure cases.

You can and should "ignore" it.

If you need to provide an element, you can provide `tt`

.

@Cyril Cohen I think (at least part of) the question is why this is necessary for `finmap`

but not for `finset`

. After all, the keys to cause some usability issues, e.g. that unfolding operations like `fsetI`

can lead to sets that look like (default) instances of `imfset`

but are not. (cf. https://github.com/math-comp/finmap/issues/73)

The answer to that question is that conversion happened to diverge for `fset`

...

(like in `matrix`

to see another example)

@Cyril Cohen Trusting that you don't introduce this kind of complexity without good reason, this answer does not help much. So let me rephrase my question as follows: Can you describe what's the difference between `finmap`

and `finset`

that causes unification/conversion to diverge for the former but not for the latter.

I cannot tell anymore... :sad:

unification behavior is unspecified and subject to change.

I admit I'm "butting in", but 8.12 broke some code that accidentally relied on good unification performance, and some suggested the bug report is a WONTFIX

@Marie Kerjean and others notes that there is also the finmap library by @Arthur Azevedo de Amorim and there are plans to merge them.

@Bas Spitters , Could you provide us with a link to said alternative library and detail what you mean by "plans to merge them"? I wasn't aware of Arthur's library nor of any plans to merge `finmap`

with anything (other than maybe `mathcomp`

).

cf https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/How.20to.20use.20finset

Christian Doczkal said:

Cyril Cohen I think (at least part of) the question is why this is necessary for

`finmap`

but not for`finset`

. After all, the keys to cause some usability issues, e.g. that unfolding operations like`fsetI`

can lead to sets that look like (default) instances of`imfset`

but are not. (cf. https://github.com/math-comp/finmap/issues/73)

Indeed, @Christian Doczkal you are better at expressing this than I am ! So I understand that `key`

is necessary at the moment but should be ignored. I will try to use `card_imfset`

again.

@Marie Kerjean , that's the gist of it, indeed. Just be aware that the notation for `imfset`

hide the key, meaning that `imfset`

expressions that look the same can be non-convertible due to different keys. So, try not to unfold the basic operations. :grinning:

Christian Doczkal said:

Marie Kerjean , that's the gist of it, indeed. Just be aware that the notation for

`imfset`

hide the key, meaning that`imfset`

expressions that look the same can be non-convertible due to different keys. So, try not to unfold the basic operations. :grinning:

Should this basic rule be added to header ?

Maybe the key should be displayed if it's not tt actually!!

Cyril Cohen said:

Maybe the key should be displayed if it's not tt actually!!

That would be one way to avoid the pit I fell into.

Cyril Cohen said:

Maybe the key should be displayed if it's not tt actually!!

FTR from 8.13 more "specific" notations win https://github.com/coq/coq/pull/12984

So adding one about `tt`

rather than a variable `k`

or `_`

may just work

What is the good way to construct an instance of an `A : finset T`

? Let us suppose that I have a predricate `p : T -> bool`

, am I supposed to encode it as a sequence to encode it as a finset using its properties or is there another way ? In the first case, is there an example that I can look at ?

@Marie Kerjean Unless `T`

has a `finType`

structure, there is no reason for an arbitrary predicate over `T`

to be representable using a finite set. Indeed, the usual way to define an element of `{fset T}`

is by some form of separation/replacement (`imfset`

) using a predicate that is statically known to have only finitely many elements (`finmempred`

). And, indeed, `seq T`

has a finmempred structure, so `[fset x in s]`

for `s : seq T`

works.

I should have specified that I am interested in specific instances of `T`

and `p`

where this is true, for example `p := fun (n : nat) => (n *n <= 9))`

. So I should give a `finmempred`

structure to `p`

, and this is done by proving ` is_finite (fun x => in_mem x p)`

?

This is one way, another way is the following set `Definition A := [fset val n | n in 'I_4 & p (val n)].`

(in this case the `p`

becomes redundant though)

Unfortunately, this is a "proper replacement" and maybe not that easy to work with.

This works only for a predicate `p`

on `nat`

for which we have an explicit upper bound on the elements in `p`

. In my case I could mathematically prove that `p`

is finite, but not have an explicit bound.

I'm not sure I follow. The definition of `is_finite`

is "there exists a list enumerating the predicate", so if you can prove that, then this list is an upper bound, right?

This is sometime called "Kurarowski finite" IIRC, it's a rather strict notion of finiteness, but it works really well constructively.

Indeed, and I think I was trying to know if there was an alternative to this strict version of finiteness for using `finmap`

. Thanks !

That's a good question. With sufficient classical assumptions (XM+epsilon) you should be able to prove that the notions of finiteness coincide and define a generic instance for that.

But without epsilon, I guess you're out of luck.

As a user of `math-comp-analysis`

I am very happy with epsilon :). Thank you very much for your insights !

Just out of curiosity, what is your definition of finiteness?

Intuitively, and I understand now that there is no hope to handle it without axioms, it would be "not infinetess". That is ` ~~ (forall n : nat, exists2 m, (n <= m) /\ p m)) )`

.

Sorry, I am really not a constructivist, and this gives me a hard time with Coq sometimes.

Yes, but with XM+epsilon it should be fairly straightforward to "prove" `not_infinite p -> is_finite p`

. I say "prove" because the conclusion is a structure rather than a Proposition.

Still, the definition `fset val n | n in 'I_4 & p (val n)]`

seems the easiest to use. thanks !

@Christian Doczkal @Marie Kerjean Two more questions on this topic: First, I see now how to build an {fset K} from a finmempred on K, but what exactly is the syntax to build a finmempred in the first place? Assuming that I have a predicate p and a proof of (is_finite p), I do not manage to write down the corresponding finmempred object...

Second question: when I define an fset using "fset val n" as suggested above, the definition is accepted but I cannot unfold the definition of the set using inE ("rewrite !inE" and related tactics do not seem to work in this case)...

The second one is easy, `[fset f x | x in p]`

is a "proper" replacement, not a "separation" so `inE`

does not work. However, in the particular case where `f`

is `val`

there are `in_fset_val`

and `val_in_fset`

depending on whether the element is already of the form `val x`

or not.

In the general case, one would of course use `imfsetP`

.

For the other one, the most idiomatic way of constructing finite sets is to carve them out of a finite superset as above, with the `finmempred`

being something that's canonically finite (e.g., a finite type, a list, or another finite set). I've never had to manually prove `is_finite p`

.

All right, in that case I will stick to this method and unfold the definition of 'I_p properly. Thank you very much for your explanations!

I also tried to use `finmempred`

and did not succeed. It seems to me that this is the most mathematically intuitive way to proceed however. Maybe @Cyril Cohen could help ?

Okay, it seems not that hard after all:

```
Section finmem.
Variable (T : eqType) (p : {pred T}) (fin_p : is_finite p).
Definition finmem_p : finmempred T := @FinMemPred T (mem p) fin_p.
Goal forall x : T, (x \in p) = (x \in finmem_p). by []. Abort.
End finmem.
```

@Christian Doczkal This is very clear, thanks! One last question: when I do the same using "nat" instead of T: eqType, it doesn't work. I would have thought that nat could be considered as an eqType automatically. But I get the error message: In environment p : {pred nat}

fin_p : is_finite p

The term "nat" has type "Set" while it is expected to have type "eqType".

The interface was not designed to do that, but indeed this would be missing...

Guillaume Dubach said:

Christian Doczkal This is very clear, thanks! One last question: when I do the same using "nat" instead of T: eqType, it doesn't work. I would have thought that nat could be considered as an eqType automatically. But I get the error message: In environment p : {pred nat}

fin_p : is_finite p

The term "nat" has type "Set" while it is expected to have type "eqType".

To get the same result with nat write `[eqType of nat]`

where you get the error message.

Christian Doczkal said:

The second one is easy,

`[fset f x | x in p]`

is a "proper" replacement, not a "separation" so`inE`

does not work. However, in the particular case where`f`

is`val`

there are`in_fset_val`

and`val_in_fset`

depending on whether the element is already of the form`val x`

or not.

@Christian Doczkal Sorry to got back to this but actually I do not manage to use in_fset_val and val_in_fset... I have a `proper replacement' A:{fset nat} of the kind you mention above and none of these lemmas allow me to transform a sentence like x \in A into a proposition about x... Am I missing something about the syntax ?

Indeed, having a closer look, the type of `in_fset_val`

. In particular, the `(p : finmempred [eqType of A])`

looks strange to me. IIUC, `[eqType of A] `

is usually *not* convertible to the canonical `eqType`

instance inferred for `A`

, if `A`

has one, that is. This might be related to @Cyril Cohen s earlier comment.

Of course, for the particular shape I mentioned above, you can easily prove an unfolding lemma using `imfsetP`

:

```
Lemma foo (k : nat) (p : {pred nat}) (A := [fset val n | n in 'I_k & p (val n)]) x :
(x \in A) = (x < k) && (x \in p).
Proof.
apply/imfsetP/andP => /= [[z ? -> //]|[lt_x_k px]].
by exists (Sub x lt_x_k).
Qed.
```

And the same should work for variations.

Christian Doczkal said:

IIUC,

`[eqType of A]`

is usuallynotconvertible to the canonical`eqType`

instance inferred for`A`

, if`A`

has one, that is.

Unless I missed something it is... `[eqType of A]`

triggers a unification and outputs the inferred canonical `eqType`

instance for `A`

. Why would you think otherwise?

I think it may be syntactically different, but for sure convertible. There is likely to be a beta redex involving a Phant...

Enrico Tassi said:

I think it may be syntactically different, but for sure convertible. There is likely to be a beta redex involving a Phant...

Indeed, Enrico seems to be right. I just remembered that replacing say `[finType of A + B]`

with `sum_finType A B`

(for large `A`

and `B`

) lead to much smaller terms and alleviated (to some degree) some efficiency problems I ran into when nesting graph operations. So I knew they differ significantly, but apparently not enough for Coq to distinguish them :grinning_face_with_smiling_eyes:

So, for the record, `in_fset_val`

does not work, because it's type restricts `p`

to be a `finmempred`

over an `fset_sub_type`

rather than an arbitrary subtype.

The lemma I would have expected in its place is:

```
Lemma in_fset_val' (key : unit) (K : choiceType) (p : {pred K})
(sK : subType p) (fp : finmempred [eqType of sK]) (x : K) :
x \in imfset key val fp = match insub x with
| Some a => in_mem a fp
| None => false
end.
Proof.
apply/imfsetP/idP => /= [[z fp_z ->]|]; first by rewrite valK.
by case: insubP => // u px ux fp_u; exists u.
Qed.
```

the same goes for `in_fset_valP`

which seems more useful, as it avoids the use if `insub`

. :shrug:

Last updated: Dec 07 2023 at 14:02 UTC