Stream: math-comp users

Topic: finmap and key

Marie Kerjean (Nov 21 2020 at 10:52):

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|

Cyril Cohen (Nov 24 2020 at 15:38):

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.

Cyril Cohen (Nov 24 2020 at 15:39):

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

Christian Doczkal (Nov 24 2020 at 15:46):

@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)

Cyril Cohen (Nov 24 2020 at 15:48):

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

Cyril Cohen (Nov 24 2020 at 15:50):

(like in matrix to see another example)

Christian Doczkal (Nov 24 2020 at 15:57):

@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.

Cyril Cohen (Nov 24 2020 at 16:09):

I cannot tell anymore... :sad:

Paolo Giarrusso (Nov 24 2020 at 16:40):

unification behavior is unspecified and subject to change.

Paolo Giarrusso (Nov 24 2020 at 16:40):

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

Bas Spitters (Nov 25 2020 at 10:04):

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

Christian Doczkal (Nov 25 2020 at 12:29):

@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).

Cyril Cohen (Nov 25 2020 at 12:45):

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

Marie Kerjean (Nov 25 2020 at 13:49):

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.

Christian Doczkal (Nov 25 2020 at 13:54):

@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:

Marie Kerjean (Nov 25 2020 at 13:56):

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 ?

Cyril Cohen (Nov 25 2020 at 13:57):

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

Christian Doczkal (Nov 25 2020 at 14:05):

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.

Enrico Tassi (Nov 25 2020 at 14:08):

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

Enrico Tassi (Nov 25 2020 at 14:08):

So adding one about tt rather than a variable k or _ may just work

Marie Kerjean (Nov 26 2020 at 15:06):

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 ?

Christian Doczkal (Nov 26 2020 at 16:03):

@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.

Marie Kerjean (Nov 26 2020 at 16:19):

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) ?

Christian Doczkal (Nov 26 2020 at 16:31):

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)

Christian Doczkal (Nov 26 2020 at 16:32):

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

Marie Kerjean (Nov 26 2020 at 16:34):

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.

Christian Doczkal (Nov 26 2020 at 16:38):

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?

Christian Doczkal (Nov 26 2020 at 16:39):

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

Marie Kerjean (Nov 26 2020 at 16:41):

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

Christian Doczkal (Nov 26 2020 at 16:46):

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.

Christian Doczkal (Nov 26 2020 at 16:46):

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

Marie Kerjean (Nov 26 2020 at 16:48):

As a user of math-comp-analysis I am very happy with epsilon :). Thank you very much for your insights !

Christian Doczkal (Nov 26 2020 at 16:50):

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

Marie Kerjean (Nov 26 2020 at 17:00):

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)) ).

Marie Kerjean (Nov 26 2020 at 17:01):

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

Christian Doczkal (Nov 26 2020 at 17:07):

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.

Marie Kerjean (Nov 26 2020 at 17:25):

Still, the definition fset val n | n in 'I_4 & p (val n)] seems the easiest to use. thanks !

Guillaume Dubach (Jan 25 2021 at 10:52):

@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...

Guillaume Dubach (Jan 25 2021 at 10:54):

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)...

Christian Doczkal (Jan 25 2021 at 10:59):

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 (Jan 25 2021 at 10:59):

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

Christian Doczkal (Jan 25 2021 at 11:03):

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.

Guillaume Dubach (Jan 25 2021 at 11:07):

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!

Marie Kerjean (Jan 25 2021 at 11:09):

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 ?

Christian Doczkal (Jan 25 2021 at 11:25):

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.

Guillaume Dubach (Jan 25 2021 at 13:07):

@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".

Cyril Cohen (Jan 25 2021 at 13:15):

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

Cyril Cohen (Jan 25 2021 at 13:15):

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.

Guillaume Dubach (Feb 05 2021 at 16:03):

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 ?

Christian Doczkal (Feb 05 2021 at 16:48):

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.

Christian Doczkal (Feb 05 2021 at 16:50):

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.

Cyril Cohen (Feb 06 2021 at 00:03):

Christian Doczkal said:

IIUC, [eqType of A] is usually not convertible 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?

Enrico Tassi (Feb 06 2021 at 08:33):

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

Christian Doczkal (Feb 06 2021 at 10:32):

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:

Christian Doczkal (Feb 06 2021 at 11:07):

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: Oct 13 2024 at 01:02 UTC