Module TabTree

Section TabTree.

Variable A:Set.
Variable bot:A.

Inductive tree : Set :=
   leaf : A -> tree
 | node : A -> tree -> tree -> tree.

Fixpoint apply_tree [t:tree;p:positive]: A :=
 Cases p t of
  | xH (leaf a) => a
  | xH (node a tO tI) => a
  | (xO p) (leaf _) => bot
  | (xI p) (leaf _) => bot
  | (xO p) (node a tO tI) => (apply_tree tO p)
  | (xI p) (node a tO tI) => (apply_tree tI p)
 end.

Fixpoint subst_tree [t:tree;p:positive] : A -> tree :=
 [v]
 Cases t p of
   (leaf a) xH => (leaf v)
 | (leaf a) (xO p') => (node a (subst_tree (leaf bot) p' v) (leaf bot))
 | (leaf a) (xI p') => (node a (leaf bot) (subst_tree (leaf bot) p' v))
 | (node a tO tI) xH => (node v tO tI)
 | (node a tO tI) (xO p') => (node a (subst_tree tO p' v) tI)
 | (node a tO tI) (xI p') => (node a tO (subst_tree tI p' v))
 end.

Lemma apply_subst_tree1 : (t:tree;p:positive;v:A)
 (apply_tree (subst_tree t p v) p)=v.
NewInduction t; Intros.
Generalize a; Clear a; NewInduction p; Simpl; Intros.
Rewrite IHp; Reflexivity.
Rewrite IHp; Reflexivity.
Reflexivity.
Case p; Simpl; Auto.
Qed.

Lemma apply_subst_tree2 : (t:tree;p,x:positive;v:A)
 ~x=p -> (apply_tree (subst_tree t p v) x)=(apply_tree t x).
NewInduction t; Intros.
Generalize x a H; Clear H a x; NewInduction p; Simpl; Intros.
Generalize H; Clear H; Case x; Simpl; Intros.
Rewrite IHp.
Case p0; Auto.
Red; Intros H'; Elim H; Rewrite H'; Auto.
Case p0; Auto.
Auto.
Generalize H; Clear H; Case x; Simpl; Intros.
Case p0; Auto.
Rewrite IHp.
Case p0; Auto.
Red; Intros H'; Elim H; Rewrite H'; Auto.
Auto.
Generalize H; Clear H; Case x; Simpl; Intros; Auto.
Elim H; Auto.
Generalize x a H; Clear H a x; NewInduction p; Simpl; Intros.
Generalize IHp H; Clear IHp H; Case x; Simpl; Intros; Auto.
Apply IHt2.
Red; Intros H'; Elim H; Rewrite H'; Auto.
Generalize IHp H; Clear IHp H; Case x; Simpl; Intros; Auto.
Apply IHt1.
Red; Intros H'; Elim H; Rewrite H'; Auto.
Generalize H; Clear H; Case x; Simpl; Intros; Auto.
Elim H; Auto.
Qed.

End TabTree.

Section map_tree.
 
Variable A,B:Set.
Variable f:A->B.
 
Fixpoint map_tree [t:(tree A)] : (tree B) :=
 Cases t of
   (leaf a) => (leaf ? (f a))
 | (node a tO tI) => (node ? (f a) (map_tree tO) (map_tree tI))
 end.

Variable botA:A.
Variable botB:B.

Lemma map_tree_correct : (t:(tree A);p:positive)
 (f botA)=botB ->
 (apply_tree B botB (map_tree t) p)=(f (apply_tree A botA t p)).
NewInduction t; Destruct p; Simpl; Intros; Auto.
Qed.

End map_tree.

Section app_positive.

Fixpoint inv_pos [p1:positive] : positive -> positive :=
 [p2]
 Cases p1 of
  | xH => p2
  | (xO p) => (inv_pos p (xO p2))
  | (xI p) => (inv_pos p (xI p2))
 end.

