Huffman.Frequency

(* 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 Lesser General 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: Frequency.v
Frequency list from a message and some properties
Definitions: frequency_list, number_of_occurrences
Initial author: Laurent.Thery@inria.fr (2003)

From Huffman Require Import AuxLib.
Require Import List.
From Huffman Require Import UniqueKey.
From Huffman Require Import Permutation.

Section Frequency.
Variable A : Type.
Variable eqA_dec : a b : A, {a = b} + {a b}.

(* Create a list of a given length with a given element  *)
Fixpoint id_list (a : A) (n : ) {struct n} : list A
  match n with
  | O []
  | S a id_list a
  end.

(* An element in a frequency list *)
Fixpoint add_frequency_list (a : A) (l : list (A )) {struct l} :
 list (A )
  match l with
  | [] (a, 1) []
  | (b, n)
      match eqA_dec a b with
      | left _ (a, S n)
      | right _ (b, n) add_frequency_list a
      end
  end.

(* 
  Adding an element gives the same list upto permutation if
  the frequency list is developed
*)

Theorem add_frequency_list_perm :
  (a : A) l,
 permutation (a flat_map (fun p id_list (fst p) (snd p)) l)
   (flat_map (fun p id_list (fst p) (snd p)) (add_frequency_list a l)).
Proof using.
intros a l; generalize a; elim l; simpl in |- *; clear a l; auto.
intros (a, n) l H b.
case (eqA_dec b a); auto.
intros e; simpl in |- *; rewrite e; auto.
simpl in |- *.
intros e;
 apply
  permutation_trans
   with
     (id_list a n
      (b []) flat_map (fun p id_list (fst p) (snd p)) l);
 [ idtac | simpl in |- *; auto ].
change
  (permutation
     ((b [])
      id_list a n flat_map (fun p id_list (fst p) (snd p)) l)
     (id_list a n
      (b []) flat_map (fun p id_list (fst p) (snd p)) l))
 in |- *.
repeat rewrite app_ass; auto.
Qed.


(* Inversion theorem *)
Theorem add_frequency_list_in_inv :
  ( : A) ( : ) l,
 In (, ) (add_frequency_list l) = In (, ) l.
Proof using.
intros l; elim l; simpl in |- *; auto.
intros [| ]; auto; injection ; auto.
intros (, ) Rec; simpl in |- *; auto.
case (eqA_dec ); simpl in |- *; auto.
intros e H; cut (In (, ) ((, S ) )); auto.
simpl in |- *; intros [| ]; auto.
injection ; auto.
intuition.
Qed.


(* Adding an element does not change the unique key property *)
Theorem add_frequency_list_unique_key :
  (a : A) l, unique_key l unique_key (add_frequency_list a l).
Proof using.
intros a l; elim l; simpl in |- *; auto.
intros (, ) Rec H; case (eqA_dec a ).
intros e; apply unique_key_perm with ( (a, S ) ); auto.
apply unique_key_cons; auto.
intros b; red in |- *; intros ; case (unique_key_in _ _ _ _ b _ H); auto.
rewrite e; auto.
apply unique_key_inv with (1 H); auto.
intros n; apply unique_key_cons; auto.
intros b; red in |- *; intros ;
 case add_frequency_list_in_inv with (1 ); auto.
intros ; case (unique_key_in _ _ _ _ b _ H); auto.
apply Rec; apply unique_key_inv with (1 H); auto.
Qed.


(* Adding an element that was not in the list gives a frequency of 1 *)
Theorem add_frequency_list_1 :
  a l,
 ( ca, In (a, ca) l) In (a, 1) (add_frequency_list a l).
Proof using.
intros a l; generalize a; elim l; clear a l; simpl in |- *; auto.
intros (, ) H a .
case (eqA_dec a ); auto.
intros ; case ( ); left;
 apply f_equal2 with (f pair (AA) (B)); auto.
intros n; apply in_cons; auto; apply H; auto.
intros ca; red in |- *; intros ; case ( ca); auto.
Qed.


(* Adding an element increments the frequency *)
Theorem add_frequency_list_in :
  m a n,
 unique_key m In (a, n) m In (a, S n) (add_frequency_list a m).
Proof using.
intros m; elim m; clear m; simpl in |- *; auto.
intros (, ) l Rec a n H ; case (eqA_dec a ); simpl in |- *; auto.
intros ; case ; auto.
intros ; left; apply f_equal2 with (f pair (AA) (B));
 injection ; auto.
rewrite ; intros ; case unique_key_in with (1 H) ( n); auto.
intros ; right; apply Rec.
apply unique_key_inv with (1 H); auto.
case ; auto.
intros ; case ; injection ; auto.
Qed.


(* Adding an element just changes the frequency of this element *)
Theorem add_frequency_list_not_in :
  m a b n, a b In (a, n) m In (a, n) (add_frequency_list b m).
Proof using.
intros m; elim m; clear m; simpl in |- *; auto.
intros (, ) l H b n [| ]; case (eqA_dec b ); simpl in |- *;
 auto.
intros ; case ; injection ; auto.
intros; apply trans_equal with (2 sym_equal ); auto.
Qed.


(* Create a frequency list from a message *)
Fixpoint frequency_list (l : list A) : list (A )
  match l with
  | [] []
  | a add_frequency_list a (frequency_list )
  end.

(* Keys of the frequency are in the original message *)
Theorem frequency_list_in :
  a n m, In (a, n) (frequency_list m) In a m.
Proof using.
intros a n m; generalize n; elim m; clear m n; simpl in |- *; auto.
intros l H n ; case add_frequency_list_in_inv with (1 ); auto.
intros ; right; apply (H n); auto.
Qed.


(* Developing the frequency list gives a permutation of the initial message *)
Theorem frequency_list_perm :
  l : list A,
 permutation l
   (flat_map (fun p id_list (fst p) (snd p)) (frequency_list l)).
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a H.
apply
 permutation_trans with (2 add_frequency_list_perm a (frequency_list ));
 auto.
Qed.


Theorem frequency_list_unique :
  l : list A, unique_key (frequency_list l).
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a H; apply add_frequency_list_unique_key; auto.
Qed.

Hint Resolve frequency_list_unique : core.

(* Elements of the message are keys of the frequency list *)
Theorem in_frequency_map :
  l a, In a l In a (map fst (frequency_list l)).
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a H [| ]; auto.
rewrite ; elim (frequency_list ); simpl in |- *; auto.
intros (, ) ; simpl in |- *; auto.
case (eqA_dec ); simpl in |- *; auto.
cut (In (map (fst (AA) (B)) (frequency_list ))); auto.
elim (frequency_list ); simpl in |- *; auto.
intros (, ) ; simpl in |- *; auto.
case (eqA_dec a ); simpl in |- *; auto.
intros e [| ]; auto; left; rewrite ; auto.
intros e [| ]; auto.
Qed.

Hint Resolve in_frequency_map : core.

(* Keys of the frequency list are elements of the message *)
Theorem in_frequency_map_inv :
  l a, In a (map (fst (B_)) (frequency_list l)) In a l.
Proof using.
intros l a H; case in_map_inv with (1 H); auto.
intros (, ) (, ); simpl in |- *.
rewrite ; apply frequency_list_in with (1 ).
Qed.


(* Compute the number of occurrences of an element in a message *)
Fixpoint number_of_occurrences (a : A) (l : list A) {struct l} :
  match l with
  | [] 0
  | b
      match eqA_dec a b with
      | left _ S (number_of_occurrences a )
      | right _ number_of_occurrences a
      end
  end.

(* If an element is not in a message, its number is 0 *)
Theorem number_of_occurrences_O :
  a l, In a l number_of_occurrences a l = 0.
Proof using.
intros a l; elim l; simpl in |- *; auto.
intros H ; case (eqA_dec a ); auto.
intros ; case ; auto.
Qed.


(* All the occurrences of an element can be gathered in the list *)
Theorem number_of_occurrences_permutation_ex :
  (m : list A) (a : A),
  : list A,
   permutation m (id_list a (number_of_occurrences a m) ) In a .
Proof using.
intros m; elim m; simpl in |- *; auto.
intros a; exists []; split; auto with datatypes.
intros a l H .
case (eqA_dec a); simpl in |- *; intros .
case (H ); intros (, ).
exists ; split; auto.
pattern at 1 in |- *; rewrite ; auto.
case (H ); intros (, ).
exists (a ); split; auto.
apply
 permutation_trans
  with ((a ) id_list (number_of_occurrences l));
 auto.
simpl in |- *; apply permutation_skip; auto.
apply permutation_trans with (1 ); auto.
simpl in |- *; contradict ; case ; intros ; auto; case ; auto.
Qed.


(* Number of occurrences in an appended list is the sum of the occurrences *)
Theorem number_of_occurrences_app :
  a,
 number_of_occurrences a ( ) =
 number_of_occurrences a + number_of_occurrences a .
Proof using.
intros ; elim ; simpl in |- *; auto.
intros a l H ; case (eqA_dec a); intros ; simpl in |- *; auto.
Qed.


(* Permutation preserves the number of occurrences *)
Theorem number_of_occurrences_permutation :
  a,
 permutation number_of_occurrences a = number_of_occurrences a .
Proof using.
intros a H; generalize a; elim H; clear H a ; simpl in |- *; auto.
intros a H ; case (eqA_dec a ); simpl in |- *; auto;
 case (eqA_dec a); simpl in |- *; auto.
intros a b L ; case (eqA_dec a); simpl in |- *; auto;
 case (eqA_dec b); simpl in |- *; auto.
intros H a; apply trans_equal with (1 a); auto.
Qed.


(* The frequency list contains the number of occurrences *)
Theorem frequency_number_of_occurrences :
  a m, In a m In (a, number_of_occurrences a m) (frequency_list m).
Proof using.
intros a m; generalize a; elim m; clear m a; simpl in |- *; auto.
intros a l H ; case (eqA_dec a); simpl in |- *; auto.
intros e; case (In_dec eqA_dec l).
intros ; rewrite e; apply add_frequency_list_in; auto.
apply (H a); rewrite e; auto.
intros ; rewrite number_of_occurrences_O; auto.
rewrite e; apply add_frequency_list_1.
intros ca; contradict ; auto.
rewrite e; apply frequency_list_in with (1 ).
intros ; case ; auto.
intros ; case ; auto.
intros ; apply add_frequency_list_not_in; auto.
Qed.


End Frequency.
Arguments id_list [A].
Arguments add_frequency_list [A].
Arguments frequency_list [A].
Arguments number_of_occurrences [A].
Hint Resolve in_frequency_map : core.
Hint Resolve frequency_list_unique : core.