Huffman.PBTree

(* 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: PBTree.v                             
                                                                     
    Definition of partial binary trees (nodes have upto 2 sons)      
                                                                     
    Definitions:                                                     
        pbtree, inpb, pbfree, compute_pbcode, pbadd                  
        pbbuild, all_pbleaves, distinct_pbleaves, compute_pbcode     
                                                                     
                                    Laurent.Thery@inria.fr (2003)    
 **********************************************************************)


Require Import List.
From Huffman Require Import Aux.
From Huffman Require Import Code.
From Huffman Require Import Build.
From Huffman Require Import ISort.
Require Import Compare_dec.
From Huffman Require Import Permutation.
From Huffman Require Import UniqueKey.
From Huffman Require Import sTactic.

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

(* Partial Binary Tree (no more than 2 sons *)
Inductive pbtree : Type
  | pbleaf : A pbtree
  | pbleft : pbtree pbtree
  | pbright : pbtree pbtree
  | pbnode : pbtree pbtree pbtree.

(* Predictate for belonging *)
Theorem pbleaf_or_not :
  p, ( a : _, p = pbleaf a) ( a : A, p pbleaf a).
Proof using.
intros p; case p; simpl in |- *;
 try (intros; right; red in |- *; intros; discriminate).
intros a; left; exists a; simpl in |- *; auto.
Qed.


(* Predicate for belonging *)
Inductive inpb : pbtree pbtree Prop
  | inpb_leaf : t : pbtree, inpb t t
  | inpb_left : t : pbtree, inpb t inpb t (pbleft )
  | inpb_right : t : pbtree, inpb t inpb t (pbright )
  | inpb_node_l : t : pbtree, inpb t inpb t (pbnode )
  | inpb_node_r : t : pbtree, inpb t inpb t (pbnode ).
Hint Constructors inpb : core.

(* Equality on partial trees is decidable *)
Definition pbtree_dec : a b : pbtree, {a = b} + {a b}.
intros a; elim a; simpl in |- *; auto.
intros b; case b; try (intros; right; red in |- *; intros; discriminate).
intros ; case (eqA_dec ); intros .
left; rewrite ; auto.
right; red in |- *; Contradict ; inversion ; auto.
intros p H b; case b; try (intros; right; red in |- *; intros; discriminate).
intros ; case (H ).
intros e; rewrite e; auto.
intros ; right; Contradict ; inversion ; auto.
intros p H b; case b; try (intros; right; red in |- *; intros; discriminate).
intros ; case (H ).
intros e; rewrite e; auto.
intros ; right; Contradict ; inversion ; auto.
intros p H b; case b;
 try (intros; right; red in |- *; intros; discriminate).
intros ; case (H ); intros .
case ( ); intros .
left; rewrite ; rewrite ; auto.
right; Contradict ; injection ; auto.
right; Contradict ; injection ; auto.
Defined.

(* Belonging is decidable *)
Definition inpb_dec : a b, {inpb a b} + { inpb a b}.
intros a b; elim b.
intros ; case a;
 try (intros; right; red in |- *; intros HH; inversion HH; auto; fail).
intros ; case (eqA_dec ); intros HH.
left; rewrite HH; auto.
right; Contradict HH; inversion HH; auto.
intros p Hp; case Hp; auto; intros HH.
case (pbtree_dec a (pbleft p)); intros .
left; rewrite ; auto.
right; red in |- *; intros ; generalize HH ; inversion ; auto.
intros p Hp; case Hp; auto; intros HH.
case (pbtree_dec a (pbright p)); intros .
left; rewrite ; auto.
right; red in |- *; intros ; generalize HH ; inversion ; auto.
intros p H .
case H; auto; intros .
case ; auto; intros .
case (pbtree_dec a (pbnode p )); intros .
left; rewrite ; auto.
right; red in |- *; intros ; generalize ; inversion ; auto.
Defined.

(* inpb is transitive *)
Theorem inpb_trans : , inpb inpb inpb .
Proof using.
intros H ; generalize H; elim ; clear H ; auto.
Qed.


(* A partial tree has always a leaf *)
Theorem inpb_ex : t : pbtree, x : _, inpb (pbleaf x) t.
Proof using.
intros t; elim t; simpl in |- *; auto.
intros a; exists a; auto.
intros b (a, H); exists a; auto.
intros b (a, H); exists a; auto.
intros b (a, H) ; exists a; auto.
Qed.


(* Predicate for Partial Trees with Different Leaves *)
Definition distinct_pbleaves (t : pbtree) : Prop
   : pbtree,
  inpb (pbnode ) t inpb inpb .

(* A leaf tree has distinct leaves *)
Theorem distinct_pbleaves_Leaf : a : A, distinct_pbleaves (pbleaf a).
Proof using.
intros a; red in |- *.
intros H; inversion H.
Qed.

Hint Resolve distinct_pbleaves_Leaf : core.

(* Direct subtrees of a tree with distinct leaves have distinct leaves *)
Theorem distinct_pbleaves_l :
  : pbtree,
 distinct_pbleaves (pbnode ) distinct_pbleaves .
Proof using.
intros H; red in |- *.
intros a .
apply (H a ); auto.
Qed.


(* Direct subtrees of a tree with distinct leaves have distinct leaves *)
Theorem distinct_pbleaves_r :
  : pbtree,
 distinct_pbleaves (pbnode ) distinct_pbleaves .
Proof using.
intros H; red in |- *.
intros a .
apply (H a ); auto.
Qed.


(* Direct subtrees of a tree with distinct leaves have distinct leaves *)
Theorem distinct_pbleaves_pl :
  : pbtree, distinct_pbleaves (pbleft ) distinct_pbleaves .
Proof using.
intros H; red in |- *.
intros a .
apply (H a ); auto.
Qed.


(* Direct subtrees of a tree with distinct leaves have distinct leaves *)
Theorem distinct_pbleaves_pr :
  : pbtree, distinct_pbleaves (pbright ) distinct_pbleaves .
Proof using.
intros H; red in |- *.
intros a .
apply (H a ); auto.
Qed.


(* A leaf have distinct leaves *)
Theorem distinct_pbleaves_pbleaf : a : A, distinct_pbleaves (pbleaf a).
Proof using.
intros a; red in |- *.
intros H; inversion H.
Qed.

Hint Resolve distinct_pbleaves_pbleaf : core.

(* A left has distinct leaves if its subtree has it *)
Theorem distinct_pbleaves_pbleft :
  t, distinct_pbleaves t distinct_pbleaves (pbleft t).
Proof using.
intros t H; red in |- *.
intros a ; apply (H a ); auto.
inversion ; auto.
Qed.


(* A right has distinct leaves if its subtree has it *)
Theorem distinct_pbleaves_pbright :
  t, distinct_pbleaves t distinct_pbleaves (pbright t).
Proof using.
intros t H; red in |- *.
intros a ; apply (H a ); auto.
inversion ; auto.
Qed.

Hint Resolve distinct_pbleaves_pbleft distinct_pbleaves_pbright : core.

(* Transform a tree in a code *)
Fixpoint compute_pbcode (a : pbtree) : code A
  match a with
  | pbleaf b (b, nil) nil
  | pbleft
      map
        (fun v : A list bool
         match v with
         | (, ) (, false )
         end) (compute_pbcode )
  | pbright
      map
        (fun v : A list bool
         match v with
         | (, ) (, true )
         end) (compute_pbcode )
  | pbnode
      map
        (fun v : A list bool
         match v with
         | (, ) (, false )
         end) (compute_pbcode )
      map
        (fun v : A list bool
         match v with
         | (, ) (, true )
         end) (compute_pbcode )
  end.

(* Computed code are not empty *)
Theorem compute_pbcode_not_null : p, compute_pbcode p nil.
Proof using.
intros p; elim p; simpl in |- *; auto;
 try (intros ; case (compute_pbcode ); simpl in |- *; auto);
 intros; red in |- *; intros ; discriminate.
Qed.

Hint Resolve compute_pbcode_not_null : core.

(* Keys in the computed code are leaves of the tree *)
Theorem in_pbcompute_inpb :
  (t : pbtree) (a : A) (l : list bool),
 In (a, l) (compute_pbcode t) inpb (pbleaf a) t.
Proof using.
intros t; elim t; simpl in |- *; auto.
intros a l [| ]; try (case ; fail).
injection ; intros ; rewrite ; auto.
intros p H a l ; apply inpb_left; auto.
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ); apply (H a ); auto.
injection ; intros ; rewrite ; auto.
intros p H a l ; apply inpb_right; auto.
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ); apply (H a ); auto.
injection ; intros ; rewrite ; auto.
intros h H a l .
case in_app_or with (1 ); auto; intros .
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ); auto.
apply inpb_node_l; apply (H a ).
injection ; intros ; rewrite ; auto.
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ); auto.
apply inpb_node_r; apply ( a ).
injection ; intros ; rewrite ; auto.
Qed.


