Today I learned a thing about generalization: sometimes it is the only way to solve a problem even though it may be quite non-obvious.

At the moment I am reading “Software Foundations” by B. Pierce and currently I’m making my way through `Imp.v`. It shows a tiny language of arithmetical expressions (pure and halting!):

``````(** Syntax *)
Inductive aexp : Type :=
| ANum : nat -> aexp
| AId : id -> aexp
| APlus : aexp -> aexp -> aexp
| AMinus : aexp -> aexp -> aexp
| AMult : aexp -> aexp -> aexp.
(** Evaluation *)
Fixpoint aeval (st : state) (a : aexp) : nat :=
match a with
| ANum n => n
| AId x => st x
| APlus a1 a2 => (aeval st a1) + (aeval st a2)
| AMinus a1 a2 => (aeval st a1) - (aeval st a2)
| AMult a1 a2 => (aeval st a1) * (aeval st a2)
end.
``````

and a tiny virtual machine for evaluating expressions in this language:

It is stack-based (it loads constants or values from an environment on stack and leaves its result there):

``````Fixpoint s_execute (st: state) (stack: list nat) (prog: list sinstr) : list nat
(**
I will not post the body of this function to fulfil
the request of the book author to avoid posting solutions
to exercises in public; the only thing I say about it is
that my version ignores stack underflow: the stack is
not changed by [SPlus]/[SMult]/[SMinus] if there are
less than two values on it
**)
``````

The next necessity is a compiler from `aexp` to `list sinst`:

``````Fixpoint s_compile (e : aexp) : list sinstr := (* censored *)
``````

The climax of this exercise is proving `s_compile` correct, i.e.

``````Theorem s_compile_correct : forall (st : state) (e : aexp),
s_execute st [] (s_compile e) = [ aeval st e ].
``````

(I hope that the following text does not count as a ready solution, rather as a hint).

After some fiddling with the assertion, it became obvious that it would be useful to define small-step lemmas:

``````Lemma s_execute_step :
forall (st : state) (s : list nat) (i : sinstr) (p : list sinstr),
s_execute st s (i :: p) = s_execute st (s_execute st s [i]) p.

Lemma s_execute_map :
forall (st : state) (s : list nat) (p1 p2 : list sinstr),
s_execute st s (p1 ++ p2) = s_execute st (s_execute st s p1) p2.
``````

Having been armed with this lemmas, I started tackling the theorem. Quite quickly I decided to assert that the language of aexp cannot modify the stack below its expression (`s_compile` never produces a `list sinstr` that underflows the stack):

``````Lemma aexp_never_underflows:
forall (st : state) (s : list nat) (e : aexp) (v : nat),
s_execute st [] (s_compile e) = [v] -> s_execute st s (s_compile e) = v :: s.
``````

and tried to prove this lemma. The funny thing was that this lemma seemed to be dependent on `s_compile_correct` and vice versa! After some time (I am omitting the related emotional rollercoaster) I realized that it’s not going to work and tried to step back to get the big picture. The lucky idea was to combine the lemmas into one (why not?):

``````Lemma s_compile_correct_s :
forall (st : state) (e : aexp) (s : list nat),
s_execute st s (s_compile e) = (aeval st e :: s).
``````

As soon as I had it written down, I realized that it’s not a lemma, it’s the theorem I am going after! It’s a more general version of `s_compile_correct` that I’ve been told to prove! To save your time scrolling back, here is `s_compile_correct`:

``````Theorem s_compile_correct :
forall (st : state) (e : aexp),
s_execute st [] (s_compile e) = [ aeval st e ].
Proof.
intros. apply s_compile_correct_s.
(* I hope this solution is trivial enough to publish it *)
Qed.
``````

`s_compile_correct_s` was not the easiest thing to prove, but it was doable and straightforward, compared to my previous roundabout wandering in the maze of special cases.

Conclusion: Even though I knew the concept that some problems are much easier in a generalized form, this exercise was a real eye-opener: sometimes it takes a lot of time and effort to recognize a subtle need for generalization.