The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

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.

Parameter A : Set.

Parameter xx:A.

Inductive bint : Set :=
 Node : bint -> bint -> bint
| Leaf : A -> bint.

Fixpoint step (l:list bint) : list bint :=
 match l with
   t1::t2::t3::nil => t1 :: Node t2 t3 :: nil
 | t1::t2::l' => Node t1 t2 :: step l'
 | _ => l
 end.

Fixpoint iter (l:list bint) (n:nat) {struct n} : bint :=
 match step l, n with
   t :: nil, _ => t
 | nil, _ => Leaf xx (* if the original list is empty... *)
 | l', S k => iter l' k
 | _, O => Leaf xx (* never happens list reduces  to one elt in 
log(length) steps*)
 end.

Definition list2bint l := iter (map Leaf l) (length l).

I haven't done any proof, but it seems that step n has the following 
invariant:
all the trees in the list are perfect of height n, except the last 2 
that are only complete of height n (if we consider a perfect tree of 
height n - 1 as a complete tree of height n).
Complexity is linear.

Bruno.