Library operationalSemantics

Require Export language.

Definition ZZeroMax v :=
match v with
| Zpos p => nat_of_P p
| _ => 0
end.

Inductive Opsem: State -> Command -> State -> Prop :=
  Skip_OS: forall s, Opsem s Skip s
| Seq_OS: forall s s' s'' C1 C2, Opsem s C1 s'' -> Opsem s'' C2 s' -> Opsem s (Seq C1 C2) s'
| AAssign_OS: forall s s' x v A a, AExp a = A -> (AEval a s) = Some v ->
         s' = (aUpdate s x v) -> Opsem s (Assign (ASkalVar x) A) s'
| BAssign_OS: forall s s' x v B b, BExp b = B -> (BEval b s) = Some v ->
         s' = (bUpdate s x v) -> Opsem s (Assign (BSkalVar x) B) s'
| HAssign_OS: forall s s' x v H h, HExp h = H -> (HEval h s) = Some v ->
         s' = (hUpdate s x v) -> Opsem s (Assign (HSkalVar x) H) s'
| Assert_OS: forall s B, (BEval B s) = Some true -> Opsem s (Assert B) s
| CondT_OS: forall s s' B C1 C2, (BEval B s) = Some true -> Opsem s C1 s' -> Opsem s (Cond B C1 C2) s'
| CondF_OS: forall s s' B C1 C2, (BEval B s) = Some false -> Opsem s C2 s' -> Opsem s (Cond B C1 C2) s'
| WhileF_OS: forall s B C, BEval B s = Some false -> Opsem s (While B C) s
| WhileT_OS: forall s s' s'' B C, BEval B s = Some true -> Opsem s C s' ->
    Opsem s' (While B C) s'' -> Opsem s (While B C) s''
| For_OS : forall M s q m C s' f v, AEval (SvarExpr m) s = Some v -> M = ZZeroMax v -> M > 0 ->
                    (forall (i:nat), (i<= M) -> Opsem ((aUpdate (f i) q (Z_of_nat (S i)))) C (f (S i))) ->
                     s' = aUpdate (f M) q (Z_of_nat (S M)) -> s = f 0 ->
                     Opsem s (For q m C) s'
| ForE_OS : forall s q m C, AEval (SvarExpr m) s = Some 0%Z -> Opsem s (For q m C) (aUpdate s q 1%Z).

Lemma increasingState : forall s C t x, Opsem s C t ->
 (exists v, lookup s x = Some v) -> (exists v', lookup t x= Some v').
intros.
induction H. destruct H0. exists x0. assumption.
apply IHOpsem2. apply IHOpsem1. apply H0.
subst. destruct H0. destruct s. destruct p. destruct x. simpl in H.
simpl.
remember (a0 a1). destruct o. inversion H. subst. clear H.
remember (beq_SkalVar (ASkalVar x0) (ASkalVar a1)). destruct b0. eexists. auto.
eexists. auto. inversion H.
simpl. simpl in H. remember (b b0). destruct o. eexists. auto. inversion H.

simpl in *. destruct (h h0). eauto. inv H.

subst. destruct H0. destruct s. destruct p. destruct x. simpl in H. simpl.
remember (a a0). destruct o. eexists. auto. inversion H.
simpl in *.
remember (b0 b1). destruct o. remember (beq_SkalVar (BSkalVar x0) (BSkalVar b1)).
destruct b3. eexists. auto. eexists. auto. inversion H.

simpl in *. destruct (h h0). eauto. inv H.

subst. destruct H0. destruct s. destruct p. destruct x; simpl in *.
destruct (a a0). eauto. inv H. destruct (b b0). eauto.
inv H. destruct (h0 h1). remember (beq_SkalVar (HSkalVar x0) (HSkalVar h1)).
destruct b0. eauto. eauto. inv H.

destruct H0. exists x0. apply H0. apply IHOpsem. apply H0.
apply IHOpsem. apply H0.

destruct H0. eexists. eauto.

apply IHOpsem2. apply IHOpsem1. assumption.

subst. destruct (ZZeroMax v). simpl in *. (destruct (f 0)). destruct p.
simpl in *. destruct H0. destruct x. simpl. remember (beq_SkalVar (ASkalVar q) (ASkalVar a0)).
destruct b0. eauto. simpl in H0. remember (a a0). destruct (o). eauto. inv H0.

simpl in *. destruct (b b0). eauto. inv H0.

simpl in *. destruct (h h0). eauto. inv H0.

simpl in *.
assert(
forall i : nat,
     i <= S n ->
     (exists v : Val, lookup (aUpdate (f 0) q (Z_of_nat (S 0))) x = Some v) ->
     exists v' : Val, lookup (f (S i)) x = Some v').
intros i. induction i; intros. auto.
destruct IHi. intuition. auto. apply H4. auto.
remember (f (S i)). destruct s. destruct p. simpl. destruct x. simpl in *.
remember (beq_SkalVar (ASkalVar q) (ASkalVar a0)). destruct b0. eauto.
destruct (a a0). eauto. inv H5. eauto. eauto. eauto.
clear H4. assert (exists v' : Val, lookup (f (S n)) x = Some v').
apply H1. auto. simpl. remember (beq_SkalVar (ASkalVar q) x). destruct b.
destruct x; inv Heqb. simpl. destruct (f 0). destruct p. simpl. rewrite <- H5.
eauto. destruct q. inv H5. destruct q; inv H5. rewrite lookupNeqa. apply H0.
auto.
clear H2. remember (beq_SkalVar (ASkalVar q) x). destruct b. destruct x.
destruct (f (S n)). destruct p. simpl. rewrite <- Heqb. eauto. destruct q; inv Heqb.
destruct q; inv Heqb. rewrite lookupNeqa. auto. auto.

destruct H0. destruct s. destruct p. simpl in *.
destruct x. simpl in *. remember (beq_SkalVar (ASkalVar q) (ASkalVar a0)).
destruct b0. eauto. destruct (a a0). eauto. inv H0. eauto. eauto.
Qed.