Week 3: Interpreters

Author: Adam Chlipala, with modifications by CS-428 staff.
License: No redistribution allowed (usage by permission in CS-428).

A Simple Arithmetic Language

This lecture shows how to define the semantics of a programming language using an interpreter, and how to reason about the correctness of various program transformations using semantics. We'll start with the language of arithmetic expressions we've seen previously, but will extend it with a new operation for subtraction.

Notation var := string.

Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).

Here are a couple of examples of arithmetic expressions in the language: one that describes the computation that computes the constant 42; and another that describes the computation that adds y to the product of x and 3.

Example ex1 := Const 42.

Example ex2 := Plus (Var "y") (Times (Var "x") (Const 3)).

To define the semantics of arithmetic expressions, we'll need some way of determining the values of variables. To do that, we'll use a valuation, which encodes a finite map from variables to natural numbers, represented concretely as a Coq function that returns an option.

Definition valuation := var -> option nat.

Definition empty : valuation := fun _ => None.

Definition get (x:var) (v:valuation) : option nat := v x.

Definition set (x:var) (n:nat) (v:valuation) : valuation :=
  fun y =>
    match string_dec x y with
        | left H => Some n
        | right H' => get y v
    end.

Interpreter for Arithmetic Expressions

Now we can define the semantics of the language via an interpreter that takes an and a valuation as input and computes the natural number that it describes. The interpreter is recursive, but only makes recursive calls on sub-expressions, so Coq's termination checker accepts it.

Fixpoint interp (e : arith) (v : valuation) : nat :=
  match e with
  | Const n => n
  | Var x =>
    match v x with
    | None => 0
    | Some n => n
    end
  | Plus e1 e2 => interp e1 v + interp e2 v
  | Minus e1 e2 => interp e1 v - interp e2 v
  | Times e1 e2 => interp e1 v * interp e2 v
  end.

We can check that the interpreter computes the expected results for the example arithmetic expressions defined above.

Definition valuation0 : valuation :=
  set "y" 3 (set "x" 17 empty).

Example interp_ex1 : interp ex1 valuation0 = 42.interp ex1 valuation0 = 42
Proof.interp ex1 valuation0 = 42
  reflexivity.
Qed.

Example interp_ex2 : interp ex2 valuation0 = 54.interp ex2 valuation0 = 54
Proof.interp ex2 valuation0 = 54
  reflexivity.
Qed.

Transformations on Arithmetic Expressions

Next, let's define a transformation on arithmetic expressions that commutes the order of some sub-expressions. Note that we do not commute the order of Minus expressions as subtraction is not commutative.

Fixpoint commuter (e : arith) : arith :=
  match e with
  | Const _ => e
  | Var _ => e
  | Plus e1 e2 => Plus (commuter e2) (commuter e1)
  | Minus e1 e2 => Minus (commuter e1) (commuter e2)
  | Times e1 e2 => Times (commuter e2) (commuter e1)
  end.

Previously we reasoned about the correctness of program transformations like commuter by reasoning syntactically about its behavior. Now that we have an interpreter that defines the semantics of arithmetic expressions, we can state a theorm that captures correctness directly: for all expressions e and valuations v, interpreting the commuted version of e produces the same result as e does, under valuation v.

Theorem commuter_ok : forall v e, interp (commuter e) v = interp e v.forall (v : valuation) (e : arith),
interp (commuter e) v = interp e v
Proof.forall (v : valuation) (e : arith),
interp (commuter e) v = interp e v
  induction e.v: valuation
n: nat
interp (commuter (Const n)) v = interp (Const n) v
v: valuation
x: var
interp (commuter (Var x)) v = interp (Var x) v
v: valuation
e1, e2: arith
IHe1: interp (commuter e1) v = interp e1 v
IHe2: interp (commuter e2) v = interp e2 v
interp (commuter (Plus e1 e2)) v =
interp (Plus e1 e2) v
v: valuation
e1, e2: arith
IHe1: interp (commuter e1) v = interp e1 v
IHe2: interp (commuter e2) v = interp e2 v
interp (commuter (Minus e1 e2)) v =
interp (Minus e1 e2) v
v: valuation
e1, e2: arith
IHe1: interp (commuter e1) v = interp e1 v
IHe2: interp (commuter e2) v = interp e2 v
interp (commuter (Times e1 e2)) v =
interp (Times e1 e2) v
  -v: valuation
