Huffman.Aux

(* 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: Aux.v                                
                                                                     
    Auxillary functions & Theorems                                   
                                                                     
    Definitions:                                                     
      le_bool, map2, first_n, skip_n find_min find_max               
                                                                     
    Theorems: minus, map, app                                        
                                                                     
                                    Laurent.Thery@inria.fr (2003)    
 **********************************************************************)


Require Export List.
Require Export Arith.
From Huffman Require Export sTactic.
Require Import Inverse_Image.
Require Import Wf_nat.

(* Some facts about the minus operator *)
Section Minus.

Theorem lt_minus_O : n m, m < n 0 < n - m.
Proof using.
intros n; elim n; simpl in |- *; auto.
intros m ; Contradict ; auto with arith.
intros Rec m; case m; simpl in |- *; auto.
intros ; apply Rec; apply lt_S_n; auto.
Qed.


Theorem le_minus : a b : , a - b a.
Proof using.
intros a; elim a; simpl in |- *; auto.
intros n H b; case b; simpl in |- *; auto.
Qed.


Theorem minus_minus_simpl4 :
  a b c : , b c c a a - b - (a - c) = c - b.
Proof using.
intros a b c H .
apply plus_minus; auto with arith.
rewrite minus_plus_simpl_l_reverse with (p b + c).
repeat rewrite plus_assoc_reverse.
rewrite le_plus_minus; auto with arith.
repeat rewrite plus_assoc.
rewrite (plus_comm b c).
repeat rewrite plus_assoc_reverse.
rewrite le_plus_minus; auto with arith.
repeat rewrite (fun x plus_comm x a).
rewrite minus_plus_simpl_l_reverse; auto with arith.
apply le_trans with (1 H); auto.
Qed.


Theorem plus_minus_simpl4 :
  a b c : , b a c b a - b + (b - c) = a - c.
Proof using.
intros a b c H .
apply plus_minus.
rewrite (fun x y plus_comm (x - y)).
rewrite plus_assoc.
rewrite le_plus_minus; auto.
rewrite le_plus_minus; auto.
Qed.


End Minus.
Hint Resolve le_minus: arith.

(* Equality test on boolean *)
Section EqBool.

Definition eq_bool_dec : a b : bool, {a = b} + {a b}.
intros a b; case a; case b; simpl in |- *; auto.
right; red in |- *; intros; discriminate.
Defined.

End EqBool.

(*A function to compare naturals *)
Section LeBool.

Fixpoint le_bool (a b : ) {struct b} : bool
  match a, b with
  | O, _ true
  | S , S le_bool
  | _, _ false
  end.

Theorem le_bool_correct1 : a b : , a b le_bool a b = true.
Proof using.
intros a; elim a; simpl in |- *; auto.
intros b; case b; simpl in |- *; auto.
intros n H b; case b; simpl in |- *.
intros ; inversion .
intros ; apply H.
apply le_S_n; auto.
Qed.


Theorem le_bool_correct2 : a b : , b < a le_bool a b = false.
Proof using.
intros a; elim a; simpl in |- *; auto.
intros b ; inversion .
intros n H b; case b; simpl in |- *; auto.
intros ; apply H.
apply lt_S_n; auto.
Qed.


Theorem le_bool_correct3 : a b : , le_bool a b = true a b.
Proof using.
intros a; elim a; simpl in |- *; auto.
intros b; case b; simpl in |- *; auto with arith.
intros n H b; case b; simpl in |- *; try (intros; discriminate);
 auto with arith.
Qed.


Theorem le_bool_correct4 : a b : , le_bool a b = false b a.
Proof using.
intros a; elim a; simpl in |- *; auto.
intros b; case b; simpl in |- *; try (intros; discriminate); auto with arith.
intros n H b; case b; simpl in |- *; try (intros; discriminate);
 auto with arith.
Qed.


End LeBool.

(* Properties of the fold operator *)
Section fold.
Variables (A : Type) (B : Type).
Variable f : A B A.
Variable g : B A A.
Variable h : A A.
Variable eqA_dec : a b : A, {a = b} + {a b}.

Theorem fold_left_app :
  a , fold_left f ( ) a = fold_left f (fold_left f a).
Proof using.
intros a ; generalize a; elim ; simpl in |- *; auto; clear a .
Qed.


Theorem fold_left_eta :
  l a ,
 ( a b, In b l f a b = a b) fold_left f l a = fold_left l a.
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a H .
rewrite ; auto.
Qed.


Theorem fold_left_map :
  (C : Type) a l (k : C B),
 fold_left f (map k l) a = fold_left (fun a b f a (k b)) l a.
Proof using.
intros C a l k; generalize a; elim l; simpl in |- *; auto.
Qed.


