The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I suggest reading the lemma statement more carefully.  IMO, it's clearly 
false even in common intuitive interpretations, and Coq agrees.

Theorem not_existence_exists : ~(forall A (a : A) (P : A -> Prop), 
(exists y : A, P y) = P a).
Proof.
  intro Hnee.
  specialize (Hnee bool false (eq true)).
  assert (exists y, true = y) by eauto.
  rewrite Hnee in H.
  discriminate.
Qed.


On 08/08/2014 02:35 AM, John Wiegley wrote:
> I'm trying to prove the following lemma:
>
>    Lemma existence_exists {A} (a : A) (P : A → Prop) : (∃ y : A, P y) = P a.
>
> I cannot find the right tactic to prove that given 'a', these two statements
> are effectively equal.  Any hints?