Software Foundations: Simple Imperative Programs

Imp.v

Require Import Bool.
Require Import Nat.
Require Import String.

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

Import Total.

Definition state := map nat.

Definition empty := _ !-> 0.

Notation "k '!->' v" := (update empty k v) (at level 100).

Definition x : key := "x"%string.
Definition y : key := "y"%string.
Definition z : key := "z"%string.

Declare Scope imp_scope.

Delimit Scope imp_scope with imp.

Module A.

Inductive expr : Type :=
| num (n : nat)
| var (k : key)
| plus (e1 e2 : expr)
| monus (e1 e2 : expr)
| mult (e1 e2 : expr).

Fixpoint eval (s : state) (e : expr) : nat :=
match e with
| num n => n
| var k => s k
| plus e1 e2 => eval s e1 + eval s e2
| monus e1 e2 => eval s e1 - eval s e2
| mult e1 e2 => eval s e1 * eval s e2
end.

End A.

Coercion A.num : nat >-> A.expr.
Coercion A.var : key >-> A.expr.

Bind Scope imp_scope with A.expr.

Notation "e1 + e2" := (A.plus e1 e2) (at level 50, left associativity) : imp_scope.
Notation "e1 - e2" := (A.monus e1 e2) (at level 50, left associativity) : imp_scope.
Notation "e1 * e2" := (A.mult e1 e2) (at level 40, left associativity) : imp_scope.

Module B.

Definition btrue : bool := true.
Definition bfalse : bool := false.

Inductive expr : Type :=
| true
| false
| eq (e1 e2 : A.expr)
| le (e1 e2 : A.expr)
| and (e1 e2 : expr)
| not (e1 : expr).

Fixpoint eval (s : state) (e : expr) : bool :=
match e with
| true => btrue
| false => bfalse
| eq e1 e2 => A.eval s e1 =? A.eval s e2
| le e1 e2 => A.eval s e1 <=? A.eval s e2
| and e1 e2 => eval s e1 && eval s e2
| not e1 => negb (eval s e1)
end.

End B.

Definition bool_expr (b : bool) : B.expr :=
  if b then B.true else B.false.

Coercion bool_expr : bool >-> B.expr.

Bind Scope imp_scope with B.expr.

Notation "e1 = e2" := (B.eq e1 e2) (at level 70, no associativity) : imp_scope.
Notation "e1 <= e2" := (B.le e1 e2) (at level 70, no associativity) : imp_scope.
Notation "e1 && e2" := (B.and e1 e2) (at level 40, left associativity) : imp_scope.
Notation "'~' e" := (B.not e) (at level 75, right associativity) : imp_scope.

Inductive command : Type :=
| skip'
| break'
| assign_command (k : key) (e : A.expr)
| seq_command (c1 c2 : command)
| test_command (e : B.expr) (c1 c2 : command)
| while_command (e : B.expr) (c1 : command).

Bind Scope imp_scope with command.

Notation "k '::=' e" :=
  (assign_command k e) (at level 60) : imp_scope.
Notation "c1 ;; c2" :=
  (seq_command c1 c2) (at level 80, right associativity) : imp_scope.
Notation "'while' e 'do' c 'end'" :=
  (while_command e c) (at level 80, right associativity) : imp_scope.
Notation "'test' e 'then' c1 'else' c2 'end'" :=
  (test_command e c1 c2) (at level 80, right associativity) : imp_scope.

Reserved Notation "s1 '=[' c ']=>' s2 '//' b" (at level 40).