Lemma inv_pos_inv_pos : (p1,p2:positive)
 (inv_pos (inv_pos p1 p2) xH)=(inv_pos p2 p1).
NewInduction p1; Simpl; Intros; Auto.
Rewrite IHp1; Simpl; Auto.
Rewrite IHp1; Simpl; Auto.
Qed.

End app_positive.

Section mapIt_tree.

Variable A,B:Set.
Variable f:positive->A->B.
 
Fixpoint mapIt_tree_rec [p:positive;t:(tree A)] : (tree B) :=
 Cases t of
   (leaf a) => (leaf ? (f (inv_pos p xH) a))
 | (node a tO tI) => (node ? (f (inv_pos p xH) a)
                             (mapIt_tree_rec (xO p) tO)
                             (mapIt_tree_rec (xI p) tI))
 end.

Variable botA:A.
Variable botB:B.

Lemma mapIt_tree_rec_correct : (t:(tree A);p0,p:positive)
 ((p:positive)(f p botA)=botB) ->
 (apply_tree B botB (mapIt_tree_rec p0 t) p)=(f (inv_pos (inv_pos p p0) xH) (apply_tree A botA t p)).
NewInduction t; Destruct p; Simpl; Intros; Auto.
Qed.

Definition mapIt_tree :=
 [t](mapIt_tree_rec xH t).

Lemma mapIt_tree_correct : (t:(tree A);p:positive)
 ((p:positive)(f p botA)=botB) ->
 (apply_tree B botB (mapIt_tree t) p)=(f p (apply_tree A botA t p)).
Unfold mapIt_tree; Intros.
Generalize (mapIt_tree_rec_correct t xH p H).
Replace (inv_pos (inv_pos p xH) xH) with p.
Auto.
Rewrite inv_pos_inv_pos; Simpl; Auto.
Qed.

End mapIt_tree.

Lemma positive_dec : (p1,p2:positive){p1=p2}+{~p1=p2}.
NewInduction p1; Intros.
Case p2; Intros.
Case (IHp1 p); Intros.
Left; Rewrite e; Auto.
Right; Red; Intros H'; Elim n; Injection H'; Auto.
Right; Red; Intros H'; Discriminate H'.
Right; Red; Intros H'; Discriminate H'.
Case p2; Intros.
Right; Red; Intros H'; Discriminate H'.
Case (IHp1 p); Intros.
Left; Rewrite e; Auto.
Right; Red; Intros H'; Elim n; Injection H'; Auto.
Right; Red; Intros H'; Discriminate H'.
Case p2; Intros.
Right; Red; Intros H'; Discriminate H'.
Right; Red; Intros H'; Discriminate H'.
Left; Auto.
Qed.

Inductive inf_log : positive -> nat -> Prop :=
   inf_log_xH : (n:nat) (inf_log xH n)
 | inf_log_xO : (p:positive;n:nat)
    (inf_log p n) -> (inf_log (xO p) (S n))
 | inf_log_xI : (p:positive;n:nat)
    (inf_log p n) -> (inf_log (xI p) (S n)).

Fixpoint log_positive [p:positive] : nat :=
 Cases p of
   xH => O
 | (xO p') => (S (log_positive p'))
 | (xI p') => (S (log_positive p'))
 end.

Lemma inf_log_trans : (max:nat;p2,p1:positive)
 (inf_log p2 max) -> (compare p1 p2 EGAL)=INFERIEUR ->
 (inf_log p1 max).
NewInduction max.
Intros p2 p1 H.
Inversion_clear H.
Case p1; Simpl; Intros; Try Discriminate H.
Destruct p2.
Intros p p1 H; Inversion_clear H.
Case p1; Simpl; Intros; Constructor; Auto.
Apply IHmax with p; Auto.
Elim (ZLII ? ? H); Intros.
Apply IHmax with p; Auto.
Rewrite H1; Auto.
Intros p p1 H; Inversion_clear H.
Case p1; Simpl; Intros; Constructor; Auto.
Apply IHmax with p; Auto.
Apply ZLSI; Auto.
Apply IHmax with p; Auto.
Destruct p1; Simpl; Intros; Try Discriminate H0.
Qed.

