Stream: math-comp users

Topic: has vs exists


view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Jan 14 2023 at 21:54):

maybe look around hasP?

view this post on Zulip Reynald Affeldt (Jan 14 2023 at 21:57):

(and of course existsP to move from Prop to bool for existential quantification over a finType)

view this post on Zulip Patrick Nicodemus (Jan 15 2023 at 00:12):

Thank you!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 12:37):

(EDIT: foo -> foo')

view this post on Zulip 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.                             *)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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