(* Leaves in the tree are keys in the code *)
Theorem inpb_compute_ex :
  a p, inpb (pbleaf a) p l : _, In (a, l) (compute_pbcode p).
Proof using.
intros a p; elim p; simpl in |- *; auto.
intros H; inversion H.
exists (nil (Abool)); auto.
intros H ; case H; auto.
inversion ; auto.
intros ; elim (compute_pbcode ); simpl in |- *; auto.
intros HH; case HH.
intros l [| ]; auto.
exists (false ); left; rewrite ; auto.
case ; auto.
intros x ; exists x; auto.
intros H ; case H; auto.
inversion ; auto.
intros ; elim (compute_pbcode ); simpl in |- *; auto.
intros HH; case HH.
intros l [| ]; auto.
exists (true ); left; rewrite ; auto.
case ; auto.
intros x ; exists x; auto.
intros H ; inversion .
case H; auto.
intros x Hx; exists (false x).
apply in_or_app; left; auto.
change
  (In ((fun v match v with
                 | (, ) (, false )
                 end) (a, x))
     (map (fun v match v with
                    | (, ) (, false )
                    end) (compute_pbcode ))) in |- *;
 apply in_map; auto.
case ; auto.
intros x Hx; exists (true x).
apply in_or_app; right; auto.
change
  (In ((fun v match v with
                 | (, ) (, true )
                 end) (a, x))
     (map (fun v match v with
                    | (, ) (, true )
                    end) (compute_pbcode ))) in |- *;
 apply in_map; auto.
Qed.


(* The computing code has the first property to be prefix *)
Theorem pb_unique_prefix1 :
  (t : pbtree) ( : A) ( : list bool),
 In (, ) (compute_pbcode t)
 In (, ) (compute_pbcode t) is_prefix = :>A.
Proof using.
intros t; elim t; simpl in |- *; auto.
intros leaf .
case ; intros ; [ injection | case ].
case ; intros ; [ injection | case ].
intros H ; apply trans_equal with (2 ); auto.
intros p H .
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ).
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ).
apply (H ); auto.
injection ; intros ; rewrite ; auto.
injection ; intros ; rewrite ; auto.
cut (is_prefix (false ) (false ));
 [ intros ; inversion ; auto | idtac ].
