Require Import ZArith List String.
Open Scope Z_scope.
Open Scope string_scope
.
(* This is an example where one uses inductive types and predicates
  to define a small programming language. *)

(* The type of arithmetic expressions. *)

Inductive aexpr : Type := 
  avar (s : string) | anum (n :Z) | aplus (e1 e2:aexpr) | amult (e1 e2:aexpr).

(* The type of boolean expression. *)

Inductive bexpr : Type :=  blt (e1 e2 : aexpr) | bconj (b1 b2 : bexpr).

(* The type of instructions. *)

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

Definition env := list(string*Z).

(* aeval r e v means that in the state r, the expression e has value v *)

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

Hint Resolve ae_int ae_var1 ae_var2 ae_plus ae_mult.

(* beval r e v, has the same meaning as aeval r e v, but for boolean
   expressions and boolean values. *)

Inductive beval : env -> bexpr -> bool -> Prop :=
| be_lt1 : forall r e1 e2 v1 v2,
            aeval r e1 v1 -> aeval r e2 v2 ->
            v1 < v2 -> beval r (blt e1 e2) true
| be_lt2 : forall r e1 e2 v1 v2,
            aeval r e1 v1 -> aeval r e2 v2 ->
            v2 <= v1 -> beval r (blt e1 e2) false
| be_cj1 : forall r b1 b2, beval r b1 false ->
              beval r (bconj b1 b2) false
| be_cj2 : forall r b1 b2 v, beval r b1 true -> beval r b2 v ->
              beval r (bconj b1 b2) v.
        
(* s_update r x v r' means that r' is the same environment except that the
   value of x is changed to v *)

Inductive s_update : env->string->Z->env->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').

