osa1

On proof automations -- part 3

September 23, 2013 - Tagged as: en, coq.

Over the past several days I learned few things that changed my ideas about proof automation. See my first two posts about proof automation here: #1 #2

First, it’s really possible to use proof automation without first writing the whole proof. After started working on theorems defined on more complex languages, I realized one thing: Most of the cases of inductions/inversions are trivial to solve. Generally you only interested in one or two cases, while you have in total 20 cases. Why not use automation to eliminate 18 cases automatically? Proving that parts manually only makes it more obscure.

Second thing I learned is that automations like auto, eauto, iauto never perform rewrite, subst, case analysis(inversion, destruct, maybe others?) and induction. I think this is very important point, because this means that your proofs still have to resemble the structure of your non-automated proofs(i.e. structure of your terms). Which prevents your proofs from being too much magical.

Now let’s work on an example to see how some automation is good thing. I’ll prove progress property of STLC(simply-typed lambda calculus), as defined in Software Foundations chapter Stlc.

Here’s an initial version without using any kind of automation.

Theorem progress_no_auto : forall t T,
     empty |- t \in T ->
     value t \/ exists t', t ==> t'.
Proof.
  intros t T TD. remember (@empty ty).
  (* induction on typing derivation *)
  has_type_cases (induction TD) Case.
  Case "T_Var".
    (* this case is impossible because vars are not well-typed in empty env,
       find a contradiction *)
    rewrite Heqp in H. inversion H.
  Case "T_Abs".
    (* lambdas are values *)
    left. apply v_abs.
  Case "T_App".
    (* well-typed applications should take a step *)
    right. destruct IHTD1. assumption.
    SCase "t1 is a value". destruct IHTD2. assumption.
      SSCase "t2 is a value".
        (* t1 should be a lambda *)
        inversion TD1; subst; inversion H. (* inversion on typing derivation of t1,
                                              most cases can be eliminated with inversion H,
                                              because t1 can only be lambda expression to be well-typed *)
        SSSCase "t1 is tabs". eexists. apply ST_AppAbs. assumption.
      SSCase "t2 can take a step".
        inversion H0. eexists. apply ST_App2. assumption. apply H1.
    SCase "t1 can take a step". inversion H. eexists. apply ST_App1. apply H0.
  Case "T_True". left. constructor.
  Case "T_False". left. constructor.
  Case "T_If".
    (* well-typed T_If can always take a step *)
    destruct IHTD1. assumption.
    SCase "t1 is value". inversion H; subst.
      SSCase "t1 is a lambda". inversion TD1.
      SSCase "t1 is ttrue". right. exists t2. constructor.
      SSCase "t1 is tfalse". right. exists t3. constructor.
    SCase "t1 can take a step". inversion H; subst. right.
      exists (tif x0 t2 t3). constructor. assumption.
Qed.

I leave comments to explain what’s going on. The point here is not to get shortest proof, but to show with some automation proofs could be more readable.

When you look to this proof you can realize that our interesting cases are:

T_Var case, in which we need to show that it’s impossible.
T_App and T_If cases, in which we need to use induction hypothesis.

T_Abs, T_True and T_False cases are completely trivial and we don’t want to make our proof harder to write, read and maintain more.

Second thing to realize that, if you count ; operator as a automation, then it makes me using automation even in that proof. In the case of T_App, I’m eliminating all cases of t1(because for T_App to be well-typed, t1 can only be a lambda abstraction – other cases should be eliminated with contradictions) with inversion H; subst.. Without ; operator, I would have to write this:

inversion TD1; subst.
SSSCase "t1 is tvar". inversion H.
SSSCase "t1 is tabs". eexists. apply ST_AppAbs. assumption.
SSSCase "t1 is tapp". inversion H.
SSSCase "t1 is tif". inversion H.

and when the language gets bigger, more cases with just inversion H would follow.

Now here’s an automated version:

Theorem progress : forall t T,
     empty |- t \in T ->
     value t \/ exists t', t ==> t'.
Proof with eauto.
  intros t T TD. remember (@empty ty). has_type_cases (induction TD) Case; auto.
  Case "T_Var". rewrite Heqp in H. inversion H.
  Case "T_App". right. destruct IHTD1...
    SCase "t1 is a value". destruct IHTD2...
      SSCase "t2 is a value". inversion TD1; subst; try (solve by inversion)...
      SSCase "t2 can take a step". inversion H0; subst...
    SCase "t1 can take a step". inversion H; subst...
  Case "T_If". right. destruct IHTD1. assumption.
    SCase "t1 is a value". inversion H; subst; eauto.
      SSCase "t1 is tabs". solve by inversion.
    SCase "t1 can take a step". inversion H...
Qed.

IMO this proof is a lot more simple and readable. It eliminates all trivial cases and only leave us with interesting ones. And even in that cases we simply finished with ... or explicitly running auto/eauto.

(Show comments)