Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

# Chapter 4: Semantics via Interpreters

Authors: Adam Chlipala A chapter from FRAP (CC-BY), used to demo Alectryon

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

 [1] good pun, right?
```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:valuationn:natn = nv:valuationx:varmatch v \$? x with
| Some n => n
| None => 0
end = match v \$? x with
| Some n => n
| None => 0
endv:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp (commuter e2) v + interp (commuter e1) v =
interp e1 v + interp e2 vv:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp (commuter e1) v - interp (commuter e2) v =
interp e1 v - interp e2 vv:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp (commuter e2) v * interp (commuter e1) v =
interp e1 v * interp e2 v
-v:valuationn:natn = n equality.
-v:valuationx:varmatch v \$? x with
| Some n => n
| None => 0
end = match v \$? x with
| Some n => n
| None => 0
end equality.
-v:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp (commuter e2) v + interp (commuter e1) v =
interp e1 v + interp e2 v linear_arithmetic.
-v:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp (commuter e1) v - interp (commuter e2) v =
interp e1 v - interp e2 v equality.
-v:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp (commuter e2) v * interp (commuter e1) v =
interp e1 v * interp e2 v rewrite IHe1.v:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp (commuter e2) v * interp e1 v =
interp e1 v * interp e2 v
rewrite IHe2.v:valuatione1, e2:arithIHe1:interp (commuter e1) v = interp e1 vIHe2:interp (commuter e2) v = interp e2 vinterp 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:valuationreplaceThis:varwithThis:arithx:varinterp (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:arithIHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0v:valuationinterp
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 ve1, e2:arithIHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0v:valuationinterp
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:arithIHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0v:valuationinterp
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:nate2:arithIHe1:valuation -> n = nIHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0v:valuationinterp
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:arithIHe1:forall v0 : valuation,
interp (doSomeArithmetic e1) v0 = interp e1 v0IHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0v:valuationinterp
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:nate2:arithIHe1:valuation -> n = nIHe2:forall v0 : valuation,
interp (doSomeArithmetic e2) v0 = interp e2 v0v:valuationinterp
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)
| 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
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:natv:valuationis:list instructionstack:list natrun is v (n :: stack) = run is v (n :: stack)x:varv:valuationis:list instructionstack:list natrun 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:arithIHe1: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:valuationis:list instructionstack:list natrun ((compile e1 ++ compile e2 ++ [Add]) ++ is) v
stack =
run is v (interp e1 v + interp e2 v :: stack)e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((compile e1 ++ compile e2 ++ [Subtract]) ++ is) v
stack =
run is v (interp e1 v - interp e2 v :: stack)e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((compile e1 ++ compile e2 ++ [Multiply]) ++ is) v
stack =
run is v (interp e1 v * interp e2 v :: stack)

-n:natv:valuationis:list instructionstack:list natrun is v (n :: stack) = run is v (n :: stack) equality.
-x:varv:valuationis:list instructionstack:list natrun 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:arithIHe1: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:valuationis:list instructionstack:list natrun ((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 ++ napp_assoc:
forall (A : Type) (l m n : list A),
l ++ m ++ n = (l ++ m) ++ ne1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((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:arithIHe1: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:valuationis:list instructionstack:list natrun (compile e1 ++ (compile e2 ++ [Add]) ++ is) v
stack =
run is v (interp e1 v + interp e2 v :: stack)
rewrite IHe1.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((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:arithIHe1: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:valuationis:list instructionstack:list natrun (compile e2 ++ [Add] ++ is) v
(interp e1 v :: stack) =
run is v (interp e1 v + interp e2 v :: stack)
rewrite IHe2.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ([Add] ++ is) v
(interp e2 v :: interp e1 v :: stack) =
run is v (interp e1 v + interp e2 v :: stack)
simplify.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun is v (interp e1 v + interp e2 v :: stack) =
run is v (interp e1 v + interp e2 v :: stack)
equality.

-e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((compile e1 ++ compile e2 ++ [Subtract]) ++ is) v
stack =
run is v (interp e1 v - interp e2 v :: stack) rewrite app_assoc_reverse.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun (compile e1 ++ (compile e2 ++ [Subtract]) ++ is) v
stack =
run is v (interp e1 v - interp e2 v :: stack)
rewrite IHe1.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((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:arithIHe1: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:valuationis:list instructionstack:list natrun (compile e2 ++ [Subtract] ++ is) v
(interp e1 v :: stack) =
run is v (interp e1 v - interp e2 v :: stack)
rewrite IHe2.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ([Subtract] ++ is) v
(interp e2 v :: interp e1 v :: stack) =
run is v (interp e1 v - interp e2 v :: stack)
simplify.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun is v (interp e1 v - interp e2 v :: stack) =
run is v (interp e1 v - interp e2 v :: stack)
equality.

-e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((compile e1 ++ compile e2 ++ [Multiply]) ++ is) v
stack =
run is v (interp e1 v * interp e2 v :: stack) rewrite app_assoc_reverse.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun (compile e1 ++ (compile e2 ++ [Multiply]) ++ is) v
stack =
run is v (interp e1 v * interp e2 v :: stack)
rewrite IHe1.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ((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:arithIHe1: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:valuationis:list instructionstack:list natrun (compile e2 ++ [Multiply] ++ is) v
(interp e1 v :: stack) =
run is v (interp e1 v * interp e2 v :: stack)
rewrite IHe2.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun ([Multiply] ++ is) v
(interp e2 v :: interp e1 v :: stack) =
run is v (interp e1 v * interp e2 v :: stack)
simplify.e1, e2:arithIHe1: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:valuationis:list instructionstack:list natrun 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:arithv:valuationrun (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 ++ [] = le:arithv:valuationrun (compile e) v [] = [interp e v]
rewrite (app_nil_end (compile e)).e:arithv:valuationrun (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:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputv = v \$+ ("input", 0) \$+ ("output", output * 1)input:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some outputselfCompose
(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))```

