The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Oops, indeed; the two propositions are not equivalent, even less equal. To make it provable, you would need to use propositional extensionality and assume that P a is provable:

Axiom prop_ext : forall P Q : Prop, P <-> Q -> P = Q.

Lemma existence_exists :

  forall A (P : A -> Prop) (a : A),

    P a ->

    (exists x, P x) = P a.

Proof.

  intros A P a H.

  apply prop_ext; eauto.

Qed.

 

On Aug 8, 2014 2:32 PM, "Adam Chlipala" <adamc AT csail.mit.edu> wrote:

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?