Patrick Nicodemus (Jan 14 2023 at 20:01): Patrick Nicodemus (Jan 14 2023 at 20:01):Is there a lemma in finType or another closely related library relating "has P (enum A)" to "[exists x : A , P]"? I could not find one
Reynald Affeldt (Jan 14 2023 at 21:54):maybe look around hasP?
Reynald Affeldt (Jan 14 2023 at 21:57):(and of course existsP to move from Prop to bool for existential quantification over a finType)
Patrick Nicodemus (Jan 15 2023 at 00:12):Thank you!
Pierre Jouvelot (Jan 15 2023 at 11:59):I only managed to get this weaker version of an equivalence:
Lemma foo (A : finType) (P : A -> bool) :
(#|A| = size (index_enum A) -> [exists x : A, P x] -> has P (enum A)) /\
(has P (enum A) -> [exists x : A, P x]).
Proof.
split=> [eqcAs /existsP [] x px|/hasP [x _ px]].
- apply/hasP.
exists x => //.
apply/(nthP x).
exists (index x (index_enum A)).
- by rewrite size_map -enumT -cardT eqcAs index_mem mem_index_enum.
- have ltxs : index x (index_enum A) < size (index_enum A) by rewrite index_mem.
by rewrite (nth_map x) // -enumT -deprecated_filter_index_enum // (nth_map x) // nth_index.
- apply/existsP.
by exists x.
Qed.
One problem to get the stronger version might be to find how to mix properly eqType and finType.
Paolo Giarrusso (Jan 15 2023 at 12:37):Added bar, but I was expecting to find it:
Lemma bar (A : finType) :
#|A| = size (index_enum A).
Proof.
rewrite [card]unlock /enum_mem [index_enum A]unlock.
by elim: (Finite.enum A) => //= _ l ->.
Qed.
Lemma foo' (A : finType) (P : A -> bool) :
([exists x : A, P x] -> has P (enum A)) /\
(has P (enum A) -> [exists x : A, P x]).
Proof.
split=> [/existsP [] x px|/hasP [x _ px]].
- apply/hasP.
exists x => //.
apply/(nthP x).
exists (index x (index_enum A)).
- by rewrite size_map -enumT -cardT bar index_mem mem_index_enum.
- have ltxs : index x (index_enum A) < size (index_enum A) by rewrite index_mem.
by rewrite (nth_map x) // -enumT -deprecated_filter_index_enum // (nth_map x) // nth_index.
- apply/existsP.
by exists x.
Qed.
(EDIT: foo -> foo')
Paolo Giarrusso (Jan 15 2023 at 12:39):I've read the comment on deprecated_filter_index_enum (below for others), but it seems that bar will remain true even when enum and index_enum/Finite.enum are just permutations?
(* Legacy mathcomp scripts have been relying on the fact that enum A and *)
(* filter A (index_enum T) are convertible. This is likely to change in the *)
(* next mathcomp release when enum, pick, subset and card are generalised to *)
(* predicates with finite support in a choiceType - in fact the two will only *)
(* be equal up to permutation in this new theory. *)
I don't know if the above proof is robust, but I guess the library could expose one?
About "mixing eqType and finType properly — finType coerces to eqType, so isn't quantifying over finType fine?
In both cases, I'm no math-comp expert so corrections welcome
Pierre Jouvelot (Jan 15 2023 at 14:40):Thanks for the bar lemma. I didn't think of unlocking those definitions, expecting I was just missing something already existing.
As for the finType vs. eqType remark, this was related to the fact that has uses equality in its definition, something not immediately visible in the definition of the finite exists property. But the coercion you mention should work.
Paolo Giarrusso (Jan 15 2023 at 15:37):I think I agree something's missing — I guess perm_eq (enum A) (Finite.enum A) would survive the planned change and suffice for these proofs?
Pierre Jouvelot (Jan 15 2023 at 19:51):Paolo Giarrusso said:
I think I agree something's missing — I guess
perm_eq (enum A) (Finite.enum A)would survive the planned change and suffice for these proofs?
Indeed, that would work:
Lemma foo (A : finType) (P : A -> bool) (penum : perm_eq (enum A) (Finite.enum A)) :
[exists x : A, P x] <-> has P (enum A).
Proof.
split=> [/existsP [x px]|/hasP [x _ px]].
- apply/hasP.
exists x => //.
by rewrite (perm_mem penum) mem_index_enum.
- apply/existsP.
by exists x.
Qed.
what about ?
Lemma foo (A : finType) (P : pred A) :
[exists x : A, P x] = has P (enum A).
Proof. by apply/existsP/hasP=> [] [x Hx]; exists x; rewrite ?enumT. Qed.
Patrick Nicodemus said:
Is there a lemma in finType or another closely related library relating "has P (enum A)" to "[exists x : A , P]"? I could not find one
Thanks to @Paolo Giarrusso's suggestion, here is the proof of equivalence of these propositions:
Lemma perm_enum {A : finType} : perm_eq (enum A) (Finite.enum A).
Proof. by rewrite enumT. Qed.
Lemma exists_has {A : finType} (P : A -> bool) : [exists x : A, P x] <-> has P (enum A).
Proof.
split=> [/existsP [x px]|/hasP [x _ px]]; last by apply/existsP; exists x.
by apply/hasP; exists x => //; rewrite (perm_mem perm_enum) mem_index_enum.
Qed.
Maybe this could be added to the finType library.
Pierre Jouvelot (Jan 16 2023 at 10:03):Laurent Théry said:
what about ?
Lemma foo (A : finType) (P : pred A) : [exists x : A, P x] = has P (enum A). Proof. by apply/existsP/hasP=> [] [x Hx]; exists x; rewrite ?enumT. Qed.
Indeed! This is even nicer :smile:
Last updated: Oct 13 2024 at 01:02 UTC