injection ; injection ; intros ; rewrite ;
 rewrite ; auto.
intros p H .
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ).
case (in_map_inv _ _ _ _ _ ).
intros (, ) (, ).
apply (H ); auto.
injection ; intros ; rewrite ; auto.
injection ; intros ; rewrite ; auto.
cut (is_prefix (true ) (true ));
 [ intros ; inversion ; auto | idtac ].
injection ; injection ; intros ; rewrite ;
 rewrite ; auto.
intros .
case (in_app_or _ _ _ ); case (in_app_or _ _ _ ); clear ;
 intros .
generalize ; inversion .
intros ; case (in_map_inv _ _ _ _ _ ).
intros x; case x; intros (, ); discriminate.
intros ; apply with ( ) ( ); auto.
case (in_map_inv _ _ _ _ _ ).
intros x; case x.
intros a l (, ); injection .
intros ; rewrite ; rewrite ; auto.
case (in_map_inv _ _ _ _ _ ).
intros x; case x.
intros a l (, ); injection .
intros ; rewrite ; rewrite ; auto.
generalize .
case (in_map_inv _ _ _ _ _ ).
intros x; case x; intros (, ).
case (in_map_inv _ _ _ _ _ ).
intros ; case ; intros (, ).
inversion ; inversion ; intros ; inversion .
generalize .
case (in_map_inv _ _ _ _ _ ).
intros x; case x; intros (, ).
case (in_map_inv _ _ _ _ _ ).
intros ; case ; intros (, ).
inversion ; inversion ; intros ; inversion .
generalize ; inversion .
intros ; case (in_map_inv _ _ _ _ _ ).
intros x; case x; intros (, ); discriminate.
intros ; apply with ( ) ( ); auto.
case (in_map_inv _ _ _ _ _ ).
intros x; case x.
intros a l (, ); injection .
intros ; rewrite ; rewrite ; auto.
case (in_map_inv _ _ _ _ _ ).
intros x; case x.
intros a l (, ); injection .
intros ; rewrite ; rewrite ; auto.
Qed.


(* The computed code has unique keys *)
Theorem pb_unique_key :
  t, distinct_pbleaves t unique_key (compute_pbcode t).
Proof using.
intros t; elim t; simpl in |- *; auto.
intros p H .
apply unique_key_map; auto.
apply H; apply distinct_pbleaves_pl; auto.
intros (, ) (, ); simpl in |- *; auto.
intros p H .
apply unique_key_map; auto.
apply H; apply distinct_pbleaves_pr; auto.
intros (, ) (, ); simpl in |- *; auto.
intros p H .
apply unique_key_app; auto.
apply unique_key_map; auto.
apply H; apply distinct_pbleaves_l with (1 ); auto.
intros (, ) (, ); simpl in |- *; auto.
apply unique_key_map; auto.
apply ; apply distinct_pbleaves_r with (1 ); auto.
intros (, ) (, ); simpl in |- *; auto.
intros a c .
case in_map_inv with (1 ); auto; case in_map_inv with (1 ); auto.
intros (, ) (, ) (, ) (, ).
apply ( (pbleaf a) p ); auto.
injection ; intros ; rewrite .
apply in_pbcompute_inpb with (1 ).
injection ; intros ; rewrite .
apply in_pbcompute_inpb with (1 ).
Qed.


(* The computed code is prefix *)
Theorem pb_unique_prefix :
  t : pbtree, distinct_pbleaves t unique_prefix (compute_pbcode t).
Proof using.
intros t ; split; try exact (pb_unique_prefix1 t); apply pb_unique_key; auto.
Qed.


(* 
  Predicate that checks if a position (a list of bool) can
  be safely added (adding an element is done without any removing)
*)

Inductive pbfree : list bool pbtree Prop
  | pbfree_left1 : b l, pbfree (true l) (pbleft b)
  | pbfree_left2 : b l, pbfree l b pbfree (false l) (pbleft b)
  | pbfree_right1 : b l, pbfree (false l) (pbright b)
  | pbfree_right2 : b l, pbfree l b pbfree (true l) (pbright b)
  | pbfree_node1 :
       b c l, pbfree l b pbfree (false l) (pbnode b c)
  | pbfree_node2 :
       b c l, pbfree l b pbfree (true l) (pbnode c b).
Hint Constructors pbfree : core.

(* Add an element in a tree at a given position (list of bool) *)
Fixpoint pbadd (a : A) (t : pbtree) (l : list bool) {struct l} : pbtree
  match l with
  | nil pbleaf a
  | false
      match t with
      | pbnode pbnode (pbadd a )
      | pbleft pbleft (pbadd a )
      | pbright pbnode (pbadd a (pbleaf empty) )
      | _ pbleft (pbadd a (pbleaf empty) )
      end
  | true
      match t with
      | pbnode pbnode (pbadd a )
      | pbright pbright (pbadd a )
      | pbleft pbnode (pbadd a (pbleaf empty) )
      | _ pbright (pbadd a (pbleaf empty) )
      end
  end.

(* Adding to  a leaf replace it *)
Theorem pbadd_prop1 :
  , compute_pbcode (pbadd (pbleaf ) ) = (, ) nil.
Proof using.
intros ; generalize ; elim ; simpl in |- *; auto;
 clear .
intros a; case a; simpl in |- *; auto.
intros l H ; rewrite H; simpl in |- *; auto.
intros l H ; rewrite H; simpl in |- *; auto.
Qed.


