Chapter 4: Semantics via Interpreters

We begin with a return to our arithmetic language from the last chapter, adding subtraction [1], which will come in handy later.

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

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

The above definition only explains what programs look like. We also care about what they mean. The natural meaning of an expression is the number it evaluates to. Actually, it's not quite that simple. We need to consider the meaning to be a function over a valuation to the variables, which in turn is itself a finite map from variable names to numbers. We use the book library's map type family.

Definition valuation := fmap var nat.

That is, the domain is var (a synonym for string) and the codomain/range is nat.

The interpreter is a fairly innocuous-looking recursive function:

Fixpoint interp (e : arith) (v : valuation) : nat :=
  match e with
  | Const n => n
  | Var x =>
    (* Note use of infix operator to look up a key in a finite map. *)
    match v $? x with
    | None => 0 (* goofy default value! *)
    | Some n => n
    end
  | Plus e1 e2 => interp e1 v + interp e2 v
  | Minus e1 e2 => interp e1 v - interp e2 v
                   (* For anyone who's wondering: this [-] sticks at 0,
                    * if we would otherwise underflow. *)
  | Times e1 e2 => interp e1 v * interp e2 v
  end.

Here's an example valuation, using an infix operator for map extension.

Definition valuation0 : valuation :=
  $0 $+ ("x", 17) $+ ("y", 3).

Unfortunately, we can't execute code based on finite maps, since, for convenience, they use uncomputable features. The reason is that we need a comparison function, a hash function, etc., to do computable finite-map implementation, and such things are impossible to compute automatically for all types in Coq. However, we can still prove theorems about execution of finite-map programs, and the simplify tactic knows how to reduce the key constructions.

Theorem interp_ex1 : interp ex1 valuation0 = 42.
interp ex1 valuation0 = 42
  simplify.
42 = 42
  equality.
Qed.

Theorem interp_ex2 : interp ex2 valuation0 = 54.
interp ex2 valuation0 = 54
  unfold valuation0.
interp ex2 ($0 $+ ("x", 17) $+ ("y", 3)) = 54
  simplify.
54 = 54
  equality.
Qed.

Here's the silly transformation we defined last time.

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)
                   (* ^-- NB: didn't change the operand order here! *)
  | Times e1 e2 => Times (commuter e2) (commuter e1)
  end.

Instead of proving various odds-and-ends properties about it, let's show what we really care about: it preserves the meanings of expressions!

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
  induct e; simplify.
v:valuation
n:nat
n = n
v:valuation
x:var
match v $? x with
| Some n => n
| None => 0
end = match v $? x with
      | Some n => n
      | None => 0
      end
v:valuation
e1, e2:arith
IHe1:interp (commuter e1) v = interp e1 v
IHe2:interp (commuter e2) v = interp e2 v
interp (commuter e2) v + interp (commuter e1) v =
interp e1 v + interp 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 e1) v - interp (commuter e2) v =
interp e1 v - interp 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 e2) v * interp (commuter e1) v =
interp e1 v * interp e2 v
  -
v:valuation
n:nat
n = n equality.
  -
v:valuation
x:var
match v $? x with
| Some n => n
| None => 0
end = match v $? x with
      | Some n => n
      | None => 0
      end equality.
  -
v:valuation
e1, e2:arith
IHe1:interp (commuter e1) v = interp e1 v
IHe2:interp (commuter e2) v = interp e2 v
interp (commuter e2) v + interp (commuter e1) v =
interp e1 v + interp e2 v linear_arithmetic.
  -
v:valuation
e1, e2:arith
IHe1:interp (commuter e1) v = interp e1 v
IHe2:interp (commuter e2) v = interp e2 v
interp (commuter e1) v - interp (commuter e2) v =
interp e1 v - interp e2 v equality.
  -