Lemma inf_log_dec : (p:positive;n:nat){(inf_log p n)}+{~(inf_log p n)}.
NewInduction p; Intros.
Case n; Intros.
Right; Intros H; Inversion H.
Case (IHp n0); Intros.
Left; Constructor; Auto.
Right; Intros H; Inversion_clear H; Elim n1; Auto.
Case n; Intros.
Right; Intros H; Inversion H.
Case (IHp n0); Intros.
Left; Constructor; Auto.
Right; Intros H; Inversion_clear H; Elim n1; Auto.
Left; Constructor.
Qed.

Lemma log_inf_log_positive : (p:positive)
 (inf_log p (log_positive p)).
NewInduction p; Simpl; Intros; Constructor; Auto.
Qed.

Lemma max_inf_log_trans : (p2,p1:positive;n:nat)
 (inf_log p1 n) -> ~(inf_log p2 n) -> (inf_log p1 (log_positive p2)).
NewInduction p2; Simpl.
Destruct p1.
Intros p n H; Inversion_clear H; Intros.
Constructor; Apply IHp2 with n0; Auto.
Red; Intros H'; Elim H; Constructor; Auto.
Intros p n H; Inversion_clear H; Intros.
Constructor; Apply IHp2 with n0; Auto.
Red; Intros H'; Elim H; Constructor; Auto.
Intros; Constructor.
Destruct p1.
Intros p n H; Inversion_clear H; Intros.
Constructor; Apply IHp2 with n0; Auto.
Red; Intros H'; Elim H; Constructor; Auto.
Intros p n H; Inversion_clear H; Intros.
Constructor; Apply IHp2 with n0; Auto.
Red; Intros H'; Elim H; Constructor; Auto.
Intros; Constructor.
Intros.
Elim H0; Constructor.
Qed.

Require PolyList.

Section max_log_list.

Variable A : Set.
Variable f : A->positive.

Fixpoint max_log_list [l:(list A)] : nat :=
 Cases l of
   nil => O
 | (cons i q) => let max=(max_log_list q) in
        Cases (inf_log_dec (f i) max) of
             (left _) => max
           | (right _) => (log_positive (f i))
        end
 end.

Lemma in_inf_log : (l:(list A);x:A)
 (In x l) ->
 (inf_log (f x) (max_log_list l)).
NewInduction l; Simpl.
Intuition.
Intros.
Decompose [or] H.
Subst.
Case inf_log_dec; Intros.
Auto.
Apply log_inf_log_positive.
Case inf_log_dec; Intros; Auto.
Apply max_inf_log_trans with (max_log_list l); Auto.
Qed.

End max_log_list.

Require Omega.

Section build_TabTree_list.

Variable A:Set.
Variable bot:A.

Fixpoint built_TabTree_rec [t:(tree A);next:positive;l:(list A)] : (tree A) :=
 Cases l of
    nil => t
 | (cons x q) => (built_TabTree_rec (subst_tree A bot t next x) (add_un next) q)
 end.

Lemma built_TabTree_rec_same : (l:(list A);t:(tree A);p,next:positive)
 (compare p next EGAL)=INFERIEUR ->
 (apply_tree A bot (built_TabTree_rec t next l) p)=(apply_tree A bot t p).
NewInduction l; Simpl; Intros.
Auto.
Rewrite IHl.
Apply apply_subst_tree2.
Red; Intros; Generalize (compare_convert_INFERIEUR ? ? H).
Subst; Intros.
Omega.
Generalize (compare_convert_INFERIEUR ? ? H); Intros.
Apply convert_compare_INFERIEUR.
Unfold convert.
Rewrite convert_add_un; Simpl.
Unfold convert in H0.
Omega.
Qed.