n: nat
interp (commuter (Const n)) v = interp (Const n) v reflexivity.
  -v: valuation
x: var
interp (commuter (Var x)) v = interp (Var x) v reflexivity.
  -v: valuation
e1, e2: arith
IHe1: interp (commuter e1) v = interp e1 v
IHe2: interp (commuter e2) v = interp e2 v
interp (commuter (Plus e1 e2)) v =
interp (Plus e1 e2) v simpl; rewrite IHe1, IHe2; lia.
  -v: valuation
e1, e2: arith
IHe1: interp (commuter e1) v = interp e1 v
IHe2: interp (commuter e2) v = interp e2 v
interp (commuter (Minus e1 e2)) v =
interp (Minus e1 e2) v simpl; rewrite IHe1, IHe2; lia.
  -v: valuation
e1, e2: arith
IHe1: interp (commuter e1) v = interp e1 v
IHe2: interp (commuter e2) v = interp e2 v
interp (commuter (Times e1 e2)) v =
interp (Times e1 e2) v simpl; rewrite IHe1, IHe2; lia.
Qed.

Next let's define a substitution operation that replaces a variable x with a value v.

Fixpoint substitute (e : arith) (x : var) (v : arith) : arith :=
  match e with
  | Const _ => e
  | Var y => if string_dec y x then v else e
  | Plus e1 e2 => Plus (substitute e1 x v) (substitute e2 x v)
  | Minus e1 e2 => Minus (substitute e1 x v) (substitute e2 x v)
  | Times e1 e2 => Times (substitute e1 x v) (substitute e2 x v)
  end.

We can prove the soundness of the substitution operation, showing that if we substitute w for x in e and then interpret the resulting expression under v, we get the same result as if we had evaluated e in an extended environment that behaves like v except that x is set to interp w v.

Theorem substitute_ok : forall v x w e,
  interp (substitute e x w) v
  = interp e (set x (interp w v) v).forall (v : valuation) (x : var) (w e : arith),
interp (substitute e x w) v =
interp e (set x (interp w v) v)
Proof.forall (v : valuation) (x : var) (w e : arith),
interp (substitute e x w) v =
interp e (set x (interp w v) v)
  induction e.v: valuation
x: var
w: arith
n: nat
interp (substitute (Const n) x w) v =
interp (Const n) (set x (interp w v) v)
v: valuation
x: var
w: arith
x0: var
interp (substitute (Var x0) x w) v =
interp (Var x0) (set x (interp w v) v)
v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute (Plus e1 e2) x w) v =
interp (Plus e1 e2) (set x (interp w v) v)
v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute (Minus e1 e2) x w) v =
interp (Minus e1 e2) (set x (interp w v) v)
v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute (Times e1 e2) x w) v =
interp (Times e1 e2) (set x (interp w v) v)
  -v: valuation
x: var
w: arith
n: nat
interp (substitute (Const n) x w) v =
interp (Const n) (set x (interp w v) v) simpl; congruence.
  -v: valuation
x: var
w: arith
x0: var
interp (substitute (Var x0) x w) v =
interp (Var x0) (set x (interp w v) v) simpl; unfold set, get;
    destruct (string_dec x0 x);
    destruct (string_dec x x0);
    simpl;
    congruence.
  -v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute (Plus e1 e2) x w) v =
interp (Plus e1 e2) (set x (interp w v) v) simpl.v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute e1 x w) v +
interp (substitute e2 x w) v =
interp e1 (set x (interp w v) v) +
interp e2 (set x (interp w v) v) congruence.
  -v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute (Minus e1 e2) x w) v =
interp (Minus e1 e2) (set x (interp w v) v) simpl.v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute e1 x w) v -
interp (substitute e2 x w) v =
interp e1 (set x (interp w v) v) -
interp e2 (set x (interp w v) v) congruence.
  -v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute (Times e1 e2) x w) v =
interp (Times e1 e2) (set x (interp w v) v) simpl.v: valuation
x: var
w, e1, e2: arith
IHe1: interp (substitute e1 x w) v =
interp e1 (set x (interp w v) v)
IHe2: interp (substitute e2 x w) v =
interp e2 (set x (interp w v) v)
interp (substitute e1 x w) v *
interp (substitute e2 x w) v =
interp e1 (set x (interp w v) v) *
interp e2 (set x (interp w v) v) congruence.
Qed.