Inductive eval : command -> state -> state -> bool -> Prop :=
| skip s1 : s1 =[ skip' ]=> s1 // true
| break s1 : s1 =[ break' ]=> s1 // false
| assign s1 k e n (eq : A.eval s1 e = n) : s1 =[ k ::= e ]=> k !-> n; s1 // true
| seq c1 c2 s1 s2 s3 b : s1 =[ c1 ]=> s2 // true -> s2 =[ c2 ]=> s3 // b -> s1 =[ c1;; c2 ]=> s3 // b
| seq_break c1 c2 s1 s2 : s1 =[ c1 ]=> s2 // false -> s1 =[ c1;; c2 ]=> s2 // false
| test_true s1 s2 e c1 c2 b (eq : B.eval s1 e = true) : s1 =[ c1 ]=> s2 // b -> s1 =[ test e then c1 else c2 end ]=> s2 // b
| test_false s1 s2 e c1 c2 b (eq : B.eval s1 e = false) : s1 =[ c2 ]=> s2 // b -> s1 =[ test e then c1 else c2 end ]=> s2 // b
| while_true s1 s2 s3 e c1 b (eq : B.eval s1 e = true) : s1 =[ c1 ]=> s2 // true -> s2 =[ while e do c1 end ]=> s3 // b -> s1 =[ while e do c1 end ]=> s3 // b
| while_break s1 s2 e c1 (eq : B.eval s1 e = true) : s1 =[ c1 ]=> s2 // false -> s1 =[ while e do c1 end ]=> s2 // true
| while_false s1 e c1 (eq : B.eval s1 e = false) : s1 =[ while e do c1 end ]=> s1 // true
where "s1 '=[' c ']=>' s2 '//' b" := (eval c s1 s2 b).

Example example_1 :
  empty =[ x ::= 1;; y ::= 2;; z ::= 3 ]=> (z !-> 3; y !-> 2; x !-> 1) // true.
Proof.
  apply seq with (x !-> 1).
  - apply assign. reflexivity.
  - apply seq with (y !-> 2; x !-> 1); constructor; reflexivity.
Qed.

Example example_2 :
  (x !-> 2) =[
    while ~(x = 0) do
      y ::= x + y;;
      x ::= x - 1
    end
  ]=> (x !-> 0; y !-> 3; x !-> 1; y !-> 2; x !-> 2) // true.
Proof.
  apply while_true with (x !-> 1; y !-> 2; x !-> 2). reflexivity.
  apply seq with (y !-> 2; x !-> 2).
    apply assign. reflexivity.
    apply assign. reflexivity.
  apply while_true with (x !-> 0; y !-> 3; x !-> 1; y !-> 2; x !-> 2). reflexivity.
  apply seq with (y !-> 3; x !-> 1; y !-> 2; x !-> 2).
    apply assign. reflexivity.
    apply assign. reflexivity.
  apply while_false. reflexivity.
Qed.

Theorem break_ignore : forall c s1 s2 b,
  s1 =[ break';; c ]=> s2 // b -> s1 = s2.
Proof.
  intros.
  inversion H; subst.
  - inversion H2.
  - inversion H5. subst. reflexivity.
Qed.

Theorem while_continue : forall e c s1 s2 b,
  s1 =[ while e do c end ]=> s2 // b -> b = true.
Proof.
  intros.
  remember (while e do c end)%imp as loop.
  induction H; auto; discriminate.
Qed.

Theorem while_break_false : forall e c s1 s2,
  B.eval s1 e = true -> s1 =[ c ]=> s2 // false -> s1 =[ while e do c end ]=> s2 // true.
Proof.
  intros e c s1 s2 eq H.
  apply while_break; assumption.
Qed.

Theorem while_break_true : forall e c s1 s3,
  s1 =[ while e do c end ]=> s3 // true -> B.eval s3 e = true -> exists s2, s2 =[ c ]=> s3 // false.
Proof.
  intros e c s1 s2 H eq.
  remember (while e do c end)%imp as loop.
  induction H; auto; try congruence.
  - injection Heqloop as []; subst.
    exists s1. assumption.
Qed.

Theorem eval_deterministic : forall s s1 s2 c b1 b2,
  s =[ c ]=> s1 // b1 -> s =[ c ]=> s2 // b2 -> s1 = s2 /\ b1 = b2.
Proof.
  intros s s1 s2 c b1 b2 H1 H2.
  generalize dependent b2.
  generalize dependent s2.
  induction H1; intros; inversion H2; subst; try congruence; auto.
  - specialize (IHeval1 s5 true H1) as []. subst.
    specialize (IHeval2 s0 b2 H6) as []. subst. auto.
  - specialize (IHeval1 s0 false H5) as []. congruence.
  - specialize (IHeval s4 true H3) as []. discriminate.
  - specialize (IHeval1 s5 true H1) as []. subst.
    specialize (IHeval2 s0 b2 H6) as []. subst. auto.
  - specialize (IHeval1 s0 false H5) as []. discriminate.
  - specialize (IHeval s4 true H3) as []. discriminate.
  - specialize (IHeval s0 false H6) as []. subst. auto.
Qed.

Example example_3 : forall s1 s2 n,
  s1 x = n -> s1 =[ x ::= 2 + x ]=> s2 // true -> s2 x = 2 + n.
Proof.
  intros s1 s2 n H Heval.
  inversion Heval. subst.
  apply update_eq.
Qed.

Example example_4 : forall s1 s2 n1 n2,
  s1 x = n1 /\ s1 y = n2 -> s1 =[ z ::= x * y ]=> s2 // true -> s2 z = n1 * n2.
Proof.
  intros s1 s2 n1 n2 [] Heval.
  inversion Heval. subst.
  apply update_eq.
Qed.

Example example_5 : forall s1 s2 b,
  ~(s1 =[ while true do skip' end ]=> s2 // b).
Proof.
  unfold not.
  intros.
  remember (while true do skip' end)%imp as loop.
  induction H; try congruence.
  - injection Heqloop as []; subst. inversion H.
  - injection Heqloop; intros; subst.
    simpl in eq. unfold B.btrue in eq. discriminate.
Qed.

Inductive loopless : command -> Prop :=
| skip_loopless : loopless skip'
| break_loopless : loopless break'
| assign_loopless k v : loopless (k ::= v)
| seq_loopless c1 c2 : loopless c1 -> loopless c2 -> loopless (c1;; c2)
| test_loopless e c1 c2 : loopless c1 -> loopless c2 -> loopless (test e then c1 else c2 end).

Open Scope imp_scope.

Fixpoint loopless' (c : command) : bool :=
match c with
| skip' => true
| break' => true
| _ ::= _ => true
| c1;; c2 => loopless' c1 && loopless' c2
| test _ then c1 else c2 end => loopless' c1 && loopless' c2
| while _ do _ end => false
end.

Close Scope imp_scope.

Theorem loopless_loopless' : forall c,
  loopless c <-> loopless' c = true.
Proof.
  split; intros.
  - induction H; try reflexivity.
    + simpl. rewrite IHloopless1, IHloopless2. reflexivity.
    + simpl. rewrite IHloopless1, IHloopless2. reflexivity.
  - induction c; try constructor.
    + simpl in H. destruct (loopless' c1); auto.
    + simpl in H. rewrite andb_comm in H. destruct (loopless' c2); auto.
    + simpl in H. destruct (loopless' c1); auto.
    + simpl in H. rewrite andb_comm in H. destruct (loopless' c2); auto.
    + simpl in H. discriminate.
Qed.

Theorem loopless_terminating : forall s1 c,
  loopless c -> exists s2 b, s1 =[ c ]=> s2 // b.
Proof.
  intros.
  generalize dependent s1.
  induction H; intros.
  - exists s1, true. apply skip.
  - exists s1, false. apply break.
  - exists (k !-> A.eval s1 v; s1), true. apply assign. reflexivity.
  - destruct IHloopless1 with s1 as [s2 [[]]].
    + destruct IHloopless2 with s2 as [s3 [b3]].
      exists s3, b3. apply seq with s2; assumption.
    + exists s2, false. apply seq_break. assumption.
  - destruct (B.eval s1 e) eqn:?.
    + destruct IHloopless1 with s1 as [s2 [b2]].
      exists s2, b2. apply test_true; assumption.
    + destruct IHloopless2 with s1 as [s2 [b2]].
      exists s2, b2. apply test_false; assumption.
Qed.

Module S.

Import List.
Import ListNotations.

Inductive instruction : Type :=
| push (n : nat)
| load (k : key)
| plus
| monus
| mult.

Fixpoint eval (s : state) (ns : list nat) (is : list instruction) : list nat :=
let operator (f : nat -> nat -> nat) : list nat :=
  match ns with
  | n1 :: n2 :: ns => f n2 n1 :: ns
  | _ => ns
  end in
match is with
| push n :: is => eval s (n :: ns) is
| load k :: is => eval s (s k :: ns) is
| plus :: is => eval s (operator (fun n1 n2 => n1 + n2)) is
| monus :: is => eval s (operator (fun n1 n2 => n1 - n2)) is
| mult :: is => eval s (operator (fun n1 n2 => n1 * n2)) is
| [] => ns
end.

Example example_6 : eval empty [] [push 5; push 3; push 1; monus] = [2; 5].
Proof. reflexivity. Qed.

Example example_7 : eval (x !-> 3) [3; 4] [push 4; load x; mult; plus] = [15; 4].
Proof. reflexivity. Qed.

Fixpoint compile (e : A.expr) : list instruction :=
match e with
| A.num n => [push n]
| A.var k => [load k]
| A.plus e1 e2 => compile e1 ++ compile e2 ++ [plus]
| A.monus e1 e2 => compile e1 ++ compile e2 ++ [monus]
| A.mult e1 e2 => compile e1 ++ compile e2 ++ [mult]
end.

Example example_8 : compile (x - 2 * y) = [load x; push 2; load y; mult; monus].
Proof. reflexivity. Qed.

Lemma compile_correct_app : forall s e ns is,
  eval s ns (compile e ++ is) = eval s (A.eval s e :: ns) is.
Proof.
  intros.
  generalize dependent is.
  generalize dependent ns.
  induction e; try reflexivity.
  - intros. simpl.
    rewrite <- app_assoc, <- app_assoc.
    rewrite IHe1. rewrite IHe2. reflexivity.
  - intros. simpl.
    rewrite <- app_assoc, <- app_assoc.
    rewrite IHe1. rewrite IHe2. reflexivity.
  - intros. simpl.
    rewrite <- app_assoc, <- app_assoc.
    rewrite IHe1. rewrite IHe2. reflexivity.
Qed.

Theorem compile_correct : forall s e,
  eval s [] (compile e) = [A.eval s e].
Proof.
  intros.
  assert (compile e = compile e ++ []) as eq.
  { rewrite app_nil_r. reflexivity. }
  rewrite eq.
  apply compile_correct_app.
Qed.

End S.