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
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
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.