Require Lattice.
Require PolyList.
Section StackLattice.
Variable A:Set.
Variable PA:(Lattice A).
Inductive stack : Set :=
| bot : stack
| top : stack
| some : (list A) -> stack.
Inductive orderS : stack -> stack -> Prop :=
| order_bot : (x:stack) (orderS bot x)
| order_top : (x:stack) (orderS x top)
| order_nil : (orderS (some (nil ?)) (some (nil ?)))
| order_cons : (x1,x2:A;l1,l2:(list A))
(order PA x1 x2) -> (orderS (some l1) (some l2)) ->
(orderS (some (cons x1 l1)) (some (cons x2 l2))).
Inductive eqS : stack -> stack -> Prop :=
| eq_bot : (eqS bot bot)
| eq_top : (eqS top top)
| eq_nil : (eqS (some (nil ?)) (some (nil ?)))
| eq_cons : (x1,x2:A;l1,l2:(list A))
(eq PA x1 x2) -> (eqS (some l1) (some l2)) ->
(eqS (some (cons x1 l1)) (some (cons x2 l2))).
Fixpoint join_stack_list [l1,l2:(list A)] : stack :=
Cases l1 l2 of
nil nil => (some (nil A))
| (cons x1 q1) (cons x2 q2) =>
Cases (join_stack_list q1 q2) of
| (some q) => (some (cons (join PA x1 x2) q))
| _ => top
end
| _ _ => top
end.
Definition joinS := [l1,l2:stack]
Cases l1 l2 of
bot _ => l2
| top _ => top
| _ bot => l1
| _ top => top
| (some q1) (some q2) => (join_stack_list q1 q2)
end.
Definition orderS_refl : (x,y:stack) (eqS x y) -> (orderS x y).
Intros x y H; NewInduction H; Constructor; Auto.
Qed.
Definition orderS_antisym : (x,y:stack) (orderS x y) -> (orderS y x) -> (eqS x y).
Intros x y H1; NewInduction H1; Intros H2; Inversion_clear H2; Try Constructor; Auto.
Qed.
Definition orderS_trans : (x,y,z:stack) (orderS x y) -> (orderS y z) -> (orderS x z).
Intros x y z H1; Generalize z; Clear z;
NewInduction H1; Intros z H2; Inversion_clear H2; Try Constructor; Auto.
Apply order_trans with x2; Auto.
Qed.
Definition eqS_refl : (x:stack) (eqS x x).
Destruct x; Try Constructor.
NewInduction l; Constructor; Auto.
Qed.
Definition eqS_sym : (x,y:stack) (eqS x y) -> (eqS y x).
Intros x y H; NewInduction H; Constructor; Auto.
Qed.
Definition eqS_trans : (x,y,z:stack) (eqS x y) -> (eqS y z) -> (eqS x z).
Intros x y z H1; Generalize z; Clear z;
NewInduction H1; Intros z H2; Inversion_clear H2; Try Constructor; Auto.
Apply eq_trans with x2; Auto.
Qed.
Definition joinS_bound1 : (x,y:stack) (orderS x (joinS x y)).
Unfold joinS; Destruct x; Try Constructor.
Destruct y; Try Constructor.
NewInduction l; Constructor; Auto.
NewInduction l.
Destruct l; Simpl; Constructor.
Destruct l0; Simpl; Try Constructor; Auto.
Intros s l1; Generalize (IHl l1); Intros.
Inversion_clear H; Constructor; Auto.
Constructor.
Constructor; Auto.
Qed.
Tactic Definition CaseEqS a :=
Generalize (refl_equal ? a); Pattern -2 a; Case a.
Definition joinS_bound2 : (x,y:stack) (orderS y (joinS x y)).
Unfold joinS; Destruct x; Try Constructor.
Intros; Apply orderS_refl; Apply eqS_refl.
Destruct y; Try Constructor.
NewInduction l; Try Constructor; Auto.
NewInduction l; Simpl.
Simpl; Constructor.
Constructor.
Destruct l0; Simpl; 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 : (l1,l2:(list A))
~(join_stack_list l1 l2)=bot.
NewInduction l1; Destruct l2; Simpl; Intuition.
Discriminate H.
Discriminate H.
Discriminate H.
Apply IHl1 with l.
Generalize H; Clear H.
Case (join_stack_list l1 l); Simpl; Intuition.
Discriminate H.
Qed.
Lemma orderS_length : (l1,l2:(list A))
(orderS (some l1) (some l2)) -> (length l1)=(length l2).
NewInduction l1; Intros.
Inversion_clear H; Simpl; Intuition.
Inversion_clear H; Simpl; Intuition.
Qed.
Lemma join_stack_list_same_length : (l1,l2:(list A))
(length l1)=(length l2) ->
(EX l:(list A) | (join_stack_list l1 l2)=(some l)).
NewInduction l1; Destruct l2; Simpl; Intros.
Exists (nil A); Auto.
Discriminate H.
Discriminate H.
Elim (IHl1 l); Intros.
Exists (cons (Lattice.join PA a a0) x); Rewrite H0; Auto.
Injection H; Auto.
Qed.
Definition joinS_least_bound : (x,y,z:stack)
(orderS x z) -> (orderS y z) -> (orderS (joinS x y) z).
Destruct x; Simpl; Try Constructor; Auto.
Destruct y; Auto.
NewInduction l; Try Constructor; Auto.
Destruct l; Simpl; Try Constructor; Auto.
Intros s l0 z H1; Inversion_clear H1.
Constructor.
Intros H; Inversion_clear H.
Destruct l0; Simpl; Try Constructor.
Intros z H1; Inversion_clear H1.
Constructor.
Intros H'; Inversion_clear H'.
Destruct z; Intros.
Inversion_clear H.
Generalize (join_stack_list_not_bot l l1); Generalize (IHl l1).
Case (join_stack_list l l1); Simpl; 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 l4)); Rewrite H2; Intros; Auto.
Rewrite (orderS_length ? ? H1).
Rewrite (orderS_length ? ? H3); Auto.
Qed.
Definition eqS_dec : (x,y:stack){(eqS x y)}+{~(eqS x y)}.
Destruct x; Destruct y; Try (Left; Constructor) Orelse (Right; Red; Intro H; Inversion H; Fail).
NewInduction l.
Destruct l.
Left; Constructor.
Right; Intros H; Inversion H.
Destruct l0; Intros.
Right; Intros H; Inversion H.
Case (eq_dec PA a a0); Intros.
Case (IHl l1); Intros.
Left; Constructor; Auto.
Right; Red; Intros H; Elim n; Inversion_clear H; Auto.
Right; Red; Intros H; Elim n; Inversion_clear H; Auto.
Qed.
Definition acc_property_top : (Acc stack ([x,y] ~(eqS y x)/\(orderS y x)) top).
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)](([x,y] ~(eqS y x)/\(orderS y x)) (some l1) (some l2)).
Lemma R_to_acc_orderS : (l:(list A)) (Acc ? R l) ->
(Acc stack ([x,y] ~(eqS y x)/\(orderS y x)) (some l)).
Intros l H; NewInduction 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; Split; Auto.
Constructor; Auto.
Qed.
Definition accR_property_some : (l:(list A)) (Acc ? R l).
NewInduction l.
Constructor.
Unfold R; Intros y (H1,H2).
Generalize H1; Inversion_clear H2; Intros.
Elim H0; Constructor.
Generalize l IHl; Clear IHl l.
NewInduction (acc_property PA a).
Clear H; Intros Hx l H.
Generalize x Hx; Clear x Hx.
NewInduction H.
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 (Lattice.eq_dec PA a x2); Intros.
Apply Hl.
Unfold R; Split; Auto.
Red; Intro; Elim H1; Constructor; Auto.
Intros y0 (H3,H4) l Hl'.
Apply Hx; Auto.
Split.
Red; Intros; Elim H3; Apply Lattice.eq_trans with a; Auto.
Apply Lattice.order_trans with x2; Auto.
Apply Hx.
Split; Auto.
Constructor; Intros; Apply H.
Unfold R in H3; Decompose [and] H3.
Unfold R; Split.
Red; Intros; Elim H4.
Apply orderS_antisym; Auto.
Apply orderS_trans with (some x); Auto.
Apply orderS_refl.
Apply eqS_sym; Auto.
Apply orderS_trans with (some l2); Auto.
Qed.
Definition acc_property_some : (l:(list A))
(Acc stack ([x,y] ~(eqS y x)/\(orderS y x)) (some l)).
Intros; Apply R_to_acc_orderS.
Apply accR_property_some.
Qed.
Definition acc_property_bot : (Acc stack ([x,y] ~(eqS y x)/\(orderS y x)) bot).
Constructor; Destruct y.
Intros (H1,H2); Elim H1; Constructor.
Intros; Apply acc_property_top.
Intros; Apply acc_property_some.
Qed.
Definition accS_property : (well_founded stack ([x,y] ~(eqS y x)/\(orderS y x))).
Unfold well_founded.
Destruct a.
Apply acc_property_bot.
Apply acc_property_top.
Apply acc_property_some.
Qed.
Definition StackLattice : (Lattice stack).
Refine (poset_constr ? orderS eqS joinS
orderS_refl orderS_antisym orderS_trans
eqS_refl eqS_sym eqS_trans
joinS_bound1 joinS_bound2 joinS_least_bound
eqS_dec bot ? top ? accS_property).
Constructor.
Constructor.
Defined.
Definition AbPush := [x:A;l:stack]
Cases l of
bot => bot
| top => top
| (some q) => (some (cons x q))
end.
Definition AbTop := [l:stack]
Cases l of
bot => (bottom PA)
| top => (Lattice.top PA)
| (some nil) => (Lattice.top PA)
| (some (cons a _)) => a
end.
Definition AbPop := [l:stack]
Cases l of
bot => bot
| top => top
| (some nil) => top
| (some (cons _ q)) => (some q)
end.
Lemma AbPush_monotone : (x1,x2:A;s1,s2:stack)
(order PA x1 x2) ->
(order StackLattice s1 s2) ->
(order StackLattice (AbPush x1 s1) (AbPush x2 s2)).
Intros x1 x2 s1 s2 H H1; Unfold AbPush.
Inversion_clear H1; Constructor; Auto.
Constructor.
Constructor; Auto.
Qed.
Lemma AbTop_monotone : (s1,s2:stack)
(order StackLattice s1 s2) ->
(order PA (AbTop s1) (AbTop s2)).
Intros s1 s2 H; Unfold AbTop.
Inversion_clear H; Auto.
Qed.
Lemma AbPop_monotone : (s1,s2:stack)
(order StackLattice s1 s2) ->
(order StackLattice (AbPop s1) (AbPop s2)).
Intros s1 S2 H; Unfold AbPop.
Inversion_clear H; Try Constructor; Auto.
Qed.
End StackLattice.
Implicits AbPush [1].
Implicits AbTop [1].
Implicits AbPop [1].
Implicits AbPush_monotone [1].
Implicits AbPop_monotone [1].
Implicits AbTop_monotone [1].