Lemma built_TabTree_rec_correct : (l:(list A);n:nat;t:(tree A);next:positive)
 ((p:positive)(compare next p EGAL)=INFERIEUR\/next=p->(apply_tree A bot t p)=bot) ->
 (nth n l bot)=
   (apply_tree A bot (built_TabTree_rec t next l) (sub_un (add (anti_convert n) next))).
NewInduction l; Simpl.
Destruct n; Intros; Simpl.
Rewrite H; Auto.
Right.
Rewrite <- ZL12bis.
Rewrite sub_add_one; Auto.
Rewrite H; Auto.
Left.
Rewrite add_sym.
Rewrite ZL14.
Rewrite sub_add_one; Auto.
Apply convert_compare_INFERIEUR.
Rewrite convert_add; Simpl.
Rewrite bij1.
Omega.
Destruct n; Simpl; Intros.
Rewrite built_TabTree_rec_same.
Rewrite <- ZL12bis.
Rewrite sub_add_one.
Rewrite apply_subst_tree1; Auto.
Rewrite <- ZL12bis.
Rewrite sub_add_one.
Apply convert_compare_INFERIEUR.
Unfold convert.
Rewrite convert_add_un; Simpl.
Omega.
Rewrite add_sym.
Rewrite ZL14.
Rewrite add_sym.
Rewrite <- ZL14.
Apply IHl.
Intros.
Cut (compare next p EGAL)=INFERIEUR; Intros.
Rewrite apply_subst_tree2; Auto.
Red; Intros; Generalize (compare_convert_INFERIEUR ? ? H1).
Subst; Intros.
Omega.
Elim H0; Clear H0; Intros.
Apply convert_compare_INFERIEUR.
Generalize (compare_convert_INFERIEUR ? ? H0).
Unfold convert.
Rewrite convert_add_un; Simpl.
Omega.
Rewrite <- H0.
Apply convert_compare_INFERIEUR.
Unfold convert.
Rewrite convert_add_un; Simpl.
Omega.
Qed.

Definition build_TabTree :=
 [l:(list A)](built_TabTree_rec (leaf ? bot) xH l).

Lemma build_TabTree_correct : (l:(list A);n:nat)
 (nth n l bot)=(apply_tree A bot (build_TabTree l) (anti_convert n)).
Unfold build_TabTree.
Intros.
Generalize (built_TabTree_rec_correct l n (leaf A bot) xH).
Rewrite add_sym.
Rewrite <- ZL12bis.
Rewrite sub_add_one; Auto.
Intros H; Apply H; Intros.
Case p; Simpl ; Auto.
Qed.

Lemma in_list_nth : (l:(list A);x:A)
 (In x l) -> (EX n:nat | x=(nth n l bot)).
NewInduction l; Simpl; Intros.
Elim H.
Elim H; Intros.
Subst.
Exists O; Auto.
Elim (IHl x H0); Intros.
Exists (S x0); Auto.
Qed.

Lemma built_TabTree_keep_property : (l:(list A);P:A->Prop)
 (P bot) -> ((x:A)(In x l) -> (P x)) ->
 ((p:positive) (P (apply_tree A bot (build_TabTree l) p))).
Intros.
Rewrite <- (bij3 p).
Elim (ZL4 p); Intros.
Rewrite H1.
Simpl.
Rewrite sub_add_one.
Rewrite <- build_TabTree_correct.
Case (nth_in_or_default x l bot); Intros; Auto.
Rewrite e; Auto.
Qed.

End build_TabTree_list.

Section build_const_TabTree.

Variable A:Set.
Variable bot:A.
Variable const:A.

Fixpoint build_const_TabTree_rec [max:nat] : (tree A) :=
 Cases max of
   O => (leaf ? const)
 | (S p) => (node ? const (build_const_TabTree_rec p)
                             (build_const_TabTree_rec p))
 end.

Lemma apply_build_const_TabTree_is_const : (max:nat;p:positive)
 (inf_log p max) ->
 (apply_tree A bot (build_const_TabTree_rec max) p)=const.
