Library ArrayLat
Require Export PosInf.
Require Import Lattice.
Require Import TabTree.
Implicit Arguments leaf [A].
Implicit Arguments node [A].
Inductive height_inf (A:Set) : tree A -> nat -> Prop :=
| inf_leaf : forall (p:nat), (height_inf A leaf p)
| inf_node : forall (a:A) (tO tI:tree A) (p:nat),
(height_inf A tO p) ->
(height_inf A tI p) ->
(height_inf A (node a tO tI) (S p)).
Implicit Arguments height_inf [A].
Record funcTree (A:Set) (max:nat) : Set := funcTree_constr
{tr : tree A;
tr_bound : height_inf tr (S max)}.
Module ArrayPoset (L:Lattice) <: PosetSet.
Definition apply_tree := apply_tree L.Pos.set L.bottom.
Definition Feq (t1 t2 : tree L.Pos.set) : Prop :=
forall p : positive, L.Pos.eq (apply_tree t1 p) (apply_tree t2 p).
Fixpoint join_tree (t1 t2 : tree L.Pos.set) {struct t2} : tree L.Pos.set :=
match (physical_eq t1 t2) with
left _ => t1
| right _ =>
match t1, t2 with
| leaf, _ => t2
| _, leaf => t1
| node a1 tO1 tI1, node a2 tO2 tI2 =>
node (L.join a1 a2) (join_tree tO1 tO2) (join_tree tI1 tI2)
end
end.
Fixpoint inter_tree (t1 t2 : tree L.Pos.set) {struct t2} : tree L.Pos.set :=
match t1, t2 with
| leaf, _ => leaf
| _, leaf => leaf
| node a1 tO1 tI1, node a2 tO2 tI2 =>
node (L.inter a1 a2) (inter_tree tO1 tO2) (inter_tree tI1 tI2)
end.
Lemma join_tree_height_inf :
forall (t1 t2 : tree L.Pos.set) (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;
case physical_eq; intros; auto.
inversion_clear H in H0.
inversion_clear H0.
constructor; auto.
Qed.
Lemma inter_tree_height_inf :
forall (t1 t2 : tree L.Pos.set) (max:nat),
height_inf t1 max ->
height_inf t2 max ->
height_inf (inter_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 L.Pos.set) (p : positive),
(height_inf t (S max)) ->
~(inf_log p max) ->
(apply_tree t p) = L.bottom.
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 L.Pos.set max -> funcTree L.Pos.set max -> funcTree L.Pos.set 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 Finter :
forall (max:nat),
funcTree L.Pos.set max -> funcTree L.Pos.set max -> funcTree L.Pos.set max.
intros max f1 f2;
refine (funcTree_constr _ _ (inter_tree (tr _ _ f1) (tr _ _ f2)) _).
apply inter_tree_height_inf.
case f1; auto.
case f2; auto.
Defined.
Definition apply_functree (max:nat)
(f : funcTree L.Pos.set max) (p : positive) :=
apply_tree (tr _ _ f) p.
Definition Forder (f1 f2 : tree L.Pos.set) : Prop :=
forall p : positive, L.Pos.order (apply_tree f1 p) (apply_tree f2 p).
Definition Fbottom :
forall (max:nat), funcTree L.Pos.set max.
refine (fun max => funcTree_constr _ _ leaf _).
intros.
constructor.
Defined.
Lemma apply_bottom :
forall (max:nat) (p : positive),
apply_functree _ (Fbottom max) p = L.bottom.
unfold apply_functree, Fbottom in |- *; simpl in |- *; intros.
reflexivity.
Qed.
Lemma apply_join_tree :
forall (t1 t2 : tree L.Pos.set) (p : positive),
L.Pos.eq (apply_tree (join_tree t1 t2) p)
(L.join (apply_tree t1 p) (apply_tree t2 p)).
induction t1 as [| a t0 IHt0 t2 IHt2]; intros t; case t; simpl in |- *;
intros; case physical_eq; auto; intros.
discriminate e.
injection e; intros; subst.
auto.
case p; simpl in |- *; auto.
Qed.
Lemma apply_inter_tree :
forall (t1 t2 : tree L.Pos.set) (p : positive),
L.Pos.eq (apply_tree (inter_tree t1 t2) p)
(L.inter (apply_tree t1 p) (apply_tree t2 p)).
induction t1 as [| a t0 IHt0 t2 IHt2]; intros t; case t; simpl in |- *;
intros.
apply L.Pos.order_antisym; auto.
case p; simpl in |- *; auto.
case p; simpl in |- *; auto.
case p; simpl in |- *; auto.
Qed.
Definition Feq_bot_dec :
forall t1 : tree L.Pos.set,
{(forall p : positive, L.Pos.eq (apply_tree t1 p) L.bottom)} +
{~ (forall p : positive, L.Pos.eq (apply_tree t1 p) L.bottom)}.
induction t1 as [| a t0 IHt0 t2 IHt2]; simpl in |- *.
left; simpl in |- *; auto.
case (L.order_dec a L.bottom); 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.
Definition Feq_dec : forall t1 t2 : tree L.Pos.set, {Feq t1 t2} + {~ Feq t1 t2}.
induction t1 as [| a t0 IHt0 t2 IHt2]; intros t; case t; intros.
left; unfold Feq in |- *; auto.
case (L.eq_dec s L.bottom); intros.
case (Feq_bot_dec t0); intros.
case (Feq_bot_dec t1); intros.
left; unfold Feq in |- *; intros.
case p; simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; intros p;
generalize (H (xI p)); simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; intros p;
generalize (H (xO p)); simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; generalize (H 1%positive); auto.
case (L.eq_dec a L.bottom); intros.
case (Feq_bot_dec t0); intros.
case (Feq_bot_dec t2); intros.
left; unfold Feq in |- *; intros.
case p; simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; intros p;
generalize (H (xI p)); simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; intros p;
generalize (H (xO p)); simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; generalize (H 1%positive); auto.
case (L.eq_dec a s); intros.
case (IHt0 t1); intros.
case (IHt2 t3); intros.
left; unfold Feq in |- *; intros.
case p; simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; intros p;
generalize (H (xI p)); simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; intros p;
generalize (H (xO p)); simpl in |- *; auto.
right; unfold Feq in |- *; intros H; elim n; generalize (H 1%positive); auto.
Qed.
Definition Forder_dec : forall t1 t2 : tree L.Pos.set, {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 (L.order_dec a L.bottom); 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 (L.order_dec a s); 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 L.Pos.set -> Prop :=
| is_bottom_leaf : is_bottom leaf
| is_bottom_node :
forall (a :L.Pos.set) (t1 t2 : tree L.Pos.set),
L.Pos.eq a L.bottom ->
is_bottom t1 -> is_bottom t2 -> is_bottom (node a t1 t2).
Inductive order' : tree L.Pos.set -> tree L.Pos.set -> Prop :=
| order'_leaf : forall t : tree L.Pos.set, order' leaf t
| order'_node_leaf :
forall (a :L.Pos.set) (t1 t2 : tree L.Pos.set),
L.Pos.eq a L.bottom ->
is_bottom t1 -> is_bottom t2 -> order' (node a t1 t2) leaf
| order'_node_node :
forall (a b :L.Pos.set) (A1 A2 B1 B2 : tree L.Pos.set),
L.Pos.order a b ->
order' A1 B1 -> order' A2 B2 -> order' (node a A1 A2) (node b B1 B2).
Inductive eq' : tree L.Pos.set -> tree L.Pos.set -> Prop :=
| eq'_leaf : eq' leaf leaf
| eq'_leaf_node :
forall (b :L.Pos.set) (t1 t2 : tree L.Pos.set),
L.Pos.eq L.bottom b ->
is_bottom t1 -> is_bottom t2 -> eq' leaf (node b t1 t2)
| eq'_node_leaf :
forall (b :L.Pos.set) (t1 t2 : tree L.Pos.set),
L.Pos.eq L.bottom b ->
is_bottom t1 -> is_bottom t2 -> eq' (node b t1 t2) leaf
| eq'_node_node :
forall (a b :L.Pos.set) (A1 A2 B1 B2 : tree L.Pos.set),
L.Pos.eq 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 L.Pos.set, {is_bottom t} + {~ is_bottom t}.
induction t.
left; constructor; auto.
case (L.order_dec a L.bottom); 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 L.Pos.set, {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 (L.order_dec a L.bottom); 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 (L.order_dec a L.bottom); 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 (L.eq_dec 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 L.Pos.set, 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 L.Pos.set, 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 L.Pos.set, 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 L.Pos.set, 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.
Module MProp := Lattice_prop L.
Export MProp.
Lemma order'_is_bottom : forall t1 t2 : tree L.Pos.set, 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 L.bottom; auto.
Qed.
Lemma order'_is_bottom2 :
forall t1 t2 : tree L.Pos.set, 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 L.Pos.set, 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 L.Pos.set, 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 L.Pos.order_trans with L.bottom; auto.
apply order'_is_bottom; auto.
apply order'_is_bottom; auto.
intros H'.
inversion_clear H'.
constructor.
apply L.Pos.order_antisym; auto.
apply L.Pos.order_trans with b; auto.
apply order'_is_bottom2 with B1; auto.
apply order'_is_bottom2 with B2; auto.
constructor.
apply L.Pos.order_trans with b; auto.
apply IHt0 with B1; auto.
apply IHt2 with B2; auto.
Qed.
Definition R (max : nat) (t1 t2 : tree L.Pos.set) :=
height_inf t1 max /\ ~ eq' t2 t1 /\ order' t2 t1.
Lemma R_acc :
forall (max : nat) (t : tree L.Pos.set), 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.
destruct t as [|a t0 t1]; intros.
auto.
inversion_clear H0.
generalize t0 t1 H1 H2; clear H2 H1 t0 t1.
induction (L.acc_property 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 (L.eq_dec x0 s); intros.
case (eq'_dec x1 t); 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 t; auto.
intros; apply H4; auto.
decompose [and] H8; clear H8.
split.
red in |- *; intros; elim H13.
apply L.Pos.eq_trans with x0; auto.
apply L.Pos.order_trans with s; 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 L.Pos.eq_trans with x0; auto.
apply L.Pos.order_trans with s; 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 (L.acc_property s).
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 (L.eq_dec x1 s); 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 L.Pos.eq_trans with x1; auto.
apply L.Pos.order_trans with s; 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 L.Pos.eq_trans with x1; auto.
apply L.Pos.order_trans with s; auto.
apply H2; eauto.
Qed.
Lemma is_bottom_apply :
forall t : tree L.Pos.set,
is_bottom t ->
forall p : positive, L.Pos.eq L.bottom (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 L.Pos.set,
(forall p : positive, L.Pos.eq L.bottom (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 L.Pos.set, 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 L.Pos.eq_sym; apply is_bottom_apply; auto.
intros; apply L.Pos.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 L.Pos.set, 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 L.Pos.set),
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 L.Pos.set max).
refine
(fun max => (funcTree_constr _ _
(build_const_TabTree_rec _ L.top max) _)).
induction max; simpl; repeat (constructor; auto).
Defined.
Lemma topF_is_top : forall (max:nat) (t:tree L.Pos.set),
(height_inf t (S max)) ->
(Forder t (build_const_TabTree_rec _ L.top 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 funcTree' := option (funcTree L.Pos.set WordSize).
Inductive eq_funcTree' : funcTree' -> funcTree' -> Prop :=
eq_funcTree'_none : eq_funcTree' None None
| eq_funcTree'_some : forall f1 f2,
(Feq (tr _ _ f1) (tr _ _ 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,
(Forder (tr _ _ f1) (tr _ _ f2)) -> order_funcTree' (Some f1) (Some f2).
Definition set := funcTree'.
Definition eq : set -> set -> Prop := eq_funcTree'.
Lemma eq_refl : forall x : set, eq x x.
destruct x; constructor; auto.
unfold eq,Feq; intros; auto.
Qed.
Lemma eq_sym : forall x y : set, eq x y -> eq y x.
intros x y H; inversion_clear H; constructor; auto.
unfold eq,Feq; intros; auto.
Qed.
Lemma eq_trans' : forall x y z : (funcTree L.Pos.set WordSize),
Feq (tr _ _ x) (tr _ _ y) -> Feq (tr _ _ y) (tr _ _ z) -> Feq (tr _ _ x) (tr _ _ z).
unfold eq,Feq in |- *; intros; auto.
apply L.Pos.eq_trans with (apply_tree (tr _ _ y) p); auto.
Qed.
Lemma eq_trans : forall x y z : set, eq x y -> eq y z -> eq x z.
intros x y z H; inversion_clear H; intros H1; inversion_clear H1; try constructor; auto.
apply eq_trans' with f2; auto.
Qed.
Definition order : set -> set -> Prop := order_funcTree'.
Lemma order_refl : forall x y : set, eq x y -> order x y.
intros x y H; inversion_clear H; constructor; auto.
unfold eq,order,Feq, Forder in |- *; intros; auto.
Qed.
Lemma order_antisym : forall x y : set, order x y -> order y x -> eq x y.
intros x y H; inversion_clear H; intros H1; inversion_clear H1; try constructor; auto.
unfold eq,order,Feq, Forder in |- *; intros; auto.
Qed.
Lemma order_trans' : forall x y z : funcTree L.Pos.set WordSize,
Forder (tr _ _ x) (tr _ _ y) -> Forder (tr _ _ y) (tr _ _ z) -> Forder (tr _ _ x) (tr _ _ z).
unfold eq,order, Feq, Forder in |- *; intros; auto.
apply L.Pos.order_trans with (apply_tree (tr _ _ y) p); auto.
Qed.
Lemma order_trans : forall x y z : set, order x y -> order y z -> order x z.
intros x y z H; inversion_clear H; intros H1; inversion_clear H1; try constructor; auto.
apply order_trans' with f2; auto.
Qed.
End ArrayPoset.
Module ArrayLattice (L:Lattice) <: Lattice.
Module Pos := ArrayPoset L.
Export Pos.
Definition join :=
(fun f1' f2' => match f1',f2' with
Some f1,Some f2 => Some (Fjoin WordSize f1 f2)
| _,_ => None
end).
Definition bottom := Some (Fbottom WordSize).
Definition top : set := None.
Lemma join_bound1 : forall x y : set, order x (join x y).
destruct x; destruct y; simpl; constructor.
unfold join,Fjoin,order,Feq, Forder in |- *; intros; simpl; auto.
apply
L.Pos.order_trans
with (L.join (apply_tree (tr _ _ f) p) (apply_tree (tr _ _ f0) p));
auto.
unfold Fjoin in |- *; generalize (apply_join_tree (tr _ _ f) (tr _ _ f0));
auto.
Qed.
Lemma join_bound2 : forall x y : set, order y (join x y).
destruct x; destruct y; simpl; constructor.
unfold order,join,Fjoin,Feq, Forder in |- *; intros; auto.
apply
L.Pos.order_trans
with (L.join (apply_tree (tr _ _ f) p) (apply_tree (tr _ _ f0) p));
auto.
generalize (apply_join_tree (tr _ _ f) (tr _ _ f0));
auto.
Qed.
Lemma join_least_bound : forall x y z : set, order x z -> order y z -> order (join x y) z.
destruct x; destruct y; destruct z; simpl; intros H1 H2; try constructor; inversion_clear H1; inversion_clear H2.
unfold order,Fjoin, Feq, Forder; simpl; intros; auto.
unfold Forder in * |- *.
apply
L.Pos.order_trans
with (L.join (apply_tree (tr _ _ f) p) (apply_tree (tr _ _ f0) p)); auto.
generalize (apply_join_tree (tr _ _ f) (tr _ _ f0)); auto.
Qed.
Definition inter := fun x y : set =>
match x,y with
None , _ => y
| _ , None => x
| Some s1, Some s2 => Some (Finter WordSize s1 s2)
end.
Lemma inter_bound1 : forall (x y : set), order (inter x y) x.
intros x y; unfold inter.
destruct x; destruct y; simpl; constructor.
unfold inter,Finter,order,Feq, Forder in |- *; intros; simpl; auto.
apply
L.Pos.order_trans
with (L.inter (apply_tree (tr _ _ f) p) (apply_tree (tr _ _ f0) p));
auto.
unfold Finter in |- *; generalize (apply_inter_tree (tr _ _ f) (tr _ _ f0));
auto.
intro; auto.
Qed.
Lemma inter_bound2 : forall x y : set, order (inter x y) y.
intros x y; unfold inter.
destruct x; destruct y; simpl; constructor.
unfold order,inter,Feq, Forder in |- *; intros; auto.
apply
L.Pos.order_trans
with (L.inter (apply_tree (tr _ _ f) p) (apply_tree (tr _ _ f0) p));
auto.
generalize (apply_inter_tree (tr _ _ f) (tr _ _ f0));
auto.
intro; auto.
Qed.
Lemma inter_greater_bound : forall x y z : set, order z x -> order z y -> order z (inter x y).
intros x y; unfold inter; intros.
destruct x; destruct y; destruct z; simpl in *; try constructor; inversion_clear H; inversion_clear H0; auto.
unfold order,inter, Feq, Forder; simpl; intros; auto.
apply
L.Pos.order_trans
with (L.inter (apply_tree (tr _ _ f) p) (apply_tree (tr _ _ f0) p)); auto.
generalize (apply_inter_tree (tr _ _ f) (tr _ _ f0)); auto.
Qed.
Lemma order_dec : forall x y : set, {order x y} + {~ order x y}.
destruct y.
destruct x.
case (Forder_dec (tr _ _ f0) (tr _ _ f)); intros; unfold order.
left; constructor; auto.
right; intros H; elim n; inversion_clear H; auto.
right; intros H; inversion_clear H.
left; constructor.
Qed.
Lemma eq_dec : forall x y : set, {eq x y} + {~ eq x y}.
destruct y.
destruct x.
case (Feq_dec (tr _ _ f0) (tr _ _ f)); intros; unfold eq.
left; constructor; auto.
right; intros H; elim n; inversion_clear H; auto.
right; intros H; inversion_clear H.
destruct x.
right; intros H; inversion_clear H.
left; constructor.
Qed.
Lemma bottom_is_a_bottom : forall x : set, order bottom x.
destruct x; unfold bottom; constructor.
intros p.
generalize (apply_bottom WordSize p); unfold bottom,apply_functree in |- *; intros.
unfold Fbottom in H; simpl tr in H; simpl; auto.
Qed.
Lemma top_is_top : forall x : set, order x top.
unfold top; constructor.
Qed.
Lemma acc_property' :
well_founded (fun x y : funcTree L.Pos.set WordSize => ~ Feq (tr _ _ y) (tr _ _ x) /\ Forder (tr _ _ y) (tr _ _ x)).
intros y.
destruct y; simpl; intros.
generalize (R'_acc _ _ tr_bound0); intros.
generalize tr_bound0; clear tr_bound0.
induction H; intros.
constructor.
destruct y; simpl; intros.
apply H0.
intuition.
Qed.
Lemma acc_property : well_founded (fun x y => ~ eq y x /\ order y x).
intros x.
cut (Acc
(fun x0 y : set => ~ eq y x0 /\ order y x0)
None); intros.
destruct x; auto.
induction (acc_property' 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.
Qed.
Definition applyFunc (max:nat) :
forall (f : funcTree L.Pos.set max) (p : posInf max), L.Pos.set :=
fun t p =>
apply_functree max t (proj1_sig p).
Definition modify_tree := modify_tree L.Pos.set L.bottom.
Lemma height_inf_modify :
forall (t:tree L.Pos.set) (p:positive) (n:nat) (v:L.Pos.set->L.Pos.set),
(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 L.Pos.set max)
(p : posInf max) (v : L.Pos.set -> L.Pos.set), funcTree L.Pos.set 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 L.Pos.set max)
(x p : posInf max) (v : L.Pos.set -> L.Pos.set),
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 L.Pos.set max)
(x p : posInf max) (v : L.Pos.set -> L.Pos.set),
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 L.Pos.set max) (p : posInf max) (v : L.Pos.set) : funcTree L.Pos.set max :=
modifyFunc max f p (fun _ => v).
Lemma apply_subst1' :
forall (max:nat) (f : funcTree L.Pos.set max)
(x p : posInf max) (v : L.Pos.set),
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 L.Pos.set max)
(x p : posInf max) (v : L.Pos.set),
proj1_sig x <> proj1_sig p ->
applyFunc _ (substFunc _ f p v) x = (applyFunc _ f x).
intros; unfold substFunc; rewrite apply_modify2'; auto.
Qed.
Definition apply : set -> Word -> L.Pos.set :=
fun f' => match f' with
None => fun _ => L.top
| Some f => fun p => (applyFunc WordSize f p)
end.
Lemma apply_monotone : forall f1 f2,
order f1 f2 ->
forall p, L.Pos.order (apply f1 p) (apply f2 p).
intros.
inversion_clear H; simpl; auto.
unfold applyFunc, apply_functree.
apply H0.
Qed.
Definition modify : set -> Word -> (L.Pos.set->L.Pos.set) -> set :=
fun f' p g => match f' with
None => None
| Some f => Some (modifyFunc WordSize f p g)
end.
Definition subst : set -> Word -> L.Pos.set -> set :=
fun f' p v => match f' with
None => None
| Some f => Some (substFunc WordSize f p v)
end.
Lemma apply_modify1 : forall t x1 x2 v,
eq_word x2 x1 ->
L.Pos.order (v (apply t x2))
(apply (modify t x1 v) x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, modifyFunc, apply_functree, apply_tree, modify_tree; simpl.
destruct x1; destruct x2; simpl in H; subst.
simpl.
rewrite (apply_modify_tree1 _ L.bottom (tr _ WordSize f)); auto.
Qed.
Lemma apply_modify2 : forall t x1 x2 v,
~eq_word x2 x1 ->
(apply (modify t x1 v) x2)=(apply t x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, modifyFunc, apply_functree, apply_tree, modify_tree; simpl.
rewrite apply_modify_tree2; auto.
destruct x1; destruct x2; red; intros; elim H; simpl in *; auto.
Qed.
Lemma apply_subst1 : forall t x1 x2 v,
eq_word x2 x1 ->
L.Pos.order v (apply (subst t x1 v) x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, substFunc, apply_functree, apply_tree, modify_tree; simpl.
destruct x1; destruct x2; simpl in H; subst.
simpl.
unfold modify_tree.
rewrite apply_modify_tree1; auto.
Qed.
Lemma apply_subst2 : forall t x1 x2 v,
~eq_word x2 x1 ->
(apply (subst t x1 v) x2)=(apply t x2).
intros.
destruct t; simpl; auto.
unfold applyFunc, substFunc, apply_functree; simpl.
unfold modify_tree, apply_tree.
rewrite apply_modify_tree2; auto.
destruct x1; destruct x2; red; intros; elim H; simpl in *; auto.
Qed.
Lemma modify_monotone : forall t1 t2 x1 x2 v1 v2,
order t1 t2 ->
eq_word x1 x2 ->
(forall x1 x2, L.Pos.order x1 x2 -> L.Pos.order (v1 x1) (v2 x2)) ->
order (modify t1 x1 v1) (modify t2 x2 v2).
Proof.
intros.
inversion_clear H; simpl; constructor.
intros p.
unfold modifyFunc, apply_tree, modify_tree; simpl.
case (positive_dec (proj1_sig x1) p); intros.
rewrite e; rewrite apply_modify_tree1.
case (positive_dec (proj1_sig x2) p); intros.
rewrite e0; rewrite apply_modify_tree1; auto.
elim n; rewrite <- e.
destruct x1; destruct x2; simpl in *; auto.
case (positive_dec (proj1_sig x2) p); intros.
elim n; rewrite <- e.
destruct x1; destruct x2; simpl in *; auto.
rewrite apply_modify_tree2; auto.
rewrite apply_modify_tree2; auto.
Qed.
Lemma subst_monotone : forall t1 t2 x1 x2 v1 v2,
order t1 t2 ->
eq_word x1 x2 ->
L.Pos.order v1 v2 ->
order (subst t1 x1 v1) (subst t2 x2 v2).
Proof.
intros.
inversion_clear H; simpl; constructor.
intros p.
unfold substFunc, modifyFunc, apply_tree, modify_tree; simpl.
case (positive_dec (proj1_sig x1) p); intros.
rewrite e; rewrite apply_modify_tree1.
case (positive_dec (proj1_sig x2) p); intros.
rewrite e0; rewrite apply_modify_tree1; auto.
elim n; rewrite <- e.
destruct x1; destruct x2; simpl in *; auto.
case (positive_dec (proj1_sig x2) p); intros.
elim n; rewrite <- e.
destruct x1; destruct x2; simpl in *; auto.
rewrite apply_modify_tree2; auto.
rewrite apply_modify_tree2; auto.
Qed.
Lemma subst_eq : forall t1 t2 x1 x2 v1 v2,
eq t1 t2 ->
eq_word x1 x2 ->
L.Pos.eq v1 v2 ->
eq (subst t1 x1 v1) (subst t2 x2 v2).
Proof.
intros.
inversion_clear H; simpl; constructor.
intros p.
unfold substFunc, modifyFunc, apply_tree, modify_tree; simpl.
case (positive_dec (proj1_sig x1) p); intros.
rewrite e; rewrite apply_modify_tree1.
case (positive_dec (proj1_sig x2) p); intros.
rewrite e0; rewrite apply_modify_tree1; auto.
elim n; rewrite <- e.
destruct x1; destruct x2; simpl in *; auto.
case (positive_dec (proj1_sig x2) p); intros.
elim n; rewrite <- e.
destruct x1; destruct x2; simpl in *; auto.
rewrite apply_modify_tree2; auto.
rewrite apply_modify_tree2; auto.
Qed.
Lemma order_subst : forall t x v,
L.Pos.order (apply t x) v ->
order t (subst t x v).
intros; destruct t; simpl.
constructor.
intros p.
unfold applyFunc, substFunc, apply_functree, apply_tree, modify_tree; simpl.
unfold modify_tree.
case (positive_dec p (proj1_sig x)); intros.
subst; rewrite apply_modify_tree1.
apply H.
rewrite apply_modify_tree2; auto.
constructor.
Qed.
Lemma apply_eq_word : forall t (p1 p2:Word),
eq_word p1 p2 ->
(apply t p1)=(apply t p2).
unfold apply; intros.
destruct t; auto.
unfold applyFunc; intros.
destruct p1; destruct p2; simpl in H.
subst; auto.
Qed.
Hint Resolve apply_eq_word : eq_dat.
Lemma apply_eq : forall t1 t2 (p1 p2:Word),
eq t1 t2 ->
eq_word p1 p2 ->
L.Pos.eq (apply t1 p1) (apply t2 p2).
unfold apply; intros.
inversion_clear H; auto.
unfold applyFunc.
destruct p1; destruct p2; simpl in *.
subst.
unfold apply_functree.
apply H1.
Qed.
Coercion apply : set >-> Funclass.
End ArrayLattice.
Index
This page has been generated by coqdoc