The Coq mailing list

[Amy Felty <afelty AT site.uottawa.ca>]

I have a question about the use of Fixpoint.  In my example, I have a
tree data structure where the label at each node is a list of natural
numbers defined as:

Require Import PolyList.
Inductive Tree : Set :=
  Node : (list nat) -> (list Tree) -> Tree.

The second argument represents the children of a node as a list of
trees.  If the list is empty, the Node is considered a leaf.

I want to write a function that takes a list of nats and builds a tree
as follows: the input list is the label of the root; the labels of the
children are determined from the label of the parent (via a function
call); for the base case, there is a function that determines if a
particular list of nats should be the label of a leaf.  For this
example, it doesn't matter how these functions work, so they are
introduced as parameters:

Parameter getSublists : (list nat) -> (list (list nat)).
Parameter check_for_base : (list nat) -> bool.

The maximum depth of the tree that is created is known in advance, and
this number is used as a decreasing measure in the recursive calls.

I tried to define this function using mutual recursion via Fixpoint as
follows:

Fixpoint buildTree [l:(list nat)][n:nat] : Tree :=
  (Cases n of
     O => (Node (nil nat) (nil Tree))
   | (S m) => (if (check_for_base l)
               then (Node l (mapBuildTree m (getSublists l)))
               else (Node l (nil Tree)))
     end)
with mapBuildTree [n:nat][l:(list (list nat))] : (list Tree) :=
  (Cases l of
     nil => (nil Tree)
   | (cons x xs) => (cons (buildTree x n) (mapBuildTree n xs))
   end).

but I get an error message that doesn't give much information:

  Recursive call applied to an illegal term
  The 1-th recursive definition buildTree :=
  [l:(list nat); n:nat]
   Cases n of
     O => (Node (nil nat) (nil Tree))
   | (S m) =>
      (if (check_for_base l)
       then (Node l (mapBuildTree m (getSublists l)))
       else (Node l (nil Tree)))
   end is not well-formed

If I try to break the mutual recursion by assuming each node has at
most one child, then it works:

Parameter getSublist : (list nat) -> (list nat).
Fixpoint buildTree [l:(list nat)][n:nat] : Tree :=
  (Cases n of
     O => (Node (nil nat) (nil Tree))
   | (S m) => (if (check_for_base l)
               then (Node l (cons (buildTree (getSublist l) m) (nil Tree)))
               else (Node l (nil Tree)))
     end).
Fixpoint mapBuildTree [n:nat][l:(list (list nat))] : (list Tree) :=
  (Cases l of
     nil => (nil Tree)
   | (cons x xs) => (cons (buildTree x n) (mapBuildTree n xs))
   end).

Is this a limitation of Fixpoint, or am I doing something wrong?
Thanks in advance for any information.

Amy