NewInduction max; Simpl; Intros.
Inversion_clear H; Simpl; Auto.
Generalize H; Clear H.
Case p; Intros.
Inversion_clear H; Simpl; Auto.
Inversion_clear H; Simpl; Auto.
Simpl; Auto.
Qed.

Lemma apply_build_const_TabTree_is_bot : (max:nat;p:positive)
 ~(inf_log p max) ->
 (apply_tree A bot (build_const_TabTree_rec max) p)=bot.
NewInduction max; Simpl; Intros.
Generalize H; Clear H.
Case p; Intros; Simpl; Auto.
Elim H; Constructor.
Generalize H; Clear H.
Case p; Intros; Simpl; Auto.
Apply IHmax.
Red; Intros; Elim H; Constructor; Auto.
Apply IHmax.
Red; Intros; Elim H; Constructor; Auto.
Elim H; Constructor.
Qed.

End build_const_TabTree.

Lemma inf_log_trans' : (max2,max1:nat;p:positive)
 (inf_log p max1) -> (le max1 max2) ->
 (inf_log p max2).
NewInduction max2; Intros.
Inversion H0.
Rewrite H1 in H; Auto.
Generalize H; Clear H; Case p; Intros.
Generalize H0; Clear H0; Inversion_clear H; Intros; Constructor.
Apply IHmax2 with n; Auto with zarith.
Generalize H0; Clear H0; Inversion_clear H; Intros; Constructor.
Apply IHmax2 with n; Auto with zarith.
Constructor.
Qed.

Section join_tabtree.

Variable A,B:Set.
Variable bot:A.
Variable f:positive->A->B.
Variable j:B->B->B->B.

Fixpoint join_tabtree_rec [p:positive;t:(tree A)] : B :=
 Cases t of
   (leaf a) => (f (inv_pos p xH) a)
 | (node a tO tI) => (j (f (inv_pos p xH) a)
                           (join_tabtree_rec (xO p) tO)
                           (join_tabtree_rec (xI p) tI))
 end.

Variable P:B->B->Prop.
Hypothesis Hf1:(b,b1,b2:B) (P b (j b b1 b2)).
Hypothesis Hf2:(x,b,b1,b2:B) (P x b1)->(P x (j b b1 b2)).
Hypothesis Hf3:(x,b,b1,b2:B) (P x b2)->(P x (j b b1 b2)).
Hypothesis Hf4:(b:B) (P b b).
Hypothesis Hbot : (b:B;p:positive)(P (f p bot) b).

Lemma join_tabtree_rec_prop : (t:(tree A);p0,p:positive)
 (P (f (inv_pos (inv_pos p p0) xH) (apply_tree A bot t p)) (join_tabtree_rec p0 t)).
NewInduction t; Destruct p; Simpl; Intros; Auto.
Qed.

Variable Q:B->Prop.
Hypothesis Hf1':(b,b1,b2:B) (Q b) -> (Q b1) -> (Q b2) -> (Q (j b b1 b2)).
Hypothesis Hf2': (p:positive;a:A) (Q (f p a)).

Lemma join_tabtree_rec_prop' : (t:(tree A);p:positive)
 (Q (join_tabtree_rec p t)).
NewInduction t; Destruct p; Simpl; Intros; Auto.
Qed.

Definition join_tabtree : (tree A)->B :=
 [t](join_tabtree_rec xH t).

Lemma join_tabtree_prop : (t:(tree A);p:positive)
 (P (f p (apply_tree A bot t p)) (join_tabtree t)).
Intros t p.
Generalize (join_tabtree_rec_prop t xH p).
Replace (inv_pos (inv_pos p xH) xH) with p.
Auto.
Rewrite inv_pos_inv_pos; Simpl; Auto.
Qed.

Lemma join_tabtree_prop' : (t:(tree A))
 (Q (join_tabtree t)).
Intros t.
Generalize (join_tabtree_rec_prop' t xH).
Auto.
Qed.