(* Adding at a free position add to the code *)
Theorem pbadd_prop2 :
  ,
 pbfree
 permutation (compute_pbcode (pbadd ))
   ((, ) compute_pbcode ).
Proof using.
intros H; generalize ; elim H; clear H ; simpl in |- *;
 auto.
intros b l ; rewrite pbadd_prop1; simpl in |- *; auto.
apply
 permutation_trans
  with
    (((, true l) nil)
     map (fun v match v with
                   | (, ) (, false )
                   end) (compute_pbcode b)); auto.
simpl in |- *; auto.
intros b l H .
apply
 permutation_trans
  with
    (map (fun v match v with
                   | (, ) (, false )
                   end) ((, l) compute_pbcode b));
 auto.
intros b l ; rewrite pbadd_prop1; simpl in |- *; auto.
intros b l H .
apply
 permutation_trans
  with
    (map (fun v match v with
                   | (, ) (, true )
                   end) ((, l) compute_pbcode b));
 auto.
intros b c l H .
apply
 permutation_trans
  with
    (map (fun v match v with
                   | (, ) (, false )
                   end) ((, l) compute_pbcode b)
     map (fun v match v with
                   | (, ) (, true )
                   end) (compute_pbcode c)); auto.
intros b c l H .
apply
 permutation_trans
  with
    (map (fun v match v with
                   | (, ) (, false )
                   end) (compute_pbcode c)
     map (fun v match v with
                   | (, ) (, true )
                   end) ((, l) compute_pbcode b));
 auto.
apply
 permutation_trans
  with
    (map (fun v match v with
                   | (, ) (, true )
                   end) ((, l) compute_pbcode b)
     map (fun v match v with
                   | (, ) (, false )
                   end) (compute_pbcode c)); auto;
 simpl in |- *; auto.
Qed.


(* The free positions have not changed *)
Theorem pbfree_pbadd_prop1 :
  l ,
  is_prefix l
  is_prefix l pbfree l (pbadd (pbleaf empty) ).
Proof using.
intros l ; generalize l; elim ; simpl in |- *; auto; clear l .
intros l H ; elim ; auto.
intros a; case a.
intros l H ; case .
intros ; elim ; auto.
intros b; case b; simpl in |- *; auto.
intros ; apply pbfree_right2.
apply H; auto.
intros l H ; case ; simpl in |- *; auto.
intros ; elim ; auto.
intros b; case b; simpl in |- *; auto.
intros ; apply pbfree_left2.
apply H; auto.
Qed.


(* The free positions now include the ones of the added tree *)
Theorem pbfree_pbadd_prop2 :
  a ,
 pbfree
  is_prefix is_prefix pbfree (pbadd a ).
Proof using.
intros a ; generalize a ; elim ; simpl in |- *; auto.
intros H ; case ; auto.
intros ; case .
intros l H ; case .
intros ; inversion .
intros b; case b; simpl in |- *; auto.
intros ; case ; simpl in |- *; auto.
intros ; apply pbfree_right2.
apply pbfree_pbadd_prop1; auto.
intros p ; apply pbfree_node2.
apply pbfree_pbadd_prop1; auto.
intros ; apply pbfree_right2.
apply H; auto.
inversion ; auto.
intros p ; apply pbfree_node2.
apply H; auto.
inversion ; auto.
intros ; case ; simpl in |- *; auto.
intros p ; apply pbfree_node1.
inversion ; auto.
intros p ; apply pbfree_node1.
inversion ; auto.
intros l H ; case .
intros ; inversion .
intros b; case b; simpl in |- *; auto.
intros ; case ; simpl in |- *; auto.
intros p ; apply pbfree_node2.
inversion ; auto.
intros p ; apply pbfree_node2.
inversion ; auto.
intros ; case ; simpl in |- *; auto.
intros ; apply pbfree_left2.
apply pbfree_pbadd_prop1; auto.
intros ; apply pbfree_left2.
apply H; auto.
inversion ; auto.
intros p ; apply pbfree_node1.
apply pbfree_pbadd_prop1; auto.
intros p ; apply pbfree_node1.
apply H; auto.
inversion ; auto.
Qed.


(* The free positions have not changed *)
Theorem distinct_pbleaves_pbadd_prop1 :
  a , distinct_pbleaves (pbadd (pbleaf a) ).
Proof using.
intros a ; generalize a ; elim ; simpl in |- *; auto; clear a .
intros ; case ; auto.
Qed.


(* Adding in leaf does not create nodes  *)
Theorem in_pbleaf_node :
  l, inpb (pbnode ) (pbadd (pbleaf ) l).
Proof using.
intros l; generalize ; elim l; simpl in |- *; auto;
 clear l.
intros ; red in |- *; intros H; inversion H.
intros a; case a.
intros l H ; red in |- *; intros ; case (H empty).
inversion ; auto.
intros l H ; red in |- *; intros ; case (H empty).
inversion ; auto.
Qed.


(* Adding in leaf just replace the leaf *)
Theorem inpbleaf_eq :
  l, inpb (pbleaf ) (pbadd (pbleaf ) l) = .
Proof using.
intros l; generalize ; elim l; simpl in |- *; auto;
 clear l.
intros H; inversion H; auto.
intros a; case a.
intros l H ; apply (H empty).
inversion ; auto.
intros l H ; apply (H empty).
inversion ; auto.
Qed.


(* Adding a leaf we just effectivement add a leaf *)
Theorem inpbleaf_pbadd_inv :
  l,
 inpb (pbleaf ) (pbadd l) = inpb (pbleaf ) .
