The Coq mailing list

[Milad Niqui <milad AT cs.kun.nl>]

Solange Coupet-Grimal wrote:
> 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))).
> _____________________________________________________________________

Doesn't this only makes a tree with label "a" for every node?

I think this should be modified to:

----------------
Variable default:label.

CoFixpoint makeTree2: label -> tree:=
fun a => (Node a (fun (n:nat) (Hm: {m:nat| m <n}) => (makeTree2 (nth 
(proj1_sig Hm) (children a) default)))).
----------------

(or in 7.4 syntax:

----------------
CoFixpoint makeTree2: label -> tree:=
     [a](Node a
        [n:nat; H_m:({m:nat | (lt m n)})]
         (makeTree2
           (nth (let (m, _) = H_m in m) (children a) default))).
----------------
)

makeTree2 is still not what Venanzio wanted but at least it contains 
Venanzio's tree (plus infinitely many "default" children for each node).

I agree with Venanzio that this example shows the lack of expressiveness 
of guardedness condition, because one has to change the datatype to be 
able to define the function in question.

Regards,

Milad

> 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


--
Milad Niqui

Computing Science Department,                tel:+31 24 365 2631
University of Nijmegen,                      fax:+31 24 365 2525
P.O.B. 9010,                                 email: 
milad AT cs.kun.nl
6500 GL Nijmegen,                            http://www.cs.kun.nl/~milad
The Netherlands.
==============================================================================================
The University of Nijmegen will be named Radboud University Nijmegen as 
of September 1st, 2004