proposition: Theorem pbbuild_compute_perm : forall c, c <> [] -> unique_prefix c -> Permutation (compute_pbcode (pbbuild c)) c.
proof: Proof. intros c; elim c; simpl in |- *; auto. intros H; case H; auto. intros (a1, l1) l. case l. unfold pbbuild in |- *; simpl in |- *; auto. intros H H0 H1; rewrite pbadd_prop1; auto. intros (a2, l2) l3; simpl in |- *. intros H H0 H1; apply Permutation_trans with ((a1, l1) :: compute_pbcode (pbadd a2 (pbbuild l3) l2)). unfold pbbuild in |- *; simpl in |- *; apply pbadd_prop2. cut (~ is_prefix l1 l2); [ intros Ip1 | idtac ]. cut (~ is_prefix l2 l1); [ intros Ip2 | idtac ]. generalize H1; case l3; auto. intros H2; apply pbfree_pbadd_prop1; auto. intros p l0 H2. apply pbfree_pbadd_prop2; auto. change (pbfree l1 (pbbuild (p :: l0))) in |- *. apply pbfree_pbbuild_prop1 with (a := a1); auto. red in |- *; intros; discriminate. apply unique_prefix_inv with (a := a2) (l := l2). apply unique_prefix_permutation with (2 := H2); auto. red in |- *; intros HH2; absurd (a1 = a2). red in |- *; intros H3; case unique_key_in with (a := a1) (b1 := l1) (b2 := l2) (1 := unique_prefix2 _ _ H1); simpl in |- *; auto. rewrite H3; auto. apply sym_equal; apply unique_prefix1 with (1 := H1) (lb1 := l2) (lb2 := l1); simpl in |- *; auto. red in |- *; intros HH2; absurd (a1 = a2). red in |- *; intros H3; case unique_key_in with (a := a1) (b1 := l1) (b2 := l2) (1 := unique_prefix2 _ _ H1); simpl in |- *; auto. rewrite H3; auto. apply unique_prefix1 with (1 := H1) (lb1 := l1) (lb2 := l2); simpl in |- *; auto. apply perm_skip. apply H; auto. red in |- *; intros Hj; discriminate. apply unique_prefix_inv with (1 := H1); auto. Qed.
imports: Coq(List Compare_dec Sorting.Permutation) Huffman(AuxLib Code Build ISort UniqueKey)