The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi folks,

Arthur and I refined Daniel's example to show that Propositional 
Extensionality (even the weaker version of it) as defined in Coq's 
standard library is inconsistent in Coq's current theory:


---------------------------------------------

Require Import ClassicalFacts.

Section func_unit_discr.

Hypothesis Heq : (False -> False) = True.

Fixpoint contradiction (u : True) : False :=
contradiction (
        match Heq in (_ = T) return T with
        | eq_refl => fun f:False => match f with end
        end
        ).

End func_unit_discr.

Lemma foo : provable_prop_extensionality -> False.
Proof.
intro; apply contradiction.
apply H.
trivial.
trivial.
Qed.

Print Assumptions foo.

Print provable_prop_extensionality.

---------------------------------------------

(Typechecked with Coq 8.4pl2).

Was that fact known?

Maxime.