The Coq mailing list

[Christine Paulin <christine.paulin AT lri.fr>]

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