Theorem fold_right_app :
  a ,
 fold_right g a ( ) = fold_right g (fold_right g a ) .
Proof using.
intros a ; generalize a; elim ; simpl in |- *; auto; clear a .
intros a l H ; rewrite H; auto.
Qed.


Theorem fold_left_init :
 ( (a : A) (b : B), h (f a b) = f (h a) b)
  (a : A) (l : list B), fold_left f l (h a) = h (fold_left f l a).
Proof using.
intros H a l; generalize a; elim l; clear l a; simpl in |- *; auto.
intros a l .
rewrite H; auto.
Qed.


End fold.

(* Some properties of list operators: app, map, ... *)
Section List.
Variables (A : Type) (B : Type) (C : Type).
Variable f : A B.

(* An induction theorem for list based on length *)
Theorem list_length_ind :
  P : list A Prop,
 ( : list A,
  ( : list A, length < length P ) P )
  l : list A, P l.
Proof using.
intros P H l;
 apply well_founded_ind with (R fun x y : list A length x < length y);
 auto.
apply wf_inverse_image with (R lt); auto.
apply lt_wf.
Qed.


Definition list_length_induction :
   P : list A Type,
  ( : list A,
   ( : list A, length < length P ) P )
   l : list A, P l.
intros P H l;
 apply
  well_founded_induction_type with (R fun x y : list A length x < length y);
 auto.
apply wf_inverse_image with (R lt); auto.
apply lt_wf.
Defined.

Theorem in_ex_app :
  (a : A) (l : list A),
 In a l : list A, ( : list A, l = a ).
Proof using.
intros a l; elim l; clear l; simpl in |- *; auto.
intros H; case H.
intros l H [| ]; auto.
exists (nil (AA)); exists l; simpl in |- *; auto.
apply f_equal2 with (f cons (AA)); auto.
case H; auto; intros (, ); exists ( ); exists ;
 simpl in |- *; auto.
apply f_equal2 with (f cons (AA)); auto.
Qed.


(* Properties of app *)
Theorem length_app :
  : list A, length ( ) = length + length .
Proof using.
intros ; elim ; simpl in |- *; auto.
Qed.


Theorem app_inv_head :
  : list A, = = .
Proof using.
intros ; elim ; simpl in |- *; auto.
intros a l H ; apply H; injection ; auto.
Qed.


Theorem app_inv_tail :
  : list A, = = .
Proof using.
intros ; generalize ; elim ; clear ; simpl in |- *; auto.
intros ; case ; auto.
intros b l H; absurd (length ((b l) ) length ).
simpl in |- *; rewrite length_app; auto with arith.
rewrite H; auto with arith.
intros a l H ; case .
simpl in |- *; intros ; absurd (length (a l ) length ).
simpl in |- *; rewrite length_app; auto with arith.
rewrite ; auto with arith.
simpl in |- *; intros b ; injection .
intros ; apply f_equal2 with (f cons (AA)); auto.
apply H with (1 ); auto.
Qed.


Theorem app_inv_app :
  a,
  = a
 ( : list A, = a )
 ( : _, = a ).
Proof using.
intros ; elim ; simpl in |- *; auto.
intros a H; right; exists ; auto.
intros a l H ; case ; simpl in |- *.
intros ; left; exists l; apply f_equal2 with (f cons (AA));
 injection ; auto.
intros b ; case (H ); auto.
injection ; auto.
intros (, ).
left; exists ; apply f_equal2 with (f cons (AA)); injection ; auto.
Qed.


Theorem app_inv_app2 :
  a b,
  = a b
 ( : list A, = a b )
 ( : _, = a b )
  = a nil = b .
Proof using.
intros ; elim ; simpl in |- *; auto.
intros a b H; right; left; exists ; auto.
intros a l H b; case ; simpl in |- *.
case l; simpl in |- *.
intros ; right; right; injection ; split; auto.
apply f_equal2 with (f cons (AA)); auto.
intros ; left; exists ; injection ; intros;
 repeat apply f_equal2 with (f cons (AA)); auto.
intros ; case (H b); auto.
injection ; auto.
intros (, ); left; exists ; apply f_equal2 with (f cons (AA));
 auto; injection ; auto.
intros [| (, )]; auto.
right; right; split; auto; apply f_equal2 with (f cons (AA)); auto;
 injection ; auto.
Qed.


Theorem same_length_ex :
  (a : A) ,
 length ( a ) = length
  : _,
   ( : _,
      ( b : B,
         length = length length = length = b )).
Proof using.
intros a ; elim ; simpl in |- *; auto.
intros ; case ; simpl in |- *; try (intros; discriminate).
intros b l H; exists (nil (AB)); exists l; exists b; repeat (split; auto).
intros l H ; case ; simpl in |- *; try (intros; discriminate).
intros b .
case (H ); auto.
intros (, (, (, (, )))).
exists (b ); exists ; exists ; repeat (simpl in |- *; split; auto).
apply f_equal2 with (f cons (AB)); auto.
Qed.


