The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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)

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

V.