Library StackAlgebraImplem_struct
Require Export AlgebraType.
Inductive gammaSum (V:Set) (g:(V->Value->Prop)) : list V -> (list Value) -> Prop :=
gammaSum_nil : gammaSum V g nil nil
| gammaSum_cons : forall X x L l,
g X x -> gammaSum V g L l -> gammaSum V g (X::L) (x::l).
Definition gammaStack (V:Set) (PV:Lattice V):
Gamma (PowPoset Value) PV ->
Gamma (PowPoset OperandStack) (StackLattice PV).
Proof.
intros V PV g.
refine (gamma_constr _ _
(fun s' => match s' with
bot_stack => fun _ => False
| some_stack s => fun l => gammaSum V g s l
| top_stack => fun _ => True
end) _).
intros b1 b2 H.
destruct b1; destruct b2; try (inversion H;fail) || (intros x H'; intuition; fail).
generalize dependent l0; induction l; intros l0 H.
destruct l0.
auto.
inversion H.
inversion H.
intros s.
destruct s; simpl; intros.
inversion H5.
inversion H5; constructor.
apply (gamma_monotone g a x2); auto.
apply (IHl _ H4); auto.
Defined.
Lemma no_gammaSum_cons_nil : forall V g a l,
~ gammaSum V g (a :: l) nil.
Proof.
red; intros.
inversion H.
Qed.
Lemma split_gammaSum_cons_cons : forall V g X L x l,
gammaSum V g (X :: L) (x :: l) ->
g X x /\ gammaSum V g L l.
Proof.
intros.
inversion H; auto.
Qed.
Definition StackAlgebra : forall (V:Set) (PV:Lattice V),
Stack.Connect PV.
Proof.
intros.
refine (Stack.Build_Connect
(gammaStack _ PV) _
(some_stack nil) _
(fun l =>
match l with
| bot_stack => bot_stack _
| top_stack => top_stack _
| some_stack l0 => match l0 with
| nil => bot_stack _
| _ :: q => some_stack q
end
end) _
(fun l =>
match l with
| bot_stack => bottom PV
| top_stack => top PV
| some_stack l0 => match l0 with
| nil => bottom PV
| a :: _ => a
end
end) _
(fun v l =>
match l with
| bot_stack => bot_stack _
| top_stack => top_stack _
| some_stack l0 => some_stack (v::l0)
end) _).
intros g1 g2 H1 S s.
destruct S; simpl; auto.
generalize dependent s.
induction l; destruct s; simpl; intros; try constructor.
inversion_clear H.
elim (no_gammaSum_cons_nil _ _ _ _ H).
elim (split_gammaSum_cons_cons _ _ _ _ _ _ H); intros.
apply H1; auto.
elim (split_gammaSum_cons_cons _ _ _ _ _ _ H); intros.
apply IHl; auto.
intros g s H; subst; simpl; constructor.
intros g S s H.
inversion_clear H.
inversion_clear H0 in H1.
destruct S; simpl; simpl in H1; auto.
destruct l; simpl in H1.
inversion H1.
elim (split_gammaSum_cons_cons _ _ _ _ _ _ H1); intros; auto.
intros g S s H.
inversion_clear H.
inversion_clear H0 in H1.
destruct S; simpl; simpl in H1; auto.
inversion H1.
apply (gamma_top g (fun _ => True)); auto.
inversion_clear H1; auto.
intros g v S s H.
inversion_clear H.
inversion_clear H0 in H1 H2.
destruct S; simpl; simpl in H2; auto.
constructor; auto.
Defined.
Implicit Arguments StackAlgebra [V].
Index
This page has been generated by coqdoc