coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/15/2012
- Re: [Coq-Club] equality of equality of equality of equality, Adam Chlipala, 05/15/2012
- Re: [Coq-Club] equality of equality of equality of equality, Daniel Schepler, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, Favonia, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, AUGER Cédric, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, AUGER Cédric, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, AUGER Cédric, 05/17/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, AUGER Cédric, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, Favonia, 05/16/2012
- Re: [Coq-Club] equality of equality of equality of equality, Vladimir Voevodsky, 05/17/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/18/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/18/2012
- Re: [Coq-Club] equality of equality of equality of equality, Daniel Schepler, 05/19/2012
- Re: [Coq-Club] equality of equality of equality of equality, Daniel Schepler, 05/20/2012
- Re: [Coq-Club] equality of equality of equality of equality, Daniel Schepler, 05/19/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/18/2012
- Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/18/2012
Archive powered by MHonArc 2.6.18.