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

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.