Library StackLattice
Require Export Lattice.
Require Import List.
Set Implicit Arguments.
Section StackLattice.
Variable A : Set.
Variable PA : Lattice A.
Inductive stack : Set :=
| bot_stack : stack
| top_stack : stack
| some_stack : list A -> stack.
Inductive orderS : stack -> stack -> Prop :=
| order_bot_stack : forall x : stack, orderS bot_stack x
| order_top_stack : forall x : stack, orderS x top_stack
| order_nil : orderS (some_stack nil) (some_stack nil)
| order_cons :
forall (x1 x2 : A) (l1 l2 : list A),
order PA x1 x2 ->
orderS (some_stack l1) (some_stack l2) ->
orderS (some_stack (x1 :: l1)) (some_stack (x2 :: l2)).
Inductive eqS : stack -> stack -> Prop :=
| eq_bot_stack : eqS bot_stack bot_stack
| eq_top_stack : eqS top_stack top_stack
| eq_nil : eqS (some_stack nil) (some_stack nil)
| eq_cons :
forall (x1 x2 : A) (l1 l2 : list A),
eq PA x1 x2 ->
eqS (some_stack l1) (some_stack l2) -> eqS (some_stack (x1 :: l1)) (some_stack (x2 :: l2)).
Fixpoint join_stack_list (l1 l2 : list A) {struct l2} : stack :=
match l1, l2 with
| nil, nil => some_stack nil
| x1 :: q1, x2 :: q2 =>
match join_stack_list q1 q2 with
| some_stack q => some_stack (join PA x1 x2 :: q)
| _ => top_stack
end
| _, _ => top_stack
end.
Definition joinS (l1 l2 : stack) :=
match l1, l2 with
| bot_stack, _ => l2
| top_stack, _ => top_stack
| _, bot_stack => l1
| _, top_stack => top_stack
| some_stack q1, some_stack q2 => join_stack_list q1 q2
end.
Definition orderS_refl : forall x y : stack, eqS x y -> orderS x y.
intros x y H; induction H; constructor; auto.
Qed.
Definition orderS_antisym :
forall x y : stack, orderS x y -> orderS y x -> eqS x y.
intros x y H1; induction H1; intros H2; inversion_clear H2; try constructor;
auto.
Qed.
Definition orderS_trans :
forall x y z : stack, orderS x y -> orderS y z -> orderS x z.
intros x y z H1; generalize z; clear z; induction H1; intros z H2;
inversion_clear H2; try constructor; auto.
apply order_trans with x2; auto.
Qed.
Definition eqS_refl : forall x : stack, eqS x x.
simple destruct x; try constructor.
induction l; constructor; auto.
Qed.
Definition eqS_sym : forall x y : stack, eqS x y -> eqS y x.
intros x y H; induction H; constructor; auto.
Qed.
Definition eqS_trans : forall x y z : stack, eqS x y -> eqS y z -> eqS x z.
intros x y z H1; generalize z; clear z; induction H1; intros z H2;
inversion_clear H2; try constructor; auto.
apply eq_trans with x2; auto.
Qed.
Definition joinS_bound1 : forall x y : stack, orderS x (joinS x y).
unfold joinS in |- *; simple destruct x; try constructor.
simple destruct y; try constructor.
induction l; constructor; auto.
induction l.
simple destruct l; simpl in |- *; constructor.
simple destruct l0; simpl in |- *; try constructor; auto.
intros s l1; generalize (IHl l1); intros.
inversion_clear H; constructor; auto.
constructor.
constructor; auto.
Qed.
Ltac CaseEqS a := generalize (refl_equal a); pattern a at -2 in |- *; case a.
Definition joinS_bound2 : forall x y : stack, orderS y (joinS x y).
unfold joinS in |- *; simple destruct x; try constructor.
intros; apply orderS_refl; apply eqS_refl.
simple destruct y; try constructor.
induction l; try constructor; auto.
induction l; simpl in |- *.
simpl in |- *; constructor.
constructor.
simple destruct l0; simpl in |- *; try constructor; auto.
intros s l1; generalize (IHl l1).
CaseEqS (join_stack_list l l1); intros.
inversion_clear H0.
constructor.
constructor; auto.
Qed.
Lemma join_stack_list_not_bot :
forall l1 l2 : list A, join_stack_list l1 l2 <> bot_stack.
induction l1; simple destruct l2; simpl in |- *; intuition.
discriminate H.
discriminate H.
discriminate H.
apply IHl1 with l.
generalize H; clear H.
case (join_stack_list l1 l); simpl in |- *; intuition.
discriminate H.
Qed.
Lemma orderS_length :
forall l1 l2 : list A, orderS (some_stack l1) (some_stack l2) -> length l1 = length l2.
induction l1; intros.
inversion_clear H; simpl in |- *; intuition.
inversion_clear H; simpl in |- *; intuition.
Qed.
Lemma join_stack_list_same_length :
forall l1 l2 : list A,
length l1 = length l2 -> exists l : list A, join_stack_list l1 l2 = some_stack l.
induction l1; simple destruct l2; simpl in |- *; intros.
exists (nil (A:=A)); auto.
discriminate H.
discriminate H.
elim (IHl1 l); intros.
exists (join PA a a0 :: x); rewrite H0; auto.
injection H; auto.
Qed.
Definition joinS_least_bound :
forall x y z : stack, orderS x z -> orderS y z -> orderS (joinS x y) z.
simple destruct x; simpl in |- *; try constructor; auto.
simple destruct y; auto.
induction l; try constructor; auto.
simple destruct l; simpl in |- *; try constructor; auto.
intros s l0 z H1; inversion_clear H1.
constructor.
intros H; inversion_clear H.
simple destruct l0; simpl in |- *; try constructor.
intros z H1; inversion_clear H1.
constructor.
intros H'; inversion_clear H'.
simple destruct z; intros.
inversion_clear H.
generalize (join_stack_list_not_bot l l1); generalize (IHl l1).
case (join_stack_list l l1); simpl in |- *; intros.
elim H2; auto.
constructor.
constructor.
generalize H0; clear H0; inversion_clear H; intros.
inversion_clear H2.
elim (join_stack_list_same_length l l1); intros.
rewrite H2; constructor; auto.
generalize (IHl l1 (some_stack l4)); rewrite H2; intros; auto.
rewrite (orderS_length H1).
rewrite (orderS_length H3); auto.
Qed.
Definition eqS_dec : forall x y : stack, {eqS x y} + {~ eqS x y}.
simple destruct x; simple destruct y;
try
(left; constructor) || (right; red in |- *; intro H; inversion H; fail).
induction l.
simple destruct l.
left; constructor.
right; intros H; inversion H.
simple destruct l0; intros.
right; intros H; inversion H.
case (eq_dec PA a a0); intros.
case (IHl l1); intros.
left; constructor; auto.
right; red in |- *; intros H; elim n; inversion_clear H; auto.
right; red in |- *; intros H; elim n; inversion_clear H; auto.
Qed.
Definition acc_property_top : Acc (fun x y => ~ eqS y x /\ orderS y x) top_stack.
constructor; intros y (H1, H2); generalize H1; clear H1; inversion_clear H2;
intros H1; try (elim H1; constructor).
Qed.
Definition R (l1 l2 : list A) :=
(fun x y => ~ eqS y x /\ orderS y x) (some_stack l1) (some_stack l2).
Lemma R_to_acc_orderS :
forall l : list A,
Acc R l -> Acc (fun x y => ~ eqS y x /\ orderS y x) (some_stack l).
intros l H; induction H; intros.
constructor; intros y (H1, H2).
generalize H0 H1; clear H0 H1; inversion_clear H2; intros.
apply acc_property_top.
elim H1; constructor.
apply H2.
unfold R in |- *; split; auto.
constructor; auto.
Qed.
Definition accR_property_some_stack : forall l : list A, Acc R l.
induction l.
constructor.
unfold R in |- *; intros y (H1, H2).
generalize H1; inversion_clear H2; intros.
elim H0; constructor.
generalize l IHl; clear IHl l.
induction (acc_property PA a).
generalize H0; clear H0 H; intros Hx l H.
generalize x Hx; clear x Hx.
induction H.
generalize H0; clear H0; intros Hl a Hx.
constructor.
intros y Hy.
unfold R in Hy.
decompose [and] Hy.
generalize H0; clear H0 Hy; inversion_clear H1; intros.
case (eq_dec PA a x2); intros.
apply Hl.
unfold R in |- *; split; auto.
red in |- *; intro; elim H1; constructor; auto.
intros y0 (H3, H4) l Hl'.
apply Hx; auto.
split.
red in |- *; intros; elim H3; apply eq_trans with a; auto.
apply order_trans with x2; auto.
apply Hx.
split; auto.
constructor; intros; apply H.
unfold R in H3; decompose [and] H3.
unfold R in |- *; split.
red in |- *; intros; elim H4.
apply orderS_antisym; auto.
apply orderS_trans with (some_stack x); auto.
apply orderS_refl.
apply eqS_sym; auto.
apply orderS_trans with (some_stack l2); auto.
Qed.
Definition acc_property_some_stack :
forall l : list A, Acc (fun x y => ~ eqS y x /\ orderS y x) (some_stack l).
intros; apply R_to_acc_orderS.
apply accR_property_some_stack.
Qed.
Definition acc_property_bot : Acc (fun x y => ~ eqS y x /\ orderS y x) bot_stack.
constructor; simple destruct y.
intros (H1, H2); elim H1; constructor.
intros; apply acc_property_top.
intros; apply acc_property_some_stack.
Qed.
Definition accS_property : well_founded (fun x y => ~ eqS y x /\ orderS y x).
unfold well_founded in |- *.
simple destruct a.
apply acc_property_bot.
apply acc_property_top.
apply acc_property_some_stack.
Qed.
Definition StackPoset : Poset stack.
exact (poset_constr _ eqS eqS_refl eqS_sym eqS_trans
orderS orderS_refl orderS_antisym orderS_trans).
Defined.
Definition StackLattice : Lattice stack.
refine
(lattice_constr _ StackPoset
joinS joinS_bound1 joinS_bound2 joinS_least_bound
_ bot_stack _ top_stack _ accS_property).
destruct x.
left; constructor.
destruct y.
right; intros H; inversion H.
left; constructor.
right; intros H; inversion H.
destruct y.
right; intros H; inversion H.
left; constructor.
generalize l0; clear l0.
induction l; destruct l0.
left; constructor.
right; intros H; inversion H.
right; intros H; inversion H.
case (order_dec PA a a0); intros.
case (IHl l0); intros.
left; constructor; auto.
right; intros H; elim n; inversion_clear H; auto.
right; intros H; elim n; inversion_clear H; auto.
constructor.
constructor.
Defined.
End StackLattice.
Index
This page has been generated by coqdoc