Proof using.
intros l; generalize ; elim l; simpl in |- *; auto;
 clear l.
intros ; inversion ; auto.
intros a; case a.
intros l H ; case ; auto.
intros ; left; apply (inpbleaf_eq empty l); auto.
inversion ; auto.
intros p ; inversion ; auto.
left; apply (inpbleaf_eq empty l); auto.
intros p ; case (H p); auto.
inversion ; auto.
intros p ; inversion ; auto.
case (H ); auto.
intros l H ; case ; auto.
intros ; left; apply (inpbleaf_eq empty l); auto.
inversion ; auto.
intros p ; case (H p); auto.
inversion ; auto.
intros p ; inversion .
left; apply (inpbleaf_eq empty l); auto.
case ; auto.
intros p ; inversion .
case (H p); auto.
case ; auto.
Qed.


(* Adding creates a new leaf *)
Theorem inpb_pbadd : , inpb (pbleaf ) (pbadd ).
Proof using.
intros ; elim ; simpl in |- *; auto.
intros b; case b; simpl in |- *; auto.
intros l H ; (case ; simpl in |- *; auto).
intros l H ; (case ; simpl in |- *; auto).
Qed.

Hint Resolve inpb_pbadd : core.

(* 
  Subtrees in an added tree either contains the added leaf or
  was a subtree of the initial tree
*)

Theorem inpb_pbadd_ex :
  t,
 inpb t (pbadd ) inpb (pbleaf ) t inpb t .
Proof using.
intros ; elim ; simpl in |- *; auto.
intros t H; inversion H; auto.
intros a l H t; case a; case ; simpl in |- *; auto.
intros ; inversion ; auto.
generalize H; case l; simpl in |- *; auto.
intros p ; inversion ; auto.
left; generalize ; elim l; simpl in |- *; auto.
intros HH; inversion HH; auto.
intros b; case b; simpl in |- *; auto.
intros ; inversion ; auto.
intros ; inversion ; auto.
intros p ; inversion ; auto.
case (H p t); auto.
intros p ; inversion ; auto.
case (H t); auto.
intros ; inversion ; auto.
left; generalize ; elim l; simpl in |- *; auto.
intros HH; inversion HH; auto.
intros b; case b; simpl in |- *; auto.
intros ; inversion ; auto.
intros ; inversion ; auto.
intros p ; inversion ; auto.
case (H p t); auto.
intros p ; inversion ; auto.
left; generalize ; elim l; simpl in |- *; auto.
intros HH; inversion HH; auto.
intros b; case b; simpl in |- *; auto.
intros ; inversion ; auto.
intros ; inversion ; auto.
intros p ; inversion ; auto.
case (H p t); auto.
Qed.


(* Compute all the leaves *)
Fixpoint all_pbleaves (t : pbtree) : list A
  match t with
  | pbleaf a a nil
  | pbleft all_pbleaves
  | pbright all_pbleaves
  | pbnode all_pbleaves all_pbleaves
  end.

(* a leaf is in the list of all leaves *)
Theorem all_pbleaves_in :
  t a, inpb (pbleaf a) t In a (all_pbleaves t).
Proof using.
intros t; elim t; simpl in |- *; auto.
intros a H; inversion H; auto.
intros p H a ; inversion ; auto.
intros p H a ; inversion ; auto.
intros b H a ; apply in_or_app; inversion ; auto.
Qed.


(* An element of the list of all leaves is a leaf of the tree *)
Theorem all_pbleaves_inpb :
  t a, In a (all_pbleaves t) inpb (pbleaf a) t.
Proof using.
intros t; elim t; simpl in |- *; auto.
intros a [H| H]; [ rewrite H | case H ]; auto.
intros b H a ; case in_app_or with (1 ); auto.
Qed.


(* If the list of all leaves is unique, the tree has distinct leaves *)
Theorem all_pbleaves_unique :
  t, ulist (all_pbleaves t) distinct_pbleaves t.
Proof using.
intros t; elim t; simpl in |- *; auto.
intros b H ; red in |- *.
intros ; inversion .
intros ; case (inpb_ex ); intros a HH.
apply ulist_app_inv with (a a) (1 ); auto; apply all_pbleaves_in;
 apply inpb_trans with (1 HH); auto.
apply H; auto; try apply ulist_app_inv_l with (1 ).
apply ; auto; try apply ulist_app_inv_r with (1 ).
Qed.


(* If the tree has distinct leaves, the list of all leaves is unique *)
Theorem all_pbleaves_ulist :
  t, distinct_pbleaves t ulist (all_pbleaves t).
Proof using.
intros t; elim t; simpl in |- *; auto.
intros p H ; apply H; apply distinct_pbleaves_pl; auto.
intros p H ; apply H; apply distinct_pbleaves_pr; auto.
intros b H ; apply ulist_app; auto.
apply H; apply distinct_pbleaves_l with (1 ).
apply ; apply distinct_pbleaves_r with (1 ).
intros a ; case ( (pbleaf a) b ); auto.
apply all_pbleaves_inpb with (1 ).
apply all_pbleaves_inpb with (1 ).
Qed.


(* Adding a leaf change the list of all leaves *)
Theorem all_pbleaves_pbadd :
  l,
 In (all_pbleaves (pbadd l )) = In (all_pbleaves l).
