The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 16 May 2012 16:12:16 +0200,
Andrej Bauer 
<andrej.bauer AT andrej.com>
 a écrit :

> > Inductive endpoints (T : Type) : nat -> Type :=
> > | End : T -> endpoints T O
> > | Step : forall n (a b : endpoints T n), a = b -> endpoints T (S n).
> >
> > I don't know if it is what you wish.
> > Typically, if you have something of type "endpoints T 2", you can
> > decompose it into:
> > a : T
> > b : T
> > c : T
> > d : T
> > Hab : End a = End b (* thus a = b *)
> > Hcd : End c = End d (* thus c = d *)
> > Habcd : Step Hab = Step Hcd
> 
> Thanks. I would have to think a bit about this because we get the
> unwanted wrappers "Step (Step ... End a)...)". This may complicate
> matters a bit. For a perfect solution we'd also want a function which
> strips off the "End"s and "Steps" so that, for example, Hab above
> would have the type a = b and Habcd woudl have the type Hab = Hcd.
> 
> But it is perhaps easier to use your definition and define an
> auxiliary function which performes the stripping as an afterthought.
> 
> With kind regards,
> 
> Andrej

 Inductive endpoints (T : Type) (a b : T) : nat -> Type :=
 | End : a = b -> endpoints T O
 | Step : forall n (X Y : endpoints T a b n), X = Y ->
           endpoints T a b (S n).

Is another version which avoids to have many T at the end.
But you still won't be able to unwrap it completely, as
you will have:

H1 : a = b
H2 : a = b
H3 : a = b
H4 : a = b
H5 : H1 = H2
H6 : H3 = H4
H7 : H5 = H6 ← type mismatch H1=H2 vs H3=H4