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. *)
Qed.

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.

Theorem update_eval :
  forall r x v r', s_update r x v r' -> a_eval r' (avar x) v.
Proof.
(* Do this proof. *)
Qed.

Theorem a_eval_det :
  forall r e v, a_eval r e v -> forall v', a_eval r e v' -> v = v'.
Proof.
(* Do this proof. *)
Qed.

(* What we want to do here, is to show that some program transformations
can be made without changing the behavior of programs.  The first
thing we can do, is to model the operation of replacing occurrences
of some fragment by some other fragment. *)

Inductive subst (pat target: instr) : instr -> instr -> Prop :=
  sc1 : subst pat target pat target
| sc2 : forall i, subst pat target i i
| sc3 : forall i1 i2 i3 i4,
    subst pat target i1 i3 -> subst pat target i2 i4 ->
    subst pat target (sequence i1 i2) (sequence i3 i4)
| sc4 : forall b i1 i2, subst pat target i1 i2 ->
        subst pat target (while b i1) (while b i2).

(* If we replace a fragment by another that always has the same
  behavior, then the whole program's behavior is unchanged. *)

Theorem subst_equiv :
  forall p t,
   (forall rs rs', s_exec rs p rs' -> s_exec rs t rs') ->
  forall r r' i, 
     s_exec r i r' -> forall i', subst p t i i' -> s_exec r i' r'.
(* Do this proof. *)
Qed.

(* You will need the following lemma. *)

Lemma arith_fact :  ~1 <= 0.
intro; omega.
Qed.

Theorem ex_transformation :
   forall x i r r',
     s_exec r (sequence (assign x (aint 1))
                   (while (blt (aint 0)(avar x)) i)) r' ->
     s_exec r (sequence (assign x (aint 1))
                   (sequence i (while (blt (aint 0) (avar x)) i))) r'.
Proof.
 (* Do this proof. *)
Qed.