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

view this post on Zulip Notification Bot (Nov 03 2022 at 16:38):

Cyril Cohen has marked this topic as resolved.

view this post on Zulip Pierre Roux (Nov 04 2022 at 08:42):

@Ana de Almeida Borges added: https://github.com/math-comp/math-comp/pull/941

view this post on Zulip Ana de Almeida Borges (Nov 04 2022 at 11:35):

Awesome!


Last updated: Oct 13 2024 at 01:02 UTC