maps_equal

This tactic proves that two finite maps are equal by considering all the relevant cases for mappings of different keys.

```  -output:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputv = v \$+ ("input", 0) \$+ ("output", output * 1) maps_equal.output:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputv \$? "output" = Some (output * 1)output:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputH1:"output" <> "input"v \$? "input" = Some 0

+output:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputv \$? "output" = Some (output * 1) rewrite H0.output:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputSome output = Some (output * 1)
f_equal.output:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputoutput = output * 1
linear_arithmetic.```

trivial

Coq maintains a database of simple proof steps, such as proving a fact by direct appeal to a matching hypothesis. trivial asks to try all such simple steps.

```    +output:natv:fmap var natH:v \$? "input" = Some 0H0:v \$? "output" = Some outputH1:"output" <> "input"v \$? "input" = Some 0 trivial.

-input:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some outputselfCompose
(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:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some outputselfCompose
(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:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some outputv \$+ ("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:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some output(v \$+ ("output", output * S input) \$+ ("input",
S input - 1)) \$? "input" =
Some inputinput:natIHinput: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:natv:fmap var natH: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:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some outputSome (output * S input * fact input) =
Some (output * (fact input + input * fact input))input:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some output(v \$+ ("output", output * S input) \$+ ("input",
S input - 1)) \$? "input" =
Some inputinput:natIHinput: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:natv:fmap var natH: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:natIHinput: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:natv:fmap var natH:v \$? "input" = Some (S input)H0:v \$? "output" = Some outputSome (output * S input * fact input) =
Some (output * (fact input + input * fact input)) f_equal; ring.
+input:natIHinput: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:natv:fmap var natH: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:natIHinput: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:natv:fmap var natH: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 natinput:natH:v \$? "input" = Some inputselfCompose
(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 natinput:natH:v \$? "input" = Some inputselfCompose
(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 natinput:natH:v \$? "input" = Some inputSome (fact input + 0) = Some (fact input)v:fmap var natinput:natH:v \$? "input" = Some inputv \$? "input" = Some inputv:fmap var natinput:natH:v \$? "input" = Some inputSome 1 = Some 1
f_equal; linear_arithmetic.v:fmap var natinput:natH:v \$? "input" = Some inputv \$? "input" = Some inputv:fmap var natinput:natH:v \$? "input" = Some inputSome 1 = Some 1
trivial.v:fmap var natinput:natH:v \$? "input" = Some inputSome 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:Typef, g:A -> An:natIHn:forall x0 : A,
(forall y : A, f y = g y) -> selfCompose f n x0 = selfCompose g n x0x:AH:forall y : A, f y = g yselfCompose f n (f x) = selfCompose g n (g x)

rewrite H.A:Typef, g:A -> An:natIHn:forall x0 : A,
(forall y : A, f y = g y) -> selfCompose f n x0 = selfCompose g n x0x:AH:forall y : A, f y = g yselfCompose f n (g x) = selfCompose g n (g x)
apply IHn.A:Typef, g:A -> An:natIHn:forall x0 : A,
(forall y : A, f y = g y) -> selfCompose f n x0 = selfCompose g n x0x:AH:forall y : A, f y = g yforall 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:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationexec
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:natc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationexec (seqself (unroll c) n) v =
selfCompose (exec c) n vx:varc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (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 ve1, e2:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (exec (unroll c))
(interp e1 v + interp e2 v) v =
selfCompose (exec c) (interp e1 v + interp e2 v) ve1, e2:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (exec (unroll c))
(interp e1 v - interp e2 v) v =
selfCompose (exec c) (interp e1 v - interp e2 v) ve1, e2:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (exec (unroll c))
(interp e1 v * interp e2 v) v =
selfCompose (exec c) (interp e1 v * interp e2 v) v

-n:natc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationexec (seqself (unroll c) n) v =
selfCompose (exec c) n v rewrite seqself_ok.n:natc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (exec (unroll c)) n v =
selfCompose (exec c) n v
apply selfCompose_extensional.n:natc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationforall y : valuation, exec (unroll c) y = exec c y
trivial.

-x:varc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (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:varc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationforall y : valuation, exec (unroll c) y = exec c y
trivial.

-e1, e2:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (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:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationforall y : valuation, exec (unroll c) y = exec c y
trivial.

-e1, e2:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (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:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationforall y : valuation, exec (unroll c) y = exec c y
trivial.

-e1, e2:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationselfCompose (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:arithc:cmdIHc:forall v0 : valuation, exec (unroll c) v0 = exec c v0v:valuationforall y : valuation, exec (unroll c) y = exec c y
trivial.
Qed.```