Proof using.
intros ; elim ; simpl in |- *; auto.
intros l [H| H]; auto; case H.
intros a; case a.
intros l H ; case ; simpl in |- *; auto.
intros ; elim l; simpl in |- *; auto.
intuition.
intros ; case ; simpl in |- *; auto.
intros p ; case in_app_or with (1 ); auto.
elim l; simpl in |- *; auto.
intuition.
intros ; case ; simpl in |- *; auto.
intros p ; case in_app_or with (1 ); auto with datatypes.
intros ; case H with (1 ); intuition.
intros l H ; case ; simpl in |- *; auto.
intros ; elim l; simpl in |- *; auto.
intuition.
intros ; case ; simpl in |- *; auto.
intros p ; case in_app_or with (1 ); auto.
elim l; simpl in |- *; auto.
intuition.
intros ; case ; simpl in |- *; auto.
intros p ; case in_app_or with (1 ); auto with datatypes.
intros ; case H with (1 ); intuition.
Qed.


(* Adding in a leaf just creates a singleton list *)
Theorem all_pbleaves_pbleaf :
  l , all_pbleaves (pbadd (pbleaf ) l) = nil.
Proof using.
intros l; elim l; simpl in |- *; auto.
intros b; case b; simpl in |- *; auto.
Qed.


(* Adding a new leaf preserves the uniqueness of the list of all leaves *)
Theorem ulist_pbadd_prop2 :
  t,
  inpb (pbleaf ) t
 ulist (all_pbleaves t) ulist (all_pbleaves (pbadd t )).
Proof using.
intros ; elim ; simpl in |- *; auto.
intros b; case b; simpl in |- *; auto.
intros l H t; case t; simpl in |- *; auto.
intros a ; rewrite all_pbleaves_pbleaf; simpl in |- *; auto.
rewrite all_pbleaves_pbleaf; intros p .
apply ulist_app; simpl in |- *; auto.
intros a [| ]; auto; (case ; rewrite ); auto.
apply all_pbleaves_inpb; auto.
intros p ; apply ulist_app; auto.
apply ulist_app_inv_l with (1 ); auto.
apply H.
Contradict ; auto.
apply ulist_app_inv_r with (1 ); auto.
intros a ; case all_pbleaves_pbadd with (1 ).
intros ; Contradict ; rewrite ; apply all_pbleaves_inpb;
 simpl in |- *; auto with datatypes.
intros ; apply ulist_app_inv with (1 ) (a a); auto.
intros l H t; case t; simpl in |- *; auto.
intros a ; rewrite all_pbleaves_pbleaf; simpl in |- *; auto.
rewrite all_pbleaves_pbleaf; intros p .
apply ulist_app; simpl in |- *; auto.
intros a [| ] ; auto; (case ; rewrite ); auto.
apply all_pbleaves_inpb; auto.
intros p ; apply ulist_app; auto.
apply H.
Contradict ; auto.
apply ulist_app_inv_l with (1 ); auto.
apply ulist_app_inv_r with (1 ); auto.
intros a ; case all_pbleaves_pbadd with (1 ).
intros ; Contradict ; rewrite ; apply all_pbleaves_inpb;
 simpl in |- *; auto with datatypes.
intros ; apply ulist_app_inv with (1 ) (a a); auto.
Qed.


(*
  Adding a new leaf to a tree with distinct leaves
  creates a tree with distinct leaves 
*)

Theorem distinct_pbleaves_pbadd_prop2 :
  l,
  inpb (pbleaf ) l
 distinct_pbleaves l distinct_pbleaves (pbadd l ).
Proof using.
intros l H ; apply all_pbleaves_unique.
apply ulist_pbadd_prop2; auto.
apply all_pbleaves_ulist; auto.
Qed.


(* Adding always on the left creates a left tree *)
Theorem fold_pbadd_prop_left :
  l a,
 l nil
 fold_right (fun a (c : pbtree) pbadd (fst a) c (snd a))
   (pbleaf a)
   (map (fun v match v with
                  | (, ) (, false )
                  end) l) =
 pbleft
   (fold_right (fun a (c : pbtree) pbadd (fst a) c (snd a)) (pbleaf a) l).
Proof using.
intros l; elim l.
intros a H; elim H; simpl in |- *; auto.
simpl in |- *; intros (, ) ; case .
case ; simpl in |- *; auto.
intros p H a .
rewrite H; auto.
red in |- *; intros ; discriminate.
Qed.


(* Adding always on the right  creates a right tree *)
Theorem fold_pbadd_prop_right :
  l a,
 l nil
 fold_right (fun a (c : pbtree) pbadd (fst a) c (snd a))
   (pbleaf a)
   (map (fun v match v with
                  | (, ) (, true )
                  end) l) =
 pbright
   (fold_right (fun a (c : pbtree) pbadd (fst a) c (snd a)) (pbleaf a) l).
Proof using.
intros l; elim l.
intros a H; elim H; simpl in |- *; auto.
simpl in |- *; intros (, ) ; case .
case ; simpl in |- *; auto.
intros p H a .
rewrite H; auto.
red in |- *; intros ; discriminate.
Qed.


(* Adding always on the right on a left tree  creates a node tree *)
Theorem fold_pbadd_prop_node :
  l a,
 l nil
 fold_right (fun a (c : pbtree) pbadd (fst a) c (snd a))
   (pbright a)
   (map (fun v match v with
                  | (, ) (, false )
                  end) l) =
 pbnode
   (fold_right (fun a (c : pbtree) pbadd (fst a) c (snd a))
      (pbleaf empty) l) a.
Proof using.
intros l; elim l.
intros a H; elim H; simpl in |- *; auto.
simpl in |- *; intros (, ) ; case .
case ; simpl in |- *; auto.
intros p H a .
rewrite H; auto.
red in |- *; intros ; discriminate.
Qed.