(* Properties of map *)
Theorem in_map_inv :
  (b : B) (l : list A),
 In b (map f l) a : A, In a l b = f a.
Proof using.
intros b l; elim l; simpl in |- *; auto.
intros tmp; case tmp.
intros H [| ]; auto.
exists ; auto.
case (H ); intros (, ); exists ; auto.
Qed.


Theorem in_map_fst_inv :
  a (l : list (B C)),
 In a (map (fst (B_)) l) c : _, In (a, c) l.
Proof using.
intros a l; elim l; simpl in |- *; auto.
intros H; case H.
intros H [| ]; auto.
exists (snd ); left; rewrite ; case ; simpl in |- *; auto.
case H; auto; intros ; exists ; auto.
Qed.


Theorem length_map : l, length (map f l) = length l.
Proof using.
intros l; elim l; simpl in |- *; auto.
Qed.


Theorem map_app : , map f ( ) = map f map f .
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a H ; apply f_equal2 with (f cons (AB)); auto.
Qed.


(* Properties of flat_map *)
Theorem in_flat_map :
  (l : list B) (f : B list C) a b,
 In a (f b) In b l In a (flat_map f l).
Proof using.
intros l g; elim l; simpl in |- *; auto.
intros a H b [| ]; apply in_or_app; auto.
left; rewrite ; auto.
right; apply H with (b b); auto.
Qed.


Theorem in_flat_map_ex :
  (l : list B) (f : B list C) a,
 In a (flat_map f l) b : _, In b l In a (f b).
Proof using.
intros l g; elim l; simpl in |- *; auto.
intros a H; case H.
intros a H ; case in_app_or with (1 ); simpl in |- *; auto.
intros ; exists a; auto.
intros ; case H with (1 ).
intros b (, ); exists b; simpl in |- *; auto.
Qed.


End List.

(* Definition of a map2 *)
Section map2.
Variables (A : Type) (B : Type) (C : Type).
Variable f : A B C.

Fixpoint ( : list A) : list B list C
  fun
  match with
  | nil nil
  | a
      match with
      | nil nil
      | b f a b
      end
  end.

Theorem map2_app :
  ,
 length = length
  ( ) ( ) = .
Proof using.
intros ; elim ; auto.
intros ; case ; simpl in |- *; auto; intros; discriminate.
intros a l H ; case .
simpl in |- *; intros; discriminate.
intros b .
apply trans_equal with (f a b (l ) ( )).
simpl in |- *; auto.
rewrite H; auto.
Qed.


End map2.
Arguments [A B C].

(* Definitions of the first and skip function *)
Section First.
Variable A : Type.

(* Take the first elements of a list *)
Fixpoint first_n (l : list A) (n : ) {struct n} :
 list A
  match n with
  | O nil
  | S match l with
            | nil nil
            | a a first_n
            end
  end.

(* Properties of first_n *)
Theorem first_n_app1 :
  (n : ) ( : list A),
 length n first_n ( ) n = first_n (n - length ).
Proof using.
intros n; elim n; simpl in |- *; auto.
intros ; case ; simpl in |- *; auto.
intros b l H; Contradict H; auto with arith.
intros H ; case ; simpl in |- *; auto with arith.
intros b l ; rewrite H; auto with arith.
Qed.


Theorem first_n_app2 :
  (n : ) ( : list A),
 n length first_n ( ) n = first_n n.
Proof using.
intros n; elim n; simpl in |- *; auto.
intros H ; case ; simpl in |- *.
intros ; Contradict ; auto with arith.
intros a l ; (apply f_equal2 with (f cons (AA)); auto).
apply H; apply le_S_n; auto.
Qed.


Theorem first_n_length :
  (n : ) ( : list A), n length length (first_n n) = n.
Proof using.
intros n ; generalize n; elim ; clear n ; simpl in |- *; auto.
intros n; case n; simpl in |- *; auto.
intros ; Contradict ; auto with arith.
intros a l H n; case n; simpl in |- *; auto with arith.
Qed.


Theorem first_n_id : l : list A, first_n l (length l) = l.
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a H; apply f_equal2 with (f cons (AA)); auto.
Qed.


(* Skip the first elements of a list *)
Fixpoint skip_n (l : list A) (n : ) {struct n} :
 list A
  match n with
  | O l
  | S match l with
            | nil nil
            | a skip_n
            end
  end.

Theorem skip_n_app1 :
  (n : ) ( : list A),
 length n skip_n ( ) n = skip_n (n - length ).