Now let's write an optimizer for our arithmetic computations that does a form of constant folding.

Fixpoint optimize (e : arith) : arith :=
  match e with
  | Const _ => e
  | Var _ => e
  | Plus (Const n1) (Const n2) => Const (n1 + n2)
  | Plus e1 e2 => Plus (optimize e1) (optimize e2)
  | Minus (Const n1) (Const n2) => Const (n1 - n2)
  | Minus e1 e2 => Minus (optimize e1) (optimize e2)
  | Times (Const n1) (Const n2) => Const (n1 * n2)
  | Times e1 e2 => Times (optimize e1) (optimize e2)
  end.

Once again, using the semantics implemented by our interpreter, we can prove the optimizer sound.

Theorem optimize_ok : forall e v, interp (optimize e) v = interp e v.forall (e : arith) (v : valuation),
interp (optimize e) v = interp e v
Proof.forall (e : arith) (v : valuation),
interp (optimize e) v = interp e v
  induction e.n: nat
forall v : valuation,
interp (optimize (Const n)) v = interp (Const n) v
x: var
forall v : valuation,
interp (optimize (Var x)) v = interp (Var x) v
e1, e2: arith
IHe1: forall v : valuation,
interp (optimize e1) v = interp e1 v
IHe2: forall v : valuation,
interp (optimize e2) v = interp e2 v
forall v : valuation,
interp (optimize (Plus e1 e2)) v =
interp (Plus e1 e2) v
e1, e2: arith
IHe1: forall v : valuation,
interp (optimize e1) v = interp e1 v
IHe2: forall v : valuation,
interp (optimize e2) v = interp e2 v
forall v : valuation,
interp (optimize (Minus e1 e2)) v =
interp (Minus e1 e2) v
e1, e2: arith
IHe1: forall v : valuation,
interp (optimize e1) v = interp e1 v
IHe2: forall v : valuation,
interp (optimize e2) v = interp e2 v
forall v : valuation,
interp (optimize (Times e1 e2)) v =
interp (Times e1 e2) v
  -n: nat
forall v : valuation,
interp (optimize (Const n)) v = interp (Const n) v simpl.n: nat
valuation -> n = n congruence.
  -x: var
forall v : valuation,
interp (optimize (Var x)) v = interp (Var x) v simpl.x: var
forall v : valuation,
match v x with
| Some n => n
| None => 0
end = match v x with
      | Some n => n
      | None => 0
      end congruence.
  -e1, e2: arith
IHe1: forall v : valuation,
interp (optimize e1) v = interp e1 v
IHe2: forall v : valuation,
interp (optimize e2) v = interp e2 v
forall v : valuation,
interp (optimize (Plus e1 e2)) v =
interp (Plus e1 e2) v destruct e1, e2; simpl in *; try congruence.
  -e1, e2: arith
IHe1: forall v : valuation,
interp (optimize e1) v = interp e1 v
IHe2: forall v : valuation,
interp (optimize e2) v = interp e2 v
forall v : valuation,
interp (optimize (Minus e1 e2)) v =
interp (Minus e1 e2) v destruct e1, e2; simpl in *; try congruence.
  -e1, e2: arith
IHe1: forall v : valuation,
interp (optimize e1) v = interp e1 v
IHe2: forall v : valuation,
interp (optimize e2) v = interp e2 v
forall v : valuation,
interp (optimize (Times e1 e2)) v =
interp (Times e1 e2) v destruct e1, e2; simpl in *; try congruence.
Qed.

Compiler to a Stack Machine

Now let's switch gears and define a more complicated transformation -- a compiler. We'll use a stack machine to serve as the target of our compiler, with instructions defined as follows.

Inductive instruction :=
| PushConst (n : nat)
| PushVar (x : var)
| Add
| Subtract
| Multiply.

We can define the semantics of our stack machine via an interpreter. First, we define an interpreter for a single instruction.

Definition run1 (i : instruction) (v : valuation) (stack : list nat)
  : list nat :=
  match i with
  | PushConst n => n :: stack
  | PushVar x => (match get x v with
                  | None => 0
                  | Some n => n
                 end) :: stack
  | Add =>
      match stack with
      | arg2 :: arg1 :: stack' => arg1 + arg2 :: stack'
      | _ => stack
      end
  | Subtract =>
      match stack with
      | arg2 :: arg1 :: stack' => arg1 - arg2 :: stack'
      | _ => stack
      end
  | Multiply =>
      match stack with
      | arg2 :: arg1 :: stack' => arg1 * arg2 :: stack'
      | _ => stack end
  end.