(* Turn a code into a tree *)
Definition pbbuild (l : code A) : pbtree
  fold_right (fun a c pbadd (fst a) c (snd a)) (pbleaf empty) l.

(*
  All the path that are not prefix in the code are free in
  the corresponding tree
*)

Theorem pbfree_pbbuild_prop1 :
  a ,
  nil unique_prefix ((a, ) ) pbfree (pbbuild ).
Proof using.
intros a ; generalize a ; elim ; clear a ; simpl in |- *; auto.
intros a H; elim H; auto.
intros (, ) l; case l.
unfold pbbuild in |- *; simpl in |- *; intros H a ;
 apply pbfree_pbadd_prop1.
red in |- *; intros ; absurd (a = ).
red in |- *; intros ;
 case
  unique_key_in
   with (a a) ( ) ( ) (1 unique_prefix2 _ _ );
 simpl in |- *; auto.
rewrite ; auto.
apply unique_prefix1 with (1 ) ( ) ( ); simpl in |- *;
 auto.
red in |- *; intros ; absurd (a = ).
red in |- *; intros ;
 case
  unique_key_in
   with (a a) ( ) ( ) (1 unique_prefix2 _ _ );
 simpl in |- *; auto.
rewrite ; auto.
apply sym_equal; apply unique_prefix1 with (1 ) ( ) ( );
 simpl in |- *; auto.
intros p H a .
unfold pbbuild in |- *; simpl in |- *.
apply pbfree_pbadd_prop2; auto.
apply H with (a a).
red in |- *; intros; discriminate.
apply unique_prefix_inv with (a ) (l ).
apply unique_prefix_permutation with (2 ); auto.
red in |- *; intros ; absurd (a = ).
red in |- *; intros ;
 case
  unique_key_in
   with (a a) ( ) ( ) (1 unique_prefix2 _ _ );
 simpl in |- *; auto.
rewrite ; auto.
apply sym_equal; apply unique_prefix1 with (1 ) ( ) ( );
 simpl in |- *; auto.
red in |- *; intros ; absurd (a = ).
red in |- *; intros ;
 case
  unique_key_in
   with (a a) ( ) ( ) (1 unique_prefix2 _ _ );
 simpl in |- *; auto.
rewrite ; auto.
apply unique_prefix1 with (1 ) ( ) ( ); simpl in |- *;
 auto.
Qed.


(* The keys of the code are a permutation of the leaves of the tree *)
Theorem all_pbleaves_compute_pb :
  t, permutation (map (fst (B_)) (compute_pbcode t)) (all_pbleaves t).
Proof using.
cut
 ( b l,
  map (fst (B_))
    (map (fun v : A list bool let (, ) v in (, b )) l) =
  map (fst (B_)) l); [ intros HH | idtac ].
intros t; elim t; simpl in |- *; auto.
intros p H; rewrite HH; auto.
intros p H; rewrite HH; auto.
intros p H ; rewrite map_app; apply permutation_app_comp; auto.
repeat rewrite HH; auto.
repeat rewrite HH; auto.
intros b l; elim l; simpl in |- *; auto.
intros a ; apply f_equal2 with (f cons (AA)); auto.
case a; simpl in |- *; auto.
Qed.


(*
  Taking a code, turning it in a tree, then computing a code
  gives a permutation of the initial code
*)

Theorem pbbuild_compute_perm :
  c,
 c nil unique_prefix c permutation (compute_pbcode (pbbuild c)) c.
Proof using.
intros c; elim c; simpl in |- *; auto.
intros H; case H; auto.
intros (, ) l.
case l.
unfold pbbuild in |- *; simpl in |- *; auto.
intros H ; rewrite pbadd_prop1; auto.
intros (, ) ; simpl in |- *.
intros H ;
 apply
  permutation_trans
   with ((, ) compute_pbcode (pbadd (pbbuild ) )).
unfold pbbuild in |- *; simpl in |- *; apply pbadd_prop2.
cut ( is_prefix ); [ intros | idtac ].
cut ( is_prefix ); [ intros | idtac ].
generalize ; case ; auto.
intros ; apply pbfree_pbadd_prop1; auto.
intros p .
apply pbfree_pbadd_prop2; auto.
change (pbfree (pbbuild (p ))) in |- *.
apply pbfree_pbbuild_prop1 with (a ); auto.
red in |- *; intros; discriminate.
apply unique_prefix_inv with (a ) (l ).
apply unique_prefix_permutation with (2 ); auto.
red in |- *; intros ; absurd ( = ).
red in |- *; intros ;
 case
  unique_key_in
   with (a ) ( ) ( ) (1 unique_prefix2 _ _ );
 simpl in |- *; auto.
rewrite ; auto.
apply sym_equal; apply unique_prefix1 with (1 ) ( ) ( );
 simpl in |- *; auto.
red in |- *; intros ; absurd ( = ).
red in |- *; intros ;
 case
  unique_key_in
   with (a ) ( ) ( ) (1 unique_prefix2 _ _ );
 simpl in |- *; auto.
rewrite ; auto.
apply unique_prefix1 with (1 ) ( ) ( ); simpl in |- *;
 auto.
apply permutation_skip.
apply H; auto.
red in |- *; intros Hj; discriminate.
apply unique_prefix_inv with (1 ); auto.
Qed.


(* 
  Building tree from a code, the list of leaves is a permutation of
  the keys of the code
*)

Theorem all_pbleaves_pbbuild :
  c,
 c nil
 unique_prefix c
 permutation (map (fst (B_)) c) (all_pbleaves (pbbuild c)).
