The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Note that we can build a similar contradiction without using a pattern 
matching with no branches :

Require Import ClassicalFacts.

Inductive True1 : Prop := I1 : True1
with True2 : Prop := I2 : True1 -> True2.

Section func_unit_discr.
 
 Hypothesis Heq : True1 = True2.
 
 Fixpoint contradiction (u : True2) : False :=
 contradiction (
     match u with
       | I2 Tr =>
          match Heq in (_ = T) return T with
          | eq_refl => Tr
          end
     end).
 
End func_unit_discr.

Lemma foo : provable_prop_extensionality -> False.
Proof.
 intro; apply contradiction.
 etransitivity. apply H. constructor.
 symmetry. apply H. constructor. constructor.
 constructor. constructor.
Qed.


I am not sure I have understood the tentative fix of Christine Paulin, but it 
seems like this would not solve this case either (True1 and True2 are in the 
same inductive definition. 

-- 
JH

----- Mail original -----
> De: "Maxime Dénès" 
> <mail AT maximedenes.fr>
> À: 
> coq-club AT inria.fr
> Envoyé: Jeudi 12 Décembre 2013 22:41:18
> Objet: [Coq-Club] Propositional extensionality is inconsistent in Coq
> 
> 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.
>