(* 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                                                     *)

Build process to iteratively merge two smaller trees

  • Key definitions: build, build_fun
  • Initial author: Laurent.Thery@inria.fr (2003)

From Huffman Require Export OneStep HeightPred CoverMin OrderedCover SubstPred.
From Coq Require Import ArithRing Sorting.Permutation.

Set Default Proof Using "Type".

Section Build.
Variable A : Type.
Variable f : A .

Local Hint Constructors Permutation : core.
Local Hint Resolve Permutation_refl : core.
Local Hint Resolve Permutation_app : core.
Local Hint Resolve Permutation_app_swap : core.

Iterative the one step predicate
Inductive build : list (btree A) btree A Prop
  | build_one : t : btree A, build (t []) t
  | build_step :
       (t : btree A) (l1 l2 : list (btree A)),
      one_step f build t build t.

Building gives a cover
Theorem build_cover : l t, build l t cover l t.
Proof.
intros l t H; elim H; clear H l t; auto.
intros t (, (, (, (HH, (, ))))) ; try assumption.
apply cover_node with (1 ); auto.
apply cover_permutation with (2 ); auto.
Qed.


Building is compatible with the weight
Theorem build_comp :
  (l1 l2 : list (btree A)) (t1 t2 : btree A),
 build
 build
 weight_tree_list f = weight_tree_list f
 same_sum_leaves f weight_tree f = weight_tree f .
Proof.
intros H; generalize ; elim H; clear H .
intros t H (, (, (, (, )))).
generalize ; inversion H; clear .
simpl in |- *; repeat rewrite plus_n_O; auto.
case .
intros (, (, (, (, )))).
absurd (length = length ( )).
rewrite Permutation_length with (1 ).
rewrite map_length with (f sum_leaves f) (l ).
rewrite .
rewrite map_length with (f sum_leaves f).
rewrite Permutation_length with (1 Permutation_sym ).
simpl in |- *; red in |- *; intros; discriminate.
apply Permutation_length with (1 ).
intros t H .
inversion .
case H.
intros (, (, (, (, )))).
case .
intros (, (, (, ))).
absurd (length = length ( )).
rewrite Permutation_length with (1 ).
rewrite map_length with (f sum_leaves f) (l ).
rewrite .
rewrite map_length with (f sum_leaves f).
rewrite Permutation_length with (1 Permutation_sym ).
rewrite ; simpl in |- *; red in |- *; intros; discriminate.
apply Permutation_length with (1 ).
apply with (1 ).
case one_step_comp with (3 H) (4 ); auto.
case one_step_comp with (3 H) (4 ); auto.
Qed.


Two built trees have same weight
Theorem build_same_weight_tree :
  (l : list (btree A)) (t1 t2 : btree A),
 build l build l weight_tree f = weight_tree f .
Proof.
intros l H ; apply build_comp with ( l) ( l); auto.
exists l; exists l; simpl in |- *; auto.
Qed.


Building is compatible with permutation
Theorem build_permutation :
  (l1 l2 : list (btree A)) (t : btree A),
 build t Permutation build t.
Proof.
intros t H; generalize ; elim H; clear H t; auto.
intros t H; rewrite Permutation_length_1_inv with (1 H); auto.
apply build_one.
intros t H .
apply build_step with ( ); auto.
case H.
intros (, (, (, (, )))).
exists ; exists ; exists ; repeat (split; auto).
apply Permutation_trans with (2 ); auto.
apply Permutation_sym; auto.
Qed.


Definition obuildf :
   l : list (btree A),
  l [] ordered (sum_order f) l {t : btree A | build l t}.
Proof.
intros l; elim l using list_length_induction.
intros ; case ; clear .
intros H ; case ; auto.
intros b ; case .
intros H ; exists b; auto.
apply build_one.
intros H .
case (H (insert (le_sum f) (node b ) )); auto.
rewrite Permutation_length with
 (1 insert_permutation _ (le_sum f) (node b ));
 simpl in |- *; auto.
red in |- *; intros ;
 absurd
  (length (node b ) = length (insert (le_sum f) (node b ) )).
rewrite ; simpl in |- *; intros; discriminate.
apply Permutation_length
  with (1 insert_permutation _ (le_sum f) (node b ));
 simpl in |- *; auto.
apply insert_ordered; auto.
intros; apply le_sum_correct1; auto.
intros; apply le_sum_correct2; auto.
apply ordered_inv with (a ); auto.
apply ordered_inv with (a b); auto.
intros t Ht; exists t.
apply build_step with (2 Ht).
red in |- *; auto.
exists ; exists b; exists ; (repeat split; auto).
apply Permutation_sym; apply insert_permutation.
Defined.


a function to buid tree from a cover list merging smaller trees
Definition buildf :
   l : list (btree A), l [] {t : btree A | build l t}.