Proof using.
intros c H ;
 apply permutation_trans with (map (fst (B_)) (compute_pbcode (pbbuild c))).
apply permutation_map.
apply permutation_sym; apply pbbuild_compute_perm; auto.
apply all_pbleaves_compute_pb; auto.
Qed.


(* Leaves in a built tree are elements of the codes *)
Theorem inpb_pbbuild_inv :
  a c,
 c nil inpb (pbleaf a) (pbbuild c) l : _, In (a, l) c.
Proof using.
intros a c; generalize a; elim c; simpl in |- *; auto.
intros H; elim H; auto.
intros (, ).
intros l; case l.
simpl in |- *; auto.
unfold pbbuild in |- *; simpl in |- *; intros H ; exists ; left;
 apply f_equal2 with (f pair (AA) (Blist bool));
 auto.
apply sym_equal; apply inpbleaf_eq with (1 ).
unfold pbbuild in |- *; simpl in |- *; intros p H .
case inpbleaf_pbadd_inv with (1 ); auto; intros .
exists ; left; apply f_equal2 with (f pair (AA) (Blist bool)); auto.
case (H ); auto.
red in |- *; intros ; discriminate.
intros x ; exists x; simpl in |- *; auto.
Qed.


(* Built tree from prefix code has distinct leaves *)
Theorem pbbuild_distinct_pbleaves :
  c, unique_prefix c distinct_pbleaves (pbbuild c).
Proof using.
intros c; elim c; unfold pbbuild in |- *; simpl in |- *; auto.
intros (, ) l; case l; auto.
simpl in |- *; intros H ; apply distinct_pbleaves_pbadd_prop1; auto.
intros (, ) ; apply distinct_pbleaves_pbadd_prop2; auto.
change ( inpb (pbleaf ) (pbbuild ((, ) ))) in |- *.
red in |- *; intros ; case inpb_pbbuild_inv with (2 ).
red in |- *; intros H; discriminate.
intros x H; case unique_key_in with ( x) (1 unique_prefix2 _ _ );
 auto.
apply .
apply unique_prefix_inv with (1 ); auto.
Qed.


(*
  The composition of building and computing on trees
  with distinct leaves is the identity
*)

Theorem pbbuild_compute_peq :
  t, distinct_pbleaves t pbbuild (compute_pbcode t) = t.
Proof using.
intros t; elim t; simpl in |- *; auto.
intros p H ; unfold pbbuild in |- *.
rewrite fold_pbadd_prop_left; auto.
change (pbleft (pbbuild (compute_pbcode p)) = pbleft p) in |- *.
apply f_equal with (f pbleft); auto; apply H.
apply distinct_pbleaves_pl with (1 ).
intros p H ; unfold pbbuild in |- *.
rewrite fold_pbadd_prop_right; auto.
change (pbright (pbbuild (compute_pbcode p)) = pbright p) in |- *.
apply f_equal with (f pbright); auto; apply H.
apply distinct_pbleaves_pr with (1 ).
intros p H .
unfold pbbuild in |- *.
rewrite fold_right_app.
rewrite fold_pbadd_prop_right; auto.
rewrite fold_pbadd_prop_node; auto.
change
  (pbnode (pbbuild (compute_pbcode p)) (pbbuild (compute_pbcode )) =
   pbnode p ) in |- *.
apply f_equal2 with (f pbnode).
apply H; apply distinct_pbleaves_l with (1 ).
apply ; apply distinct_pbleaves_r with (1 ).
Qed.


(* 
  Adding a true in all the element in the code adds  a right 
  on top the built tree
*)

Theorem pbbuild_true_pbright :
  c,
 c nil
 pbbuild (map (fun x (fst x, true snd x)) c) = pbright (pbbuild c).
Proof using.
intros c; elim c; simpl in |- *; auto.
intros H; case H; auto.
intros a l; case a; case l.
intros H ; simpl in |- *; auto.
intros p H ; rewrite H; auto.
intros; discriminate.
Qed.


(* 
  Building can be decomposed in the codes starting with true
  and the one starting by false
*)

Theorem pbbuild_pbnode :
  ,
  nil
  nil
 pbbuild
   (map (fun x (fst x, false snd x))
    map (fun x (fst x, true snd x)) ) =
 pbnode (pbbuild ) (pbbuild ).
Proof using.
intros ; unfold pbbuild in |- *.
rewrite fold_right_app.
fold pbbuild in |- *.
generalize pbbuild_true_pbright; unfold pbbuild in |- *; intros tmp;
 rewrite tmp; clear tmp; auto.
generalize ; elim ; simpl in |- *; auto.
intros H; case H; auto.
intros a l; case a; case l; simpl in |- *; auto.
intros p H ; rewrite H; auto.
intros; discriminate.
Qed.


End PBTree.
Arguments pbleaf [A].
Arguments pbleft [A].
Arguments pbright [A].
Arguments pbnode [A].
Arguments inpb [A].
Arguments pbfree [A].
Arguments compute_pbcode [A].
Arguments pbadd [A].
Arguments pbbuild [A].
Arguments all_pbleaves [A].
Arguments distinct_pbleaves [A].
Arguments compute_pbcode [A].
Arguments inpb_dec [A].
Hint Constructors inpb : core.
Hint Resolve distinct_pbleaves_pbleaf : core.
Hint Resolve distinct_pbleaves_pbleft distinct_pbleaves_pbright : core.
Hint Resolve compute_pbcode_not_null : core.
Hint Resolve compute_pbcode_not_null : core.
Hint Constructors pbfree : core.