The Coq mailing list

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

Oh, I see.

Am I wrong if I say that this "recursive subterm" notion is superseeded by the criterion Christine Paulin is proposing ? That is, with this other criterion, we would not be able to use a subterm that is not recursive ?

---

De: "Matthieu Sozeau" <mattam AT mattam.org>
À: "Jacques-Henri Jourdan" <jacques-henri.jourdan AT inria.fr>
Cc: "Maxime Dénès" <mail AT maximedenes.fr>, coq-club AT inria.fr
Envoyé: Vendredi 13 Décembre 2013 14:07:47
Objet: Re: [Coq-Club] Propositional extensionality is inconsistent in Coq

Tr is not a recursive subterm of u here. The initial exemple relies on the fact that there is no recursive subterm to consider, ie the condition is vacuously true.

Le vendredi 13 décembre 2013, Jacques-Henri Jourdan a écrit :

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

--
-- Matthieu