The Coq mailing list

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

Le Sun, 11 Oct 2009 10:03:18 +0200, André Hirschowitz <ah AT unice.fr> a  
écrit:

> > As said by Adam, I am wondering if don't have confusion between Records  
> > and Inductives:
> 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).

If that is not what you meant, I apologize for not having understood

"Suppose for example that T= Prop. Then, a function from I1 to T should be  
a triple (P_1, P_2, prf) where P_1, P_2: Prop and prf: P_1 <-> P_2 is a  
proof of their equivalence."
A function is not a triple; did you meant
Record fun_spe T P :=
{ fun : T -> T;
  spe : forall t, P t <-> P (fun t)
}. ?

By the way it is a shame that we cannot build recursive record,
 as there is no reason to forbide that since they are coded by inductives
(I don't mention the not well found version:
Record Stream := {elt : nat; next : Stream} which should be authorized as
co-inductive;
but the well founded version:
Inductive List :=
  nil : List
| labeled_cons : RecList -> List
with
 RecList :
 mk_reclist {elt : nat; next : List})
I submited a feature suggestion a long time ago for that...

Better Notations should also be handful, for now the only solution I  
found  is:

Inductive List :=
  nil : List
| labeled_cons : RecList -> List
with
 RecList :
 mk_reclist : nat -> List -> RecList.

Notation "{ 'elt' = n ; 'next' = l }" :=
(mk_reclist n l).

Notation "r '.(' 'elt' )" :=
(match r with mk_reclist elt _ => elt end).
Notation "r '.(' 'next' )" :=
(match r with mk_reclist _ next => next end).

to be able to use {elt = 0; next = {elt = 1; next = nil}} which is by far  
better
than the mk_reclist 0 (mk_reclist 1 nil)

)

> Although this does not exist in Coq, there is probably some room for  
> some kind of "freely presented" types, where constructors are given,  
> together with a bunch of relations, yielding a kind of setoid with some  
> initial property.
>
> ah
>
> --------------------------------------------------------
> 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/