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:

Inductive id : Type := Id : nat -> id.

Inductive sinstr : Type :=
  | SPush : nat -> sinstr  (* load a constant on the stack *)
  | SLoad : id -> sinstr   (* load a value from the environment on the stack *)
  | SPlus : sinstr    (* take two values from the stack, push their sum back *)
  | SMinus : sinstr
  | SMult : sinstr.

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.