Stream: math-comp users

Topic: Instantiate [exists _, _]


view this post on Zulip Ana de Almeida Borges (Oct 20 2022 at 12:03):

Is there a way to provide a witness to a goal of the form [exists _, _] without first applying existsP? Basically something analogous to rewriting with a hypothesis H : b = true when our goal is b && b' instead of going through apply/andP; split=> //.

view this post on Zulip Cyril Cohen (Oct 20 2022 at 12:26):

Not that I know of, but we could add

Lemma existsb (T : finType) (P : {pred T}) (x : T) : P x -> [exists x, P x].
Proof. by move=> Px; apply/existsP; exists x. Qed.
Arguments existsb {T P}.

So that rewrite (existsb x). would do what you want?

view this post on Zulip Ana de Almeida Borges (Oct 20 2022 at 12:43):

Yes! Thanks


Last updated: Feb 08 2023 at 07:02 UTC