The Coq mailing list

[CoqUser CoqUser <coquser AT yahoo.com>]

In the (very simplified) example below some coinductive types are defined for a Parent and Child relationship.  How can a Parent or Child be instantiated since they both co-refer to each other?  Can it be done as in object oriented programming where a Parent would be defined with a 'null' child first and similarly the Child be defined with 'null' and later the fields be updated to refer to each other?  How?

Require Import String.
CoInductive Parent:Set :=
| Build_Parent (fatherOrMother:string)(child:Child)
with
Child:Set :=
| Build_Child (father:Parent)(mother:Parent).
(*Functions for Parent fields.*)
Definition fatherOrMother:Parent -> string :=              
     (fun p:Parent =>
         match p with
         | (Build_Parent fm ch) => fm
         end).
Definition child:Parent -> Child :=              
     (fun p:Parent =>
         match p with
         | (Build_Parent fm ch) => ch
         end).
(*Functions for Child*)
Definition father:Child -> Parent :=              
     (fun p:Child =>
         match p with
         | (Build_Child f m) => f
         end).
Definition mother:Child -> Parent :=              
     (fun p:Child =>
         match p with
         | (Build_Child f m) => m
         end).

(*Instantiate a Parent*)
Definition father:Parent := Build_Parent "father"
(
   (Build_Child ( (*Father ??? How to refer to the same father Instance being defined here???*)) ((*Mother*)))
).

(*Same problem if we try to instantiate the Child first.*)