Require Lattice.
Require TabTree.
Section funcTree.
Variable A:Set.
Variable PA:(Lattice A).
Local tree:=(tree A).
Implicits leaf [1].
Implicits node [1].
Local apply_tree := (apply_tree A (bottom PA)).
Inductive height_inf : tree -> nat -> Prop :=
| inf_leaf : (a:A;p:nat) (height_inf (leaf a) p)
| inf_node : (a:A;tO,tI:tree;p:nat)
(height_inf tO p) ->
(height_inf tI p) ->
(height_inf (node a tO tI) (S p)).
Record funcTree [max:nat]: Set := funcTree_constr {
tr : tree;
tr_bound : (height_inf tr max)
}.
Definition Feq : tree -> tree -> Prop :=
[t1,t2](p:positive)(eq PA (apply_tree t1 p) (apply_tree t2 p)).
Fixpoint join_tree [t1,t2:tree]: tree :=
Cases t1 t2 of
| (leaf a1) (leaf a2) => (leaf (join PA a1 a2))
| (leaf a1) (node a2 tO tI) => (node (join PA a1 a2) tO tI)
| (node a1 tO tI) (leaf a2) => (node (join PA a1 a2) tO tI)
| (node a1 tO1 tI1) (node a2 tO2 tI2) =>
(node (join PA a1 a2) (join_tree tO1 tO2) (join_tree tI1 tI2))
end.
Lemma join_tree_heigth : (t1,t2:tree)(max:nat)
(height_inf t1 max) -> (height_inf t2 max) ->
(height_inf (join_tree t1 t2) max).
NewInduction t1; Simpl; Intros t; Case t; Simpl; Intros.
Constructor.
Inversion_clear H0; Constructor; Auto.
Inversion_clear H; Constructor; Auto.
Generalize H0; Clear H0.
Inversion_clear H; Intros; Constructor; Auto.
Inversion_clear H2.
Apply IHt0; Auto.
Inversion_clear H2.
Apply IHt2; Auto.
Qed.
Definition Fjoin : (max:nat) (funcTree max) -> (funcTree max) -> (funcTree max).
Intros max f1 f2; Refine (funcTree_constr ? (join_tree (tr ? f1) (tr ? f2)) ?).
Apply join_tree_heigth.
Case f1; Auto.
Case f2; Auto.
Defined.
Definition apply := [max:nat;f:(funcTree max);p:positive]
(apply_tree (tr ? f) p).
Local Forder : tree -> tree -> Prop :=
[f1,f2](p:positive)
(order PA (apply_tree f1 p) (apply_tree f2 p)).
Definition Fbottom : (max:nat)(funcTree max).
Refine [max](funcTree_constr ? (leaf (bottom PA)) ?).
Constructor.
Defined.
Lemma apply_bottom : (max:nat;p:positive)
(apply ? (Fbottom max) p)=(bottom PA).
Unfold apply Fbottom; Simpl; Intros.
Case p; Simpl; Intros; Auto.
Qed.
Lemma apply_join_tree : (t1,t2:tree;p:positive)
(eq PA (apply_tree (join_tree t1 t2) p) (join PA (apply_tree t1 p) (apply_tree t2 p))).
NewInduction t1; Intros t; Case t; Simpl; Intros.
Case p; Simpl; Auto.
Case p; Simpl; Auto.
Case p; Simpl; Auto.
Case p; Simpl; Auto.
Qed.
Local Feq_bot_dec :
(t1:tree){(p:positive)(eq PA (apply_tree t1 p) (bottom PA))}+{~(p:positive)(eq PA (apply_tree t1 p) (bottom PA))}.
NewInduction t1; Simpl.
Case (eq_dec PA a (bottom PA)); Intros.
Left; Destruct p; Simpl; Auto.
Right; Red; Intros H; Elim n; Generalize (H xH); Simpl; Auto.
Case (eq_dec PA a (bottom PA)); Intros.
Case IHt0; Intros.
Case IHt2; Intros.
Left; Destruct p; Simpl; Auto.
Right; Red; Intros H; Elim n; Intros p; Generalize (H (xI p)); Simpl; Auto.
Right; Red; Intros H; Elim n; Intros p; Generalize (H (xO p)); Simpl; Auto.
Right; Red; Intros H; Elim n; Generalize (H xH); Simpl; Auto.
Qed.
Local Feq_dec : (t1,t2:tree){(Feq t1 t2)}+{~(Feq t1 t2)}.
NewInduction t1; Intros t; Case t; Intros.
Case (eq_dec PA a a0); Intros.
Left; Unfold Feq; Intros.
Case p; Simpl; Auto.
Unfold Feq; Right; Red; Intros H; Elim n.
Generalize (H xH); Simpl; Auto.
Case (eq_dec PA a a0); Intros.
Case (Feq_bot_dec t0); Intros.
Case (Feq_bot_dec t1); Intros.
Left; Unfold Feq; Intros.
Case p; Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Intros p; Generalize (H (xI p)); Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Intros p; Generalize (H (xO p)); Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Generalize (H xH); Auto.
Case (eq_dec PA a a0); Intros.
Case (Feq_bot_dec t0); Intros.
Case (Feq_bot_dec t2); Intros.
Left; Unfold Feq; Intros.
Case p; Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Intros p; Generalize (H (xI p)); Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Intros p; Generalize (H (xO p)); Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Generalize (H xH); Auto.
Case (eq_dec PA a a0); Intros.
Case (IHt0 t1); Intros.
Case (IHt2 t3); Intros.
Left; Unfold Feq; Intros.
Case p; Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Intros p; Generalize (H (xI p)); Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Intros p; Generalize (H (xO p)); Simpl; Auto.
Right; Unfold Feq; Intros H; Elim n; Generalize (H xH); Auto.
Qed.
Definition topF : (max:nat)(funcTree max).
Refine [max] (funcTree_constr ? (build_const_TabTree_rec ? (top PA) max) ?).
NewInduction max; Simpl; Constructor; Auto.
Defined.
Lemma topF_is_top : (max:nat;t:tree)
(height_inf t max) ->
(Forder t (build_const_TabTree_rec ? (top PA) max)).
Unfold Forder; Intros.
Case (inf_log_dec p max); Intros.
Unfold apply_tree.
Rewrite apply_build_const_TabTree_is_const; Auto.
Unfold apply_tree.
Rewrite apply_build_const_TabTree_is_bot; Auto.
Generalize p t H n; Clear H n.
NewInduction max; Intros.
Inversion_clear H; Simpl.
NewDestruct p0; Simpl; Auto.
Elim n; Constructor.
NewDestruct p0; Simpl.
NewDestruct t0; Simpl; Auto.
Inversion_clear H; Apply IHmax; Auto.
Red; Intros; Elim n; Constructor; Auto.
NewDestruct t0; Simpl; Auto.
Inversion_clear H; Apply IHmax; Auto.
Red; Intros; Elim n; Constructor; Auto.
Elim n; Constructor.
Qed.
Inductive is_bottom : tree -> Prop :=
is_bottom_leaf : (a:A) (eq PA a (bottom PA)) -> (is_bottom (leaf a))
| is_bottom_node : (a:A;t1,t2:tree)
(eq PA a (bottom PA)) -> (is_bottom t1) -> (is_bottom t2) ->
(is_bottom (node a t1 t2)).
Inductive order' : tree -> tree -> Prop :=
order'_leaf_leaf : (a,b:A)
(order PA a b) -> (order' (leaf a) (leaf b))
| order'_leaf_node : (a,b:A;t1,t2:tree)
(order PA a b) -> (order' (leaf a) (node b t1 t2))
| order'_node_leaf : (a,b:A;t1,t2:tree)
(order PA a b) -> (is_bottom t1) -> (is_bottom t2) ->
(order' (node a t1 t2) (leaf b))
| order'_node_node : (a,b:A;A1,A2,B1,B2:tree)
(order PA a b) -> (order' A1 B1) -> (order' A2 B2) ->
(order' (node a A1 A2) (node b B1 B2)).
Inductive eq' : tree -> tree -> Prop :=
eq'_leaf : (a,b:A) (eq PA a b) -> (eq' (leaf a) (leaf b))
| eq'_leaf_node : (a,b:A;t1,t2:tree)
(eq PA a b) -> (is_bottom t1) -> (is_bottom t2) ->
(eq' (leaf a) (node b t1 t2))
| eq'_node_leaf : (a,b:A;t1,t2:tree)
(eq PA a b) -> (is_bottom t1) -> (is_bottom t2) ->
(eq' (node b t1 t2) (leaf a))
| eq'_node_node : (a,b:A;A1,A2,B1,B2:tree)
(eq PA a b) -> (eq' A1 B1) -> (eq' A2 B2) ->
(eq' (node a A1 A2) (node b B1 B2)).
Definition R := [max:nat;t1,t2:tree]
(height_inf t1 max)/\~(eq' t2 t1)/\(order' t2 t1).
Tactic Definition CaseEq a :=
Generalize (refl_equal ? a); Pattern -1 a; Case a.
Lemma is_bottom_dec : (t:tree){(is_bottom t)}+{~(is_bottom t)}.
NewInduction t.
Case (eq_dec PA a (bottom PA)); Intros.
Left; Constructor; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Case (eq_dec PA a (bottom PA)); Intros.
Case IHt1; Intros.
Case IHt2; Intros.
Left; Constructor; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Qed.
Lemma eq'_dec : (t1,t2:tree){(eq' t1 t2)}+{~(eq' t1 t2)}.
NewInduction t1.
NewInduction t2.
Case (eq_dec PA a a0); Intros.
Left; Constructor; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Case (eq_dec PA a a0); Intros.
Case (is_bottom_dec t0); Intros.
Case (is_bottom_dec t1); Intros.
Left; Constructor; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Intros t3; NewInduction t3.
Case (eq_dec PA a a0); Intros.
Case (is_bottom_dec t0); Intros.
Case (is_bottom_dec t2); Intros.
Left; Constructor; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Case (eq_dec PA a a0); Intros.
Case (IHt0 t1); Intros.
Case (IHt2 t4); Intros.
Left; Constructor; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Right; Red; Intros; Elim n.
Inversion_clear H; Auto.
Qed.
Lemma is_bottom2_eq' : (t1,t2:tree)
(is_bottom t1) -> (is_bottom t2) -> (eq' t1 t2).
NewInduction t1.
Intros.
Inversion_clear H; Inversion_clear H0; Constructor; EAuto.
Intros.
Inversion_clear H; Inversion_clear H0; Constructor; EAuto.
Qed.
Lemma is_bottom_eq' : (t1,t2:tree)
(is_bottom t1) -> (eq' t1 t2) -> (is_bottom t2).
NewInduction t1.
Intros.
Inversion_clear H.
Inversion_clear H0; Constructor; EAuto.
Intros.
Inversion_clear H.
Inversion_clear H0; Constructor; EAuto.
Qed.
Hints Resolve is_bottom_eq' is_bottom2_eq'.
Lemma eq'_sym : (t1,t2:tree)(eq' t1 t2)->(eq' t2 t1).
NewInduction t1; Intros.
Inversion_clear H; Constructor; Auto.
Inversion_clear H; Constructor; Auto.
Qed.
Lemma eq'_trans : (t1,t2,t3:tree)(eq' t1 t2)->(eq' t2 t3)->(eq' t1 t3).
NewInduction t1.
Intros t2 t3 H; Inversion_clear H;
Intros H'; Inversion_clear H';
Constructor; EAuto.
Intros t3 t4 H; Inversion_clear H;
Intros H'; Inversion_clear H';
Constructor; EAuto.
Apply is_bottom_eq' with B1; Auto.
Apply eq'_sym; Auto.
Apply is_bottom_eq' with B2; Auto.
Apply eq'_sym; Auto.
Qed.
Lemma order'_is_bottom : (t1,t2:tree)
(is_bottom t1) -> (order' t1 t2).
NewInduction t1; Intros.
Inversion_clear H.
Case t2; Constructor.
Apply eq_order_order with (bottom PA); Auto.
Apply eq_order_order with (bottom PA); Auto.
Inversion_clear H; Case t1; Constructor; Auto.
Apply eq_order_order with (bottom PA); Auto.
Apply eq_order_order with (bottom PA); Auto.
Qed.
Lemma order'_is_bottom2 : (t1,t2:tree)
(is_bottom t2) -> (order' t1 t2) -> (is_bottom t1).
NewInduction t1; Intros.
Generalize H0; Clear H0; Inversion_clear H.
Intros H; Inversion_clear H; Constructor; EAuto.
Intros H; Inversion_clear H; Constructor; EAuto.
Generalize H0; Clear H0; Inversion_clear H.
Intros H; Inversion_clear H; Constructor; EAuto.
Intros H; Inversion_clear H; Constructor; EAuto.
Qed.
Lemma order'_trans : (t1,t2,t3:tree)(order' t1 t2)->(order' t2 t3)->(order' t1 t3).
NewInduction t1.
Intros t2 t3 H; Inversion_clear H;
Intros H'; Inversion_clear H';
Constructor; EAuto.
Intros t3 t4 H; Inversion_clear H;
Intros H'; Inversion_clear H';
Constructor; EAuto.
Apply order'_is_bottom; Auto.
Apply order'_is_bottom; Auto.
Apply order'_is_bottom2 with B1; Auto.
Apply order'_is_bottom2 with B2; Auto.
Qed.
Lemma R_acc : (max:nat;t:tree) (height_inf t max) -> (Acc ? (R max) t).
NewInduction max.
Destruct t; Intros.
NewInduction (acc_property PA a); Intros.
Constructor; Intros.
Unfold R in H2; Decompose [and] H2; Clear H2.
Generalize H5 H6; Clear H6 H5; Inversion H3.
Intros; Apply H; Auto.
Split.
Red; Intros; Elim H5; Unfold Feq.
Constructor; Auto.
Inversion H6; Auto.
Rewrite H2; Auto.
Inversion H.
Cut (a:A)(Acc tree (R (S max)) (leaf a)); Intro.
Destruct t; Intros.
Auto.
Inversion_clear H0.
Generalize t0 t1 H1 H2; Clear H2 H1 t0 t1.
NewInduction (acc_property PA a); Intros.
Clear H0; Generalize (IHmax ? H2) x t1 H1 H3; Clear H1 H3 H2 t1 x; Intro.
NewInduction H0; Intros.
Clear H0; Generalize (IHmax ? H3) x0 x H1 H2; Clear H1 H2 x0 x; Intro.
NewInduction H0; Intros.
Clear H0; Constructor.
Destruct y; Intros.
Auto.
Unfold R in H0; Decompose [and] H0; Clear H0.
Inversion_clear H5.
Inversion_clear H8.
Case (eq_dec PA x0 a); Intros.
Case (eq'_dec x1 t0); Intros.
Apply H3; Auto.
Unfold R; Split; Auto.
Split; Auto.
Red; Intros; Elim H7; Constructor; Auto.
Intros.
Apply H2; Auto.
Unfold R; Unfold R in H8; Decompose [and] H8; Clear H8.
Intuition.
Elim H15; Apply eq'_trans with x1; Auto.
Apply eq'_sym; Auto.
Apply order'_trans with t0; Auto.
Intros; Apply H4; Auto.
Decompose [and] H8; Clear H8.
Split.
Red; Intros; Elim H13.
Apply eq_trans with x0; Auto.
Apply order_trans with a; Auto.
Apply H2; EAuto.
Unfold R; Split; Auto.
Intros; Apply H4; Auto.
Decompose [and] H8; Clear H8.
Split.
Red; Intros; Elim H13.
Apply eq_trans with x0; Auto.
Apply order_trans with a; Auto.
Apply H4; EAuto.
NewInduction (acc_property PA a); Intros.
Constructor.
Destruct y; Intros.
Apply H0.
Unfold R in H1; Intuition.
Elim H1; Constructor; Auto.
Inversion_clear H4; Auto.
Unfold R in H1; Decompose [and] H1; Clear H1.
Inversion_clear H5.
Inversion_clear H2.
Clear H.
Clear H4.
Generalize t0 t H3 H5 H1; Clear H1 H3 H5 t0 t.
NewInduction (acc_property PA a).
Clear H; Intros.
Generalize t0 x0 H1 H5 H; Clear H H5 H1 x0 t0.
Generalize (IHmax ? H3); Clear H3; Intro.
NewInduction H.
Clear H; Intros.
Generalize x1 x0 H H1 H2; Clear H2 H1 H x0 x1.
Generalize (IHmax ? H5); Clear H5; Intro.
NewInduction H; Intros.
Constructor.
Destruct y0; Intros.
Apply H0.
Unfold R in H5; Decompose [and] H5; Clear H5.
Split.
Red; Intros; Inversion_clear H9.
Elim H8; Constructor; Auto.
Apply order_antisym; Auto.
Apply order_trans with x; Auto.
Inversion_clear H9; Apply order_trans with x1; Auto.
Unfold R in H5; Decompose [and] H5; Clear H5.
Inversion_clear H9.
Inversion_clear H6.
Case (eq_dec PA x1 a); Intros.
Case (eq'_dec x2 t); Intros.
Apply H1.
Unfold R; Split; Auto.
Split; Auto.
Red; Intros; Elim H8; Constructor; Auto.
Intros.
Apply H2.
Unfold R; Unfold R in H6; Decompose [and] H6; Clear H6.
Intuition.
Elim H17; Apply eq'_trans with x2; Auto.
Apply eq'_sym; Auto.
Apply order'_trans with t; Auto.
Auto.
Auto.
Intros; Apply H14; Auto.
Apply order_trans with x1; Auto.
Intros; Apply H4; Auto.
Decompose [and] H6; Clear H6.
Split.
Red; Intros; Elim H15.
Apply eq_trans with x1; Auto.
Apply order_trans with a; Auto.
Apply H2; EAuto.
Unfold R; Split; Auto.
Intros; Apply H4; Auto.
Decompose [and] H6; Clear H6.
Split.
Red; Intros; Elim H15.
Apply eq_trans with x1; Auto.
Apply order_trans with a; Auto.
Apply H4; EAuto.
Qed.
Lemma is_bottom_apply : (t:tree)
(is_bottom t) ->
(p:positive) (eq PA (bottom PA) (apply_tree t p)).
Intros t H; NewInduction H.
Destruct p; Auto.
Destruct p; Auto.
Qed.
Lemma apply_is_bottom : (t:tree)
((p:positive) (eq PA (bottom PA) (apply_tree t p))) ->
(is_bottom t).
NewInduction t; Intros; Constructor.
Generalize (H xH); Auto.
Generalize (H xH); Auto.
Apply IHt1; Intros.
Generalize (H (xO p)); Auto.
Apply IHt2; Intros.
Generalize (H (xI p)); Auto.
Qed.
Lemma eq'_to_Feq : (t1,t2:tree) (eq' t1 t2) -> (Feq t1 t2).
NewInduction t1; Intros.
Inversion_clear H.
Unfold Feq.
Destruct p; Auto.
Unfold Feq.
Destruct p; Simpl; Auto.
Apply is_bottom_apply; Auto.
Apply is_bottom_apply; Auto.
Unfold Feq.
Inversion_clear H.
Destruct p; Simpl; Auto.
Intros; Apply eq_sym; Apply is_bottom_apply; Auto.
Intros; Apply eq_sym; Apply is_bottom_apply; Auto.
Destruct p; Simpl; Auto.
Apply IHt2; Auto.
Apply IHt0; Auto.
Qed.
Lemma Forder_to_order' : (t1,t2:tree) (Forder t1 t2) -> (order' t1 t2).
Unfold Forder; NewInduction t1.
Destruct t2; Intros; Constructor.
Generalize (H xH); Auto.
Generalize (H xH); Auto.
Destruct t3; Intros; Constructor.
Generalize (H xH); Auto.
Apply apply_is_bottom; Intros.
Generalize (H (xO p)); Auto.
Apply apply_is_bottom; Intros.
Generalize (H (xI p)); Auto.
Generalize (H xH); Auto.
Apply IHt0; Intros.
Generalize (H (xO p)); Auto.
Apply IHt2; Intros.
Generalize (H (xI p)); Auto.
Qed.
Lemma R'_acc : (max:nat;t:tree) (height_inf t max) ->
(Acc ?
[t1,t2](height_inf t1 max)/\~(Feq t2 t1)/\(Forder t2 t1)
t).
Intros.
Generalize (R_acc ? ? H); Intros.
Clear H; NewInduction H0.
Clear H; Intros.
Constructor; Intros.
Decompose [and] H0; Clear H0.
Apply H.
Unfold R; Split; Auto.
Split.
Red; Intros; Elim H3.
Apply eq'_to_Feq; Auto.
Apply Forder_to_order'; Auto.
Qed.
Definition funcTree_Lattice : (max:nat)(Lattice (funcTree max)).
Refine [max](poset_constr (funcTree max)
[f1,f2](Forder (tr ? f1) (tr ? f2)) [f1,f2](Feq (tr ? f1) (tr ? f2))
(Fjoin max) ? ? ? ? ? ? ? ? ? ?
(Fbottom max) ? (topF ?) ? ?).
Unfold Feq Forder; Intros; Auto.
Unfold Feq Forder; Intros; Auto.
Unfold Feq Forder; Intros; Auto.
Apply order_trans with (apply_tree (tr max y) p); Auto.
Unfold Feq; Intros; Auto.
Unfold Feq; Intros; Auto.
Unfold Feq; Intros; Auto.
Apply eq_trans with (apply_tree (tr max y) p); Auto.
Unfold Feq Forder; Intros; Auto.
Apply order_trans with (join PA (apply_tree (tr max x) p) (apply_tree (tr max y) p)); Auto.
Unfold Fjoin; Generalize (apply_join_tree (tr max x) (tr max y) ); Auto.
Unfold Feq Forder; Intros; Auto.
Apply order_trans with (join PA (apply_tree (tr max x) p) (apply_tree (tr max y) p)); Auto.
Unfold Fjoin; Generalize (apply_join_tree (tr max x) (tr max y) ); Auto.
Unfold Feq Forder; Intros; Auto.
Apply order_trans with (join PA (apply_tree (tr max x) p) (apply_tree (tr max y) p)); Auto.
Unfold Fjoin; Generalize (apply_join_tree (tr max x) (tr max y) ); Auto.
Destruct x; Destruct y; Simpl; Intros.
Apply Feq_dec.
Unfold Forder; Intros.
Generalize (apply_bottom max p); Unfold apply; Intros.
Rewrite H; Auto.
Intros f; Case f; Simpl; Apply topF_is_top; Auto.
Unfold well_founded.
Destruct a; Intros.
Generalize (R'_acc ? ? tr_bound0); Intros.
Generalize tr_bound0; Clear tr_bound0.
NewInduction H; Intros.
Constructor.
Destruct y; Intros.
Decompose [and] H1; Clear H1.
Apply H0; Auto.
Defined.
Local subst_tree := (subst_tree A (bottom PA)).
Lemma height_inf_subst : (p:positive;t:tree;n:nat;v:A)
(height_inf t n) -> (inf_log p n) ->
(height_inf (subst_tree t p v) n).
NewInduction p; Intros.
Generalize H; Clear H; Inversion_clear H0.
Case t; Simpl; Intros.
Clear H0.
Constructor.
Constructor.
Apply IHp; Constructor Orelse Auto.
Inversion_clear H0.
Constructor; Auto.
Generalize H; Clear H; Inversion_clear H0.
Case t; Simpl; Intros.
Clear H0.
Constructor.
Apply IHp; Constructor Orelse Auto.
Constructor.
Inversion_clear H0.
Constructor; Auto.
Generalize H; Clear H H0; Case t; Intros; Simpl.
Constructor.
Inversion_clear H; Constructor; Auto.
Qed.
Definition subst' : (max:nat;f:(funcTree max);p:positive;v:A)
(inf_log p max) -> (funcTree max).
Refine [max,f,p,v,H]
(funcTree_constr ? (subst_tree (tr ? f) p v) ?).
Apply height_inf_subst.
Case f; Auto.
Auto.
Defined.
Definition subst : (max:nat;f:(funcTree max);p:positive;v:A) (funcTree max) :=
[max,f,p,v]
Cases (inf_log_dec p max) of
| (left H) => (subst' max f p v H)
| (right _) => f
end.
Lemma apply_subst1 : (max:nat;f:(funcTree max);p:positive;v:A)
(inf_log p max) ->
(apply ? (subst ? f p v) p)=v.
Destruct f; Unfold subst subst' apply; Simpl; Intros.
Case inf_log_dec; Intros.
Unfold apply_tree subst_tree; Simpl.
Apply apply_subst_tree1.
Elim n; Auto.
Qed.
Lemma apply_subst2 : (max:nat;f:(funcTree max);x,p:positive;v:A)
(inf_log p max) ->
~x=p -> (apply ? (subst ? f p v) x)=(apply ? f x).
Destruct f; Unfold subst subst' apply; Simpl; Intros.
Case inf_log_dec; Intros; Simpl.
Unfold apply_tree subst_tree.
Apply apply_subst_tree2.
Auto.
Elim n; Auto.
Qed.
Lemma apply_monotone : (max:nat;f1,f2:(funcTree max))
(order (funcTree_Lattice max) f1 f2) ->
(p:positive)(order PA (apply ? f1 p) (apply ? f2 p)).
Unfold funcTree_Lattice Forder; Simpl; Intros.
Unfold apply; Apply H.
Qed.
Lemma subst_monotone : (max:nat;f1,f2:(funcTree max);p:positive;v1,v2:A)
(order (funcTree_Lattice max) f1 f2) ->
(order PA v1 v2) ->
(order (funcTree_Lattice max)(subst ? f1 p v1) (subst ? f2 p v2)).
Unfold subst subst' funcTree_Lattice Forder subst_tree apply_tree; Simpl; Intros.
Case inf_log_dec; Intros; Simpl.
Unfold subst_tree; Case (positive_dec p p0); Intros.
Subst.
Do 2 Rewrite apply_subst_tree1; Auto.
Rewrite apply_subst_tree2; Auto.
Rewrite apply_subst_tree2; Auto.
Auto.
Qed.
Lemma subst_order_inf : (max:nat;f,g:(funcTree max);p:positive;v:A)
(inf_log p max) ->
(order (funcTree_Lattice max) (subst ? f p v) g) ->
(order PA v (apply ? g p)).
Intros.
Rewrite <- (apply_subst1 max f p v).
Apply apply_monotone; Auto.
Auto.
Qed.
Lemma funcTree_order : (max:nat;f1,f2:(funcTree max))
((p:positive)(order PA (apply ? f1 p) (apply ? f2 p)))->
(order (funcTree_Lattice max) f1 f2).
Unfold funcTree_Lattice Forder apply; Simpl; Auto.
Qed.
Lemma apply_funcTree_not_inf_log : (max:nat;f:(funcTree max);p:positive)
~(inf_log p max) ->
(apply ? f p)=(bottom PA).
Destruct f; Unfold apply; Simpl.
Intros t.
Generalize max; Clear f max.
NewInduction t; Destruct p; Simpl; Auto; Intros.
Elim H; Constructor.
Generalize H; Clear H; Inversion_clear tr_bound0; Intros.
Apply (IHt2 p1); Auto.
Red; Intros; Elim H1; Constructor; Auto.
Generalize H; Clear H; Inversion_clear tr_bound0; Intros.
Apply (IHt1 p1); Auto.
Red; Intros; Elim H1; Constructor; Auto.
Elim H; Constructor.
Qed.
Lemma subst_funcTree_not_inf_log : (max:nat;f:(funcTree max);p:positive;v:A)
~(inf_log p max) ->
(subst ? f p v)=f.
Destruct f; Unfold subst.
Intros.
Case inf_log_dec; Intros.
Elim H; Auto.
Auto.
Qed.
Lemma subst_order : (max:nat;f1,f2:(funcTree max);p0:positive;v:A)
((p:positive)~p=p0->(order PA (apply ? f1 p) (apply ? f2 p))) ->
(order PA v (apply ? f2 p0)) ->
(order (funcTree_Lattice max) (subst ? f1 p0 v) f2).
Intros.
Apply funcTree_order.
Intros p; Case (positive_dec p p0); Intros.
Subst.
Case (inf_log_dec p0 max); Intros.
Rewrite apply_subst1; Auto.
Rewrite apply_funcTree_not_inf_log; Auto.
Case (inf_log_dec p0 max); Intros.
Rewrite apply_subst2; Auto.
Rewrite subst_funcTree_not_inf_log; Auto.
Qed.
Lemma apply_on_bottom : (max:nat;p:positive)
(apply ? (bottom (funcTree_Lattice max)) p)=(bottom PA).
Unfold funcTree_Lattice apply; Simpl; Intros.
NewInduction p; Simpl; Auto.
Qed.
Lemma apply_on_top : (max:nat;p:positive)
(inf_log p max) ->
(apply ? (top (funcTree_Lattice max)) p)=(top PA).
Unfold funcTree_Lattice apply; Simpl; Intros.
Unfold apply_tree.
Apply (apply_build_const_TabTree_is_const A (bottom PA)); Auto.
Qed.
End funcTree.
Section map_tree.
Variable A,B:Set.
Variable PA:(Lattice A).
Variable PB:(Lattice B).
Definition map : (max:nat) (A->B) -> (funcTree A max) -> (funcTree B max).
Refine [max,f,t]
(funcTree_constr ? ? (map_tree ? ? f (tr ? ? t)) ?).
Case t; Intros.
Simpl; Generalize max tr_bound0; Clear t tr_bound0.
NewInduction tr0; Simpl; Intros.
Constructor.
Inversion_clear tr_bound0.
Constructor; Auto.
Defined.
Lemma map_correct : (max:nat;f:(A->B);t:(funcTree A max);p:positive)
(f (bottom PA))=(bottom PB) ->
(apply B PB max (map max f t) p)=(f (apply A PA max t p)).
Unfold apply map; Simpl; Intros.
Apply map_tree_correct; Auto.
Qed.
Lemma map_monotone : (max:nat;f,g:(A->B);x,y:(funcTree A max))
(f (bottom PA))=(bottom PB) ->
(g (bottom PA))=(bottom PB) ->
((x,y:A)(order PA x y)->(order PB (f x) (g y))) ->
(order (funcTree_Lattice A PA max) x y) ->
(order (funcTree_Lattice B PB max) (map max f x) (map max g y)).
Intros.
Apply funcTree_order; Intros.
Rewrite map_correct; Auto.
Rewrite map_correct; Auto.
Apply H1.
Apply apply_monotone; Auto.
Qed.
End map_tree.
Section mapIt_tree.
Variable A,B:Set.
Variable PA:(Lattice A).
Variable PB:(Lattice B).
Lemma height_inf_mapIt_rec : (f:positive->A->B;t:(tree A);max:nat;p:positive)
(height_inf ? t max) -> (height_inf ? (mapIt_tree_rec ? ? f p t) max).
NewInduction t; Simpl.
Constructor.
Intros.
Inversion_clear H; Constructor; Auto.
Qed.
Definition mapIt : (max:nat) (positive->A->B) -> (funcTree A max) -> (funcTree B max).
Refine [max,f,t]
(funcTree_constr ? ? (mapIt_tree ? ? f (tr ? ? t)) ?).
Unfold mapIt_tree; Apply height_inf_mapIt_rec.
Case t; Auto.
Defined.
Lemma mapIt_correct : (max:nat;f:(positive->A->B);t:(funcTree A max);p:positive)
((p:positive)(f p (bottom PA))=(bottom PB)) ->
(apply B PB max (mapIt max f t) p)=(f p (apply A PA max t p)).
Unfold apply mapIt; Simpl; Intros.
Apply mapIt_tree_correct; Auto.
Qed.
End mapIt_tree.
Implicits map [1 2 3].
Implicits mapIt [1 2 3].
Implicits apply [1 3].
Implicits subst [1 3].
Hints Resolve apply_monotone subst_monotone.