Library prelude.bintree

Inductive bintree:Set :=
  Leaf : bintree
| Bin : bintree -> bintree -> bintree.

Inductive unit : Set := void.

Definition decompose : bintree -> unit + bintree * bintree.
 intro t;case t.
 left.
 constructor.
 intros t1 t2;right;exact (pair t1 t2).
Defined.

Definition compose : ( unit + bintree * bintree) -> bintree.
destruct 1.
exact Leaf.
case p. intros t1 t2;exact (Bin t1 t2).
 Defined.

Lemma bij : forall t, compose (decompose t)=t.
destruct t;simpl;auto.
Qed.

Lemma bijR : forall t:( unit + bintree * bintree), decompose (compose t)=t.
destruct t.
 simpl.
 case u.
 trivial.

simpl;auto.
 case p.
 simpl;auto.
Qed.

Definition K (n p:nat) := (n+p)*(S (n +p)).
Definition shift_n_omega_l (n:nat) (i:nat) := i.
Definition shift_n_omega_r (n:nat) (i:nat) := (S (i + n)).

Fixpoint tree_nat (t:bintree) : nat :=
 match t with Leaf => shift_n_omega_l 0 0
            | Bin t1 t2 => shift_n_omega_r 0 (K (tree_nat t1) (tree_nat t2))
 end.

Eval compute in (tree_nat Leaf).

Eval compute in (tree_nat (Bin Leaf Leaf)).

Eval compute in (tree_nat (Bin Leaf (Bin Leaf Leaf))).