Home
March 27, 2018

PL Optimization: Chlipala's Use of CoInductive + Heavy Automation

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:

 Inductive cmd : Set :=
 | Assign : var -> exp -> cmd
 | Seq : cmd -> cmd -> cmd
+| If : exp -> cmd -> cmd                        
 | While : exp -> cmd -> cmd.

Then, we add two constructors to the co-inductive evaluation relation: one for when the conditional’s guard is false, the other for true:

 CoInductive evalCmd : vars -> cmd -> vars -> Prop :=
 | EvalAssign : forall vs v e, evalCmd vs (Assign v e) (set vs v (evalExp vs e))
 | EvalSeq : forall vs1 vs2 vs3 c1 c2,
     evalCmd vs1 c1 vs2 ->
     evalCmd vs2 c2 vs3 ->
     evalCmd vs1 (Seq c1 c2) vs3
+| EvalIfFalse : forall vs e c,
+    evalExp vs e = 0 ->
+    evalCmd vs (If e c) vs
+| EvalIfTrue : forall vs1 vs2 e c,
+    evalExp vs1 e <> 0 ->
+    evalCmd vs1 c vs2 ->
+    evalCmd vs1 (If e c) vs2
 | EvalWhileFalse : forall vs e c,
     evalExp vs e = 0 ->
     evalCmd vs (While e c) vs
 | EvalWhileTrue : forall vs1 vs2 vs3 e c,
     evalExp vs1 e <> 0 ->
     evalCmd vs1 c vs2 ->
     evalCmd vs2 (While e c) vs3 ->
     evalCmd vs1 (While e c) vs3.

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:

 Section evalCmd_coind.
   Variable R : vars -> cmd -> vars -> Prop. 

   Hypothesis AssignCase : forall vs1 vs2 v e, R vs1 (Assign v e) vs2
                           -> vs2 = set vs1 v (evalExp vs1 e).
   Hypothesis SeqCase : forall vs1 vs3 c1 c2, R vs1 (Seq c1 c2) vs3
                        -> exists vs2, R vs1 c1 vs2 /\ R vs2 c2 vs3.
+  Hypothesis IfCase : forall vs1 vs2 e c, R vs1 (If e c) vs2
+                      -> (evalExp vs1 e = 0 /\ vs1 = vs2)
+                         \/ (evalExp vs1 e <> 0 /\ R vs1 c vs2).
   Hypothesis WhileCase : forall vs1 vs3 e c, R vs1 (While e c) vs3
                          -> (evalExp vs1 e = 0 /\ vs3 = vs1)
                          \/ exists vs2, evalExp vs1 e <> 0
                             /\ R vs1 c vs2 /\ R vs2 (While e c) vs3.

   Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2.
     cofix; intros; destruct c.
     rewrite (AssignCase H); constructor.
     destruct (SeqCase H) as [? [? ?]]. econstructor; eauto.
+    destruct (IfCase H) as [[? ?] | [? ?]]; subst; constructor; auto.
     destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto.
   Qed.
 End evalCmd_coind.

Finally, we add a rule describing how to optimize if commands:

 Fixpoint optCmd (c : cmd) : cmd :=
   match c with
   | Assign v e => Assign v (optExp e)
   | Seq c1 c2 => Seq (optCmd c1) (optCmd c2)
+  | If e c => If (optExp e) (optCmd c)
   | While e c => While (optExp e) (optCmd c)
   end.

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:

Fixpoint optimize_0plus (a:aexp) : aexp :=
  match a with
  | ANum n => ANum n
  | APlus (ANum 0) e2 => optimize_0plus e2
  | APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2)
  | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2)
  | AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2)
  end.

 Theorem optimize_0plus_sound': forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  induction a;
    try (simpl; rewrite IHa1; rewrite IHa2; reflexivity).
  - reflexivity.
  - destruct a1;
      try (simpl; simpl in IHa1; rewrite IHa1;
           rewrite IHa2; reflexivity).
    + destruct n;
      simpl; rewrite IHa2; reflexivity.
Qed.

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.

← return home