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

maybe look around `hasP`

?

(and of course `existsP`

to move from `Prop`

to `bool`

for existential quantification over a `finType`

)

Thank you!

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`

.

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

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

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.

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?

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.

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