The Coq mailing list

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

We can find the inconsistency in another way. Instead of changing the type of the subterm here I change the type of the fixpoint itself.

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

(************)

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

Theorem T1T: True1=True.
Proof.
apply prop_ext;split;auto.
intros. constructor.
Qed.

Theorem T2T: True2=True.
Proof.
apply prop_ext;split;auto.
intros. constructor. rewrite T1T. exact H.
Qed.

Theorem T2F_T1F: (True2->False)=(True1->False).
Proof.
rewrite T2T. rewrite T1T. reflexivity.
Qed.

Fixpoint con1 (x:True2) :False :=
match x with
I2 y => (match T2F_T1F in _=T return T with eq_refl=>con1 end) y
end.


(***********)

Inductive True3:Prop:= I3: (False->True3)->True3.

Theorem T3T: True3=True.
Proof.
apply prop_ext;split;auto.
intros. constructor. apply False_rect.
Qed.

Theorem T3F_FT3F : (True3->False)=((False->True3)->False).
Proof.
rewrite T3T.
apply prop_ext;split;auto.
Qed.

Fixpoint con2 (x:True3) :False :=
match x with
I3 f => (match T3F_FT3F in _=T return T with eq_refl=>con2 end) f
end.


(************)


For the case of the empty branch it does not work. I fails with "Recursive call to con1 has not enough arguments."

Theorem TF_F: (True->False)=False.
Proof.
apply prop_ext;split;auto.
Qed.

Fixpoint con3 (x:True) :False :=
match
 match TF_F in _=T return T with eq_refl=> con3 end
with end.

---

Date: Tue, 17 Dec 2013 18:33:05 +0100
From: christine.paulin AT lri.fr
To: nakacristo AT hotmail.com
CC: jacques-henri.jourdan AT inria.fr; mail AT maximedenes.fr; coq-club AT inria.fr
Subject: Re: [Coq-Club] Propositional extensionality is inconsistent in Coq

Yes it is true that if you can build a generic relation

lower: forall {T:Type}, T->True2->Prop
such that  (lower Tr (l2 Tr))

then you can prove your match term is smaller

but could you prove it is well-founded ? I doubt it (because of the parametricity)

my point was to stay with the relation associated to the inductive definitions comparing objects in True1 and True2 only

Christine

On 12/17/2013 06:06 PM, Cristóbal Camarero Coterillo wrote:

The hypothesis "forall y:False, f y < x" certainly does not give any information and we cannot prove "(match Heq in (False->True2=True2) return fun X _ => X with eq_refl => f end) < x" .

But returning to the example of the mutually inductive type we can do the following (by adding proof-irrelevance):

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

(*proof-irrelevance for eq*)
Axiom destruct_eq: forall {T:Type} {x:T} (H:x=x), H=eq_refl.

Theorem structural: forall (lower: forall {T:Type}, T->True2->Prop) (x:True2),
match x with
I2 Tr => (lower Tr x)
  -> lower (match Heq with eq_refl => Tr end) x
end.
Proof.
intros. destruct x.
set(Heq':=Heq). clearbody Heq'.
set(I2':=I2). clearbody I2'.
revert t Heq' I2'. rewrite Heq.
intros. rewrite (destruct_eq Heq').
exact H.
Qed.

End func_unit_discr.

I think the theorem "structural" is what is required for the fixpoint to work.
Although Heq cannot be immediately eliminated we can work around it.

> Date: Mon, 16 Dec 2013 20:35:08 +0100
> From: Christine.Paulin AT lri.fr
> To: nakacristo AT hotmail.com
> CC: jacques-henri.jourdan AT inria.fr; mail AT maximedenes.fr; coq-club AT inria.fr
> Subject: Re: [Coq-Club] Propositional extensionality is inconsistent in Coq
>
>
> >
> > 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.
> Very nice example but we should not misinterpret this last point
> in order to identify
>
> Inductive True2:Prop:= I2: True2->True2.
> with
> Inductive True2:Prop:= I2: (False -> True2)->True2.
>
> you need (False -> X) = X forall X (which is not provable when X is
> False) and not just False -> True2 = True2
> because the name is bound in the inductive definition
>
> so the problem is still the same around the elimination on Heq "
>
> assume < is the structural order related to True2 generated by (forall
> y, f y < l2 f)
>
> Fixpoint con (x:True2) :False :=
> match x with
> I2 f => con (match Heq with eq_refl => f end)
> end.
>
> The hypothesis
> forall y, f y < x
> we would like to prove
>
> (match Heq in (False->True2=True2) return fun X _ => X with eq_refl => f
> end) < x
>
> but eliminating Heq requires a generalisation
>
> (match Heq in (False->True2=Z) return fun X _ => X with eq_refl => f
> end) < x
>
> which is not well-typed.
>
> This is this situation we need to detect and forbid.
> The point being not to miss tricky situations
>
> Christine
>
>
>
>
>