Next, we define an interpreter that works on a list of instructions. It simply folds over the list of instructions, using the same valuation and accumulating the results on the stack.

Fixpoint run (is : list instruction) (v : valuation) (stack : list nat)
  : list nat :=
  match is with
  | nil => stack
  | i :: is' => run is' v (run1 i v stack)
  end.

Now we are ready to define the compiler which translates arithmetic expressions into list of instructions for our stack machine.

Fixpoint compile (e : arith) : list instruction :=
  match e with
  | Const n => PushConst n :: nil
  | Var x => PushVar x :: nil
  | Plus e1 e2 => compile e1 ++ compile e2 ++ Add :: nil
  | Minus e1 e2 => compile e1 ++ compile e2 ++ Subtract :: nil
  | Times e1 e2 => compile e1 ++ compile e2 ++ Multiply :: nil
  end.

To prove the compiler is sound, we will first prove a slightly stronger lemma. The induction hypothesis generated by Coq for this lemma is sufficiently strong to handle all cases. Note that the proof is slightly repetitive and tedious. We'll see how to use Coq's LTac language and automation to streamline this in the next lecture.

Lemma compile_ok' : forall e v is stack,
    run (compile e ++ is) v stack = run is v (interp e v :: stack).forall (e : arith) (v : valuation)
  (is : list instruction) (stack : list nat),
run (compile e ++ is) v stack =
run is v (interp e v :: stack)
Proof.forall (e : arith) (v : valuation)
  (is : list instruction) (stack : list nat),
run (compile e ++ is) v stack =
run is v (interp e v :: stack)
  induction e.n: nat
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Const n) ++ is) v stack =
run is v (interp (Const n) v :: stack)
x: var
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Var x) ++ is) v stack =
run is v (interp (Var x) v :: stack)
e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Plus e1 e2) ++ is) v stack =
run is v (interp (Plus e1 e2) v :: stack)
e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Minus e1 e2) ++ is) v stack =
run is v (interp (Minus e1 e2) v :: stack)
e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Times e1 e2) ++ is) v stack =
run is v (interp (Times e1 e2) v :: stack)
  -n: nat
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Const n) ++ is) v stack =
run is v (interp (Const n) v :: stack) reflexivity.
  -x: var
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Var x) ++ is) v stack =
run is v (interp (Var x) v :: stack) reflexivity.
  -e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Plus e1 e2) ++ is) v stack =
run is v (interp (Plus e1 e2) v :: stack) intros.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile (Plus e1 e2) ++ is) v stack =
run is v (interp (Plus e1 e2) v :: stack) simpl.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ((compile e1 ++ compile e2 ++ [Add]) ++ is) v
  stack =
run is v (interp e1 v + interp e2 v :: stack)
    rewrite <- app_assoc.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile e1 ++ (compile e2 ++ [Add]) ++ is) v
  stack =
run is v (interp e1 v + interp e2 v :: stack)
    rewrite IHe1.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ((compile e2 ++ [Add]) ++ is) v
  (interp e1 v :: stack) =
run is v (interp e1 v + interp e2 v :: stack)
    rewrite <- app_assoc.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile e2 ++ [Add] ++ is) v
  (interp e1 v :: stack) =
run is v (interp e1 v + interp e2 v :: stack)
    rewrite IHe2.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ([Add] ++ is) v
  (interp e2 v :: interp e1 v :: stack) =
run is v (interp e1 v + interp e2 v :: stack)
    simpl in *.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run is v (interp e1 v + interp e2 v :: stack) =
run is v (interp e1 v + interp e2 v :: stack)
    congruence.
  -e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Minus e1 e2) ++ is) v stack =
run is v (interp (Minus e1 e2) v :: stack) intros.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile (Minus e1 e2) ++ is) v stack =
run is v (interp (Minus e1 e2) v :: stack) simpl.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ((compile e1 ++ compile e2 ++ [Subtract]) ++ is) v
  stack =
run is v (interp e1 v - interp e2 v :: stack)
    rewrite <- app_assoc.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile e1 ++ (compile e2 ++ [Subtract]) ++ is) v
  stack =
run is v (interp e1 v - interp e2 v :: stack)
    rewrite IHe1.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ((compile e2 ++ [Subtract]) ++ is) v
  (interp e1 v :: stack) =
