flatten_len.v

Inductive Tree (A : Type) :=
| tip : A -> Tree A
| bin : Tree A -> Tree A -> Tree A.

Fixpoint flatten {A} (t : Tree A) : list A :=
  match t with
  | tip _ x => x :: nil
  | bin _ l r => flatten l ++ flatten r
  end.

Fixpoint leafCount {A} (t : Tree A) : nat :=
  match t with
  | tip _ _ => 1
  | bin _ l r => leafCount l + leafCount r
  end.

Theorem append_len : forall {A} {xs ys : list A},
  length (xs ++ ys) = length xs + length ys.
Proof.
  induction xs.
  + easy.
  + intros. simpl.
    rewrite IHxs.
    reflexivity.
Qed.

Theorem flatten_len {A} : forall {t : Tree A},
  leafCount t = length (flatten t).
Proof.
  induction t.
  + easy.
  + simpl.
    rewrite IHt1.
    rewrite IHt2.
    rewrite <- append_len.
    reflexivity.
Qed.