Library ArrayLattice
Require Export Lattice.
Require Export TabTree.
Section funcTree.
Variable A : Set.
Variable PA : Lattice A.
Let tree := tree A.
Implicit Arguments leaf [A].
Implicit Arguments node [A].
Let apply_tree := apply_tree A (bottom PA).
Inductive height_inf : tree -> nat -> Prop :=
| inf_leaf : forall (p:nat), (height_inf leaf p)
| inf_node : forall (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 (S max)}.
Definition Feq (t1 t2 : tree) : Prop :=
forall p : positive, eq PA (apply_tree t1 p) (apply_tree t2 p).
Fixpoint join_tree (t1 t2 : tree) {struct t2} : tree :=
match t1, t2 with
| leaf, _ => t2
| _, leaf => t1
| 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_height_inf :
forall (t1 t2 : tree) (max:nat),
height_inf t1 max ->
height_inf t2 max ->
height_inf (join_tree t1 t2) max.
induction t1 as [|a t11 t12]; destruct t2 as [|b t21 t22]; simpl; intros; auto.
inversion_clear H in H0.
inversion_clear H0.
constructor; auto.
Qed.
Lemma apply_tree_bot :
forall (max:nat) (t : tree) (p : positive),
(height_inf t (S max)) ->
~(inf_log p max) ->
(apply_tree t p) = (bottom PA).
induction max; simpl; intros; auto.
inversion_clear H; simpl; auto.
inversion_clear H1; simpl.
inversion_clear H2; simpl.
destruct p; auto.
elim H0; constructor.
inversion_clear H; simpl; auto.
destruct p.
apply IHmax; auto.
red; intros; elim H0; constructor; auto.
apply IHmax; auto.
red; intros; elim H0; constructor; auto.
elim H0; constructor.
Qed.
Definition Fjoin :
forall (max:nat),
funcTree max -> funcTree max -> funcTree max.
intros max f1 f2;
refine (funcTree_constr _ (join_tree (tr _ f1) (tr _ f2)) _).
apply join_tree_height_inf.
case f1; auto.
case f2; auto.
Defined.
Definition apply_functree (max:nat)
(f : funcTree max) (p : positive) :=
apply_tree (tr _ f) p.
Let Forder (f1 f2 : tree) : Prop :=
forall p : positive, order PA (apply_tree f1 p) (apply_tree f2 p).
Definition Fbottom :
forall (max:nat), funcTree max.
refine (fun max => funcTree_constr _ leaf _).
intros.
constructor.
Defined.
Lemma apply_bottom :
forall (max:nat) (p : positive),
apply_functree _ (Fbottom max) p = bottom PA.
unfold apply_functree, Fbottom in |- *; simpl in |- *; intros.
reflexivity.
Qed.
Lemma apply_join_tree :
forall (t1 t2 : tree) (p : positive),
eq PA (apply_tree (join_tree t1 t2) p)
(join PA (apply_tree t1 p) (apply_tree t2 p)).
induction t1 as [| a t0 IHt0 t2 IHt2]; intros t; case t; simpl in |- *;
intros.
case p; simpl in |- *; auto.
case p; simpl in |- *; auto.
case p; simpl in |- *; auto.
case p; simpl in |- *; auto.
Qed.
Let Feq_bot_dec :
forall t1 : tree,
{(forall p : positive, eq PA (apply_tree t1 p) (bottom PA))} +
{~ (forall p : positive, eq PA (apply_tree t1 p) (bottom PA))}.
induction t1 as [| a t0 IHt0 t2 IHt2]; simpl in |- *.
left; simpl in |- *; auto.
case (order_dec PA a (bottom PA)); intros.
case IHt0; intros.
case IHt2; intros.
left; simple destruct p; simpl in |- *; auto.
right; red in |- *; intros H; elim n; intros p; generalize (H (xI p));
simpl in |- *; auto.
right; red in |- *; intros H; elim n; intros p; generalize (H (xO p));
simpl in |- *; auto.
right; red in |- *; intros H; elim n; generalize (H 1%positive);
simpl in |- *; auto.
Qed.
Let Forder_dec : forall t1 t2 : tree, {Forder t1 t2} + {~ Forder t1 t2}.
induction t1 as [| a t0 IHt0 t2 IHt2]; intros t; case t; intros.
left; unfold Forder in |- *; auto.
left; unfold Forder in |- *; auto.
unfold apply_tree; simpl; auto.
case (order_dec PA a (bottom PA)); intros.
case (Feq_bot_dec t0); intros.
case (Feq_bot_dec t2); intros.
left; unfold Forder in |- *; intros.
case p; simpl in |- *; auto.
right; unfold Forder in |- *; intros H; elim n; intros p;
generalize (H (xI p)); simpl in |- *; auto.
right; unfold Forder in |- *; intros H; elim n; intros p;
generalize (H (xO p)); simpl in |- *; auto.
right; unfold Forder in |- *; intros H; elim n; generalize (H 1%positive); auto.
case (order_dec PA a a0); intros.
case (IHt0 t1); intros.
case (IHt2 t3); intros.
left; unfold Forder in |- *; intros.
case p; simpl in |- *; auto.
right; unfold Forder in |- *; intros H; elim n; intros p;
generalize (H (xI p)); simpl in |- *; auto.
right; unfold Forder in |- *; intros H; elim n; intros p;
generalize (H (xO p)); simpl in |- *; auto.
right; unfold Forder in |- *; intros H; elim n; generalize (H 1%positive); auto.
Qed.
Inductive is_bottom : tree -> Prop :=
| is_bottom_leaf : is_bottom leaf
| is_bottom_node :
forall (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 : forall t : tree, order' leaf t
| order'_node_leaf :
forall (a : A) (t1 t2 : tree),
eq PA a (bottom PA) ->
is_bottom t1 -> is_bottom t2 -> order' (node a t1 t2) leaf
| order'_node_node :
forall (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 : eq' leaf leaf
| eq'_leaf_node :
forall (b : A) (t1 t2 : tree),
eq PA (bottom PA) b ->
is_bottom t1 -> is_bottom t2 -> eq' leaf (node b t1 t2)
| eq'_node_leaf :
forall (b : A) (t1 t2 : tree),
eq PA (bottom PA) b ->
is_bottom t1 -> is_bottom t2 -> eq' (node b t1 t2) leaf
| eq'_node_node :
forall (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).
Ltac CaseEq a := generalize (refl_equal a); pattern a at -1 in |- *; case a.
Lemma is_bottom_dec : forall t : tree, {is_bottom t} + {~ is_bottom t}.
induction t.
left; constructor; auto.
case (order_dec PA a (bottom PA)); intros.
case IHt1; intros.
case IHt2; intros.
left; constructor; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
Qed.
Lemma eq'_dec : forall t1 t2 : tree, {eq' t1 t2} + {~ eq' t1 t2}.
induction t1 as [| a t0 IHt0 t2 IHt2].
induction t2 as [| a t0 IHt0 t1 IHt1].
left; constructor; auto.
case (order_dec PA a (bottom PA)); intros.
case (is_bottom_dec t0); intros.
case (is_bottom_dec t1); intros.
left; constructor; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
intros t3; induction t3 as [| a0 t1 IHt1 t4 IHt4].
case (order_dec PA a (bottom PA)); intros.
case (is_bottom_dec t0); intros.
case (is_bottom_dec t2); intros.
left; constructor; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; 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 in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
right; red in |- *; intros; elim n.
inversion_clear H; auto.
Qed.
Lemma is_bottom2_eq' :
forall t1 t2 : tree, is_bottom t1 -> is_bottom t2 -> eq' t1 t2.
induction t1 as [| a t0 IHt0 t2 IHt2].
intros.
inversion_clear H; inversion_clear H0; constructor; eauto.
intros.
inversion_clear H; inversion_clear H0; constructor; eauto.
Qed.
Lemma is_bottom_eq' :
forall t1 t2 : tree, is_bottom t1 -> eq' t1 t2 -> is_bottom t2.
induction t1 as [| a t0 IHt0 t2 IHt2].
intros.
inversion_clear H.
inversion_clear H0; constructor; eauto.
intros.
inversion_clear H.
inversion_clear H0; constructor; eauto.
Qed.
Hint Resolve is_bottom_eq' is_bottom2_eq'.
Lemma eq'_sym : forall t1 t2 : tree, eq' t1 t2 -> eq' t2 t1.
induction t1 as [| a t0 IHt0 t2 IHt2]; intros.
inversion_clear H; constructor; auto.
inversion_clear H; constructor; auto.
Qed.
Lemma eq'_trans : forall t1 t2 t3 : tree, eq' t1 t2 -> eq' t2 t3 -> eq' t1 t3.
induction t1 as [| a t0 IHt0 t2 IHt2].
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 : forall t1 t2 : tree, is_bottom t1 -> order' t1 t2.
induction t1 as [| a t0 IHt0 t2 IHt2]; intros.
constructor.
inversion_clear H; case t1; constructor; auto.
apply eq_order_order with (bottom PA); auto.
Qed.
Lemma order'_is_bottom2 :
forall t1 t2 : tree, is_bottom t2 -> order' t1 t2 -> is_bottom t1.
induction t1 as [| a t0 IHt0 t2 IHt2]; 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'_antisym :
forall t1 t2 : tree, order' t1 t2 -> order' t2 t1 -> eq' t1 t2.
intros t1 t2 H.
induction H
as [t| a t1 t2 H H0 H1| a b A1 A2 B1 B2 H H1 IHorder'1 H2 IHorder'2];
intros H4.
inversion H4; constructor; auto.
constructor; auto.
inversion_clear H4; constructor; auto.
Qed.
Lemma order'_trans :
forall t1 t2 t3 : tree, order' t1 t2 -> order' t2 t3 -> order' t1 t3.
induction t1 as [| a t0 IHt0 t2 IHt2].
intros t2 t3 H; inversion_clear H; intros H'; inversion_clear H'; constructor;
eauto.
intros t3 t4 H; inversion_clear H.
intros; destruct t4 as [| a0 t t1]; constructor; try assumption.
apply order_trans with (bottom PA); auto.
apply order'_is_bottom; auto.
apply order'_is_bottom; auto.
intros H'.
inversion_clear H'.
constructor.
apply order_antisym; auto.
apply order_trans with b; auto.
apply order'_is_bottom2 with B1; auto.
apply order'_is_bottom2 with B2; auto.
constructor.
apply order_trans with b; auto.
apply IHt0 with B1; auto.
apply IHt2 with B2; auto.
Qed.
Definition R (max : nat) (t1 t2 : tree) :=
height_inf t1 max /\ ~ eq' t2 t1 /\ order' t2 t1.
Lemma R_acc :
forall (max : nat) (t : tree), height_inf t max -> Acc (R max) t.
induction max.
simple destruct t; intros.
constructor; intros.
unfold R in H0; decompose [and] H0.
generalize H3; inversion_clear H1; intros.
elim H1; constructor.
inversion H.
cut (Acc (R (S max)) leaf).
intro.
simple destruct t; intros.
auto.
inversion_clear H0.
generalize t0 t1 H1 H2; clear H2 H1 t0 t1.
induction (acc_property PA a); intros.
clear H0; generalize (IHmax _ H2) x t1 H1 H3; clear H1 H3 H2 t1 x; intro.
induction H0; intros.
clear H0; generalize (IHmax _ H3) x0 x H1 H2; clear H1 H2 x0 x; intro.
induction H0; intros.
clear H0; constructor.
simple 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 H1; auto.
unfold R in |- *; split; auto.
split; auto.
red in |- *; intros; elim H7; constructor; auto.
intros.
apply H2; auto.
unfold R in |- *; 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 in |- *; intros; elim H13.
apply eq_trans with x0; auto.
apply order_trans with a; auto.
apply H2; eauto.
unfold R in |- *; split; auto.
intros; apply H4; auto.
decompose [and] H8; clear H8.
split.
red in |- *; intros; elim H13.
apply eq_trans with x0; auto.
apply order_trans with a; auto.
apply H4; eauto.
constructor.
simple destruct y; intros.
unfold R in H; intuition.
elim H; constructor.
unfold R in H; decompose [and] H; clear H.
inversion_clear H0.
clear H2 H3.
generalize t0 t H H1; clear H1 H t0 t.
induction (acc_property PA a).
clear H; intros.
generalize t0 x H1 H0; clear H0 H1 x t0.
generalize (IHmax _ H); clear H; intro.
induction H.
clear H; intros.
generalize x x0 H0 H2; clear H0 H2 x0 x.
generalize (IHmax _ H1); clear H1; intro.
induction H; intros.
constructor.
simple destruct y0; intros.
elim H3; intuition.
elim H6.
apply order'_antisym; auto.
constructor.
unfold R in H3; decompose [and] H3; clear H3.
inversion_clear H4.
inversion_clear H7.
case (eq_dec PA x1 a); intros.
case (eq'_dec x0 t); intros.
apply H0.
unfold R in |- *; split; auto.
split; auto.
red in |- *; intros; elim H6; constructor; auto.
intros.
apply H1.
unfold R in |- *; unfold R in H7; decompose [and] H7; clear H7.
intuition.
elim H14; apply eq'_trans with x0; auto.
apply eq'_sym; auto.
apply order'_trans with t; auto.
auto.
auto.
intros; apply H2; auto.
decompose [and] H7; clear H7.
split.
red in |- *; intros; elim H12.
apply eq_trans with x1; auto.
apply order_trans with a; auto.
apply H1; eauto.
unfold R in |- *; split; auto.
intros; apply H2; auto.
decompose [and] H7; clear H7.
split.
red in |- *; intros; elim H12.
apply eq_trans with x1; auto.
apply order_trans with a; auto.
apply H2; eauto.
Qed.
Lemma is_bottom_apply :
forall t : tree,
is_bottom t ->
forall p : positive, eq PA (bottom PA) (apply_tree t p).
intros t H; induction H as [| a t1 t2 H H1 IHis_bottom1 H2 IHis_bottom2].
simple destruct p; auto.
simple destruct p; auto.
Qed.
Lemma apply_is_bottom :
forall t : tree,
(forall p : positive, eq PA (bottom PA) (apply_tree t p)) ->
is_bottom t.
induction t; intros; constructor.
generalize (H 1%positive); auto.
apply IHt1; intros.
generalize (H (xO p)); auto.
apply IHt2; intros.
generalize (H (xI p)); auto.
Qed.
Lemma eq'_to_Feq : forall t1 t2 : tree, eq' t1 t2 -> Feq t1 t2.
induction t1 as [| a t0 IHt0 t2 IHt2]; intros.
inversion_clear H.
unfold Feq in |- *.
simple destruct p; auto.
unfold Feq in |- *.
simple destruct p; simpl in |- *; auto.
apply is_bottom_apply; auto.
apply is_bottom_apply; auto.
unfold Feq in |- *.
inversion_clear H.
simple destruct p; simpl in |- *; auto.
intros; apply eq_sym; apply is_bottom_apply; auto.
intros; apply eq_sym; apply is_bottom_apply; auto.
simple destruct p; simpl in |- *; auto.
apply IHt2; auto.
apply IHt0; auto.
Qed.
Lemma Forder_to_order' : forall t1 t2 : tree, Forder t1 t2 -> order' t1 t2.
unfold Forder in |- *; induction t1 as [| a t0 IHt0 t2 IHt2].
simple destruct t2; intros; constructor.
simple destruct t3; intros.
constructor.
generalize (H 1%positive); auto.
apply apply_is_bottom; intros.
generalize (H (xO p)); auto.
apply apply_is_bottom; intros.
generalize (H (xI p)); auto.
constructor.
generalize (H 1%positive); auto.
apply IHt0; intros.
generalize (H (xO p)); auto.
apply IHt2; intros.
generalize (H (xI p)); auto.
Qed.
Lemma R'_acc :
forall (max : nat) (t : tree),
height_inf t max ->
Acc (fun t1 t2 => height_inf t1 max /\ ~ Feq t2 t1 /\ Forder t2 t1) t.
intros.
generalize (R_acc _ _ H); intros.
clear H; induction H0.
clear H; intros.
constructor; intros.
decompose [and] H; clear H.
apply H0.
unfold R in |- *; split; auto.
split.
red in |- *; intros; elim H3.
apply eq'_to_Feq; auto.
apply Forder_to_order'; auto.
Qed.
Definition topF : forall (max:nat), (funcTree max).
refine
(fun max => (funcTree_constr _
(build_const_TabTree_rec _ (top PA) max) _)).
induction max; simpl; repeat (constructor; auto).
Defined.
Lemma topF_is_top : forall (max:nat) (t:tree),
(height_inf t (S 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.
induction max.
intros.
inversion_clear H; simpl.
auto.
generalize n; clear n; case p0; intros.
inversion_clear H1.
unfold apply_tree; auto.
inversion_clear H0.
unfold apply_tree; auto.
elim n; constructor.
intros.
inversion_clear H.
unfold apply_tree; auto.
simpl.
generalize n; clear n; case p0; intros.
apply IHmax; auto.
red; intros; elim n; constructor; auto.
apply IHmax; auto.
red; intros; elim n; constructor; auto.
elim n; constructor.
Qed.
Definition const : forall (max:nat), A -> (funcTree max).
refine
(fun max a => (funcTree_constr _
(build_const_TabTree_rec _ a max) _)).
induction max; simpl; repeat (constructor; auto).
Defined.
Lemma apply_const : forall (max:nat) a p,
inf_log p max ->
(apply_functree max (const max a) p) = a.
unfold apply_functree, apply_tree, const; simpl; intros.
rewrite apply_build_const_TabTree_is_const; auto.
Qed.
Definition funcTree_Poset : forall (max:nat), Poset (funcTree max).
intros max.
refine (poset_constr (funcTree max)
(fun t1 t2 => Feq (tr _ t1) (tr _ t2)) _ _ _
(fun t1 t2 => Forder (tr _ t1) (tr _ t2)) _ _ _).
unfold Feq in |- *; intros; auto.
unfold Feq in |- *; intros; auto.
unfold Feq in |- *; intros; auto.
apply eq_trans with (apply_tree (tr max y) p); auto.
unfold Feq, Forder in |- *; intros; auto.
unfold Feq, Forder in |- *; intros; auto.
unfold Feq, Forder in |- *; intros; auto.
apply order_trans with (apply_tree (tr max y) p); auto.
Defined.
Definition funcTree_Lattice :
forall (max:nat), Lattice (funcTree max).
refine
(fun max =>
lattice_constr (funcTree max)
(funcTree_Poset max)
(Fjoin max) _ _ _ _
(Fbottom max) _ (topF max) _ _); unfold funcTree_Poset; simpl.
intros.
unfold Feq, Forder in |- *; intros; auto.
apply
order_trans
with (join PA (apply_tree (tr max x) p) (apply_tree (tr max y) p));
auto.
unfold Fjoin in |- *; generalize (apply_join_tree (tr max x) (tr max y));
auto.
unfold Feq, Forder in |- *; intros; auto.
apply
order_trans
with (join PA (apply_tree (tr max x) p) (apply_tree (tr max y) p));
auto.
unfold Fjoin in |- *; generalize (apply_join_tree (tr max x) (tr max y));
auto.
simpl in |- *; unfold Feq, Forder in |- *; intros; auto.
apply
order_trans
with (join PA (apply_tree (tr max x) p) (apply_tree (tr max y) p));
auto.
unfold Fjoin in |- *; generalize (apply_join_tree (tr max x) (tr max y));
auto.
intros x y; apply Forder_dec.
unfold Forder in |- *; intros.
generalize (apply_bottom max p); unfold apply_functree in |- *; intros.
unfold Fbottom in H; simpl tr in H.
rewrite H; auto.
intros; unfold topF; simpl.
apply topF_is_top.
case x; simpl; auto.
intros; constructor.
unfold well_founded in |- *.
destruct y; simpl; intros.
generalize (R'_acc _ _ tr_bound0); intros.
generalize tr_bound0; clear tr_bound0.
induction H0; intros.
constructor.
destruct y; simpl; intros.
apply H1.
intuition.
intuition.
elim H3.
unfold Feq,Forder in *; intros.
apply order_antisym; auto.
apply order_trans with (apply_tree tr0 p); auto.
unfold Feq,Forder in *; intros.
apply order_trans with (apply_tree x p); auto.
Defined.
Definition applyFunc (max:nat) :
forall (f : funcTree max) (p : posInf max), A :=
fun t p =>
apply_functree max t (proj1_sig p).
Lemma applyFunc_monotone (max:nat) :
forall (f1 f2 : funcTree max) (p : posInf max),
order (funcTree_Lattice max) f1 f2 ->
order PA (applyFunc max f1 p) (applyFunc max f2 p).
Proof.
intros.
generalize (H (proj1_sig p)); unfold applyFunc; auto.
Qed.
Let modify_tree := modify_tree A (bottom PA).
Lemma height_inf_modify :
forall (t:tree) (p:positive) (n:nat) (v:A->A),
(height_inf t (S n)) -> (inf_log p n) ->
(height_inf (modify_tree t p v) (S n)).
induction t; simpl; intros.
generalize p H0; clear H0 H p.
induction n; simpl; intros.
inversion_clear H0; simpl.
repeat constructor.
destruct p; simpl; constructor ;auto.
constructor.
apply IHn.
inversion_clear H0; assumption.
apply IHn.
inversion_clear H0; assumption.
constructor.
constructor.
constructor.
inversion_clear H.
destruct p; constructor; auto.
inversion_clear H0 in H1 H2.
apply IHt2; auto.
inversion_clear H0 in H1 H2.
apply IHt1; auto.
Qed.
Definition modifyFunc :
forall (max:nat) (f : funcTree max)
(p : posInf max) (v : A -> A), funcTree max.
refine
(fun max f p v =>
(funcTree_constr _ (modify_tree (tr _ f) (proj1_sig p) v) _)).
apply height_inf_modify.
destruct f; auto.
destruct p; auto.
Defined.
Lemma apply_modify1 :
forall (max:nat) (f : funcTree max)
(x p : posInf max) (v : A -> A),
proj1_sig x = proj1_sig p ->
applyFunc _ (modifyFunc _ f p v) x = v (applyFunc _ f x).
destruct f; unfold applyFunc, modifyFunc, apply_functree in |- *; simpl; intros.
rewrite H.
unfold apply_tree, modify_tree; rewrite apply_modify_tree1.
intuition.
Qed.
Lemma apply_modify2 :
forall (max:nat) (f : funcTree max)
(x p : posInf max) (v : A -> A),
proj1_sig x <> proj1_sig p ->
applyFunc _ (modifyFunc _ f p v) x = (applyFunc _ f x).
destruct f; unfold applyFunc, modifyFunc, apply_functree in |- *; simpl; intros.
unfold apply_tree, modify_tree; rewrite apply_modify_tree2; intuition.
Qed.
Definition substFunc (max:nat)
(f : funcTree max) (p : posInf max) (v : A) : funcTree max :=
modifyFunc max f p (fun _ => v).
Lemma apply_subst1 :
forall (max:nat) (f : funcTree max)
(x p : posInf max) (v : A),
proj1_sig x = proj1_sig p ->
applyFunc _ (substFunc _ f p v) x = v.
intros; unfold substFunc; rewrite apply_modify1; auto.
Qed.
Lemma apply_subst2 :
forall (max:nat) (f : funcTree max)
(x p : posInf max) (v : A),
proj1_sig x <> proj1_sig p ->
applyFunc _ (substFunc _ f p v) x = (applyFunc _ f x).
intros; unfold substFunc; rewrite apply_modify2; auto.
Qed.
End funcTree.
Record LatticeFuncType (A:Set) (LA:(Lattice A))
(max:nat) : Type := cLatticeFunc {
lat :> (Lattice (funcTree A max));
apply : funcTree A max -> posInf max -> A;
modify : funcTree A max -> posInf max -> (A->A) -> funcTree A max;
subst : funcTree A max -> posInf max -> A -> funcTree A max
}.
Definition LatticeFunc (A:Set) (LA:(Lattice A))
(max:nat) : (LatticeFuncType A LA max) :=
(cLatticeFunc _ _ _
(funcTree_Lattice A LA max)
(applyFunc A LA max)
(modifyFunc A LA max)
(substFunc A LA max)).
Implicit Arguments LatticeFunc [A].
Implicit Arguments LatticeFuncType [A].
Implicit Arguments subst [A LA max].
Implicit Arguments apply [A LA max].
Implicit Arguments modify [A LA max].
Lemma apply_monotone :
forall (A:Set) (LA:Lattice A) (max:nat)
(F1 F2 : funcTree A max)
(p : posInf max),
(order (LatticeFunc LA max) F1 F2) ->
(order LA
(apply (LatticeFunc LA max) F1 p)
(apply (LatticeFunc LA max) F2 p)).
unfold LatticeFunc, applyFunc, apply_functree; simpl; intros.
apply H.
Qed.
Implicit Arguments apply_monotone [A LA max].
Lemma order_func_def :
forall (A:Set) (LA:Lattice A) (max:nat)
(F1 F2 : funcTree A max),
(forall (p : posInf max),
(order LA
(apply (LatticeFunc LA max) F1 p)
(apply (LatticeFunc LA max) F2 p))) ->
(order (LatticeFunc LA max) F1 F2).
unfold LatticeFunc, applyFunc, apply_functree; simpl; intros.
case (inf_log_dec p max); intros.
generalize (H (exist (fun p => (inf_log p max)) p i)).
simpl; auto.
rewrite (apply_tree_bot _ LA (max)); auto.
case F1; simpl; auto.
Qed.
Lemma modify_monotone :
forall (A:Set) (LA:Lattice A) (max:nat)
(F1 F2 : funcTree A max) (v1 v2 : A->A)
(p : posInf max),
(order (LatticeFunc LA max) F1 F2) ->
(forall (x1 x2:A), (order LA x1 x2) -> (order LA (v1 x1) (v2 x2))) ->
(order (LatticeFunc LA max)
(modify (LatticeFunc LA max) F1 p v1)
(modify (LatticeFunc LA max) F2 p v2)).
unfold LatticeFunc, applyFunc, substFunc; simpl; intros.
case (positive_dec (proj1_sig p) p0); intros.
rewrite e; rewrite apply_modify_tree1.
rewrite apply_modify_tree1; auto.
rewrite apply_modify_tree2; auto.
rewrite apply_modify_tree2; auto.
Qed.
Lemma subst_monotone :
forall (A:Set) (LA:Lattice A) (max:nat)
(F1 F2 : funcTree A max) (v1 v2 : A)
(p : posInf max),
(order (LatticeFunc LA max) F1 F2) ->
(order LA v1 v2) ->
(order (LatticeFunc LA max)
(subst (LatticeFunc LA max) F1 p v1)
(subst (LatticeFunc LA max) F2 p v2)).
unfold LatticeFunc, applyFunc, substFunc; simpl; intros.
case (positive_dec (proj1_sig p) p0); intros.
rewrite e; rewrite apply_modify_tree1.
rewrite apply_modify_tree1; auto.
rewrite apply_modify_tree2; auto.
rewrite apply_modify_tree2; auto.
Qed.
Lemma modify_increase :
forall (A:Set) (LA:Lattice A) (max:nat) (F : funcTree A max) (v : A->A)
(p : posInf max),
(order LA (apply (LatticeFunc LA max) F p) (v (apply (LatticeFunc LA max) F p))) ->
(order (LatticeFunc LA max) F (modify (LatticeFunc LA max) F p v)).
unfold LatticeFunc, applyFunc, substFunc; simpl; intros.
case (positive_dec (proj1_sig p) p0); intros.
rewrite e; rewrite apply_modify_tree1.
rewrite e in H; unfold apply_functree in H; apply H.
rewrite apply_modify_tree2; auto.
Qed.
Lemma subst_increase :
forall (A:Set) (LA:Lattice A) (max:nat) (F : funcTree A max) (v : A)
(p : posInf max),
(order LA (apply (LatticeFunc LA max) F p) v) ->
(order (LatticeFunc LA max) F (subst (LatticeFunc LA max) F p v)).
unfold LatticeFunc, applyFunc, substFunc; simpl; intros.
case (positive_dec (proj1_sig p) p0); intros.
rewrite e; rewrite apply_modify_tree1.
rewrite e in H; unfold apply_functree in H; apply H.
rewrite apply_modify_tree2; auto.
Qed.
Lemma apply_modify_eq1 :
forall (A:Set) (LA:Lattice A) (max:nat) (F : funcTree A max)
(x p : posInf max) (v : A -> A),
proj1_sig x = proj1_sig p ->
(apply (LatticeFunc LA max) (modify (LatticeFunc LA max) F x v) p) = (v (apply (LatticeFunc LA max) F p)).
intros; unfold LatticeFunc; simpl.
rewrite apply_modify1; auto.
Qed.
Lemma apply_modify_eq2 :
forall (A:Set) (LA:Lattice A) (max:nat) (F : funcTree A max)
(x p : posInf max) (v : A -> A),
~ proj1_sig x = proj1_sig p ->
(apply (LatticeFunc LA max) (modify (LatticeFunc LA max) F x v) p) = (apply (LatticeFunc LA max) F p).
intros; unfold LatticeFunc; simpl.
rewrite apply_modify2; auto.
Qed.
Lemma apply_subst_eq1 :
forall (A:Set) (LA:Lattice A) (max:nat) (F : funcTree A max)
(x p : posInf max) (v : A),
proj1_sig x = proj1_sig p ->
(apply (LatticeFunc LA max) (subst (LatticeFunc LA max) F x v) p) = v.
intros; unfold LatticeFunc; simpl.
rewrite apply_subst1; auto.
Qed.
Lemma apply_subst_eq2 :
forall (A:Set) (LA:Lattice A) (max:nat) (F : funcTree A max)
(x p : posInf max) (v : A),
~ proj1_sig x = proj1_sig p ->
(apply (LatticeFunc LA max) (subst (LatticeFunc LA max) F x v) p) = (apply (LatticeFunc LA max) F p).
intros; unfold LatticeFunc; simpl.
rewrite apply_subst2; auto.
Qed.
Definition xHposInf (max:nat) : posInf max.
intros; exists xH.
constructor.
Qed.
Opaque LatticeFunc.
Section functree'.
Variable A : Set.
Variable PA : Lattice A.
Variable max : nat.
Definition funcTree' := option (funcTree A max).
Inductive eq_funcTree' : funcTree' -> funcTree' -> Prop :=
eq_funcTree'_none : eq_funcTree' None None
| eq_funcTree'_some : forall f1 f2,
(eq (funcTree_Lattice A PA max) f1 f2) -> eq_funcTree' (Some f1) (Some f2).
Inductive order_funcTree' : funcTree' -> funcTree' -> Prop :=
order_funcTree'_none : forall f', order_funcTree' f' None
| order_funcTree'_some : forall f1 f2,
(order (funcTree_Lattice A PA max) f1 f2) -> order_funcTree' (Some f1) (Some f2).
Definition ArrayPoset : Poset funcTree'.
refine (poset_constr _
eq_funcTree' _ _ _ order_funcTree' _ _ _).
destruct x; constructor; auto.
intros x y H; inversion_clear H; constructor; auto.
intros x y z H; inversion_clear H; intros H1; inversion_clear H1; try constructor; auto.
apply eq_trans with f2; auto.
intros x y H; inversion_clear H; constructor; auto.
intros x y H; inversion_clear H; intros H1; inversion_clear H1; try constructor; auto.
intros x y z H; inversion_clear H; intros H1; inversion_clear H1; try constructor; auto.
apply order_trans with f2; auto.
Defined.
Definition ArrayLattice : Lattice funcTree'.
refine (let L:=(funcTree_Lattice A PA max) in
lattice_constr _ ArrayPoset
(fun f1' f2' => match f1',f2' with
Some f1,Some f2 => Some (join L f1 f2)
| _,_ => None
end) _ _ _ _ (Some (bottom L)) _ None _ _).
destruct x.
destruct y; constructor; auto.
constructor.
destruct x.
destruct y; constructor; auto.
constructor.
intros x y z H; inversion_clear H; intros H1; inversion_clear H1; constructor.
apply join_least_bound; auto.
destruct x.
destruct y.
case (order_dec L f f0); intros.
left; constructor; auto.
right; intros H; elim n; inversion_clear H; auto.
left; constructor.
destruct y.
right; intros H; inversion_clear H.
left; constructor.
destruct x; constructor; auto.
constructor.
intros x.
cut (Acc
(fun x0 y : funcTree' => ~ eq ArrayPoset y x0 /\ order ArrayPoset y x0)
None); intros.
destruct x; auto.
induction (acc_property L f).
clear H0; constructor; intros y (H0,H2).
inversion_clear H2 in H0; auto.
apply H1; intuition.
elim H0; constructor; auto.
constructor; intros y (H1,H2).
elim H1; inversion_clear H2; constructor.
Defined.
Definition applyArray : funcTree' -> posInf max -> A :=
fun f' => match f' with
None => fun _ => top PA
| Some f => fun p => (applyFunc A PA max f p)
end.
Lemma applyArray_monotone : forall f1 f2,
order ArrayLattice f1 f2 ->
forall p, order PA (applyArray f1 p) (applyArray f2 p).
intros.
inversion_clear H; simpl; auto.
unfold funcTree_Lattice in H0; simpl in H0.
unfold applyFunc, apply_functree.
apply H0.
Qed.
Definition modifyArray : funcTree' -> posInf max -> (A->A) -> funcTree' :=
fun f' p g => match f' with
None => None
| Some f => Some (modifyFunc A PA max f p g)
end.
Definition substArray : funcTree' -> posInf max -> A -> funcTree' :=
fun f' p v => match f' with
None => None
| Some f => Some (substFunc A PA max f p v)
end.
End functree'.
Implicit Arguments ArrayLattice [A].
Implicit Arguments applyArray [A max].
Implicit Arguments substArray [A max].
Implicit Arguments modifyArray [A max].
Lemma apply_modifyArray1 : forall A (LA:Lattice A) t x1 x2 v,
eq_word x2 x1 ->
order LA (v (applyArray LA t x2))
(applyArray LA (modifyArray LA t x1 v) x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, modifyFunc, apply_functree; simpl.
destruct x1; destruct x2; simpl in H; subst.
rewrite apply_modify_tree1; auto.
Qed.
Lemma apply_modifyArray2 : forall A (LA:Lattice A) t x1 x2 v,
~eq_word x2 x1 ->
(applyArray LA (modifyArray LA t x1 v) x2)=(applyArray LA t x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, modifyFunc, apply_functree; simpl.
rewrite apply_modify_tree2; auto.
destruct x1; destruct x2; red; intros; elim H; simpl in *; auto.
Qed.
Lemma apply_substArray1 : forall A (LA:Lattice A) t x1 x2 v,
eq_word x2 x1 ->
order LA v (applyArray LA (substArray LA t x1 v) x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, substFunc, apply_functree; simpl.
destruct x1; destruct x2; simpl in H; subst.
rewrite apply_modify_tree1; auto.
Qed.
Lemma apply_substArray2 : forall A (LA:Lattice A) t x1 x2 v,
~eq_word x2 x1 ->
(applyArray LA (substArray LA t x1 v) x2)=(applyArray LA t x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, substFunc, apply_functree; simpl.
rewrite apply_modify_tree2; auto.
destruct x1; destruct x2; red; intros; elim H; simpl in *; auto.
Qed.
Lemma applyArray_eq_word : forall A (LA:Lattice A) t (p1 p2:Word),
eq_word p1 p2 ->
(applyArray LA t p1)=(applyArray LA t p2).
unfold applyArray; intros.
destruct t; auto.
unfold applyFunc; intros.
destruct p1; destruct p2; simpl in H.
subst; auto.
Qed.
Index
This page has been generated by coqdoc