Require Export ZArith List String.

Open Scope Z_scope.
Open Scope string_scope.

Inductive aexpr : Type :=
  avar (x:string) | aint (n:Z) | aplus (e1 e2 : aexpr).

Inductive bexpr : Type :=  blt (a1 a2 : aexpr).

Inductive instr : Type :=
  skip | assign (x:string)(e:aexpr) | sequence (i1 i2:instr)
| while (b:bexpr)(i:instr).

Definition env := list(string*Z).

Inductive a_eval : env -> aexpr -> Z -> Prop :=
  ae_int : forall r n, a_eval r (aint n) n
| ae_var1 : forall r x v, a_eval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' , x <> y -> a_eval r (avar x) v' ->
              a_eval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
              a_eval r e1 v1 -> a_eval r e2 v2 ->
              a_eval r (aplus e1 e2) (v1 + v2).

Theorem ex1 : a_eval (("x",2)::nil)(aplus (avar "x")(aint 4)) 6.
(* construct this proof. *)
Admitted.

Hint Resolve ae_int ae_var1 ae_var2 ae_plus.

Inductive b_eval : list(string*Z) -> bexpr -> bool -> Prop :=
| be_lt1 : forall r e1 e2 v1 v2,
            a_eval r e1 v1 -> a_eval r e2 v2 ->
            v1 < v2 -> b_eval r (blt e1 e2) true
| be_lt2 : forall r e1 e2 v1 v2,
            a_eval r e1 v1 -> a_eval r e2 v2 ->
            v2 <= v1 -> b_eval r (blt e1 e2) false.

Inductive s_update : list(string*Z)->string->Z->list(string*Z)->Prop :=
| s_up1 : forall r x v v', s_update ((x,v)::r) x v' ((x,v')::r)
| s_up2 : forall r r' x y v v', s_update r x v' r' ->
            x <> y -> s_update ((y,v)::r) x v' ((y,v)::r').

Inductive s_exec : list(string*Z)->instr->list(string*Z)->Prop :=
| SN1 : forall r, s_exec r skip r
| SN2 : forall r r' x e v,
   a_eval r e v -> s_update r x v r' -> s_exec r (assign x e) r'
| SN3 : forall r r' r'' i1 i2,
    s_exec r i1 r' -> s_exec r' i2 r'' ->
    s_exec r (sequence i1 i2) r''
| SN4 : forall r r' r'' b i,
    b_eval r b true -> s_exec r i r' -> 
    s_exec r' (while b i) r'' ->
    s_exec r (while b i) r''
| SN5 : forall r b i,
    b_eval r b false -> s_exec r (while b i) r.

Hint Resolve SN1 SN2 SN3 SN4 SN5.

Inductive sos_step : env->instr->instr->env->Prop :=
  SOS1 : forall r r' x e v,
   a_eval r e v -> s_update r x v r' ->
   sos_step r (assign x e) skip r'
| SOS2 : forall r i2, sos_step r (sequence skip i2) i2 r
| SOS3 : forall r r' i1 i1' i2,
               sos_step r i1 i1' r' ->
               sos_step r (sequence i1 i2)(sequence i1' i2) r'
| SOS4 :
     forall r b i, b_eval r b true ->
       sos_step r (while b i) (sequence i (while b i)) r
| SOS5 :
     forall r b i, b_eval r b false ->
       sos_step r (while b i) skip r.

Inductive sos_star : env->instr->instr->env->Prop :=
  SOS6 : forall r i, sos_star r i i r
| SOS7 : forall r r' r'' i i' i'',
             sos_step r i i' r' -> sos_star r' i' i'' r'' ->
             sos_star r i i'' r''.         

Hint Resolve SOS1 SOS2 SOS3 SOS5 SOS4 SOS6 SOS7.

Lemma sos_sequence_aux : forall r i is r',
  sos_star r i is r' -> is = skip ->
  forall i' i'' r'', sos_star r' i' i'' r'' ->
  sos_star r (sequence i i') i'' r''.
(* complete this proof. *)
Qed.

Lemma sn_imp_sos_star :
  forall r i r', s_exec r i r' -> sos_star r i skip r'.
(* complete this proof. *)
Qed.