The Coq mailing list

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

As far as I know, there is currently no other way (if not, I am REALLY
interested to know it).

Hopefully,
1. No notation is mandatory, that is
CoInductive A : Set :=
 | cons : A -> B -> A
with B : Set :=
 | cons2 : A -> B -> B
.
is sufficient
2. The mess is in proportions with the number of records+fields

In your exemple, there is no mutual recursion, so sort declarations and
use Records

I warn you, using coinductive can be tricky, if you can, use inductives.

Satrajit Roy a écrit :
> Hi Cedric,
>  
> Thanks for your reply. I think you did understand me quite right.
> However, I am still trying to digest what you have suggested. I will
> write back as soon as I figure out how your suggestion really works
> out for me.
>  
> I have an immediate question though, which is, if I want to extend
> this concept to more than two records e.g. A, B, C, D .... etc.
> wouldn't it get too cluttered and clumsy. Is there a cleaner way to
> extend the concept you presented?
>  
> In case the above is not clear, let me give an example in C code:
>  
>
> struct
>
> a0;
>
> struct
>
> a1;
>
> struct
>
> a2;
>
> struct
>
> b {
>
>   struct a0 *a00;
>
>   struct a1 *a10;
>
>   struct a2 *a20;
>
> };
>
> struct
>
> a0 {
>
>   int *i;
>
>   struct b0 *b00;
>
> };
>
> struct
>
> a1 {
>
>   long *j;
>
>   struct b0 *b00;
>
> };
>
> struct
>
> a2 {
>
>   double *x;
>
>   struct b0 *b00;
>
> };
>
>  
>
> Hope that makes it clearer.
>
> Thanks again.
>
>
>
> On Wed, Nov 12, 2008 at 5:24 AM, AUGER Cédric 
>Â <Cedric.Auger AT lri.fr
>Â <mailto:Cedric.Auger AT lri.fr>>
>  wrote:
>
>     Satrajit Roy a écrit :
>     > Hi guys,
>     >
>     > With reference to the following example, is there a way to forward
>     > reference Record y and use it in a function defined in Record x. For
>     > example, as an argument to createX or x''.
>     >
>     > Thanks again.
>
>     I am not sure to understand your question, do you want a mutually
>     recursive definition of Record?
>     It is sadly not yet possible for inductive, and for co-inductive
>     (http://coq.inria.fr/V8.2beta/CHANGES),
>     I don't know, but (exepted for extraction purpouses) you can "emulate"
>     Records as they just are
>     syntactical sugar.
>
>     For example,
>     >
>     > CoInductive A : Set :=
>     > | cons : A -> B -> A
>     > with B : Set :=
>     > | cons2 : A -> B -> B
>     > .
>     > Notation "'{' 'A_field' '=' x ';' 'B_field' '=' y '}'" := (cons
>     x y).
>     > Notation "'{' 'A_field2' '=' x ';' 'B_field2' '=' y '}'" :=
>     (cons2 x y).
>     >
>     > Definition A_field A := match A with cons x _ => x end.
>     > Definition B_field A := match A with cons _ x => x end.
>     > Definition A_field2 B := match B with cons2 x _ => x end.
>     > Definition B_field2 B := match B with cons2 _ x => x end.
>     > Notation "A '.(A_field)'" := (A_field A) (at level 100).
>     > Notation "A '.(B_field)'" := (B_field A) (at level 100).
>     > Notation "B '.(A_field2)'" := (A_field2 B) (at level 100).
>     > Notation "B '.(B_field2)'" := (B_field2 B) (at level 100).
>     stands for:
>     Record A : Set :=
>     cons {A_field : A; B_field : B}
>     with B : Set :=
>      cons2 {A_field2 : A; B_field2 : B}.
>
>     (you even have better syntax as you can write {A_field = a;
>     B_field = b}
>     instead of cons a b)
>
>     But send a more precise mail if I misunderstood you.
>
>     > ---------- Forwarded message ----------
>     > From: *Satrajit Roy* 
>Â <satrajit.roy AT gmail.com
>     
>Â <mailto:satrajit.roy AT gmail.com>
>     > 
>Â <mailto:satrajit.roy AT gmail.com
>  
>Â <mailto:satrajit.roy AT gmail.com>>>
>     > Date: Tue, Nov 11, 2008 at 11:01 AM
>     > Subject: Re: Lists & Strings
>     > To: 
>Â coq-club AT pauillac.inria.fr
>     
>Â <mailto:coq-club AT pauillac.inria.fr>
>     
>Â <mailto:coq-club AT pauillac.inria.fr
>     
>Â <mailto:coq-club AT pauillac.inria.fr>>
>     >
>     >
>     > Hi guys,
>     >
>     > How do I resolve the following:
>     >
>     > Require Export List.
>     > Require Export String.
>     >
>     > Module X.
>     >
>     > Record x: Set := createX {
>     >   x': string;
>     >   x'' : bool
>     > }.
>     >
>     > Record y: Set := createY {
>     >   y': string;
>     >   y'': list x;
>     >
>     >   y''': bool :=
>     >     match (length y') return bool with
>     >       | 0 => false
>     >       | _ => true
>     >   end;
>     >
>     >   y'''' : bool  :=
>     >     match (length y'') return bool with
>     >       | 0 => false
>     >       | _ => true
>     >   end
>     > }.
>     >
>     > End X.
>     >
>     > which results in:
>     >
>     > Error:
>     > In environment
>     > y' : string
>     > y'' : list x
>     > y''' := (match length y'' with
>     >          | 0 => false
>     >          | S _ => true
>     >          end:bool) : bool
>     > The term "y''" has type "list x" while it is expected to have type
>     > "string"
>     >
>     > Thanks , as always, for your time and effort.
>     >
>
>