v:valuation
e1, e2:arith
IHe1:interp (commuter e1) v = interp e1 v
IHe2:interp (commuter e2) v = interp e2 v
interp (commuter e2) v * interp (commuter e1) v =
interp e1 v * interp e2 v rewrite IHe1.
v:valuation
e1, e2:arith
IHe1:interp (commuter e1) v = interp e1 v
IHe2:interp (commuter e2) v = interp e2 v
interp (commuter e2) v * interp e1 v =
interp e1 v * interp e2 v
    rewrite IHe2.
v:valuation
e1, e2:arith
IHe1:interp (commuter e1) v = interp e1 v
IHe2:interp (commuter e2) v = interp e2 v
interp e2 v * interp e1 v = interp e1 v * interp e2 v
    ring.
Qed.

Well, that's a relief! ;-)

Let's also revisit substitution.

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

Theorem substitute_ok : forall v replaceThis withThis inThis,
  interp (substitute inThis replaceThis withThis) v
  = interp inThis (v $+ (replaceThis, interp withThis v)).
forall (v : valuation) (replaceThis : var)
  (withThis inThis : arith),
interp (substitute inThis replaceThis withThis) v =
interp inThis (v $+ (replaceThis, interp withThis v))
  induct inThis; simplify; try equality.
v:valuation
replaceThis:var
withThis:arith
x:var
interp (if x ==v replaceThis then withThis else Var x)
  v =
match
  (v $+ (replaceThis, interp withThis v)) $? x
with
| Some n => n
| None => 0
end

One case left after our basic heuristic: the variable case, naturally!

  cases (x ==v replaceThis); simplify; try equality.
Qed.

Great; we seem to have gotten that one right, too.

Let's also defined a pared-down version of the expression-simplificaton functions from last chapter.

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

Theorem doSomeArithmetic_ok :
    forall e v, interp (doSomeArithmetic e) v = interp e v.
forall (e : arith) (v : valuation),
interp (doSomeArithmetic e) v = interp e v
  induct e; simplify; try equality.
e1, e2:arith
IHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0
IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0
v:valuation
interp
  match e1 with
  | Const n1 =>
      match e2 with
      | Const n2 => Const (n1 + n2)
      | _ =>
          Plus (doSomeArithmetic e1)
            (doSomeArithmetic e2)
      end
  | _ =>
      Plus (doSomeArithmetic e1) (doSomeArithmetic e2)
  end v = interp e1 v + interp e2 v
e1, e2:arith
IHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0
IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0
v:valuation
interp
  match e1 with
  | Const n1 =>
      match e2 with
      | Const n2 => Const (n1 * n2)
      | _ =>
          Times (doSomeArithmetic e1)
            (doSomeArithmetic e2)
      end
  | _ =>
      Times (doSomeArithmetic e1)
        (doSomeArithmetic e2)
  end v = interp e1 v * interp e2 v

  -
e1, e2:arith
IHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0
IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0
v:valuation
interp
  match e1 with
  | Const n1 =>
      match e2 with
      | Const n2 => Const (n1 + n2)
      | _ =>
          Plus (doSomeArithmetic e1)
            (doSomeArithmetic e2)
      end
  | _ =>
      Plus (doSomeArithmetic e1) (doSomeArithmetic e2)
  end v = interp e1 v + interp e2 v cases e1; simplify; try equality.
n:nat
e2:arith
IHe1:valuation -> n = n
IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0
v:valuation
interp
  match e2 with
  | Const n2 => Const (n + n2)
  | _ => Plus (Const n) (doSomeArithmetic e2)
  end v = n + interp e2 v
    cases e2; simplify; equality.

  -
e1, e2:arith
IHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0
IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0
v:valuation
interp
  match e1 with
  | Const n1 =>
      match e2 with
      | Const n2 => Const (n1 * n2)
      | _ =>
          Times (doSomeArithmetic e1)
            (doSomeArithmetic e2)
      end
  | _ =>
      Times (doSomeArithmetic e1)
        (doSomeArithmetic e2)
  end v = interp e1 v * interp e2 v cases e1; simplify; try equality.