(* exec r i r' means that the execution of the instruction i from the
   state r will work normally, terminate, and return the value r'. *)

Inductive exec : env->instr->env->Prop :=
| SN1 : forall r, exec r skip r
| SN2 : forall r r' x e v, aeval r e v -> s_update r x v r' ->
    exec r (assign x e) r'
| SN3 : forall r r' r'' i1 i2,
    exec r i1 r' -> exec r' i2 r'' -> exec r (sequence i1 i2) r''
| SN4 : forall r r' r'' b i,
    beval r b true -> exec r i r' -> exec r' (while b i) r'' -> 
    exec r (while b i) r''
| SN5 : forall r b i,
    beval r b false -> exec r (while b i) r
| SN6 : forall r r' b i1 i2,
    beval r b true -> exec r i1 r' -> exec r (if_i b i1 i2) r'
| SN7 : forall r r' b i1 i2,
    beval r b false -> exec r i2 r' -> exec r (if_i b i1 i2) r'.

Hint Resolve be_lt1 be_lt2 be_cj1 be_cj2 s_up1 s_up2 SN1 SN2 SN3
  SN4 SN5 SN6 SN7.

Fixpoint lookup (r:env)(name:string){struct r} : option Z :=
  match r with
    nil => None
  | (a,b)::tl => if (string_dec a name) then Some b else lookup tl name
  end.

Definition bind (A B:Type)(v:option A)(f:A->option B) :
     option B :=
  match v with Some x => f x | None => None end.
Implicit Arguments bind.

Fixpoint af (r:env)(e:aexpr) {struct e}: option Z :=
  match e with
    avar index => lookup r index
  | anum n => Some n
  | aplus e1 e2 =>
     bind (af r e1)
     (fun v1 => bind (af r e2) (fun v2 => Some (v1+v2)))
  | amult e1 e2 =>
     bind (af r e1)
     (fun v1 => bind (af r e2) (fun v2 => Some (v1*v2)))
   end.

Fixpoint bf (r:env)(b:bexpr) {struct b} : option bool :=
  match b with
    blt e1 e2 =>
    bind (af r e1)
      (fun v1 => bind (af r e2) 
        (fun v2 => 
         if Zlt_bool v1 v2 then Some true else Some false))
  | bconj b1 b2 =>
    bind (bf r b1)
      (fun v1 => if v1 then bf r b2 else Some false)
  end.

Fixpoint uf (r:env)(x:string)(n:Z){struct r} : option(env) := 
    match r with
      nil => None
    | (y,n')::tl => 
      if string_dec y x then
        Some((x,n)::tl)
      else
        bind (uf tl x n) (fun tl' => Some ((y,n')::tl'))
    end.

Lemma aeval_lookup :
  forall r e n, aeval r e n -> 
    forall name, e = avar name -> lookup r name = Some n.
Proof.
 intros r e n H; elim H; simpl.
 intros; discriminate.
 intros r0 x v name Heq; injection Heq; intros; subst.
 destruct (string_dec name name); intuition auto.
 intros r0 x y v v' Hneq Hev Hrec name Heq;
  injection Heq; intros; subst.
  destruct (string_dec y name); auto.
  intros; elim Hneq; auto.
 intros; discriminate.
 intros; discriminate.
Qed.

(* Proving that the relation aeval is well described by the function af. *)
Lemma aeval_f :
  forall r e n, aeval r e n -> af r e = Some n.
Proof.
 induction 1; simpl; auto.
 destruct (string_dec x x); intuition.
 destruct (string_dec y x); auto.
 elim H; auto.
 rewrite IHaeval1; simpl; rewrite IHaeval2; simpl; auto.
 rewrite IHaeval1; simpl; rewrite IHaeval2; simpl; auto.
Qed.

(* Proving that the relation beval is well described by the function bf. *)
Lemma beval_f :
  forall r e b, beval r e b -> bf r e = Some b.
Proof.
  induction 1; simpl; try (
  rewrite aeval_f with (1:= H);
  rewrite aeval_f with (1:= H0);simpl;
  generalize (Zlt_cases v1 v2); case (Zlt_bool v1 v2); auto;
  intros H'; assert False by omega; contradiction).
  rewrite IHbeval; simpl; auto.
  rewrite IHbeval1; simpl; auto.
Qed.

Lemma s_update_f :
  forall r x v r', s_update r x v r' -> uf r x v = Some r'.
Proof.
 induction 1; simpl.
 case (string_dec x x); intuition.
 case (string_dec y x); intuition.
 assert False ; auto; intuition.
 rewrite IHs_update; auto.
Qed.

Lemma lookup_aeval :
  forall r x v, lookup r x = Some v -> aeval r (avar x) v.
Proof with auto.
  induction r; intros x v.
  simpl; intros; discriminate.
  destruct a as [y n]; simpl; case (string_dec y x)...
  intros Heq Heq2; injection Heq2; intros; subst...
Qed.

Hint Resolve lookup_aeval.

Ltac find_deep_bind a :=
  match a with
    bind ?a _ => find_deep_bind a
  | _ => a
  end.

Ltac unbind_hyp H v Heq :=
  match type of H with
  |  bind ?a ?b = Some _ => 
     let c := find_deep_bind a in
     (case_eq c; [intros v Heq | intros Heq]; rewrite Heq in H;
     [simpl in H | discriminate H])
  end.

Lemma af_eval :
  forall r e v, af r e = Some v -> aeval r e v.
Proof with eauto.
  induction e; intros v...
  simpl; intros Heq; injection Heq; intros; subst...
  simpl; case_eq (af r e2); case_eq (af r e1); try (intros;discriminate).
  intros v1 Heq1 v2 Heq2 Heq; injection Heq; intros; subst...
  simpl; case_eq (af r e2); case_eq (af r e1); try (intros;discriminate).
  intros v1 Heq1 v2 Heq2 Heq; injection Heq; intros; subst...
Qed.

Hint Resolve af_eval Zge_le.

Lemma bf_eval :
  forall r e v, bf r e = Some v -> beval r e v.
Proof with eauto with zarith.
  intros r b; induction b; simpl.
  case_eq (af r e1); case_eq (af r e2); try (intros; discriminate).
  intros v1 Heq1 v2 Heq2; unfold bind.
  generalize (Zlt_cases v2 v1); destruct (Zlt_bool v2 v1);
  intros comp v Heq; injection Heq; intros; subst v...
  case_eq (bf r b2); case_eq (bf r b1); try (intros; discriminate).
  intros v1 Heq1 v2 Heq2; unfold bind.
  destruct v1; intros v Heq; injection Heq; intro; subst v; simpl...
  intros [|]; try (intros; discriminate); intros Hb1 _ v Heq; 
   injection Heq; intro; subst v; simpl...
Qed.

Lemma uf_s :
  forall r x v r', uf r x v = Some r' ->
  s_update r x v r'.
Proof with eauto.
  induction r.
  simpl; intros; discriminate.
  destruct a as (y,n); simpl; intros x v r'.
  case (string_dec y x).
    intros Heq1 Heq2; injection Heq2; intros; subst; auto.

    case_eq (uf r x v); try(intros; discriminate).
    intros r'' Heqr'' Hn Heq; injection Heq; intros; subst r'; auto.
Qed.

Hint Resolve bf_eval uf_s.


(* The following exercise consists in proving that a certain program
  transformation preserves the meaning of programs. *)

(* You should erase the proofs that are already done and redo them. *)

Fixpoint tf1 (i1 i2 : instr) {struct i1} : instr :=
  match i1 with
    sequence i i' => tf1 i (tf1 i' i2)
  | _ => sequence i1 i2
  end.

Fixpoint tf2 (i :instr) : instr :=
  match i with sequence i' i'' => tf1 i' (tf2 i'') | _ => i end.

(* we would like to prove that for any instruction i, executing
  i is equivalent to executing (tf2 i).  This requires two implications,
  but only the first one is easy. *)

Lemma tf1_complete :
  forall r i r', exec r i r' -> forall i' r'', exec r' i' r'' ->
     exec r (tf1 i i') r''.
Proof.
induction 1; simpl; intros i'2 r''2; 
 try match goal with |- exec ?r3 _ _ -> exec _ _ _ =>
     intros Hex; apply SN3 with r3; eauto
 end.
 intros Hex; auto.
Qed.

Lemma tf2_complete :
  forall r i r', exec r i r' -> exec r (tf2 i) r'.
Proof.
induction 1; simpl; eauto.
eapply tf1_complete; eauto.
Qed.

(* The following exercise is to show that the proofs of execution of
  instructions can be performed by a function. *)

Fixpoint exf (r : env) (i:instr) (n:nat) {struct n} : option env :=
  match n with 
    0%nat => None 
  | S p => 
    match i with
      skip => Some r
    | assign x e => bind (af r e) (fun v => uf r x v)
    | sequence i1 i2 => bind (exf r i1 p) (fun r' => exf r' i2 p)
    | if_i b i1 i2 =>
      bind (bf r b) (fun v => if v then exf r i1 p else exf r i2 p)
    | while b i' =>
      bind (bf r b) 
        (fun v => if v then bind (exf r i' p)(fun r' => exf r' i p)
                  else Some r)
    end
  end.

Lemma exf_sound :
  forall r i r', exec r i r' ->
    forall n r'', exf r i n = Some r'' -> r' = r''.
Proof.
induction 1; intros [| n]; simpl; try (intros; discriminate).
intros r'' Heq; injection Heq; auto.
rewrite aeval_f with (1:=H); simpl; rewrite s_update_f with (1:=H0); simpl;
intros r'' Heq; injection Heq; auto.
case_eq (exf r i1 n); intros r1 q1; try (intros; discriminate).
simpl; case_eq (exf r1 i2 n); intros r2 q2; try (intros; discriminate);
intros r3 Heq; injection Heq; intro; subst r3.
apply IHexec2 with n; auto.
assert (r' = r1) by (apply IHexec1 with n; auto); subst r1; auto.
rewrite beval_f with (1:=H); simpl.
case_eq (exf r i n); intros r1 q1; try (intros; discriminate).
assert (r'=r1) by (apply IHexec1 with n; auto); subst r1.
simpl; case_eq (exf r' (while b i) n); intros r2 q2; try (intros; discriminate).
intros r3 Heq; injection Heq; intro; subst r3.
apply IHexec2 with n; auto.
rewrite beval_f with (1:=H); simpl.
intros r3 Heq; injection Heq; intro; subst r3; auto.
rewrite beval_f with (1:=H); simpl; apply IHexec.
rewrite beval_f with (1:=H); simpl; apply IHexec.
Qed.

Ltac compute_sound_exec :=
match goal with
  H : exec ?r ?i ?r', H1' : ?r = ?e, H2' : ?i = ?f |- _ =>
  let A := fresh in let B := fresh in
  let v := eval cbv beta iota zeta delta -[Zplus Zmult] in (exf e f 2) in
  match v with 
    Some ?v' => 
    assert (A : exf r i 2 = v) by (rewrite H1'; rewrite H2'; auto);
    assert (B : r' = v') by apply exf_sound with (1:=H) (2:=A);
    clear A
  end
end.
(* The following exercise is to prove that a certain program implements
  a certain function. *)

Lemma sum_prg :
  forall r i r', 
    exec r i r' ->
    forall n m,
    r = (("x", n)::("y", m)::nil) ->
    i = (while (blt (anum 0) (avar "x"))
         (sequence (assign "y" (aplus (amult (anum 2)(avar "x"))(avar "y")))
               (assign "x" (aplus (avar "x") (anum (-1)))))) ->
    0 <= n ->
    r' = (("x", 0)::("y", m+n*(n+1))::nil).
Proof.
induction 1; try (intros; discriminate).
intros n m Hr Hi Hn; injection Hi; clear Hi; intros Hi Hb.
assert (0 < n).
clear Hi Hn IHexec1 IHexec2 H1 H0; subst b.
inversion H.
apply aeval_f in H2; subst r; injection H2; intro; subst v1.
apply aeval_f in H4; injection H4; intro; subst v2; auto.
compute_sound_exec.
replace (m + n*(n+1)) with (2*n + m + (n-1)*(n-1+1)) by ring.
apply IHexec2; try (subst b i); solve [auto | omega].

intros n m Hr Hi Hn; injection Hi; clear Hi; intros Hi Hb.
subst b; inversion H.
assert (v1 = 0).
assert (H6:af r (anum 0) = Some 0) by auto.
apply aeval_f in H2; rewrite H2 in H6; injection H6; auto.
apply aeval_f in H4; subst r; simpl in H4.
injection H4; intro; subst v2 v1.
assert (H': n=0) by omega; rewrite H'.
replace (m+0*(0+1)) with m by ring; auto.
Qed.