Require Import ZArith.
Require Import String.

Open Scope string_scope.
Open Scope Z_scope.

Require Import IMPSyntax.

Definition heap : Type :=
  string -> Z.

Definition empty : heap :=
  fun v => 0.

Definition exec_op (op: binop) (i1 i2: Z) : Z :=
  match op with
  | Add => i1 + i2
  | Sub => i1 - i2
  | Mul => i1 * i2
  | Div => i1 / i2
  | Mod => i1 mod i2
  | Lt => if Z_lt_dec i1 i2 then 1 else 0
  | Lte => if Z_le_dec i1 i2 then 1 else 0
  | Conj => if Z_eq_dec i1 0 then 0 else
              if Z_eq_dec i2 0 then 0 else 1
  | Disj => if Z_eq_dec i1 0 then
              if Z_eq_dec i2 0 then 0 else 1
            else 1
  end.

Inductive eval : heap -> expr -> Z -> Prop :=
| eval_int:
    forall h i,
    eval h (Int i) i
| eval_var:
    forall h v,
    eval h (Var v) (h v)
| eval_binop:
    forall h op e1 e2 i1 i2 i3,
    eval h e1 i1 ->
    eval h e2 i2 ->
    exec_op op i1 i2 = i3 ->
    eval h (BinOp op e1 e2) i3.

Fixpoint interp_expr (h: heap) (e: expr) : Z :=
  match e with
  | Int i => i
  | Var v => h v
  | BinOp op e1 e2 =>
      exec_op op (interp_expr h e1) (interp_expr h e2)
  end.

Lemma interp_expr_eval:
  forall h e i,
  interp_expr h e = i ->
  eval h e i.
Proof.
  intros h e.
  induction e; simpl in *; intros.
  - subst; constructor.
  - subst; constructor.
  - apply eval_binop with (i1 := interp_expr h e1)
                          (i2 := interp_expr h e2).
    + apply IHe1. auto.
    + apply IHe2. auto.
    + assumption.
Qed.

Lemma eval_interp_expr:
  forall h e i,
  eval h e i ->
  interp_expr h e = i.
Proof.
  intros h e.
  induction e; simpl in *; intros.
  - inversion H; subst; auto.
  - inversion H; subst; reflexivity.
  - inversion H; subst.
    rewrite (IHe1 i1 H4).
    rewrite (IHe2 i2 H6).
    reflexivity.
Qed.

Lemma eval_interp:
  forall h e,
  eval h e (interp_expr h e).
Proof.
  intros. induction e; simpl.
  - constructor.
  - constructor.
  - econstructor.
    + eassumption.
    + eassumption.
    + reflexivity.
Qed.

Lemma eval_det:
  forall h e i1 i2,
  eval h e i1 ->
  eval h e i2 ->
  i1 = i2.
Proof.
  intros.
  apply eval_interp_expr in H.
  apply eval_interp_expr in H0.
  subst. reflexivity.
Qed.

Definition update (h: heap) (v: string) (i: Z) : heap :=
  fun v´ =>
    if string_dec v´ v then
      i
    else
      h v´.

Inductive step : heap -> stmt -> heap -> stmt -> Prop :=
| step_assign:
  forall h v e i,
  eval h e i ->
  step h (Assign v e) (update h v i) Nop
| step_seq_nop:
  forall h s,
  step h (Seq Nop s) h s
| step_seq:
  forall h s1 s2 s1´ h´,
  step h s1 h´ s1´ ->
  step h (Seq s1 s2) h´ (Seq s1´ s2)
| step_cond_true:
  forall h e s i,
  eval h e i ->
  i <> 0 ->
  step h (Cond e s) h s
| step_cond_false:
  forall h e s i,
  eval h e i ->
  i = 0 ->
  step h (Cond e s) h Nop
| step_while_true:
  forall h e s i,
  eval h e i ->
  i <> 0 ->
  step h (While e s) h (Seq s (While e s))
| step_while_false:
  forall h e s i,
  eval h e i ->
  i = 0 ->
  step h (While e s) h Nop.

Definition isNop (s: stmt) : bool :=
  match s with
  | Nop => true
  | _ => false
  end.

Lemma isNop_ok:
  forall s,
  isNop s = true <-> s = Nop.
Proof.
  destruct s; simpl; split; intros;
    auto; discriminate.
Qed.