n:nat
e2:arith
IHe1:valuation -> n = n
IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0
v:valuation
interp
  match e2 with
  | Const n2 => Const (n * n2)
  | _ => Times (Const n) (doSomeArithmetic e2)
  end v = n * interp e2 v
    cases e2; simplify; equality.
Qed.

Of course, we're going to get bored if we confine ourselves to arithmetic expressions for the rest of our journey. Let's get a bit fancier and define a stack machine, related to postfix calculators that some of you may have experienced.

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

What does it all mean? An interpreter tells us unambiguously!

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

That function explained how to run one instruction. Here's how to run several of them.

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.

Instead of writing fiddly stack programs ourselves, let's compile arithmetic expressions into equivalent stack programs.

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.

Now, of course, we should prove our compiler correct. Skip down to the next theorem to see the overall correctness statement. It turns out that we need to strengthen the induction hypothesis with a lemma, to push the proof through.

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)
  induct e; simplify.
n:nat
v:valuation
is:list instruction
stack:list nat
run is v (n :: stack) = run is v (n :: stack)
x:var
v:valuation
is:list instruction
stack:list nat
run is v
  (match v $? x with
   | Some n => n
   | None => 0
   end :: stack) =
run is v
  (match v $? x with
   | Some n => n
   | None => 0
   end :: stack)
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)

  -
n:nat
v:valuation
is:list instruction
stack:list nat
run is v (n :: stack) = run is v (n :: stack) equality.
  -
x:var
v:valuation
is:list instruction
stack:list nat
run is v
  (match v $? x with
   | Some n => n
   | None => 0
   end :: stack) =
run is v
  (match v $? x with
   | Some n => n
   | None => 0
   end :: stack) equality.
  -
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)

Here we want to use associativity of ++, to get the conclusion to match an induction hypothesis. Let's ask Coq to search its library for lemmas that would justify such a rewrite, giving a pattern with wildcards, to specify the essential structure that the rewrite should match.

    SearchRewrite ((_ ++ _) ++ _).
app_assoc_reverse:
  forall (A : Type) (l m n : list A),
  (l ++ m) ++ n = l ++ m ++ n
app_assoc:
  forall (A : Type) (l m n : list A),
  l ++ m ++ n = (l ++ m) ++ n
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)

