Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] equality of equality of equality of equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] equality of equality of equality of equality


Chronological Thread 
  • From: AUGER Cédric <sedrikov AT gmail.com>
  • To: Andrej Bauer <andrej.bauer AT andrej.com>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] equality of equality of equality of equality
  • Date: Wed, 16 May 2012 17:36:09 +0200

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.

You can't have it due to typing.

Hab : a=b
Hcd : c=d

===> Hab and Hcd do not have the same type.

There is the JMeq solution, but well… it tends to become a trip to
Hell (although my inductive may already make lose any one's sanity).

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




Archive powered by MHonArc 2.6.18.

Top of Page