As I read through Chlipala’s Certified Programming with Dependent Types, I’m starting to understand the value of heavy proof automation. Last year I worked through Pierce et al’s Logical Foundations, which I definitely recommend starting with prior to reading through CPDT; the former gives you a very well-written introduction to Coq and its fundamental tactics, while the latter jumps right in to tying those tactics together or hiding them altogether behind higher-level automation tactics.
Obviously there is no “right” way. Personally I’ve noticed feeling greater satisfaction after solving proofs with less automation, as I can see more explicitly the development and progression of the proof than I can simply by calling crush. But having recently stepped through Chapter 5 of CPDT, I’m seeing that the relationship between manual proving and automation is akin to that between assembler and a compiled language. Relying on the compiler opens up new doors, as seems to be the case when relying on automation in Coq.
To illustrate, I’ll show how, as Chlipala suggests, “curious readers might experiment with adding command constructs like if” to the simple
cmd language that he first elaborates, then proves correct after transformation by a simple arithmetic optimization, in Chapter 5 of CPDT.
The first step is simply to add an if constructor to the inductive set of commands:
Then, we add two constructors to the co-inductive evaluation relation: one for when the conditional’s guard is false, the other for true:
Next, we modify the co-inductive principle for
evalCmd; specifically, we add a hypothesis
IfCase relating any evaluation relation
R to the conditions that must follow when the guard is either true or false. This hypothesis then becomes an assumption in the context of
Theorem evalCmd_coind, to which we add a single line in the same vein as those for the other command constructs:
Finally, we add a rule describing how to optimize if commands:
And that’s it. No changes were made to any of the lemmas or theorems involved in proving that unoptimized
cmd commands are equivalent to optimized ones, yet all of those definitions continue to be accepted by Coq after making the modifications above.
Contrast this use of heavy automation with the more manual approach taken in Logical Foundations. There, an optimizer function
optimize_0plus is defined over arithmetic expressions, and is proven correct with minimal automation and no custom induction or co-induction principles:
The first thing to note here is that this proof is unlikely to be immune to the addition of new types of arithmetic expressions; more steps will likely have to be added to this proof to accomodate them. In addition, this theorem only proves equivalence over arithmetic expressions, not entire language commands. The latter would require induction on commands themselves, with a corresponding custom induction or co-induction principle to facilitate automation.
To understand exactly what Coq is doing, temporarily forgoing automation is usually helpful. But for a large-scale Coq development, it’s becoming clear to me that heavy automation is indispensable. The approach feels like conversing with an esoteric compiler, an ability that is quite difficult to do fluently but offers views of expansive cognitive vistas to those who persist.