The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

This is probably again a basic question, but it is driving me nuts:
NewInduction breaks the links between two instances of the same
thing, and I have no clue what to use instead or what I am doing
wrong.

Here is an example, I simplified the most I could:


(* an inhabitant of T is a set of inhabitants of T, indexed by some
   index type I *)

Inductive T:Type := T_cons: (I:Type) (I->T) -> T.

Inductive Tlte : T -> T -> Prop :=
  Tlte_cons : (xI:Type)(xf:xI->T) (y:T)
              ((xi:xI)(NTgte (xf xi) y)) -> (Tlte (T_cons xI xf) y)
with NTgte : T -> T -> Prop :=
  Tgte_cons : (xI:Type)(xf:xI->T) (y:T)
              (exT xI [xi:xI](Tlte (xf xi) y)) -> (NTgte (T_cons xI xf) y).


Think of "Tlte" to be an pre-order on T (less than or equal), and Tgte
as "not bigger than or equal".

Now, I want to prove that the relation between those two is indeed
what I intend of it, by induction. Let's focus on "(NTgte x y) -> ~(Tlte y 
x)".

I thus basically need this theorem:

Theorem Step: (xI:Type)(xf:xI->T) (y:T)
              [x:=(T_cons xI xf)]
              ((xi:xI) (NTgte y (xf xi)) -> ~(Tlte (xf xi) y)) ->
              ((NTgte x y) -> ~(Tlte y x)).

I do "Intros", and I have:

1 subgoal
  
  xI : Type
  xf : xI->T
  y : T
  x := (T_cons xI xf) : T
  H : (xi:xI)(NTgte y (xf xi))->~(Tlte (xf xi) y)
  H0 : (NTgte x y)
  ============================
   ~(Tlte y x)

Now, I do "NewInduction H0.", in order to get the proof of (NTgte x
y), which can only be an application of Tgte_cons, with arguments xI
xf y, and a p of type (exT xI [xi:xI](Tlte (xf xi) y)).

But somehow, Coq decides to introduce a *new* xI0 and a *new* xf0,
"forgetting" that those are xI and xf, because x:=(T_cons xI xf):


1 subgoal
  
  xI : Type
  xf : xI->T
  y : T
  H : (xi:xI)(NTgte y (xf xi))->~(Tlte (xf xi) y)
  xI0 : Type
  xf0 : xI0->T
  H0 : (EXT xi:xI0 | (Tlte (xf0 xi) y))
  ============================
   ~(Tlte y (T_cons xI0 xf0))


You see my problem? If I had (H0:(EXT xi:xI | (Tlte (xf xi) y))), I
could do "Elim H0; Intros. Absurd (Tlte (xf0 x) y). [Apply H |
Assumption]." and just have the goal "NTgte y (xf xi)" to
prove. (Which is not possible in this Environment, but if instead of /
before the "Absurd", I do "Unfold not; Intros.", it is provable from
the new hypothesis. But it gets intricate, and the names given by Coq
are confusing, so I'll spare you the expressions.)

I can't see why Coq wants to introduce a *new* xf0 and xI0 like
that. Maybe I'm simply using the bad tactic? Tried NewDestruct too,
the results are similar. Oh, and doing Zeta-reduction (replacing x by
its definition) doesn't work either.



For your convenience, the whole Coq code in one go:

Inductive T:Type := T_cons: (I:Type) (I->T) -> T.

Inductive Tlte : T -> T -> Prop :=
  Tlte_cons : (xI:Type)(xf:xI->T) (y:T)
              ((xi:xI)(NTgte (xf xi) y)) -> (Tlte (T_cons xI xf) y)
with NTgte : T -> T -> Prop :=
  Tgte_cons : (xI:Type)(xf:xI->T) (y:T)
              (exT xI [xi:xI](Tlte (xf xi) y)) -> (NTgte (T_cons xI xf) y).

Theorem Step: (xI:Type)(xf:xI->T) (y:T)
              [x:=(T_cons xI xf)]
              ((xi:xI) (NTgte y (xf xi)) -> ~(Tlte (xf xi) y)) ->
              ((NTgte x y) -> ~(Tlte y x)).
Proof.
Intros.
NewInduction H0.
Elim H0; Intros.
Absurd (Tlte (xf0 x) y).
2: Assumption.
Apply H. (* Should work! *)




Thank you for your insight,

-- 
Lionel

Attachment: pgpd65K3wkJyy.pgp
Description: PGP signature