The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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