Coq: when general is simpler
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.