The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

On Fri, 16 Dec 2005 
roconnor AT theorem.ca
 wrote:

> On Fri, 16 Dec 2005 
> roconnor AT theorem.ca
>  wrote:
>
> > By complete binary tree I mean
> > <http://www.nist.gov/dads/HTML/completeBinaryTree.html>
> >
> > but I think I would also be satified with a perfect binary tree
> > <http://www.nist.gov/dads/HTML/perfectBinaryTree.html>
>
> Er, I don't mean a perfect binary tree,  What a wanted to say is that all
> the extra leaves don't need to be to the left.  So long as all leaves are
> at either depth n or depth n-1, I am happy.

What about this:

Require Import List.

Inductive Tree: Set :=
  Leaf: nat -> Tree
| Node: Tree -> Tree -> Tree.

Fixpoint mkTree (n: nat)  (l: list Tree) {struct n}: Tree * list Tree :=
  match n with
  O =>
      match l with
        nil => (Leaf O, nil)
     | (a::l1) =>(a, l1)
     end
| S n1 => let (t1, l2) := mkTree n1 l in
                 let (t2, l3) := mkTree n1 l2 in
                  (Node t1 t2, l3)
end.

Definition mkLeaf l := map Leaf l.

Definition toTree n l := mkTree n (mkLeaf l).

Eval compute in (toTree 2 (1:: 2:: 3:: 4:: nil)).