Software Foundations: An Evaluation Function for Imp

ImpCEvalFun.v

Require Import Nat.
Require Import Omega.

(* https://gist.github.com/pedrominicz/f7bb82bcf9ba2bcefbca665219346e7a *)
Require Import Maps.
Import Total.
(* https://gist.github.com/pedrominicz/ffc64ced0d034b8edd33332eb90ccc65 *)
Require Import Imp.

Definition relation := eval.

Open Scope imp_scope.

Notation "m >>= f" := (match m with Some x => f x | None => None end)
  (left associativity, at level 50).

Fixpoint eval (n : nat) (s : state) (c : command) : option state :=
match n with
| O => None
| S n =>
  match c with
  | skip' => Some s
  | k ::= v => Some (k !-> A.eval s v; s)
  | c1;; c2 => eval n s c1 >>= fun s => eval n s c2
  | test e then c1 else c2 end =>
    if B.eval s e then eval n s c1 else eval n s c2
  | while e do c1 end =>
    if B.eval s e then eval n s c1 >>= fun s => eval n s c else Some s
  end
end.

Close Scope imp_scope.

Definition test_eval (s : state) (c : command) : option (nat * nat * nat) :=
match eval 500 s c with
| Some s => Some (s x, s y, s z)
| None => None
end.

Theorem le_injective : forall n m,
  n <= m <-> S n <= S m.
Proof. intros. omega. Qed.

Lemma eval_le : forall n1 n2 c s1 s2,
  n1 <= n2 -> eval n1 s1 c = Some s2 -> eval n2 s1 c = Some s2.
Proof.
  induction n1; intros n2 c s1 s2 Hle Heval.
  - simpl in Heval. discriminate.
  - destruct n2. inversion Hle.
    apply le_injective in Hle.
    destruct c; simpl; simpl in Heval; trivial.
    + rename s2 into s3.
      destruct (eval n1 s1 c1) as [s2 |] eqn:?.
      * apply (IHn1 n2) in Heqo; try assumption.
        rewrite Heqo.
        apply (IHn1 n2) in Heval; assumption.
      * discriminate.
    + destruct (B.eval s1 e); apply IHn1; assumption.
    + destruct (B.eval s1 e).
      * rename s2 into s3.
        destruct (eval n1 s1 c) as [s2 |] eqn:?.
        { apply (IHn1 n2) in Heqo; try assumption.
          rewrite Heqo.
          apply (IHn1 n2) in Heval; assumption. }
        { discriminate. }
      * assumption.
Qed.

Theorem eval_relation : forall c s1 s2,
  s1 =[ c ]=> s2 <-> exists n, eval n s1 c = Some s2.
Proof.
  split.
  - intros.
    induction H.
    + exists 1. reflexivity.
    + exists 1. simpl. rewrite eq. reflexivity.
    + destruct IHeval1 as [n1 H1].
      destruct IHeval2 as [n2 H2].
      destruct (le_ge_dec n2 n1) as [le | le]; unfold ge.
      * exists (S n1). simpl.
        rewrite H1.
        apply (eval_le n2 n1) in H2; assumption.
      * exists (S n2). simpl.
        apply (eval_le n1 n2) in H1; try assumption.
        rewrite H1. assumption.
    + destruct IHeval as [n].
      exists (S n). simpl.
      rewrite eq. assumption.
    + destruct IHeval as [n].
      exists (S n). simpl.
      rewrite eq. assumption.
    + destruct IHeval1 as [n1 H1].
      destruct IHeval2 as [n2 H2].
      destruct (le_ge_dec n2 n1) as [le | le]; unfold ge.
      * exists (S n1). simpl. rewrite eq.
        rewrite H1.
        apply (eval_le n2 n1) in H2; assumption.
      * exists (S n2). simpl. rewrite eq.
        apply (eval_le n1 n2) in H1; try assumption.
        rewrite H1. assumption.
    + exists 1. simpl. rewrite eq. reflexivity.
  - intros [n H].
    generalize dependent s2.
    generalize dependent s1.
    generalize dependent c.
    induction n; intros; simpl in H.
    + discriminate.
    + destruct c.
      * injection H as []. apply skip.
      * injection H as []. apply assign. reflexivity.
      * rename s2 into s3.
        destruct (eval n s1 c1) as [s2 |] eqn:?.
        { apply seq with s2; apply IHn; assumption. }
        { discriminate. }
      * destruct (B.eval s1 e) eqn:?.
        { apply test_true; try apply IHn; assumption. }
        { apply test_false; try apply IHn; assumption. }
      * destruct (B.eval s1 e) eqn:?.
        { rename s2 into s3.
          destruct (eval n s1 c) as [s2 |] eqn:?.
          - apply while_true with s2; try apply IHn; assumption.
          - discriminate. }
        { injection H as []. apply while_false. assumption. }
Qed.

Theorem eval_deterministic : forall c s1 s2 s3,
  s1 =[ c ]=> s2 -> s1 =[ c ]=> s3 -> s2 = s3.
Proof.
  intros c s1 s2 s3 Hs2 Hs3.
  apply eval_relation in Hs2.
  apply eval_relation in Hs3.
  destruct Hs2 as [n2 H2].
  destruct Hs3 as [n3 H3].
  apply eval_le with (n2 := n2 + n3) in H2; try omega.
  apply eval_le with (n2 := n2 + n3) in H3; try omega.
  rewrite H2 in H3.
  injection H3 as eq.
  assumption.
Qed.