The Coq mailing list

[Cristóbal Camarero Coterillo <nakacristo AT hotmail.com>]

I have got another example. This one without empty branches nor using mutually inductive types.

Axiom prop_ext: forall P Q, (P<->Q)->P=Q.

Inductive True2:Prop:= I2: (False->True2)->True2.

Theorem Heq: (False->True2)=True2.
Proof.
apply prop_ext. split.
- intros. constructor. exact H.
- intros. exact H.
Qed.

Fixpoint con (x:True2) :False :=
match x with
I2 f => con (match Heq with eq_refl => f end)
end.

Theorem contradiction:False.
Proof.
apply con. constructor. intros.
destruct H.
Qed.


Following the arguments of my previous email, if we rewrite (False->True2)=True2 in the inductive definition we would get
Inductive True2:Prop:= I2: True2->True2.
which is False when the original is True.


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