Ah, we see just the one!

    rewrite app_assoc_reverse.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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 (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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_reverse.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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 (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
    simplify.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
    equality.

  -
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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_reverse.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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 (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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_reverse.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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 (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
    simplify.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
    equality.

  -
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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_reverse.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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 (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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_reverse.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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 (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
    simplify.
e1, e2:arith
IHe1:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e1 ++ is0) v0 stack0 =
run is0 v0 (interp e1 v0 :: stack0)
IHe2:forall (v0 : valuation)
  (is0 : list instruction) 
  (stack0 : list nat),
run (compile e2 ++ is0) v0 stack0 =
run is0 v0 (interp e2 v0 :: stack0)
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)
    equality.
Qed.

The overall theorem follows as a simple corollary.

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]
  simplify.
e:arith
v:valuation
run (compile e) v [] = [interp e v]

To match the form of our lemma, we need to replace compile e with compile e ++ nil, adding a "pointless" concatenation of the empty list. SearchRewrite again helps us find a library lemma.

  SearchRewrite (_ ++ nil).
app_nil_end:
  forall (A : Type) (l : list A), l = l ++ []
app_nil_r: forall (A : Type) (l : list A), l ++ [] = l
e:arith
v:valuation
run (compile e) v [] = [interp e v]
  rewrite (app_nil_end (compile e)).
e:arith
v:valuation
run (compile e ++ []) v [] = [interp e v]

Note that we can use rewrite with explicit values of the first few quantified variables of a lemma. Otherwise, rewrite picks an unhelpful place to rewrite. (Try it and see!)

  apply compile_ok'.
  (* Direct appeal to a previously proved lemma *)
Qed.

Let's get a bit fancier, moving toward the level of general-purpose imperative languages. Here's a language of commands, building on the language of expressions we have defined.

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

That last constructor is for repeating a body command some number of times. Note that we sneakily avoid constructs that could introduce nontermination, since Coq only accepts terminating programs, and we want to write an interpreter for commands. In contrast to our last one, this interpreter transforms valuations. We use a helper function for self-composing a function some number of times.

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.

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

Let's define some programs and prove that they operate in certain ways.

Example factorial_ugly :=
  Sequence
    (Assign "output" (Const 1))
    (Repeat (Var "input")
            (Sequence
               (Assign "output" (Times (Var "output") (Var "input")))
               (Assign "input" (Minus (Var "input") (Const 1))))).

Ouch; that code is hard to read. Let's introduce some notations to make the concrete syntax more palatable. We won't explain the general mechanisms on display here, but see the Coq manual for details, or try to reverse-engineer them from our examples.

Coercion Const : nat >-> arith.
Coercion Var : var >-> arith.
Infix "+" := Plus : arith_scope.
Declaring a scope implicitly is deprecated; use in
advance an explicit "Declare Scope arith_scope.".
[undeclared-scope,deprecated]
Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope.
Delimit Scope arith_scope with arith.
Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";" := Sequence (at level 76).
Notation "'repeat' e 'doing' body 'done'" :=
  (Repeat e%arith body) (at level 75).

OK, let's try that program again.

Example factorial :=
  "output" <- 1;
  repeat "input" doing
    "output" <- "output" * "input";
    "input" <- "input" - 1
  done.

Now we prove that it really computes factorial. First, a reference implementation as a functional program.

Fixpoint fact (n : nat) : nat :=
  match n with
  | O => 1
  | S n' => n * fact n'
  end.

To prove that factorial is correct, the real action is in a lemma, to be proved by induction, showing that the loop works correctly. So, let's first assign a name to the loop body alone.

Definition factorial_body :=
  "output" <- "output" * "input";
  "input" <- "input" - 1.

Now for that lemma: self-composition of the body's semantics produces the expected changes in the valuation. Note that here we're careful to put the quantified variable input first, because the variables coming after it will need to change in the course of the induction. Try switching the order to see what goes wrong if we put input later.

Lemma factorial_ok' : forall input output v,
  v $? "input" = Some input
  -> v $? "output" = Some output
  -> selfCompose (exec factorial_body) input v
     = v $+ ("input", 0) $+ ("output", output * fact input).
forall (input output : nat) (v : fmap var nat),
v $? "input" = Some input ->
v $? "output" = Some output ->
selfCompose (exec factorial_body) input v =
v $+ ("input", 0) $+ ("output", output * fact input)
  induct input; simplify.
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
v = v $+ ("input", 0) $+ ("output", output * 1)
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
selfCompose
  (fun v0 : valuation =>
   v0 $+ ("output",
   match v0 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v0 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v0 $+ ("output",
      match v0 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v0 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input
  (v $+ ("output",
   match v $? "output" with
   | Some n => n
   | None => 0
   end *
   match v $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match v $? "input" with
   | Some n => n
   | None => 0
   end - 1)) =
v $+ ("input", 0) $+ ("output",
output * (fact input + input * fact input))

  -
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
v = v $+ ("input", 0) $+ ("output", output * 1) maps_equal.
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
v $? "output" = Some (output * 1)
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
H1:"output" <> "input"
v $? "input" = Some 0

    +
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
v $? "output" = Some (output * 1) rewrite H0.
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
Some output = Some (output * 1)
      f_equal.
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
output = output * 1
      linear_arithmetic.

    +
output:nat
v:fmap var nat
H:v $? "input" = Some 0
H0:v $? "output" = Some output
H1:"output" <> "input"
v $? "input" = Some 0 trivial.

  -
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
selfCompose
  (fun v0 : valuation =>
   v0 $+ ("output",
   match v0 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v0 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v0 $+ ("output",
      match v0 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v0 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input
  (v $+ ("output",
   match v $? "output" with
   | Some n => n
   | None => 0
   end *
   match v $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match v $? "input" with
   | Some n => n
   | None => 0
   end - 1)) =
v $+ ("input", 0) $+ ("output",
output * (fact input + input * fact input)) rewrite H, H0.
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
selfCompose
  (fun v0 : valuation =>
   v0 $+ ("output",
   match v0 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v0 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v0 $+ ("output",
      match v0 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v0 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input
  (v $+ ("output", output * S input) $+ ("input",
   S input - 1)) =
v $+ ("input", 0) $+ ("output",
output * (fact input + input * fact input))
    (* Note the two arguments to one ``rewrite``! *)

    rewrite (IHinput (output * S input)).
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
v $+ ("output", output * S input) $+ ("input",
S input - 1) $+ ("input", 0) $+ ("output",
output * S input * fact input) =
v $+ ("input", 0) $+ ("output",
output * (fact input + input * fact input))
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
(v $+ ("output", output * S input) $+ ("input",
 S input - 1)) $? "input" = 
Some input
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
(v $+ ("output", output * S input) $+ ("input",
 S input - 1)) $? "output" = 
Some (output * S input)
    (* Note the careful choice of a quantifier instantiation for the IH! *)

    maps_equal.
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
Some (output * S input * fact input) =
Some (output * (fact input + input * fact input))
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
(v $+ ("output", output * S input) $+ ("input",
 S input - 1)) $? "input" = 
Some input
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
(v $+ ("output", output * S input) $+ ("input",
 S input - 1)) $? "output" = 
Some (output * S input)
    +
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
Some (output * S input * fact input) =
Some (output * (fact input + input * fact input)) f_equal; ring.
    +
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
(v $+ ("output", output * S input) $+ ("input",
 S input - 1)) $? "input" = 
Some input simplify; f_equal; linear_arithmetic.
    +
input:nat
IHinput:forall (output0 : nat) (v0 : fmap var nat),
v0 $? "input" = Some input ->
v0 $? "output" = Some output0 ->
selfCompose
  (fun v1 : valuation =>
   v1 $+ ("output",
   match v1 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v1 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v1 $+ ("output",
      match v1 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v1 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input v0 =
v0 $+ ("input", 0) $+ ("output",
output0 * fact input)
output:nat
v:fmap var nat
H:v $? "input" = Some (S input)
H0:v $? "output" = Some output
(v $+ ("output", output * S input) $+ ("input",
 S input - 1)) $? "output" = 
Some (output * S input) simplify; equality.
Qed.

Finally, we have the natural correctness condition for factorial as a whole program.

Theorem factorial_ok
  : forall v input,
    v $? "input" = Some input
    -> exec factorial v $? "output" = Some (fact input).
forall (v : fmap var nat) (input : nat),
v $? "input" = Some input ->
exec factorial v $? "output" = Some (fact input)
  simplify.
v:fmap var nat
input:nat
H:v $? "input" = Some input
selfCompose
  (fun v0 : valuation =>
   v0 $+ ("output",
   match v0 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v0 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v0 $+ ("output",
      match v0 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v0 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1))
  match v $? "input" with
  | Some n => n
  | None => 0
  end (v $+ ("output", 1)) $? "output" =
Some (fact input)
  rewrite H.
v:fmap var nat
input:nat
H:v $? "input" = Some input
selfCompose
  (fun v0 : valuation =>
   v0 $+ ("output",
   match v0 $? "output" with
   | Some n => n
   | None => 0
   end *
   match v0 $? "input" with
   | Some n => n
   | None => 0
   end) $+ ("input",
   match
     (v0 $+ ("output",
      match v0 $? "output" with
      | Some n => n
      | None => 0
      end *
      match v0 $? "input" with
      | Some n => n
      | None => 0
      end)) $? "input"
   with
   | Some n => n
   | None => 0
   end - 1)) input (v $+ ("output", 1)) $? "output" =
Some (fact input)
  rewrite (factorial_ok' input 1); simplify.
v:fmap var nat
input:nat
H:v $? "input" = Some input
Some (fact input + 0) = Some (fact input)
v:fmap var nat
input:nat
H:v $? "input" = Some input
v $? "input" = Some input
v:fmap var nat
input:nat
H:v $? "input" = Some input
Some 1 = Some 1
  f_equal; linear_arithmetic.
v:fmap var nat
input:nat
H:v $? "input" = Some input
v $? "input" = Some input
v:fmap var nat
input:nat
H:v $? "input" = Some input
Some 1 = Some 1
  trivial.
v:fmap var nat
input:nat
H:v $? "input" = Some input
Some 1 = Some 1
  trivial.
Qed.

One last example: let's try to do loop unrolling, for constant iteration counts. That is, we can duplicate the loop body instead of using an explicit loop.

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

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
  (* ^-- the crucial case! *)
  | Repeat e c1 => Repeat e (unroll c1)
  end.

This obvious-sounding fact will come in handy: 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
  induct n; simplify; try equality.
A:Type
f, g:A -> A
n:nat
IHn:forall x0 : A,
(forall y : A, f y = g y) -> selfCompose f n x0 = selfCompose g n x0
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 x0 : A,
(forall y : A, f y = g y) -> selfCompose f n x0 = selfCompose g n x0
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 x0 : A,
(forall y : A, f y = g y) -> selfCompose f n x0 = selfCompose g n x0
x:A
H:forall y : A, f y = g y
forall y : A, f y = g y
  trivial.
Qed.

Crucial lemma: seqself is acting just like selfCompose, in a suitable sense.

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
  induct n; simplify; equality.
Qed.

The two lemmas we just proved are the main ingredients to prove the natural correctness condition for unroll.

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
  induct c; simplify; try equality.
e:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
exec
  match e with
  | Const n => seqself (unroll c) n
  | _ => repeat e doing unroll c done
  end v = selfCompose (exec c) (interp e v) v

  cases e; simplify; try equality.
n:nat
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
exec (seqself (unroll c) n) v =
selfCompose (exec c) n v
x:var
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  match v $? x with
  | Some n => n
  | None => 0
  end v =
selfCompose (exec c)
  match v $? x with
  | Some n => n
  | None => 0
  end v
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  (interp e1 v + interp e2 v) v =
selfCompose (exec c) (interp e1 v + interp e2 v) v
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  (interp e1 v - interp e2 v) v =
selfCompose (exec c) (interp e1 v - interp e2 v) v
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  (interp e1 v * interp e2 v) v =
selfCompose (exec c) (interp e1 v * interp e2 v) v

  -
n:nat
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
exec (seqself (unroll c) n) v =
selfCompose (exec c) n v rewrite seqself_ok.
n:nat
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c)) n v =
selfCompose (exec c) n v
    apply selfCompose_extensional.
n:nat
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
forall y : valuation, exec (unroll c) y = exec c y
    trivial.

  -
x:var
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  match v $? x with
  | Some n => n
  | None => 0
  end v =
selfCompose (exec c)
  match v $? x with
  | Some n => n
  | None => 0
  end v apply selfCompose_extensional.
x:var
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
forall y : valuation, exec (unroll c) y = exec c y
    trivial.

  -
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  (interp e1 v + interp e2 v) v =
selfCompose (exec c) (interp e1 v + interp e2 v) v apply selfCompose_extensional.
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
forall y : valuation, exec (unroll c) y = exec c y
    trivial.

  -
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  (interp e1 v - interp e2 v) v =
selfCompose (exec c) (interp e1 v - interp e2 v) v apply selfCompose_extensional.
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
forall y : valuation, exec (unroll c) y = exec c y
    trivial.

  -
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
selfCompose (exec (unroll c))
  (interp e1 v * interp e2 v) v =
selfCompose (exec c) (interp e1 v * interp e2 v) v apply selfCompose_extensional.
e1, e2:arith
c:cmd
IHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0
v:valuation
forall y : valuation, exec (unroll c) y = exec c y
    trivial.
Qed.