proposition: Theorem pbbuild_compute_peq : forall t, distinct_pbleaves t -> pbbuild (compute_pbcode t) = t.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros p H H0; unfold pbbuild in |- *. rewrite fold_pbadd_prop_left; auto. change (pbleft (pbbuild (compute_pbcode p)) = pbleft p) in |- *. apply f_equal with (f := pbleft); auto; apply H. apply distinct_pbleaves_pl with (1 := H0). intros p H H0; unfold pbbuild in |- *. rewrite fold_pbadd_prop_right; auto. change (pbright (pbbuild (compute_pbcode p)) = pbright p) in |- *. apply f_equal with (f := pbright); auto; apply H. apply distinct_pbleaves_pr with (1 := H0). intros p H p0 H0 H1. unfold pbbuild in |- *. rewrite fold_right_app. rewrite fold_pbadd_prop_right; auto. rewrite fold_pbadd_prop_node; auto. change (pbnode (pbbuild (compute_pbcode p)) (pbbuild (compute_pbcode p0)) = pbnode p p0) in |- *. apply f_equal2 with (f := pbnode). apply H; apply distinct_pbleaves_l with (1 := H1). apply H0; apply distinct_pbleaves_r with (1 := H1). Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)