Updating old proof scripts

This page is a historical guide for migrating proof scripts written for Abella 1.3.5 and earlier so that they run on Abella 2.0.0 and later. The changes it describes are already in effect in 2.0.8, so a script written for a recent release needs no migration.

Versions of Abella before 2.0.0 limited the use of embedded implications in specifications: the goals in the body of a specification clause could contain implications only if their left-hand sides were atomic. Starting with Abella 2.0.0 that restriction was lifted, and specification clauses may contain arbitrarily nested implications. This makes specifications more expressive, but it breaks proof scripts that relied on the old, limited form of the context.

When a script needs updating

Specification-level judgments are written {L |- G}, where L is the context of the judgment and G is the goal. The difference between the old and new versions appears only when the derivation of G backchains on a clause in L. A script that never reasons with a non-empty context should work unchanged. Otherwise it needs the updates described below.

The examples on this page use the type uniqueness theorem for the simply typed lambda calculus:

of (abs T R) (arrow T U) :- pi x\ (of x T => of (R x) U).
of (app M N) T :- of M (arrow U T), of N U.

Theorem type_uniq : forall L E T1 T2,
  ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.

The context predicate is:

Define ctx : olist -> prop by
  ctx nil ;
  nabla x, ctx (of x T :: L) := ctx L.

Step 1: reorder the subgoals

The proof starts with an induction on {L |- of E T1} followed by a case analysis on the resulting judgment:

induction on 2. intros. case H2.

The judgment {L |- of E T1} can be derived in three ways: by backchaining on the clause for abstraction, by backchaining on the clause for application, or by backchaining on a clause in the context L.

In Abella 1.3.5, the order of the resulting subgoals was: context, abstraction, application. In Abella 2.0.0 and later the order is: abstraction, application, context. The context case comes last because its proof becomes non-trivial and sometimes very complicated.

The first step in updating a script is therefore to rearrange the proof so that the cases for backchaining on the context come last. The rest of this page calls these the backchaining-on-context cases.

Step 2: update the backchaining-on-context cases

In Abella 1.3.5, the proof state for a backchaining-on-context case looked like this:

Variables: L, E, T1, T2
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
       T1 = T2
H1 : ctx L
H3 : {L |- of E T2}
H4 : member (of E T1) L
============================
 T1 = T2

In 1.3.5 the context L could contain only atomic formulas, so of E T1 was derived by backchaining on some clause in L exactly when it was a member of L. Hence the hypothesis member (of E T1) L.

In Abella 2.0.0 and later, the same case looks like this:

Variables: L, E, T1, T2, F
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
       T1 = T2
H1 : ctx L
H3 : {L |- of E T2}
H4 : {L, [F] |- of E T1}*
H5 : member F L
============================
 T1 = T2

Instead of the single judgment member (of E T1) L, the proof state has {L, [F] |- of E T1} and member F L. The first is a backchaining judgment: it says that of E T1 is derived by backchaining on some formula F. The second says that F is a member of L. Together they say that of E T1 is derived by backchaining on some clause F in L, where F may be an arbitrary complex program clause.

Before doing case analysis on {L, [F] |- of E T1}, the script must reveal the structure of F. The following lemma does that; its proof is straightforward:

Theorem ctx_mem : forall L E,
  ctx L -> member E L -> exists N X, E = of X N /\ name X.

Applying ctx_mem to H1 and H5 unifies F with of X N and gives:

Variables: L, E, T1, T2, F, N, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
       T1 = T2
H1 : ctx L
H3 : {L |- of E T2}
H4 : {L, [of X N] |- of E T1}*
H5 : member (of X N) L
H6 : name X
============================
 T1 = T2

Case analysis on H4 then gives:

Variables: L, E, T1, T2, F, N, X
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
       T1 = T2
H1 : ctx L
H3 : {L |- of E T2}
H5 : member (of E T1) L
H6 : name E
============================
 T1 = T2

This state is almost the one from 1.3.5, except for the extra hypothesis name E. In the 1.3.5 script, the next step applied

Theorem of_name : forall L E T,
  ctx L -> member (of E T) L -> name E.

to obtain name E anyway, so the two proof states converge at this point. Both proofs then proceed by a symmetric case analysis on {L |- of E T2} and converge again. The rest of the proof is almost the same.

Summary

In Abella 2.0.0 and later, whenever {L |- G} is derived by backchaining on the context, the system produces a judgment {L, [F] |- G} together with a hypothesis member F L. To reach the state that the old version produced for the same backchaining step:

1. prove a lemma about the form of clauses in the context L, and use it to reveal the form of F;
2. perform case analysis on {L, [F] |- G}.

After that, follow the old script until the next backchaining-on-context case appears.

Updating an old script is relatively easy because contexts in old proofs contain only atomic formulas. If you encounter difficulties, ask on the Abella mailing list. Examples that use the full power of Abella 2.0.8 are listed on the examples page.