Proof using.
intros n; elim n; simpl in |- *; auto.
intros ; case ; simpl in |- *; auto.
intros b l H; Contradict H; auto with arith.
intros H ; case ; simpl in |- *; auto with arith.
Qed.


Theorem skip_n_app2 :
  (n : ) ( : list A),
 n length skip_n ( ) n = skip_n n .
Proof using.
intros n; elim n; simpl in |- *; auto.
intros H ; case ; simpl in |- *; auto with arith.
intros ; Contradict ; auto with arith.
Qed.


Theorem skip_n_length :
  (n : ) ( : list A), length (skip_n n) = length - n.
Proof using.
intros n; elim n; simpl in |- *; auto with arith.
intros H ; case ; simpl in |- *; auto.
Qed.


Theorem skip_n_id : l : list A, skip_n l (length l) = nil.
Proof using.
intros l; elim l; simpl in |- *; auto.
Qed.


Theorem first_n_skip_n_app :
  (n : ) (l : list A), first_n l n skip_n l n = l.
Proof using.
intros n; elim n; simpl in |- *; auto.
intros H l; case l; simpl in |- *; auto.
intros a ; apply f_equal2 with (f cons (AA)); auto.
Qed.


End First.
Arguments first_n [A].
Arguments skip_n [A].

(* Existence of a first max *)
Section FirstMax.

Theorem exist_first_max :
  l : list ,
 l nil
  a : ,
   ( : list ,
      ( : list ,
         l = a
         ( , In < a) ( , In a))).
Proof using.
intros l; elim l; simpl in |- *; auto.
intros H; case H; auto.
intros a ; case .
intros H ; exists a; exists (nil (A)); exists (nil (A));
 repeat (split; simpl in |- *; auto with datatypes).
intros ; case .
intros ; case .
intros n H ; case H; clear H; auto.
red in |- *; intros ; discriminate; auto.
intros (, (, (, (, )))).
case (le_or_lt a); intros ; auto.
exists a; exists (nil (A)); exists (n );
 repeat (split; auto with datatypes).
intros ; case .
rewrite .
intros ; apply le_trans with (2 ); case in_app_or with (1 );
 auto with arith.
intros ; apply lt_le_weak; auto.
simpl in |- *; intros [| ]; [ rewrite | idtac ]; auto.
exists ; exists (a ); exists ;
 repeat (split; simpl in |- *; auto with datatypes).
apply f_equal2 with (f cons (A)); auto.
intros [| ]; [ rewrite | idtac ]; auto.
Qed.


End FirstMax.

(* Find the minimum and the maximun in a list *)
Section FindMin.
Variable A : Type.
Variable f : A .

(* Search in the list for the min with respect to a valuation function f *)
Fixpoint find_min (l : list A) : option ( A)
  match l with
  | nil None
  | a
      match find_min with
      | None Some (f a, a)
      | Some (, b)
          let f a in
          match le_lt_dec with
          | left _ Some (, b)
          | right _ Some (, a)
          end
      end
  end.

Theorem find_min_correct :
  l : list A,
 match find_min l with
 | None l = nil
 | Some (a, b) (In b l a = f b) ( c : A, In c l f b f c)
 end.
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a ; case (find_min ); simpl in |- *.
intros p; case p; simpl in |- *.
intros n b ((, ), ); case (le_lt_dec n (f a)); simpl in |- *.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; rewrite ; auto.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; auto.
apply le_trans with (f b); auto.
rewrite ; auto with arith.
intros H; rewrite H; split; simpl in |- *; auto.
intros c [| ]; rewrite || case ; auto.
Qed.


(* Search in the list for the max with respect to a valuation function f *)
Fixpoint find_max (l : list A) : option ( A)
  match l with
  | nil None
  | a
      match find_max with
      | None Some (f a, a)
      | Some (, b)
          let f a in
          match le_lt_dec with
          | right _ Some (, b)
          | left _ Some (, a)
          end
      end
  end.

Theorem find_max_correct :
  l : list A,
 match find_max l with
 | None l = nil
 | Some (a, b) (In b l a = f b) ( c : A, In c l f c f b)
 end.
Proof using.
intros l; elim l; simpl in |- *; auto.
intros a ; case (find_max ); simpl in |- *.
intros p; case p; simpl in |- *.
intros n b ((, ), ); case (le_lt_dec n (f a)); simpl in |- *.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; auto.
apply le_trans with (f b); auto.
rewrite ; auto with arith.
intros ; split; auto.
intros c [| ]; auto.
rewrite ; auto.
apply le_trans with (f b); auto.
rewrite ; auto with arith.
intros H; rewrite H; split; simpl in |- *; auto.
intros c [| ]; rewrite || case ; auto.
Qed.


End FindMin.
Arguments find_min [A].
Arguments find_max [A].