proposition: Theorem weight_tree_compute : forall (m : list A) t, distinct_leaves t -> (forall a : A, f a = number_of_occurrences A_eq_dec a m) -> length (encode A_eq_dec (compute_code t) m) = weight_tree f t.
proof: Proof. intros m t H0 H. rewrite frequency_length; auto. apply trans_equal with (0 * sum_leaves f t + weight_tree f t); auto. rewrite height_pred_weight with (1 := height_pred_compute_code 0 t). unfold prod2list in |- *. rewrite fold_left_eta with (f := fun (a : nat) (b : A * list bool) => a + number_of_occurrences A_eq_dec (fst b) m * length (snd b)) (f1 := fun (a : nat) (b : A * list bool) => a + (fun b => f (fst b) * length (snd b)) b); auto. rewrite <- (fold_left_map _ _ (fun a b : nat => a + b) _ 0 (compute_code t) (fun b : A * list bool => f (fst b) * length (snd b))) . rewrite fold_left_eta with (f := fun a b : nat => a + b) (f1 := plus); auto. apply f_equal3 with (f := fold_left (A:=nat) (B:=nat)); auto. elim (compute_code t); simpl in |- *; auto. intros a l H1; apply f_equal2 with (f := cons (A:=nat)); auto with arith. ring. apply btree_unique_prefix2; auto. Qed.
imports: Coq(ArithRing)