run is v (interp e1 v - interp e2 v :: stack)
    rewrite <- app_assoc.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile e2 ++ [Subtract] ++ is) v
  (interp e1 v :: stack) =
run is v (interp e1 v - interp e2 v :: stack)
    rewrite IHe2.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ([Subtract] ++ is) v
  (interp e2 v :: interp e1 v :: stack) =
run is v (interp e1 v - interp e2 v :: stack)
    simpl in *.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run is v (interp e1 v - interp e2 v :: stack) =
run is v (interp e1 v - interp e2 v :: stack)
    congruence.
  -e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile (Times e1 e2) ++ is) v stack =
run is v (interp (Times e1 e2) v :: stack) intros.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile (Times e1 e2) ++ is) v stack =
run is v (interp (Times e1 e2) v :: stack) simpl.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ((compile e1 ++ compile e2 ++ [Multiply]) ++ is) v
  stack =
run is v (interp e1 v * interp e2 v :: stack)
    rewrite <- app_assoc.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile e1 ++ (compile e2 ++ [Multiply]) ++ is) v
  stack =
run is v (interp e1 v * interp e2 v :: stack)
    rewrite IHe1.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ((compile e2 ++ [Multiply]) ++ is) v
  (interp e1 v :: stack) =
run is v (interp e1 v * interp e2 v :: stack)
    rewrite <- app_assoc.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run (compile e2 ++ [Multiply] ++ is) v
  (interp e1 v :: stack) =
run is v (interp e1 v * interp e2 v :: stack)
    rewrite IHe2.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run ([Multiply] ++ is) v
  (interp e2 v :: interp e1 v :: stack) =
run is v (interp e1 v * interp e2 v :: stack)
    simpl in *.e1, e2: arith
IHe1: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e1 ++ is) v stack =
run is v (interp e1 v :: stack)
IHe2: forall (v : valuation) (is : list instruction)
  (stack : list nat),
run (compile e2 ++ is) v stack =
run is v (interp e2 v :: stack)
v: valuation
is: list instruction
stack: list nat
run is v (interp e1 v * interp e2 v :: stack) =
run is v (interp e1 v * interp e2 v :: stack)
    congruence.
Qed.

The overall compiler correctness theorem is essentially a corollary of the above lemma.

Theorem compile_ok : forall e v,
    run (compile e) v nil = interp e v :: nil.forall (e : arith) (v : valuation),
run (compile e) v [] = [interp e v]
Proof.forall (e : arith) (v : valuation),
run (compile e) v [] = [interp e v]
  intros.e: arith
v: valuation
run (compile e) v [] = [interp e v] simpl.e: arith
v: valuation
run (compile e) v [] = [interp e v]
  rewrite <- (app_nil_r (compile e)).e: arith
v: valuation
run (compile e ++ []) v [] = [interp e v]
  apply compile_ok'.
Qed.

A Language of Imperative Commands

Working with expressions is fun, but for a more realistic example, let's consider a simple imperative language with assignment, sequence, and bounded loops. Note that we use Repeat rather than While to avoid any potential complications with termination.

Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| Repeat (e : arith) (body : cmd).

To define the interpreter for this language, it will be convenient to have a self-composition operator that computes the n-ary iteration of a function f. Note that this operator is defined purely semantically, in Coq's dependent type theory.

Fixpoint selfCompose {A} (f : A -> A) (n : nat) : A -> A :=
  match n with
  | O => fun x => x
  | S n' => fun x => selfCompose f n' (f x)
  end.

The following lemma will come in handy later: self-composition gives the same result, when passed two functions that map equal inputs to equal outputs.

Lemma selfCompose_extensional : forall {A} (f g : A -> A) n x,
  (forall y, f y = g y)
  -> selfCompose f n x = selfCompose g n x.forall (A : Type) (f g : A -> A) (n : nat) (x : A),
(forall y : A, f y = g y) ->
selfCompose f n x = selfCompose g n x
Proof.forall (A : Type) (f g : A -> A) (n : nat) (x : A),
(forall y : A, f y = g y) ->
selfCompose f n x = selfCompose g n x
  induction n.A: Type
f, g: A -> A
forall x : A,
(forall y : A, f y = g y) ->
selfCompose f 0 x = selfCompose g 0 x
A: Type
f, g: A -> A
n: nat
IHn: forall x : A,
(forall y : A, f y = g y) -> selfCompose f n x = selfCompose g n x
forall x : A,
(forall y : A, f y = g y) ->
selfCompose f (S n) x = selfCompose g (S n) x
  -A: Type
