The Coq mailing list

["Satrajit Roy" <satrajit.roy AT gmail.com>]

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> 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>>
> 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>
>
>
> 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.
>