Proving Binary Tree Properties

Question

As an exercise for myself, I'm trying to define and prove a few properties on binary trees.

Here's my btree definition:

Inductive tree : Type :=
| Leaf
| Node (x : nat) (t1 : tree) (t2 : tree).

The first property I wanted to prove is that the height of a btree is at least log2(n+1) where n is the number of nodes. So I defined countNodes trivially:

Fixpoint countNodes (t : tree) :=
  match t with
  | Leaf => 0
  | Node _ t1 t2 => 1 + (countNodes t1) + (countNodes t2)
  end.

And heightTree:

Fixpoint heightTree (t : tree) :=
  match t with
  | Leaf => 0
  | Node _ t1 t2 => 1 + (max (heightTree t1) (heightTree t2))
  end.

Now, here's my (incomplete) theorem. Could anyone provide me with hints on how to complete this induction? It seems like I should have 2 base cases (Leaf and Node _ Leaf Leaf), how can I do that?

Theorem height_of_tree_is_at_least_log2_Sn : forall t : tree,
    log2 (1 + (countNodes t)) <= heightTree t.
Proof.
  intros.
  induction t.
  - simpl. rewrite Nat.log2_1. apply le_n.
  - 

Remaining goal:

1 goal (ID 26)
  
  x : nat
  t1, t2 : tree
  IHt1 : log2 (1 + countNodes t1) <= heightTree t1
  IHt2 : log2 (1 + countNodes t2) <= heightTree t2
  ============================
  log2 (1 + countNodes (Node x t1 t2)) <= heightTree (Node x t1 t2)

PS: I have a similar problem when trying to prove that the degree of any node can only be 0, 1, or 2. Also issues on the inductive step.

Answer 1

There is no problem with your proof start. If you simplify your second sub-goal with simpl in *, you obtain:

1 goal (ID 47)
  
  x : nat
  t1, t2 : tree
  IHt1 : Nat.log2 (S (countNodes t1)) <= heightTree t1
  IHt2 : Nat.log2 (S (countNodes t2)) <= heightTree t2
  ============================
  Nat.log2 (S (S (countNodes t1 + countNodes t2))) <=
  S (Init.Nat.max (heightTree t1) (heightTree t2))

In order to make things more readable, you replace expressions which refer to trees with variables (with rememberfor instance):

1 goal (ID 59)
  
  x : nat
  t1, t2 : tree
  n1, n2, p1, p2 : nat
  IH1 : Nat.log2 (S n1) <= p1
  IH2 : Nat.log2 (S n2) <= p2
  ============================
  Nat.log2 (S (S (n1 + n2))) <= S (Init.Nat.max p1 p2)

It's now a goal about log2and max. Many properties on log2 are in the standard library. The lia tactic is very helpful for dealing with max.

About your question on degree of nodes: How do you formalize your statement ? Is it as follows ?

Fixpoint Forallsubtree (P : tree -> Prop) t :=
  match t with
    Leaf => P t
  | Node x t1 t2 => P t /\ Forallsubtree P t1 /\ Forallsubtree P t2
  end.

Definition root_degree (t: tree) :=
  match t with Leaf => 0 | Node _ _ _ => 2 end. 

Goal forall t,
  Forallsubtree (fun t =>  0 <= root_degree t <= 2) t.  
induction t; cbn; auto.    
Qed.

Answer 2

If you're ok with reading Mathcomp/SSReflect, take a look at this lemma:

https://github.com/clayrat/fav-ssr/blob/trunk/src/bintree.v#L102-L108

Your theorem can be then derived as a corollary:

Corollary log_h_geq t : log2n (size1_tree t) <= height t.
Proof.
rewrite -(exp2nK (height t)); apply: leq_log2n.
by exact: exp_h_geq.
Qed.