The Coq mailing list

[gallais <guillaume.allais AT ens-lyon.fr>]

I really doubt it's provable at all.

==================================================
Require Import Utf8.

Axiom existence_exists : forall {A} (a : A) (P : A → Prop), (∃ y : A, P 
y) = P a.

Theorem Argh : False.
  pose (P := fun (b : bool) => if b then False else True).
  fold (P true).
  rewrite <- existence_exists.
  exists false ; constructor.
Qed.
==================================================

On 08/08/14 07:45, Arthur Azevedo de Amorim wrote:
> This lemma is not provable in the basic theory of Coq. In order to prove
> it, you need to add an axiom to the theory, such as propositional
> extensionality:
>
> forall P Q : Prop, P <-> Q -> P = Q
>
> This definition is available in the standard library (you can look it up in
> the manual), but it was recently found to be inconsistent with the rest of
> the theory. Thus, it might be better to use just logical equivalence <->
> instead of equality until this problem is fixed.
> On Aug 8, 2014 8:36 AM, "John Wiegley" 
> <johnw AT newartisans.com>
>  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?
> >
> > Thank you,
> >    John