Huffman.Huffman

(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU LessernGeneral Public License for more details.                *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(**********************************************************************
    Proof of Huffman algorithm: Huffman.v                            
                                                                     
    The huffman algorithm and its proof of correctness               
                                                                     
    Definition: huffman                                              
                                    Laurent.Thery@inria.fr (2003)    
 **********************************************************************)

From Huffman Require Import Code.
From Huffman Require Import BTree.
From Huffman Require Import Build.
From Huffman Require Import PBTree2BTree.
From Huffman Require Import Restrict.

Section Huffman.
Variable A : Type.
Variable empty : A.
Variable eqA_dec : forall a b : A, {a = b} + {a <> b}.
Variable m : list A.
Hypothesis frequency_more_than_one : 1 < length (frequency_list eqA_dec m).

(* The message is not null *)
Theorem not_null_m : m <> nil.
Proof using A eqA_dec frequency_more_than_one m.
generalize frequency_more_than_one; case m; simpl in |- *; auto.
intros H; Contradict H; auto with arith.
intros; discriminate.
Qed.

(* Every tree that is built is of minimum weight *)
Theorem huffman_build_minimun :
 forall (c : code A) (t : btree A),
 unique_prefix c ->
 in_alphabet m c ->
 build (fun x => number_of_occurrences eqA_dec x m)
   (map (fun x => leaf (fst x)) (frequency_list eqA_dec m)) t ->
 weight eqA_dec m (compute_code t) <= weight eqA_dec m c.
Proof using A empty eqA_dec frequency_more_than_one m.
intros c t H1 H2 H3; unfold weight in |- *.
rewrite restrict_code_encode_length with (c := c).
apply
 le_trans
  with
    (length
       (encode eqA_dec
          (compute_code
             (to_btree (pbbuild empty (restrict_code eqA_dec m c)))) m));
 auto.
repeat
 rewrite
  weight_tree_compute with (f := fun x => number_of_occurrences eqA_dec x m);
 auto.
cut
 (cover_min A (fun x : A => number_of_occurrences eqA_dec x m)
    (map (fun x : A * nat => leaf (fst x)) (frequency_list eqA_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 eqA_dec m c))))).
apply cover_all_leaves.
replace (map (fun x : A * nat => leaf (fst x)) (frequency_list eqA_dec m))
 with
 (map (fun x : A => leaf x) (map (fst (B:=_)) (frequency_list eqA_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 (eqA_dec := eqA_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 eqA_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 eqA_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 eqA_dec m)) t).
apply build_cover with (1 := H3).
intros l1 (H4, H5).
apply all_leaves_unique; auto.
case permutation_map_ex with (1 := H4); auto.
intros l2 (HH1, HH2).
rewrite ulist_ordered_cover with (l1 := l1) (l2 := map (fst (B:=_)) l2); auto.
apply ulist_perm with (l1 := map (fst (B:=_)) (frequency_list eqA_dec m));
 auto.
apply permutation_map; auto.
apply permutation_sym; auto.
apply unique_key_ulist; auto.
apply ulist_perm with (l1 := map (fst (B:=_)) (frequency_list eqA_dec m));
 auto.
apply permutation_map; auto.
apply permutation_sym; auto.
apply unique_key_ulist; auto.
rewrite HH2; 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 eqA_dec m c)
                   (c2 :=
                     compute_pbcode
                       (pbbuild empty (restrict_code eqA_dec m c))).
generalize
 (to_btree_smaller _ eqA_dec (pbbuild empty (restrict_code eqA_dec m c))).
