Stream: math-comp users

Topic: has vs exists

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

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

Paolo Giarrusso (Jan 15 2023 at 12:37):

(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.                             *)
``````

Paolo Giarrusso (Jan 15 2023 at 12:45):

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 `unlock`ing 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.
``````

Laurent Théry (Jan 16 2023 at 09:54):

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

Pierre Jouvelot (Jan 16 2023 at 10:00):

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: Jul 15 2024 at 21:02 UTC