The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Hi,

Do you have any pointers about propositional extensionality being found inconsistent with CiC?

Thanks,

-Eddy

On Aug 7, 2014, at 11:45 PM, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> 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