intros H4; pattern m at 2 4 in |- *; elim m; simpl in |- *; auto.
intros a0 l H5; repeat rewrite length_app.
apply plus_le_compat; auto.
apply permutation_sym; apply pbbuild_compute_perm.
apply restrict_not_null with (eqA_dec := eqA_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.

(* Auxillary function to compute minimal code *)
Definition huffman_aux :
  forall l : list (nat * code A),
  l <> nil ->
  ordered (fun x y => fst x <= fst y) l ->
  (forall a,
   In a l -> compute_code (to_btree (pbbuild empty (snd a))) = snd a) ->
  (forall a,
   In a l ->
   sum_leaves (fun x => number_of_occurrences eqA_dec x m)
     (to_btree (pbbuild empty (snd a))) = fst a) ->
  (forall a, In a l -> snd a <> nil) ->
  {c : code A |
  compute_code (to_btree (pbbuild empty c)) = c /\
  build (fun x => number_of_occurrences eqA_dec x m)
    (map (fun x => to_btree (pbbuild empty (snd x))) l)
    (to_btree (pbbuild empty c))}.
intros l; elim l using list_length_induction; clear l.
intros l; case l.
intros H H0; case H0; auto.
intros p l0; case p; intros n1 c1; case l0; clear p l0.
intros H H0 H1 H2 H3 H4; exists c1; simpl in |- *; repeat (split; auto).
apply H2 with (a := (n1, c1)); auto with datatypes.
apply build_one.
intros p l1; case p; intros n2 c2.
intros H H0 H1 H2 H3 H4.
case
 H
  with
    (l2 := insert (fun x y => le_bool (fst x) (fst y))
             (n1 + n2,
             map (fun x => (fst x, false :: snd x)) c1 ++
             map (fun x => (fst x, true :: snd x)) c2) l1);
 auto.
rewrite
 permutation_length
                    with
                    (m :=
                      (n1 + n2,
                      map (fun x : A * list bool => (fst x, false :: snd x))
                        c1 ++
                      map (fun x : A * list bool => (fst x, true :: snd x))
                        c2) :: l1).
simpl in |- *; auto with arith.
apply permutation_sym; apply insert_permutation.
red in |- *; intros H5;
 absurd
  ((n1 + n2,
   map (fun x : A * list bool => (fst x, false :: snd x)) c1 ++
   map (fun x : A * list bool => (fst x, true :: snd x)) c2) :: l1 = nil).
intros; discriminate.
apply permutation_nil_inv; auto.
unfold code in H5; rewrite <- H5; apply insert_permutation.
apply insert_ordered; auto.
intros a b H5; apply le_bool_correct3; auto.
intros a b H5; apply le_bool_correct4; auto.
apply ordered_inv with (a := (n2, c2)).
apply ordered_inv with (a := (n1, c1)); auto.
intros a H5.
cut
 (In a
    ((n1 + n2,
     map (fun x : A * list bool => (fst x, false :: snd x)) c1 ++
     map (fun x : A * list bool => (fst x, true :: snd x)) c2) :: l1)).
simpl in |- *; intros [H6| H6]; try rewrite <- H6; simpl in |- *;
 auto with datatypes.
rewrite pbbuild_pbnode; simpl in |- *; auto with datatypes.
apply f_equal2 with (f := app (A:=A * list bool)); auto.
generalize (H2 (n1, c1)); simpl in |- *; intros tmp; rewrite tmp; clear tmp;
 auto with datatypes.
elim c1; simpl in |- *; auto.
intros a0; case a0; simpl in |- *; auto.
intros a1 l0 l2 H7; apply f_equal2 with (f := cons (A:=A * list bool)); auto.
generalize (H2 (n2, c2)); simpl in |- *; intros tmp; rewrite tmp; clear tmp;
 auto with datatypes.
elim c2; simpl in |- *; auto.
intros a0; case a0; simpl in |- *; auto.
intros a1 l0 l2 H7; apply f_equal2 with (f := cons (A:=A * list bool));
 auto with datatypes.
generalize (H4 (n1, c1)); simpl in |- *; auto with datatypes.
generalize (H4 (n2, c2)); simpl in |- *; auto with datatypes.
apply permutation_in with (2 := H5).
apply permutation_sym; apply insert_permutation.
intros a H5.
cut
 (In a
    ((n1 + n2,
     map (fun x : A * list bool => (fst x, false :: snd x)) c1 ++
     map (fun x : A * list bool => (fst x, true :: snd x)) c2) :: l1)).
simpl in |- *; intros [H6| H6]; try rewrite <- H6; simpl in |- *;
 auto with datatypes.
rewrite pbbuild_pbnode; simpl in |- *; auto with datatypes.
apply f_equal2 with (f := plus); auto.
generalize (H3 (n1, c1)); simpl in |- *; auto with datatypes.
generalize (H3 (n2, c2)); simpl in |- *; auto with datatypes.
generalize (H4 (n1, c1)); simpl in |- *; auto with datatypes.
generalize (H4 (n2, c2)); simpl in |- *; auto with datatypes.
apply permutation_in with (2 := H5).
apply permutation_sym; apply insert_permutation.
intros a H5.
cut
 (In a
    ((n1 + n2,
     map (fun x : A * list bool => (fst x, false :: snd x)) c1 ++
     map (fun x : A * list bool => (fst x, true :: snd x)) c2) :: l1)).
simpl in |- *; intros [H6| H6]; try rewrite <- H6; simpl in |- *;
 auto with datatypes.
generalize (H4 (n1, c1)); case c1; simpl in |- *; auto with datatypes.
intros; discriminate.
apply permutation_in with (2 := H5).
apply permutation_sym; apply insert_permutation.
intros c3 (HC1, HC2); exists c3; split; auto.
apply build_step with (2 := HC2); auto.
simpl in |- *; red in |- *.
exists (map (fun x : nat * code A => to_btree (pbbuild empty (snd x))) l1);
 exists (to_btree (pbbuild empty c1)); exists (to_btree (pbbuild empty c2));
 repeat (split; auto).
change
  (ordered (sum_order (fun x : A => number_of_occurrences eqA_dec x m))
     (map (fun x : nat * code A => to_btree (pbbuild empty (snd x)))
        ((n1, c1) :: (n2, c2) :: l1))) in |- *.
apply ordered_map_inv; auto.
generalize H3 H1; elim ((n1, c1) :: (n2, c2) :: l1); (simpl in |- *; auto).
intros a l0; case a; case l0; simpl in |- *; auto; clear a l0.
intros p0 l0 n4 c4; case p0; intros n5 c5; simpl in |- *; clear p0; auto.
intros H5 H6 H7; apply ordered_cons; unfold sum_order in |- *; simpl in |- *;
 auto.
generalize (H6 (n4, c4)); simpl in |- *; intros tmp; rewrite tmp; clear tmp;
 auto with datatypes.
generalize (H6 (n5, c5)); simpl in |- *; intros tmp; rewrite tmp; clear tmp;
 auto with datatypes.
change (fst (n4, c4) <= fst (n5, c5)) in |- *.
apply ordered_inv_order with (1 := H7); auto.
apply H5; auto.
apply ordered_inv with (1 := H7); auto.
apply
 permutation_trans
  with
    (map (fun x : nat * code A => to_btree (pbbuild empty (snd x)))
       ((n1 + n2,
        map (fun x : A * list bool => (fst x, false :: snd x)) c1 ++
        map (fun x : A * list bool => (fst x, true :: snd x)) c2) :: l1));
 auto.
apply permutation_map; auto.
apply permutation_sym; apply insert_permutation.
apply
 permutation_trans
  with
    (map (fun x : nat * code A => to_btree (pbbuild empty (snd x)))
       ((n1 + n2,
        map (fun x : A * list bool => (fst x, false :: snd x)) c1 ++
        map (fun x : A * list bool => (fst x, true :: snd x)) c2) :: l1));
 auto.
simpl in |- *; auto.
rewrite pbbuild_pbnode; auto.
generalize (H4 (n1, c1)); simpl in |- *; auto with datatypes.
generalize (H4 (n2, c2)); simpl in |- *; auto with datatypes.
Defined.

(* The huffman algorithm *)
Definition huffman :
  {c : code A |
  unique_prefix c /\
  in_alphabet m c /\
  (forall c1 : code A,
   unique_prefix c1 ->
   in_alphabet m c1 -> weight eqA_dec m c <= weight eqA_dec m c1)}.
case
 (huffman_aux
    (isort (fun x y => le_bool (fst x) (fst y))
       (map (fun x => (snd x, (fst x, nil) :: nil))
          (frequency_list eqA_dec m)))).
generalize frequency_more_than_one; case (frequency_list eqA_dec m);
 simpl in |- *; auto.
intros H; Contradict H; auto with arith.
intros p l frequency_more_than_one_bis H.
absurd (In (A:=nat * code A) (snd p, (fst p, nil) :: nil) nil).
simpl in |- *; intros H1; case H1.
rewrite <- H;
 apply
  permutation_in
   with
     ((snd p, (fst p, nil) :: nil)
      :: isort
           (fun x y : nat * list (A * list bool) => le_bool (fst x) (fst y))
           (map (fun x : A * nat => (snd x, (fst x, nil) :: nil)) l));
 auto with datatypes.
apply insert_permutation.
apply isort_ordered; auto.
intros a b H0; apply le_bool_correct3; auto.
intros a b H0; apply le_bool_correct4; auto.
intros a H0;
 cut
  (In a
     (map (fun x : A * nat => (snd x, (fst x, nil) :: nil))
        (frequency_list eqA_dec m))).
intros H1; case in_map_inv with (1 := H1); auto.
intros x; case x; simpl in |- *; auto.
intros a0 n (H2, H3); rewrite H3; simpl in |- *; auto.
apply permutation_in with (2 := H0); auto.
apply permutation_sym; apply isort_permutation; auto.
intros a H0;
 cut
  (In a
     (map (fun x : A * nat => (snd x, (fst x, nil) :: nil))
        (frequency_list eqA_dec m))).
intros H1; case in_map_inv with (1 := H1); auto.
intros x; case x; simpl in |- *; auto.
intros a0 n (H2, H3); rewrite H3; simpl in |- *; auto.
apply unique_key_in_inv with (a := a0) (l := frequency_list eqA_dec m); auto.
apply frequency_number_of_occurrences; auto.
apply frequency_list_in with (1 := H2); auto.
apply permutation_in with (2 := H0); auto.
apply permutation_sym; apply isort_permutation; auto.
intros a H0;
 cut
  (In a
     (map (fun x : A * nat => (snd x, (fst x, nil) :: nil))
        (frequency_list eqA_dec m))).
intros H1; case in_map_inv with (1 := H1); auto.
intros x; case x; simpl in |- *; auto.
intros a0 n (H2, H3); rewrite H3; simpl in |- *; auto.
intros; discriminate.
apply permutation_in with (2 := H0); auto.
apply permutation_sym; apply isort_permutation; auto.
intros c (Hc1, Hc2); exists c.
cut
 (build (fun x : A => number_of_occurrences eqA_dec x m)
    (map (fun x => leaf (fst x)) (frequency_list eqA_dec m))
    (to_btree (pbbuild empty c))); [ intros Hc3 | idtac ].
case
 (cover_ordered_cover _
    (map (fun x : A * nat => leaf (fst x)) (frequency_list eqA_dec m))
    (to_btree (pbbuild empty c))).
apply build_cover with (1 := Hc3).
intros l1 (H4, H5).
case permutation_map_ex with (1 := H4); auto.
intros l2 (HH1, HH2).
split; auto.
rewrite <- Hc1; auto.
apply btree_unique_prefix; auto.
apply all_leaves_unique; auto.
rewrite ulist_ordered_cover with (l1 := l1) (l2 := map (fst (B:=_)) l2); auto.
apply ulist_perm with (l1 := map (fst (B:=_)) (frequency_list eqA_dec m));
 auto.
apply permutation_map; auto.
apply permutation_sym; auto.
apply unique_key_ulist; auto.
apply ulist_perm with (l1 := map (fst (B:=_)) (frequency_list eqA_dec m));
 auto.
apply permutation_map; auto.
apply permutation_sym; auto.
apply unique_key_ulist; auto.
rewrite HH2; elim l2; simpl in |- *; auto.
intros a0 l H6; apply f_equal2 with (f := cons (A:=btree A)); auto.
split; auto.
rewrite <- Hc1; auto.
apply in_alphabet_compute_code; auto.
intros a H; apply all_leaves_inb.
rewrite ulist_ordered_cover with (l1 := l1) (l2 := map (fst (B:=_)) l2); auto.
apply permutation_in with (map (fst (B:=_)) (frequency_list eqA_dec m)); auto.
apply permutation_map; apply permutation_sym; auto.
apply ulist_perm with (l1 := map (fst (B:=_)) (frequency_list eqA_dec m));
 auto.
apply permutation_map; auto.
apply permutation_sym; auto.
apply unique_key_ulist; auto.
rewrite HH2; elim l2; simpl in |- *; auto.
intros a0 l H6; apply f_equal2 with (f := cons (A:=btree A)); auto.
intros c1 H H0.
rewrite <- Hc1.
apply huffman_build_minimun; auto.
apply build_permutation with (1 := Hc2); auto.
apply
 permutation_trans
  with
    (map (fun x : nat * code A => to_btree (pbbuild empty (snd x)))
       (map (fun x : A * nat => (snd x, (fst x, nil) :: nil))
          (frequency_list eqA_dec m))).
apply permutation_map; apply permutation_sym; apply isort_permutation.
elim (frequency_list eqA_dec m); simpl in |- *; auto.
Defined.

End Huffman.