The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Sun, 11 Oct 2009 17:49:28 +0200, Vladimir Voevodsky <vladimir AT ias.edu>  
a écrit:

> On Oct 10, 2009, at 9:18 PM, AUGER Cédric wrote:
>
> > As said by Adam, I am wondering if don't have confusion between Records  
> > and Inductives:
> >
> > Le Sat, 10 Oct 2009 23:32:28 +0200, Vladimir Voevodsky <vladimir AT ias.edu 
> > > a écrit:
> >
> > > Is there a way in Coq to make definitions such as:
> >
> > what you expect in
> > > Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
> > may be:
> >
> > Record I1 T := makeI1
> > { x0 : T;
> >  x1 : T;
> >  i : x0 = x1
> > }
>
>
> In these terms, what I wanted was:
>
> Inductive I1:Type :=
>
> def_el:  { x0 : I1; x1 : I1;  i : x0 = x1 }
>
> such that, for any T one would have (morally)

Do you mean

Record Struct I1 : Type :=
def_el
  { x0 : I1; x1 : I1;  i : x0 = x1 }.

Definition morphism T U (f : T -> U) (X : Struct T) : Struct U.
  intros.
  refine (def_el U (f (x0 T X)) (f (x1 T X)) _).
  rewrite (i T X).
  reflexivity.
Defined.

?


> (I1 -> T) = { x0 : T ;  x1 : T;  i : x0 = x1 }
>
> > I am not so happy with that example, let me propose a hopefully more  
> > enlightening one:
> >
> > you want to define
> > Z/2Z. So you would like to write for instance
> >
> > Inductive Ztwo : Type :=
> > O :Ztwo
> > | S : Ztoo ->Ztwo
> >
> > WITH  forall n :Ztwo ,  SSn =n.
> >
> > This corresponding  Ztwo_rect (or fixpoint) should generate a proof  
> > obligation for checking that the recursive formulas are compatible with  
> > the relations specified under the WITH banner.
> >
> > ah
>
> Yes, your Ztwo example is of the same kind as my I1.  It seems to be  
> just the question of what is allowed in the inductive definitions. Is  
> there a reason why something like
>
> Inductive I1:Type :=
>
> def_el:  { x0 : I1; x1 : I1;  i : x0 = x1 }
>
> or
>
> Inductive Ztwo : Type :=
>
> O :Ztwo
> | ZtwoS : {S: Ztwo ->Ztwo ;  Z2axiom :  forall n : Ztwo ,  SSn =n} .
>
>
> would be problematic?

Mainly because it has non sense (or I am stupid),
I don't even understand what would be the type of ZtwoS

> V.
>
>
>
>
>
>
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
Utilisant le client e-mail révolutionnaire d'Opera :  
http://www.opera.com/mail/