f, g: A -> A
forall x : A,
(forall y : A, f y = g y) ->
selfCompose f 0 x = selfCompose g 0 x reflexivity.
  -A: Type
f, g: A -> A
n: nat
IHn: forall x : A,
(forall y : A, f y = g y) -> selfCompose f n x = selfCompose g n x
forall x : A,
(forall y : A, f y = g y) ->
selfCompose f (S n) x = selfCompose g (S n) x intros.A: Type
f, g: A -> A
n: nat
IHn: forall x : A,
(forall y : A, f y = g y) -> selfCompose f n x = selfCompose g n x
x: A
H: forall y : A, f y = g y
selfCompose f (S n) x = selfCompose g (S n) x
    simpl.A: Type
f, g: A -> A
n: nat
IHn: forall x : A,
(forall y : A, f y = g y) -> selfCompose f n x = selfCompose g n x
x: A
H: forall y : A, f y = g y
selfCompose f n (f x) = selfCompose g n (g x)
    rewrite H.A: Type
f, g: A -> A
n: nat
IHn: forall x : A,
(forall y : A, f y = g y) -> selfCompose f n x = selfCompose g n x
x: A
H: forall y : A, f y = g y
selfCompose f n (g x) = selfCompose g n (g x)
    apply IHn.A: Type
f, g: A -> A
n: nat
IHn: forall x : A,
(forall y : A, f y = g y) -> selfCompose f n x = selfCompose g n x
x: A
H: forall y : A, f y = g y
forall y : A, f y = g y
    trivial.
Qed.

Now we can define the semantics for our imperative language.

Fixpoint exec (c : cmd) (v : valuation) : valuation :=
  match c with
  | Skip => v
  | Assign x e => set x (interp e v) v
  | Sequence c1 c2 => exec c2 (exec c1 v)
  | Repeat e body => selfCompose (exec body) (interp e v) v
  end.

As an example program transformation, we can define an optimizer that unrolls loops when the bound is a constant. We'll first define a helper function that sequentially composes a command c with itself n times.

Fixpoint seqself (c : cmd) (n : nat) : cmd :=
  match n with
  | O => Skip
  | S n' => Sequence c (seqself c n')
  end.

Loop Unrolling

Then we can define the unrolling operator itself.

Fixpoint unroll (c : cmd) : cmd :=
  match c with
  | Skip => c
  | Assign _ _ => c
  | Sequence c1 c2 => Sequence (unroll c1) (unroll c2)
  | Repeat (Const n) c1 => seqself (unroll c1) n
  | Repeat e c1 => Repeat e (unroll c1)
  end.

The crucial lemma for the soundness of unroll says that seqself behaves like selfCompose with respect to the semantics computed by the interpreter.

Lemma seqself_ok : forall c n v,
  exec (seqself c n) v = selfCompose (exec c) n v.forall (c : cmd) (n : nat) (v : valuation),
exec (seqself c n) v = selfCompose (exec c) n v
Proof.forall (c : cmd) (n : nat) (v : valuation),
exec (seqself c n) v = selfCompose (exec c) n v
  induction n; simpl; congruence.
Qed.

Now we can prove the main soundness theorem for loop unrolling.

Theorem unroll_ok : forall c v, exec (unroll c) v = exec c v.forall (c : cmd) (v : valuation),
exec (unroll c) v = exec c v
Proof.forall (c : cmd) (v : valuation),
exec (unroll c) v = exec c v
  induction c.forall v : valuation,
exec (unroll Skip) v = exec Skip v
x: var
e: arith
forall v : valuation,
exec (unroll (Assign x e)) v = exec (Assign x e) v
c1, c2: cmd
IHc1: forall v : valuation,
exec (unroll c1) v = exec c1 v
IHc2: forall v : valuation,
exec (unroll c2) v = exec c2 v
forall v : valuation,
exec (unroll (Sequence c1 c2)) v =
exec (Sequence c1 c2) v
e: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
forall v : valuation,
exec (unroll (Repeat e c)) v = exec (Repeat e c) v
  -forall v : valuation,
exec (unroll Skip) v = exec Skip v reflexivity.
  -x: var
