The Coq mailing list

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

I tried to adapt this example to find an example were there is no need to 
match over False. However, the guard conditions forbids me:

 Inductive True2 : Prop :=
   I2 : True -> True2.

 Hypothesis Heq : True = True2.
 
 Fixpoint contradiction (u : True2) : False :=
   match u with I2 Tr =>
      contradiction (match Heq in (_ = T) return T with eq_refl => Tr end)
   end.

So, what happens in this case ? Does this check be extended to make Coq 
reject the other construction ?

-- 
JH Jourdan

----- 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.
>