The Coq mailing list

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

Le Sun, 11 Oct 2009 15:53:27 +0200, André Hirschowitz 
<ah AT unice.fr>
 a
écrit:

> > > Not exactly.
> > > Inductive types are freely generated and have some initial property.
> >
> > Do you mean the [inductive_type]_rec, [inductive_type]_rect and so on...
> > You are right, I forgot to mention it, but you can define them manually
> > with fixpoints.
> >
> > So the solution using
> > "Inductive I1 T := makeI1 : forall (x0 x1 : T), x0 = x1 -> I1 T."
> > will generate them (but are trivial here).
> 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 : Ztwo ->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.

We quit induction theory in this case; I think, the best choice in this
case is to use a record (or a module if you prefer):
Record F2 :=
{ Z2 : Set;
  O : Set;
  S : Z2 -> Z2;
  HS : forall n, S (S n) = n
}
And you will lose some properties you can also add if required.
You loose pattern matching, but how can we define it?

mach z with
| O => ...
| S n => (any value is matched even O since S (S O)=O)
end

That is non determinism
> ah


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