e: arith
forall v : valuation,
exec (unroll (Assign x e)) v = exec (Assign x e) v reflexivity.
  -c1, c2: cmd
IHc1: forall v : valuation,
exec (unroll c1) v = exec c1 v
IHc2: forall v : valuation,
exec (unroll c2) v = exec c2 v
forall v : valuation,
exec (unroll (Sequence c1 c2)) v =
exec (Sequence c1 c2) v simpl.c1, c2: cmd
IHc1: forall v : valuation,
exec (unroll c1) v = exec c1 v
IHc2: forall v : valuation,
exec (unroll c2) v = exec c2 v
forall v : valuation,
exec (unroll c2) (exec (unroll c1) v) =
exec c2 (exec c1 v) congruence.
  -e: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
forall v : valuation,
exec (unroll (Repeat e c)) v = exec (Repeat e c) v intros.e: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (unroll (Repeat e c)) v = exec (Repeat e c) v simpl in *.e: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec
  match e with
  | Const n => seqself (unroll c) n
  | _ => Repeat e (unroll c)
  end v = selfCompose (exec c) (interp e v) v
    destruct e.n: nat
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (seqself (unroll c) n) v =
selfCompose (exec c) (interp (Const n) v) v
x: var
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Var x) (unroll c)) v =
selfCompose (exec c) (interp (Var x) v) v
e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Plus e1 e2) (unroll c)) v =
selfCompose (exec c) (interp (Plus e1 e2) v) v
e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Minus e1 e2) (unroll c)) v =
selfCompose (exec c) (interp (Minus e1 e2) v) v
e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Times e1 e2) (unroll c)) v =
selfCompose (exec c) (interp (Times e1 e2) v) v
    +n: nat
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (seqself (unroll c) n) v =
selfCompose (exec c) (interp (Const n) v) v simpl.n: nat
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (seqself (unroll c) n) v =
selfCompose (exec c) n v
      rewrite seqself_ok.n: nat
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
selfCompose (exec (unroll c)) n v =
selfCompose (exec c) n v
      apply selfCompose_extensional.n: nat
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
forall y : valuation, exec (unroll c) y = exec c y
      trivial.
    +x: var
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Var x) (unroll c)) v =
selfCompose (exec c) (interp (Var x) v) v apply selfCompose_extensional.x: var
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
forall y : valuation,
(fix exec (c : cmd) (v : valuation) {struct c} :
     valuation :=
   match c with
   | Skip => v
   | Assign x e => set x (interp e v) v
   | Sequence c1 c2 => exec c2 (exec c1 v)
   | Repeat e body =>
       selfCompose (exec body) (interp e v) v
   end) (unroll c) y = exec c y
      trivial.
    +e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Plus e1 e2) (unroll c)) v =
selfCompose (exec c) (interp (Plus e1 e2) v) v apply selfCompose_extensional.e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
forall y : valuation,
(fix exec (c : cmd) (v : valuation) {struct c} :
     valuation :=
   match c with
   | Skip => v
   | Assign x e => set x (interp e v) v
   | Sequence c1 c2 => exec c2 (exec c1 v)
   | Repeat e body =>
       selfCompose (exec body) (interp e v) v
   end) (unroll c) y = exec c y
      trivial.
    +e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Minus e1 e2) (unroll c)) v =
selfCompose (exec c) (interp (Minus e1 e2) v) v apply selfCompose_extensional.e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
forall y : valuation,
(fix exec (c : cmd) (v : valuation) {struct c} :
     valuation :=
   match c with
   | Skip => v
   | Assign x e => set x (interp e v) v
   | Sequence c1 c2 => exec c2 (exec c1 v)
   | Repeat e body =>
       selfCompose (exec body) (interp e v) v
   end) (unroll c) y = exec c y
      trivial.
    +e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
exec (Repeat (Times e1 e2) (unroll c)) v =
selfCompose (exec c) (interp (Times e1 e2) v) v apply selfCompose_extensional.e1, e2: arith
c: cmd
IHc: forall v : valuation,
exec (unroll c) v = exec c v
v: valuation
forall y : valuation,
(fix exec (c : cmd) (v : valuation) {struct c} :
     valuation :=
   match c with
   | Skip => v
   | Assign x e => set x (interp e v) v
   | Sequence c1 c2 => exec c2 (exec c1 v)
   | Repeat e body =>
       selfCompose (exec body) (interp e v) v
   end) (unroll c) y = exec c y
      trivial.
Qed.