Fixpoint interp_step (h: heap) (s: stmt) : option (heap * stmt) :=
  match s with
  | Nop => None
  | Assign v e =>
      Some (update h v (interp_expr h e), Nop)
  | Seq s1 s2 =>
      if isNop s1 then
        Some (h, s2)
      else
        match interp_step h s1 with
        | Some (h´, s1´) => Some (h´, Seq s1´ s2)
        | None => None
        end
  | Cond e s =>
      if Z_eq_dec (interp_expr h e) 0 then
        Some (h, Nop)
      else
        Some (h, s)
  | While e s =>
      if Z_eq_dec (interp_expr h e) 0 then
        Some (h, Nop)
      else
        Some (h, Seq s (While e s))
  end.

Lemma interp_step_step:
  forall h s h´ s´,
  interp_step h s = Some (h´, s´) ->
  step h s h´ s´.
Proof.
  intros h s. revert h.
  induction s; simpl; intros.
  - discriminate.
  - inversion H. subst.
    constructor. apply interp_expr_eval; auto.
  - destruct (isNop s1) eqn:?.
    + rewrite isNop_ok in Heqb. subst.
      inversion H. subst. constructor.
    + destruct (interp_step h s1) as [[newHeap newStmt]|] eqn:?.
      * inversion H. subst.
        apply IHs1 in Heqo.
        constructor. assumption.
      * discriminate.
  - destruct (Z.eq_dec (interp_expr h e) 0) eqn:?.
    + inversion H. subst.
      clear Heqs0. apply interp_expr_eval in e0. econstructor.
      eassumption. auto.
    + inversion H; subst.
      eapply step_cond_true; eauto.
      apply interp_expr_eval; auto.
  - destruct (Z.eq_dec (interp_expr h e) 0) eqn:?.
    + inversion H; subst.
      eapply step_while_false; eauto.
      apply interp_expr_eval; auto.
    + inversion H; subst.
      eapply step_while_true; eauto.
      apply interp_expr_eval; auto.
Qed.

Lemma step_interp_step:
  forall h s h´ s´,
  step h s h´ s´ ->
  interp_step h s = Some (h´, s´).
Proof.
  intros. induction H; simpl; auto.
  - apply eval_interp_expr in H.
    subst; auto.
  - destruct (isNop s1) eqn:?.
    + apply isNop_ok in Heqb. subst.
      inversion H.

    + rewrite IHstep. auto.
  - apply eval_interp_expr in H. subst.
    destruct (Z.eq_dec (interp_expr h e) 0); auto.
    exfalso. unfold not in H0. apply H0. assumption.
  - apply eval_interp_expr in H. subst.
    destruct (Z.eq_dec (interp_expr h e) 0); auto.
    unfold not in n. apply n in H0.
    exfalso. assumption.
  - apply eval_interp_expr in H. subst.
    destruct (Z.eq_dec (interp_expr h e) 0); auto.
    unfold not in H0. apply H0 in e0.
    inversion e0.
  - apply eval_interp_expr in H. subst.
    destruct (Z.eq_dec (interp_expr h e) 0); auto.
    omega.
Qed.

Inductive step_n : heap -> stmt -> nat -> heap -> stmt -> Prop :=
| sn_refl:
  forall h s,
  step_n h s O h s
| sn_step:
  forall h1 s1 n h2 s2 h3 s3,
  step h1 s1 h2 s2 ->
  step_n h2 s2 n h3 s3 ->
  step_n h1 s1 (S n) h3 s3.

Fixpoint run (fuel: nat) (h: heap) (s: stmt) : (heap * stmt) :=
  match fuel with
  | O => (h, s)
  | S n =>
      match interp_step h s with
      | Some (h´, s´) => run n h´ s´
      | None => (h, s)
      end
  end.

Lemma run_stepn:
  forall fuel h s h´ s´,
  run fuel h s = (h´, s´) ->
  exists n, step_n h s n h´ s´.
Proof.
  induction fuel; simpl; intros.
  - inversion H; subst.
    exists O. constructor.
  - destruct (interp_step h s) as [[foo bar]|] eqn:?.
    + apply IHfuel in H.
      apply interp_step_step in Heqo.
      destruct H. exists (S x).
      econstructor; eauto.
    + inversion H; subst.
      exists O. constructor; auto.
Qed.

Lemma stepn_run:
  forall h s n h´ s´,
  step_n h s n h´ s´ ->
  run n h s = (h´, s´).
Proof.
  intros. induction H; simpl; auto.
  destruct (interp_step h1 s1) as [[h´ s´]|] eqn:?.
  + apply step_interp_step in H.

    rewrite H in Heqo. inversion Heqo; subst.
    assumption.
  + apply step_interp_step in H.
    rewrite H in Heqo. discriminate.
Qed.