(* 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 *)
(* 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 *)
A predicate for relating a height list with a cover
- Key definitions: height_pred
- Initial author: Laurent.Thery@inria.fr (2003)
From Coq Require Import ArithRing.
From Huffman Require Export AuxLib OrderedCover WeightTree Ordered Prod2List.
Set Default Proof Using "Type".
Section HeightPred.
Variable A : Type.
Variable f : A -> nat.
Variable A_eq_dec : forall a b : A, {a = b} + {a <> b}.
Inductive height_pred : nat -> list nat -> list (btree A) -> btree A -> Prop :=
| height_pred_nil :
forall (n : nat) (t : btree A), height_pred n (n :: []) (t :: []) t
| height_pred_node :
forall (n : nat) (ln1 ln2 : list nat) (t1 t2 : btree A)
(l1 l2 : list (btree A)),
height_pred (S n) ln1 l1 t1 ->
height_pred (S n) ln2 l2 t2 ->
height_pred n (ln1 ++ ln2) (l1 ++ l2) (node t1 t2).
Local Hint Resolve height_pred_nil height_pred_node : core.
| height_pred_nil :
forall (n : nat) (t : btree A), height_pred n (n :: []) (t :: []) t
| height_pred_node :
forall (n : nat) (ln1 ln2 : list nat) (t1 t2 : btree A)
(l1 l2 : list (btree A)),
height_pred (S n) ln1 l1 t1 ->
height_pred (S n) ln2 l2 t2 ->
height_pred n (ln1 ++ ln2) (l1 ++ l2) (node t1 t2).
Local Hint Resolve height_pred_nil height_pred_node : core.
The cover is an ordered cover
Theorem height_pred_ordered_cover :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> ordered_cover l t.
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
Qed.
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> ordered_cover l t.
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
Qed.
The height list is never empty
Theorem height_pred_not_nil1 :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> ln <> [].
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros; discriminate.
intros n0 ln1 ln2 t1 t2 l1 l2 H0; case ln1; simpl in |- *; auto.
intros; discriminate.
Qed.
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> ln <> [].
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros; discriminate.
intros n0 ln1 ln2 t1 t2 l1 l2 H0; case ln1; simpl in |- *; auto.
intros; discriminate.
Qed.
The cover list is never empty
Theorem height_pred_not_nil2 :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> l <> [].
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros; discriminate.
intros n0 ln1 ln2 t1 t2 l1 l2 H0; case l1; simpl in |- *; auto.
intros; discriminate.
Qed.
(* The height and cover lists have same length *)
Theorem height_pred_length :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> length ln = length l.
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros; repeat rewrite app_length; auto with arith.
Qed.
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> l <> [].
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros; discriminate.
intros n0 ln1 ln2 t1 t2 l1 l2 H0; case l1; simpl in |- *; auto.
intros; discriminate.
Qed.
(* The height and cover lists have same length *)
Theorem height_pred_length :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> length ln = length l.
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros; repeat rewrite app_length; auto with arith.
Qed.
The height and cover list gives a simple relation between
weight_tree, sum_leaves and the product of the two lists
Theorem height_pred_weight :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
n * sum_leaves f t + weight_tree f t = prod2list f ln l.
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros n0 ln1 ln2 t1 t2 l1 l2 H0 H1 H2 H3.
rewrite prod2list_app; auto with arith.
rewrite <- H3; rewrite <- H1; ring.
apply height_pred_length with (1 := H0); auto.
Qed.
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
n * sum_leaves f t + weight_tree f t = prod2list f ln l.
Proof.
intros n ln t l H; elim H; simpl in |- *; auto.
intros n0 ln1 ln2 t1 t2 l1 l2 H0 H1 H2 H3.
rewrite prod2list_app; auto with arith.
rewrite <- H3; rewrite <- H1; ring.
apply height_pred_length with (1 := H0); auto.
Qed.
Ordered covers can be completed with a height list
Theorem ordered_cover_height_pred :
forall (n : nat) (t : btree A) (l : list (btree A)),
ordered_cover l t -> exists ln : list nat, height_pred n ln l t.
Proof.
intros n t l H; generalize n; elim H; clear n t l H.
intros t l n; exists (n :: []); auto.
intros t1 t2 l1 l2 l3 H H0 H1 H2 n.
case (H0 (S n)); intros ln1 HH1.
case (H2 (S n)); intros ln2 HH2.
exists (ln1 ++ ln2); auto.
Qed.
forall (n : nat) (t : btree A) (l : list (btree A)),
ordered_cover l t -> exists ln : list nat, height_pred n ln l t.
Proof.
intros n t l H; generalize n; elim H; clear n t l H.
intros t l n; exists (n :: []); auto.
intros t1 t2 l1 l2 l3 H H0 H1 H2 n.
case (H0 (S n)); intros ln1 HH1.
case (H2 (S n)); intros ln2 HH2.
exists (ln1 ++ ln2); auto.
Qed.
Elements in the height list are always larger than the initial height
Theorem height_pred_larger :
forall (n n1 : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> In n1 ln -> n <= n1.
Proof.
intros n n1 ln t l H; generalize n1; elim H; clear H n ln t l n1;
auto with arith.
intros n t n1 [H2| H2]; [ rewrite H2 | case H2 ]; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 n1 H3; apply Nat.le_trans with (S n);
auto with arith.
case in_app_or with (1 := H3); auto.
Qed.
forall (n n1 : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> In n1 ln -> n <= n1.
Proof.
intros n n1 ln t l H; generalize n1; elim H; clear H n ln t l n1;
auto with arith.
intros n t n1 [H2| H2]; [ rewrite H2 | case H2 ]; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 n1 H3; apply Nat.le_trans with (S n);
auto with arith.
case in_app_or with (1 := H3); auto.
Qed.
In the height list is not a singleton, all its element are
strictly larger than the initial height
Theorem height_pred_larger_strict :
forall (n n1 : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> In n1 ln -> n < n1 \/ ln = n :: [] /\ l = t :: [].
Proof.
intros n n1 ln t l H; generalize n1; elim H; clear H n ln t l n1; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 n1 H3; left;
apply Nat.lt_le_trans with (S n); auto.
case in_app_or with (1 := H3).
intros H4; apply height_pred_larger with (1 := H); auto.
intros H4; apply height_pred_larger with (1 := H1); auto.
Qed.
forall (n n1 : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> In n1 ln -> n < n1 \/ ln = n :: [] /\ l = t :: [].
Proof.
intros n n1 ln t l H; generalize n1; elim H; clear H n ln t l n1; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 n1 H3; left;
apply Nat.lt_le_trans with (S n); auto.
case in_app_or with (1 := H3).
intros H4; apply height_pred_larger with (1 := H); auto.
intros H4; apply height_pred_larger with (1 := H1); auto.
Qed.
There always a larger element that the initial height in the heigh list
Theorem height_pred_larger_ex :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> exists n1, In n1 ln /\ n <= n1.
Proof.
intros n ln t l H; elim H; clear H n ln t l.
intros n t; exists n; auto with datatypes.
intros n ln1 ln2 t1 t2 l1 l2 H (n1, (HH1, HH2)) H1 H2.
exists n1; auto with datatypes arith.
Qed.
Lemma height_pred_disj_larger_aux :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
forall ln1 ln2 a,
ln = ln1 ++ a :: ln2 ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 ln2 -> n1 <= a) ->
(exists ln3, ln2 = a :: ln3) \/ ln = n :: [] /\ l = t :: [].
Proof.
intros n ln t l H; elim H; clear H n ln t l.
intros n t l ln1 ln2 a; case ln1; simpl in |- *; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 ln0 ln3 a H3 H4 H5.
case app_inv_app with (1 := H3).
intros (ln4, H7); auto.
cut (ln3 = ln4 ++ ln2);
[ intros E1
| apply app_inv_head with (l := ln0 ++ a :: []); repeat rewrite app_ass;
simpl in |- *; rewrite <- H3; rewrite H7; rewrite app_ass;
auto ].
case H0 with (1 := H7); auto; clear H0 H2.
intros n1 H8; apply H5; rewrite E1; auto with datatypes.
intros (ln5, HH); left; exists (ln5 ++ ln2).
apply trans_equal with (1 := E1); rewrite HH; auto.
intros (HH1, HH2).
cut (ln0 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H7; case ln0; simpl in |- *;
[ case ln4; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
generalize E1 H1; case ln2; simpl in |- *; auto; clear E1 H1.
intros E1 H1; case height_pred_not_nil2 with (1 := H1); auto.
generalize (height_pred_length _ _ _ _ H1); case l2; simpl in |- *; auto;
intros; discriminate.
intros n0 ln5 E1 H1; case height_pred_larger_strict with (n1 := n0) (1 := H1);
simpl in |- *; auto with datatypes.
intros HH6; contradict HH6; apply Nat.le_ngt; rewrite <- HH5; apply H5;
rewrite E1; auto with datatypes.
intros (H8, H9); left; exists []; injection H8.
intros HH7 HH8; rewrite HH5; rewrite <- HH8; rewrite <- HH7; rewrite E1;
rewrite HH4; auto.
intros (ln4, H7); auto.
cut (ln0 = ln1 ++ ln4);
[ intros E1
| apply app_inv_tail with (l := a :: ln3); rewrite <- H3; rewrite H7;
rewrite app_ass; auto ].
case H2 with (1 := H7); auto.
intros n1 H6; apply H4; rewrite E1; auto with datatypes.
intros (HH1, HH2).
cut (ln3 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H7; case ln4; simpl in |- *;
[ case ln3; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
case height_pred_larger_ex with (1 := H); auto.
intros n1; rewrite <- HH5; intros (HH6, HH7).
contradict HH7; apply Nat.lt_nge; apply H4; rewrite E1; auto with datatypes.
Qed.
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t -> exists n1, In n1 ln /\ n <= n1.
Proof.
intros n ln t l H; elim H; clear H n ln t l.
intros n t; exists n; auto with datatypes.
intros n ln1 ln2 t1 t2 l1 l2 H (n1, (HH1, HH2)) H1 H2.
exists n1; auto with datatypes arith.
Qed.
Lemma height_pred_disj_larger_aux :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
forall ln1 ln2 a,
ln = ln1 ++ a :: ln2 ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 ln2 -> n1 <= a) ->
(exists ln3, ln2 = a :: ln3) \/ ln = n :: [] /\ l = t :: [].
Proof.
intros n ln t l H; elim H; clear H n ln t l.
intros n t l ln1 ln2 a; case ln1; simpl in |- *; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 ln0 ln3 a H3 H4 H5.
case app_inv_app with (1 := H3).
intros (ln4, H7); auto.
cut (ln3 = ln4 ++ ln2);
[ intros E1
| apply app_inv_head with (l := ln0 ++ a :: []); repeat rewrite app_ass;
simpl in |- *; rewrite <- H3; rewrite H7; rewrite app_ass;
auto ].
case H0 with (1 := H7); auto; clear H0 H2.
intros n1 H8; apply H5; rewrite E1; auto with datatypes.
intros (ln5, HH); left; exists (ln5 ++ ln2).
apply trans_equal with (1 := E1); rewrite HH; auto.
intros (HH1, HH2).
cut (ln0 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H7; case ln0; simpl in |- *;
[ case ln4; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
generalize E1 H1; case ln2; simpl in |- *; auto; clear E1 H1.
intros E1 H1; case height_pred_not_nil2 with (1 := H1); auto.
generalize (height_pred_length _ _ _ _ H1); case l2; simpl in |- *; auto;
intros; discriminate.
intros n0 ln5 E1 H1; case height_pred_larger_strict with (n1 := n0) (1 := H1);
simpl in |- *; auto with datatypes.
intros HH6; contradict HH6; apply Nat.le_ngt; rewrite <- HH5; apply H5;
rewrite E1; auto with datatypes.
intros (H8, H9); left; exists []; injection H8.
intros HH7 HH8; rewrite HH5; rewrite <- HH8; rewrite <- HH7; rewrite E1;
rewrite HH4; auto.
intros (ln4, H7); auto.
cut (ln0 = ln1 ++ ln4);
[ intros E1
| apply app_inv_tail with (l := a :: ln3); rewrite <- H3; rewrite H7;
rewrite app_ass; auto ].
case H2 with (1 := H7); auto.
intros n1 H6; apply H4; rewrite E1; auto with datatypes.
intros (HH1, HH2).
cut (ln3 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H7; case ln4; simpl in |- *;
[ case ln3; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
case height_pred_larger_ex with (1 := H); auto.
intros n1; rewrite <- HH5; intros (HH6, HH7).
contradict HH7; apply Nat.lt_nge; apply H4; rewrite E1; auto with datatypes.
Qed.
The first maximum height in the list is immediately repeated once
Theorem height_pred_disj_larger :
forall (n a : nat) (ln1 ln2 : list nat) (t : btree A) (l : list (btree A)),
height_pred n (ln1 ++ a :: ln2) l t ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 ln2 -> n1 <= a) ->
(exists ln3, ln2 = a :: ln3) \/
(ln1 = [] /\ a = n /\ ln2 = []) /\ l = t :: [].
Proof.
intros n a ln1 ln2 t l H H0 H1;
case
height_pred_disj_larger_aux
with (a := a) (ln1 := ln1) (ln2 := ln2) (1 := H);
auto; case ln1; simpl in |- *;
[ intros (HH1, HH2); injection HH1; auto
| intros n0 l1; case l1; simpl in |- *; intuition; try discriminate ].
Qed.
Lemma height_pred_disj_larger2_aux :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
forall ln1 ln2 a,
ln = ln1 ++ a :: ln2 ->
(exists n1, In n1 ln1 /\ a <= n1) \/
(exists n1, In n1 ln2 /\ a <= n1) \/ ln = n :: [] /\ l = t :: [].
Proof.
intros n ln t l H; elim H; clear H n ln t l.
intros n t l ln1 ln2 a; case ln1; simpl in |- *; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 ln0 ln3 a H3.
case app_inv_app with (1 := H3).
intros (ln4, H4); auto.
cut (ln3 = ln4 ++ ln2);
[ intros E1
| apply app_inv_head with (l := ln0 ++ a :: []); repeat rewrite app_ass;
simpl in |- *; rewrite <- H3; rewrite H4; rewrite app_ass;
auto ].
case H0 with (1 := H4); auto; intros [(n1, (HH1, HH2))| (HH1, HH2)]; auto;
clear H0 H2.
right; left; exists n1; split; auto; rewrite E1; auto with datatypes.
cut (ln0 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H4; case ln0; simpl in |- *;
[ case ln4; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
case height_pred_larger_ex with (1 := H1); auto.
intros n1; rewrite <- HH5; intros (HM1, HM2).
right; left; exists n1; split; auto; rewrite E1; auto with datatypes.
intros (ln4, H4); auto.
cut (ln0 = ln1 ++ ln4);
[ intros E1
| apply app_inv_tail with (l := a :: ln3); rewrite <- H3; rewrite H4;
rewrite app_ass; auto ].
case H2 with (1 := H4); auto; clear H0 H2.
intros (n1, (HH1, HH2)); left; exists n1; split; auto; rewrite E1;
auto with datatypes.
intros [HH1| (HH1, HH2)]; auto.
cut (ln3 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H4; case ln4; simpl in |- *;
[ case ln3; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
case height_pred_larger_ex with (1 := H); auto.
intros n1; rewrite <- HH5; intros (HM1, HM2).
left; exists n1; split; auto; rewrite E1; auto with datatypes.
Qed.
forall (n a : nat) (ln1 ln2 : list nat) (t : btree A) (l : list (btree A)),
height_pred n (ln1 ++ a :: ln2) l t ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 ln2 -> n1 <= a) ->
(exists ln3, ln2 = a :: ln3) \/
(ln1 = [] /\ a = n /\ ln2 = []) /\ l = t :: [].
Proof.
intros n a ln1 ln2 t l H H0 H1;
case
height_pred_disj_larger_aux
with (a := a) (ln1 := ln1) (ln2 := ln2) (1 := H);
auto; case ln1; simpl in |- *;
[ intros (HH1, HH2); injection HH1; auto
| intros n0 l1; case l1; simpl in |- *; intuition; try discriminate ].
Qed.
Lemma height_pred_disj_larger2_aux :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
forall ln1 ln2 a,
ln = ln1 ++ a :: ln2 ->
(exists n1, In n1 ln1 /\ a <= n1) \/
(exists n1, In n1 ln2 /\ a <= n1) \/ ln = n :: [] /\ l = t :: [].
Proof.
intros n ln t l H; elim H; clear H n ln t l.
intros n t l ln1 ln2 a; case ln1; simpl in |- *; auto.
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 ln0 ln3 a H3.
case app_inv_app with (1 := H3).
intros (ln4, H4); auto.
cut (ln3 = ln4 ++ ln2);
[ intros E1
| apply app_inv_head with (l := ln0 ++ a :: []); repeat rewrite app_ass;
simpl in |- *; rewrite <- H3; rewrite H4; rewrite app_ass;
auto ].
case H0 with (1 := H4); auto; intros [(n1, (HH1, HH2))| (HH1, HH2)]; auto;
clear H0 H2.
right; left; exists n1; split; auto; rewrite E1; auto with datatypes.
cut (ln0 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H4; case ln0; simpl in |- *;
[ case ln4; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
case height_pred_larger_ex with (1 := H1); auto.
intros n1; rewrite <- HH5; intros (HM1, HM2).
right; left; exists n1; split; auto; rewrite E1; auto with datatypes.
intros (ln4, H4); auto.
cut (ln0 = ln1 ++ ln4);
[ intros E1
| apply app_inv_tail with (l := a :: ln3); rewrite <- H3; rewrite H4;
rewrite app_ass; auto ].
case H2 with (1 := H4); auto; clear H0 H2.
intros (n1, (HH1, HH2)); left; exists n1; split; auto; rewrite E1;
auto with datatypes.
intros [HH1| (HH1, HH2)]; auto.
cut (ln3 = [] /\ ln4 = [] /\ a = S n);
[ intros (HH3, (HH4, HH5))
| generalize HH1; rewrite H4; case ln4; simpl in |- *;
[ case ln3; try (intros; discriminate); (intros HH6; injection HH6; auto)
| intros n0 l; case l; simpl in |- *; intros; discriminate ] ].
case height_pred_larger_ex with (1 := H); auto.
intros n1; rewrite <- HH5; intros (HM1, HM2).
left; exists n1; split; auto; rewrite E1; auto with datatypes.
Qed.
There is no strict maximum in a list
Theorem height_pred_disj_larger2 :
forall (n a : nat) (ln1 ln2 : list nat) (t : btree A) (l : list (btree A)),
height_pred n (ln1 ++ a :: ln2) l t ->
(exists n1, In n1 ln1 /\ a <= n1) \/
(exists n1, In n1 ln2 /\ a <= n1) \/
(ln1 = [] /\ a = n /\ ln2 = []) /\ l = t :: [].
Proof.
intros n a ln1 ln2 t l H;
case
height_pred_disj_larger2_aux
with (a := a) (ln1 := ln1) (ln2 := ln2) (1 := H);
auto.
intros [H1| (H1, H2)]; auto.
generalize H1 H2; case ln1; simpl in |- *;
[ intros H3; injection H3; auto with datatypes | idtac ].
intros H0 H4 H5; repeat right; auto.
intros n0 l0; case l0; simpl in |- *; intros; discriminate.
Qed.
Theorem height_pred_shrink_aux :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
forall l1 l2 ln1 ln2 a b t1 t2,
ln = ln1 ++ a :: b :: ln2 ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 (b :: ln2) -> n1 <= a) ->
length ln1 = length l1 ->
l = l1 ++ t1 :: t2 :: l2 ->
height_pred n (ln1 ++ pred a :: ln2) (l1 ++ node t1 t2 :: l2) t.
Proof.
intros n ln t l H; elim H; clear n ln t l H; auto.
intros n t l1 l2 ln1 ln2 a b t1 t2; case ln1;
try (simpl in |- *; intros; discriminate).
intros n0 l0; case l0; try (simpl in |- *; intros; discriminate).
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 l0 l3 ln0 ln3 a b t0 t3 H3 H4 H5 H6
H7.
cut (length ln1 = length l1);
[ intros Eq2 | apply height_pred_length with (1 := H) ].
cut (length ln2 = length l2);
[ intros Eq3 | apply height_pred_length with (1 := H1) ].
cut (length ln3 = length l3);
[ intros Eq4
| apply Nat.add_cancel_l with (length (ln0 ++ a :: b :: []));
rewrite <- app_length; rewrite app_ass; simpl in |- *;
rewrite <- H3; repeat rewrite app_length; simpl in |- *;
rewrite Eq2; rewrite Eq3; rewrite <- app_length;
rewrite H7; repeat rewrite app_length; simpl in |- *;
repeat rewrite (fun x y => Nat.add_comm x (S y));
simpl in |- *; rewrite Nat.add_comm; auto ].
case app_inv_app2 with (1 := H3); auto.
intros (ln4, Hp1).
cut (ln3 = ln4 ++ ln2);
[ intros E1
| apply app_inv_head with (l := ln0 ++ a :: b :: []);
repeat rewrite app_ass; simpl in |- *; rewrite <- H3;
rewrite Hp1; repeat rewrite app_ass; auto ].
replace (ln0 ++ pred a :: ln3) with ((ln0 ++ pred a :: ln4) ++ ln2);
[ idtac | rewrite app_ass; rewrite E1; auto ].
cut (l3 = firstn (length ln4) l3 ++ l2).
intros HH;
replace (l0 ++ node t0 t3 :: l3) with
((l0 ++ node t0 t3 :: firstn (length ln4) l3) ++ l2);
[ idtac | pattern l3 at 2 in |- *; rewrite HH; rewrite app_ass; auto ].
apply height_pred_node; auto.
apply H0 with (1 := Hp1); auto.
intros n1 HH1; (apply H5; auto).
simpl in HH1; case HH1; intros H9; try rewrite H9; auto with datatypes.
rewrite E1; auto with datatypes.
apply app_inv_tail with (l := l2).
repeat rewrite app_ass; apply trans_equal with (1 := H7); auto.
pattern l3 at 1 in |- *; rewrite HH; auto.
apply sym_equal;
apply trans_equal with (2 := firstn_skipn (length ln4) l3).
apply f_equal2 with (f := app (A:=btree A)); auto.
apply trans_equal with (skipn (length l1 - length l1) l2).
rewrite Nat.sub_diag; simpl in |- *; auto.
rewrite <- skipn_le_app1; auto.
rewrite H7.
rewrite <- Eq2; rewrite Hp1.
rewrite skipn_le_app1.
rewrite app_length.
rewrite H6.
rewrite <- Nat.add_comm.
rewrite Nat.add_sub. simpl in |- *; auto.
rewrite <- H6; rewrite app_length; simpl in |- *; auto with arith.
intros [(ln4, HH)| (HH1, HH2)].
cut (ln0 = ln1 ++ ln4);
[ intros E1
| apply app_inv_tail with (l := a :: b :: ln3); rewrite <- H3; rewrite HH;
rewrite app_ass; auto ].
cut (l0 = l1 ++ skipn (length l1) l0).
intros Eq1; rewrite Eq1; rewrite E1; repeat rewrite app_ass.
apply height_pred_node; auto.
apply H2 with (b := b); auto.
intros n1 H8; apply H4; (rewrite E1; auto with datatypes).
rewrite skipn_length; rewrite <- Eq2; rewrite <- H6;
rewrite <- skipn_length; rewrite E1; rewrite skipn_le_app2;
auto; rewrite skipn_all; simpl in |- *; auto.
apply app_inv_head with (l := l1).
rewrite <- app_ass; rewrite <- Eq1; auto.
apply sym_equal;
apply trans_equal with (2 := firstn_skipn (length l1) l0).
apply f_equal2 with (f := app (A:=btree A)); auto.
apply trans_equal with (firstn (length l1) (l1 ++ l2)).
rewrite firstn_le_app1; auto; rewrite Nat.sub_diag; simpl in |- *;
auto with datatypes.
rewrite H7; rewrite firstn_le_app2; auto.
rewrite <- H6; rewrite <- Eq2; rewrite E1; rewrite app_length;
auto with arith.
rewrite HH1 in H; case height_pred_disj_larger2 with (1 := H); simpl in |- *;
auto.
intros (n1, (HH3, HH4)); contradict HH4; auto with arith.
intros [(n1, (HH3, HH4))| ((HH3, (HH4, HH5)), HH6)]; [ case HH3 | idtac ].
case height_pred_larger_strict with (1 := H1) (n1 := b); auto.
rewrite HH2; auto with datatypes.
rewrite <- HH4; intros HH7; contradict HH7; apply Nat.le_ngt;
auto with arith datatypes.
intros (H8, H9); rewrite HH4; rewrite HH3; simpl in |- *.
cut (l0 = []); [ intros HM1; rewrite HM1 | idtac ].
cut (ln3 = []); [ intros HM2; rewrite HM2 | idtac ].
replace l3 with (nil (A:=btree A)); simpl in |- *; auto.
rewrite HH6 in H7; rewrite H9 in H7; rewrite HM1 in H7; simpl in H7;
injection H7.
intros Ht1 Ht2 Ht3; rewrite Ht2; rewrite Ht3; auto.
generalize Eq4; rewrite HM2; case l3; simpl in |- *; auto; intros;
discriminate.
rewrite HH2 in H8; injection H8; auto.
generalize H6; rewrite HH3; case l0; simpl in |- *; auto; intros;
discriminate.
Qed.
forall (n a : nat) (ln1 ln2 : list nat) (t : btree A) (l : list (btree A)),
height_pred n (ln1 ++ a :: ln2) l t ->
(exists n1, In n1 ln1 /\ a <= n1) \/
(exists n1, In n1 ln2 /\ a <= n1) \/
(ln1 = [] /\ a = n /\ ln2 = []) /\ l = t :: [].
Proof.
intros n a ln1 ln2 t l H;
case
height_pred_disj_larger2_aux
with (a := a) (ln1 := ln1) (ln2 := ln2) (1 := H);
auto.
intros [H1| (H1, H2)]; auto.
generalize H1 H2; case ln1; simpl in |- *;
[ intros H3; injection H3; auto with datatypes | idtac ].
intros H0 H4 H5; repeat right; auto.
intros n0 l0; case l0; simpl in |- *; intros; discriminate.
Qed.
Theorem height_pred_shrink_aux :
forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)),
height_pred n ln l t ->
forall l1 l2 ln1 ln2 a b t1 t2,
ln = ln1 ++ a :: b :: ln2 ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 (b :: ln2) -> n1 <= a) ->
length ln1 = length l1 ->
l = l1 ++ t1 :: t2 :: l2 ->
height_pred n (ln1 ++ pred a :: ln2) (l1 ++ node t1 t2 :: l2) t.
Proof.
intros n ln t l H; elim H; clear n ln t l H; auto.
intros n t l1 l2 ln1 ln2 a b t1 t2; case ln1;
try (simpl in |- *; intros; discriminate).
intros n0 l0; case l0; try (simpl in |- *; intros; discriminate).
intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 l0 l3 ln0 ln3 a b t0 t3 H3 H4 H5 H6
H7.
cut (length ln1 = length l1);
[ intros Eq2 | apply height_pred_length with (1 := H) ].
cut (length ln2 = length l2);
[ intros Eq3 | apply height_pred_length with (1 := H1) ].
cut (length ln3 = length l3);
[ intros Eq4
| apply Nat.add_cancel_l with (length (ln0 ++ a :: b :: []));
rewrite <- app_length; rewrite app_ass; simpl in |- *;
rewrite <- H3; repeat rewrite app_length; simpl in |- *;
rewrite Eq2; rewrite Eq3; rewrite <- app_length;
rewrite H7; repeat rewrite app_length; simpl in |- *;
repeat rewrite (fun x y => Nat.add_comm x (S y));
simpl in |- *; rewrite Nat.add_comm; auto ].
case app_inv_app2 with (1 := H3); auto.
intros (ln4, Hp1).
cut (ln3 = ln4 ++ ln2);
[ intros E1
| apply app_inv_head with (l := ln0 ++ a :: b :: []);
repeat rewrite app_ass; simpl in |- *; rewrite <- H3;
rewrite Hp1; repeat rewrite app_ass; auto ].
replace (ln0 ++ pred a :: ln3) with ((ln0 ++ pred a :: ln4) ++ ln2);
[ idtac | rewrite app_ass; rewrite E1; auto ].
cut (l3 = firstn (length ln4) l3 ++ l2).
intros HH;
replace (l0 ++ node t0 t3 :: l3) with
((l0 ++ node t0 t3 :: firstn (length ln4) l3) ++ l2);
[ idtac | pattern l3 at 2 in |- *; rewrite HH; rewrite app_ass; auto ].
apply height_pred_node; auto.
apply H0 with (1 := Hp1); auto.
intros n1 HH1; (apply H5; auto).
simpl in HH1; case HH1; intros H9; try rewrite H9; auto with datatypes.
rewrite E1; auto with datatypes.
apply app_inv_tail with (l := l2).
repeat rewrite app_ass; apply trans_equal with (1 := H7); auto.
pattern l3 at 1 in |- *; rewrite HH; auto.
apply sym_equal;
apply trans_equal with (2 := firstn_skipn (length ln4) l3).
apply f_equal2 with (f := app (A:=btree A)); auto.
apply trans_equal with (skipn (length l1 - length l1) l2).
rewrite Nat.sub_diag; simpl in |- *; auto.
rewrite <- skipn_le_app1; auto.
rewrite H7.
rewrite <- Eq2; rewrite Hp1.
rewrite skipn_le_app1.
rewrite app_length.
rewrite H6.
rewrite <- Nat.add_comm.
rewrite Nat.add_sub. simpl in |- *; auto.
rewrite <- H6; rewrite app_length; simpl in |- *; auto with arith.
intros [(ln4, HH)| (HH1, HH2)].
cut (ln0 = ln1 ++ ln4);
[ intros E1
| apply app_inv_tail with (l := a :: b :: ln3); rewrite <- H3; rewrite HH;
rewrite app_ass; auto ].
cut (l0 = l1 ++ skipn (length l1) l0).
intros Eq1; rewrite Eq1; rewrite E1; repeat rewrite app_ass.
apply height_pred_node; auto.
apply H2 with (b := b); auto.
intros n1 H8; apply H4; (rewrite E1; auto with datatypes).
rewrite skipn_length; rewrite <- Eq2; rewrite <- H6;
rewrite <- skipn_length; rewrite E1; rewrite skipn_le_app2;
auto; rewrite skipn_all; simpl in |- *; auto.
apply app_inv_head with (l := l1).
rewrite <- app_ass; rewrite <- Eq1; auto.
apply sym_equal;
apply trans_equal with (2 := firstn_skipn (length l1) l0).
apply f_equal2 with (f := app (A:=btree A)); auto.
apply trans_equal with (firstn (length l1) (l1 ++ l2)).
rewrite firstn_le_app1; auto; rewrite Nat.sub_diag; simpl in |- *;
auto with datatypes.
rewrite H7; rewrite firstn_le_app2; auto.
rewrite <- H6; rewrite <- Eq2; rewrite E1; rewrite app_length;
auto with arith.
rewrite HH1 in H; case height_pred_disj_larger2 with (1 := H); simpl in |- *;
auto.
intros (n1, (HH3, HH4)); contradict HH4; auto with arith.
intros [(n1, (HH3, HH4))| ((HH3, (HH4, HH5)), HH6)]; [ case HH3 | idtac ].
case height_pred_larger_strict with (1 := H1) (n1 := b); auto.
rewrite HH2; auto with datatypes.
rewrite <- HH4; intros HH7; contradict HH7; apply Nat.le_ngt;
auto with arith datatypes.
intros (H8, H9); rewrite HH4; rewrite HH3; simpl in |- *.
cut (l0 = []); [ intros HM1; rewrite HM1 | idtac ].
cut (ln3 = []); [ intros HM2; rewrite HM2 | idtac ].
replace l3 with (nil (A:=btree A)); simpl in |- *; auto.
rewrite HH6 in H7; rewrite H9 in H7; rewrite HM1 in H7; simpl in H7;
injection H7.
intros Ht1 Ht2 Ht3; rewrite Ht2; rewrite Ht3; auto.
generalize Eq4; rewrite HM2; case l3; simpl in |- *; auto; intros;
discriminate.
rewrite HH2 in H8; injection H8; auto.
generalize H6; rewrite HH3; case l0; simpl in |- *; auto; intros;
discriminate.
Qed.
A cover can be shrunk at the first maximum of the height while
preserving the height list
Theorem height_pred_shrink :
forall (n a b : nat) (ln1 ln2 : list nat) (t t1 t2 : btree A)
(l1 l2 : list (btree A)),
height_pred n (ln1 ++ a :: b :: ln2) (l1 ++ t1 :: t2 :: l2) t ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 (b :: ln2) -> n1 <= a) ->
length ln1 = length l1 ->
height_pred n (ln1 ++ pred a :: ln2) (l1 ++ node t1 t2 :: l2) t.
Proof.
intros n a b ln1 ln2 t t1 t2 l1 l2 H H0 H1 H2;
apply height_pred_shrink_aux with (1 := H) (b := b);
auto.
Qed.
forall (n a b : nat) (ln1 ln2 : list nat) (t t1 t2 : btree A)
(l1 l2 : list (btree A)),
height_pred n (ln1 ++ a :: b :: ln2) (l1 ++ t1 :: t2 :: l2) t ->
(forall n1 : nat, In n1 ln1 -> n1 < a) ->
(forall n1 : nat, In n1 (b :: ln2) -> n1 <= a) ->
length ln1 = length l1 ->
height_pred n (ln1 ++ pred a :: ln2) (l1 ++ node t1 t2 :: l2) t.
Proof.
intros n a b ln1 ln2 t t1 t2 l1 l2 H H0 H1 H2;
apply height_pred_shrink_aux with (1 := H) (b := b);
auto.
Qed.
Given a tree and its associated code it is possible to build
a height list (the length of the codes) and a cover (the leaves)
that are related
Theorem height_pred_compute_code :
forall (n : nat) (t : btree A),
height_pred n (map (fun x => length (snd x) + n) (compute_code t))
(map (fun x => leaf (fst x)) (compute_code t)) t.
Proof.
intros n t; generalize n; elim t; clear t n; simpl in |- *; auto.
intros b H b0 H0 n.
repeat rewrite map_app.
cut
(forall (b : bool) l,
map (fun x : A * list bool => length (snd x) + n)
(map (fun v : A * list bool => let (a1, b1) := v in (a1, b :: b1)) l) =
map (fun x : A * list bool => length (snd x) + S n) l);
[ intros E1 | idtac ].
cut
(forall b l,
map (fun x : A * list bool => leaf (fst x))
(map (fun v : A * list bool => let (a1, b1) := v in (a1, b :: b1)) l) =
map (fun x : A * list bool => leaf (fst x)) l); [ intros E2 | idtac ].
apply height_pred_node; repeat rewrite E1; repeat rewrite E2; auto.
intros b1 l; elim l; simpl in |- *; auto.
intros a; case a; simpl in |- *; auto.
intros a0 l0 l1 H1; apply f_equal2 with (f := cons (A:=btree A)); auto.
intros b1 l; elim l; simpl in |- *; auto.
intros a; case a; simpl in |- *; auto.
intros a0 l0 l1 H1; apply f_equal2 with (f := cons (A:=nat)); auto.
Qed.
forall (n : nat) (t : btree A),
height_pred n (map (fun x => length (snd x) + n) (compute_code t))
(map (fun x => leaf (fst x)) (compute_code t)) t.
Proof.
intros n t; generalize n; elim t; clear t n; simpl in |- *; auto.
intros b H b0 H0 n.
repeat rewrite map_app.
cut
(forall (b : bool) l,
map (fun x : A * list bool => length (snd x) + n)
(map (fun v : A * list bool => let (a1, b1) := v in (a1, b :: b1)) l) =
map (fun x : A * list bool => length (snd x) + S n) l);
[ intros E1 | idtac ].
cut
(forall b l,
map (fun x : A * list bool => leaf (fst x))
(map (fun v : A * list bool => let (a1, b1) := v in (a1, b :: b1)) l) =
map (fun x : A * list bool => leaf (fst x)) l); [ intros E2 | idtac ].
apply height_pred_node; repeat rewrite E1; repeat rewrite E2; auto.
intros b1 l; elim l; simpl in |- *; auto.
intros a; case a; simpl in |- *; auto.
intros a0 l0 l1 H1; apply f_equal2 with (f := cons (A:=btree A)); auto.
intros b1 l; elim l; simpl in |- *; auto.
intros a; case a; simpl in |- *; auto.
intros a0 l0 l1 H1; apply f_equal2 with (f := cons (A:=nat)); auto.
Qed.
A consequence of the previous theorem, the weight of the tree
is exactly the encoding of the message of the corresponding code
Theorem weight_tree_compute :
forall (m : list A) t,
distinct_leaves t ->
(forall a : A, f a = number_of_occurrences A_eq_dec a m) ->
length (encode A_eq_dec (compute_code t) m) = weight_tree f t.
Proof.
intros m t H0 H.
rewrite frequency_length; auto.
apply trans_equal with (0 * sum_leaves f t + weight_tree f t); auto.
rewrite height_pred_weight with (1 := height_pred_compute_code 0 t).
unfold prod2list in |- *.
rewrite
fold_left_eta
with
(f :=
fun (a : nat) (b : A * list bool) =>
a + number_of_occurrences A_eq_dec (fst b) m * length (snd b))
(f1 :=
fun (a : nat) (b : A * list bool) =>
a + (fun b => f (fst b) * length (snd b)) b);
auto.
rewrite <-
(fold_left_map _ _ (fun a b : nat => a + b) _ 0 (compute_code t)
(fun b : A * list bool => f (fst b) * length (snd b)))
.
rewrite fold_left_eta with (f := fun a b : nat => a + b) (f1 := plus); auto.
apply f_equal3 with (f := fold_left (A:=nat) (B:=nat)); auto.
elim (compute_code t); simpl in |- *; auto.
intros a l H1; apply f_equal2 with (f := cons (A:=nat)); auto with arith.
ring.
apply btree_unique_prefix2; auto.
Qed.
End HeightPred.
Arguments height_pred [A].
#[export] Hint Resolve height_pred_nil height_pred_node : core.
forall (m : list A) t,
distinct_leaves t ->
(forall a : A, f a = number_of_occurrences A_eq_dec a m) ->
length (encode A_eq_dec (compute_code t) m) = weight_tree f t.
Proof.
intros m t H0 H.
rewrite frequency_length; auto.
apply trans_equal with (0 * sum_leaves f t + weight_tree f t); auto.
rewrite height_pred_weight with (1 := height_pred_compute_code 0 t).
unfold prod2list in |- *.
rewrite
fold_left_eta
with
(f :=
fun (a : nat) (b : A * list bool) =>
a + number_of_occurrences A_eq_dec (fst b) m * length (snd b))
(f1 :=
fun (a : nat) (b : A * list bool) =>
a + (fun b => f (fst b) * length (snd b)) b);
auto.
rewrite <-
(fold_left_map _ _ (fun a b : nat => a + b) _ 0 (compute_code t)
(fun b : A * list bool => f (fst b) * length (snd b)))
.
rewrite fold_left_eta with (f := fun a b : nat => a + b) (f1 := plus); auto.
apply f_equal3 with (f := fold_left (A:=nat) (B:=nat)); auto.
elim (compute_code t); simpl in |- *; auto.
intros a l H1; apply f_equal2 with (f := cons (A:=nat)); auto with arith.
ring.
apply btree_unique_prefix2; auto.
Qed.
End HeightPred.
Arguments height_pred [A].
#[export] Hint Resolve height_pred_nil height_pred_node : core.