proposition: Theorem huffman_build_minimum : forall (c : code A) (t : btree A), unique_prefix c -> in_alphabet m c -> build (fun x => number_of_occurrences A_eq_dec x m) (map (fun x => leaf (fst x)) (frequency_list A_eq_dec m)) t -> weight A_eq_dec m (compute_code t) <= weight A_eq_dec m c.
proof: Proof. Proof using empty frequency_more_than_one. intros c t H1 H2 H3; unfold weight in |- *. rewrite restrict_code_encode_length with (c := c). apply Nat.le_trans with (length (encode A_eq_dec (compute_code (to_btree (pbbuild empty (restrict_code A_eq_dec m c)))) m)); auto. repeat rewrite weight_tree_compute with (f := fun x => number_of_occurrences A_eq_dec x m); auto. cut (cover_min A (fun x : A => number_of_occurrences A_eq_dec x m) (map (fun x : A * nat => leaf (fst x)) (frequency_list A_eq_dec m)) t). intros (HH1, HH2); apply HH2; auto. apply cover_permutation with (l1 := map (fun x : A => leaf x) (all_leaves (to_btree (pbbuild empty (restrict_code A_eq_dec m c))))). apply cover_all_leaves. replace (map (fun x : A * nat => leaf (fst x)) (frequency_list A_eq_dec m)) with (map (fun x : A => leaf x) (map (fst (B:=_)) (frequency_list A_eq_dec m))). apply Permutation_map. rewrite to_btree_all_leaves. rewrite frequency_list_restric_code_map with (c := c). apply Permutation_sym; apply all_pbleaves_pbbuild. apply restrict_not_null with (A_eq_dec := A_eq_dec); auto. apply not_null_m; auto. apply restrict_unique_prefix; auto. apply frequency_not_null with (1 := frequency_more_than_one); auto. elim (frequency_list A_eq_dec m); simpl in |- *; auto with datatypes. intros a0 l H4; apply f_equal2 with (f := cons (A:=btree A)); auto. apply build_correct; auto. generalize frequency_more_than_one; case (frequency_list A_eq_dec m); simpl in |- *; auto. intros H; contradict H; auto with arith. intros; discriminate. apply to_btree_distinct_leaves; auto. apply pbbuild_distinct_pbleaves; auto. apply restrict_unique_prefix; auto. apply frequency_not_null with (1 := frequency_more_than_one); auto. case (cover_ordered_cover _ (map (fun x : A * nat => leaf (fst x)) (frequency_list A_eq_dec m)) t). apply build_cover with (1 := H3). intros l1 (H4, H5). apply all_leaves_unique; auto. apply Permutation_sym in H4. case Permutation_map_inv with (1 := H4); auto. intros l2 (HH1, HH2). rewrite NoDup_ordered_cover with (l1 := l1) (l2 := map (fst (B:=_)) l2); auto. apply Permutation_NoDup with (l := map (fst (B:=_)) (frequency_list A_eq_dec m)); auto. apply Permutation_map; auto. apply unique_key_NoDup; auto. apply Permutation_NoDup with (l := map (fst (B:=_)) (frequency_list A_eq_dec m)); auto. apply Permutation_map; auto. apply unique_key_NoDup; auto. rewrite HH1; elim l2; simpl in |- *; auto. intros a0 l H6; apply f_equal2 with (f := cons (A:=btree A)); auto. rewrite encode_permutation with (c1 := restrict_code A_eq_dec m c) (c2 := compute_pbcode (pbbuild empty (restrict_code A_eq_dec m c))). generalize (to_btree_smaller _ A_eq_dec (pbbuild empty (restrict_code A_eq_dec m c))). intros H4; pattern m at 2 4 in |- *; elim m; simpl in |- *; auto. intros a0 l H5; repeat rewrite app_length. apply Nat.add_le_mono; auto. apply Permutation_sym; apply pbbuild_compute_perm. apply restrict_not_null with (A_eq_dec := A_eq_dec); auto. apply not_null_m; auto. apply restrict_unique_prefix; auto. apply frequency_not_null with (1 := frequency_more_than_one); auto. apply restrict_unique_prefix; auto. apply frequency_not_null with (1 := frequency_more_than_one); auto. Qed.
imports: Coq(Sorting.Permutation) Huffman(Code BTree Build PBTree2BTree Restrict)