The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hello Amy,

Because of very obscure reasons related to the syntactical condition that Coq 
imposes on recursive definitions, or your definition to work, you have to 
inline the definition mapBuildTree in the body of buildTree. Actually, Coq 
does not connet the formal argument n of mapBuildTree with the patter 
variable m in the definition of buildTree.

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

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

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 
                let mapBuildTree = 
                   (Fix mapBuildTree 
                       {mapBuildTree [l:(list (list nat))] : (list Tree) :=
                     Cases l of
                        nil        => (nil Tree)
                     | (cons x xs) => (cons (buildTree x m) (mapBuildTree xs))
                     end})
                in  (Node l (mapBuildTree (getSublists l)))
               else (Node l (nil Tree)))
     end).
buildTree is recursively defined

Best wishes,
Eduardo Gimenez.


On Friday 09 August 2002 04:42, you wrote:
> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club