Proving Binary Tree Properties

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.

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.