Proof.
intros l Hl; cut (isort (le_sum f) l []).
intros ; cut (ordered (sum_order f) (isort (le_sum f) l)).
intros ; case (obuildf (isort (le_sum f) l) ).
intros t ; exists t; auto.
apply build_permutation with (1 ); auto.
apply Permutation_sym; apply isort_permutation; auto.
apply isort_ordered; auto.
intros; apply le_sum_correct1; auto.
intros; apply le_sum_correct2; auto.
contradict Hl; apply Permutation_nil; auto.
rewrite Hl; auto.
apply Permutation_sym.
apply isort_permutation; auto.
Defined.


Merging smaller trees gets the tree of mimimal weight for the given cover
Theorem build_correct :
  (l : list (btree A)) (t : btree A),
 l [] build l t cover_min _ f l t.
Proof.
intros l; elim l using list_length_ind.
intros H t .
case (cover_min_ex _ f) with (1 ); auto.
intros (, ).
case cover_ordered_cover with (1 ); auto.
intros (, ).
case (ordered_cover_height_pred A 0) with (1 ).
intros .
case exist_first_max with .
apply height_pred_not_nil1 with (1 ); auto.
intros a (, (, (, (, )))).
cut (length = length );
 [ intros IL | apply height_pred_length with (1 ) ].
rewrite in ; rewrite in IL; clear .
case height_pred_disj_larger with (1 ); auto.
intros (, ); rewrite in ; rewrite in IL; rewrite in ;
 clear ; auto.
case same_length_ex with (1 IL); auto.
intros (, (, (, (, )))).
generalize ; case ; try (simpl in |- *; intros; discriminate);
 clear .
intros ; rewrite in ; rewrite in IL;
 rewrite in ; rewrite in ; clear .
cut
 ( b1,
    ( c1,
       ( l4,
          Permutation ( ) ( )
          ordered (sum_order f) ( )))).
intros (, (, (, (, )))).
case
 prod2list_reorder2
  with ( ) ( ) (5 ) (6 ) (a a);
 auto with datatypes.
intros b ; apply Nat.lt_le_incl; auto with arith.
intros (, (, (, (, )))).
case height_pred_subst_pred with (1 ) ( );
 auto.
rewrite IL; repeat rewrite app_length; simpl in |- *; auto.
intros (, ).
case (buildf ( node )); auto.
case ; simpl in |- *; intros; discriminate.
intros .
case H with (3 ); auto with arith.
rewrite Permutation_length with (1 ).
rewrite Permutation_length with (1 ).
rewrite Permutation_length with (1 ).
repeat rewrite app_length; simpl in |- *; auto with arith.
case ; simpl in |- *; intros; discriminate.
intros .
split; auto.
apply build_cover with (1 ).
intros ; apply Nat.le_trans with (weight_tree f ); auto.
rewrite (build_same_weight_tree t ); auto.
apply Nat.le_trans with (weight_tree f ).
apply ; auto.
apply ordered_cover_cover.
apply (height_pred_ordered_cover A 0 ( pred a )); auto.
apply height_pred_shrink with (b a); auto.
replace (weight_tree f ) with (0 sum_leaves f + weight_tree f );
 [ idtac | simpl in |- *; auto ].
rewrite height_pred_weight with (1 ).
replace (weight_tree f ) with (0 sum_leaves f + weight_tree f );
 [ idtac | simpl in |- *; auto ].
rewrite height_pred_weight with (1 ); auto.
apply build_step with (2 ); auto.
exists ; exists ; exists ; repeat (split; auto).
apply Permutation_trans with (1 ).
apply Permutation_sym; apply Permutation_trans with (1 ).
apply Permutation_sym; apply Permutation_trans with (1 ); auto.
apply Permutation_trans with ((node ) ); auto.
simpl in |- *; apply perm_skip.
apply Permutation_cons_inv with .
apply Permutation_cons_inv with .
apply Permutation_sym; apply Permutation_trans with (1 ).
apply (Permutation_app_swap ( )).
generalize (isort_permutation _ (le_sum f) ( ));
 generalize
  (isort_ordered _ (sum_order f) (le_sum f) (le_sum_correct1 _ f)
     (le_sum_correct2 _ f) ( )).
case (isort (le_sum f) ( )); auto.
intros .
absurd ( = []); auto.
case ; simpl in |- *; intros; discriminate.
apply Permutation_sym in .
apply Permutation_nil with (1 ).
intros b ; case .
intros ; absurd ( = b []).
case ; simpl in |- *; try (intros; discriminate).
intros ; case ; try (intros; discriminate).
apply Permutation_length_1_inv with (1 Permutation_sym ).
intros ; exists b; exists ; exists ; auto.
intros ((, (, )), ); split.
apply build_cover with (1 ).
intros ; rewrite cover_one_inv with ( ) ( ).
rewrite cover_one_inv with ( ) ( t); auto.
rewrite ; apply cover_permutation with (2 ); auto.
apply build_cover with (1 ).
rewrite ; apply cover_permutation with (2 ); auto.
Qed.


Final function that tree of minimal weight for the cover
Definition build_fun :
   l : list (btree A), l [] {t : btree A | cover_min _ f l t}.
Proof.
intros l Hl; case (buildf l Hl).
intros x b; exists x.
apply build_correct; auto.
Defined.


End Build.

Arguments build [A].