The Coq mailing list

[Solange Coupet-Grimal <Solange.Coupet AT cmi.univ-mrs.fr>]

Dear Venanzio,


Your definition

 CoFixpoint makeTree: label -> Tree:=
[a](Node a (map makeTree (children a))).

is not correct since the recursive call occurs under "map".
The guard condition for the term to be accepted requires
 the recursive call to occur under the constructor "node".


I suggest the following specification  (I give it in V8 syntax).
__________________________________________________________________
Parameter Label:Set.

Definition inf : nat -> Set := fun n:nat => {m:nat|  m <n}.

CoInductive tree : Set:=
  Node : Label -> (forall n:nat, (inf n) -> tree) -> tree.


CoFixpoint makeTree: Label -> tree:=
fun a => (Node a (fun (n:nat) (m: {m:nat| m <n}) => (makeTree a))).
_____________________________________________________________________



                             Best regards,

                                                          Solange


Venanzio Capretta wrote:

Dear Coq users,
 there seems to be a problem with the implementation of coinductive types.
If I define the following type of infinite trees (I use Coq 7.4):

Variable label:Set.
Variable children: label -> (list label).

CoInductive Tree:Set :=
 Node: label -> (list Tree) -> Tree.

The following, apparently obvious definition is rejected.

CoFixpoint makeTree: label -> Tree:=
[a](Node a (map makeTree (children a))).

I tried in a more direct way (without using "map" but doing induction on the list directly in the definition) but nothing seems to work.
Does anybody know of a way to define makeTree?

For now I adopted a solution that replaces the use of "list" with a different type constructor "Vector" where (Vector X n) = (Finite n)->X with (Finite n) is a type with exactly n elements. This works, but I would prefer to be able to use lists.

The rejection is clearly wrong because coinductive types are final coalgebras and (label,children) is a coalgebra, so makeTree should exists by the very definition of coinductive type.

The error is strange, since the dual example using inductive types works without any problem:

Variable label:Set.
Variable parent: (list label) -> label.

Inductive Tree:Set :=
 Leaf: label -> Tree
| Node: (list Tree) -> Tree.

Fixpoint readTree [t:Tree]: label:=
Cases t of
 (Leaf a) => a
| (Node l) => (parent (map readTree l))
end.

Cheers,
 Venanzio
--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/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

-- 
                                   Solange COUPET-GRIMAL

_____________________________________________________________

CMI-39, rue  Frederic Joliot-Curie - 13453 Marseille Cedex 13              
Tel : (33) 04 91 11 36 17
_____________________________________________________________