Versions of Abella prior to 2.0.0 limited the use of embedded implications in specifications: goals in the bodies of specification clauses could contain implications only if their lefthand sides were atomic. Starting with Abella version 2.0.0, this limitation has been lifted. Specification clauses can contain arbitrarily nested implications, i.e., these clauses can be of arbitrary order when they are construed as types. Unfortunately, the introduction of this capability breaks proof scripts (*.thm files) from previous versions. To ease the transition to the new, more versatile version of Abella, we provide a guide here for updating old proof scripts to run under the new version.
When reasoning in the Abella system, specification-level judgments are
encoded via expressions of the form {L |- G}. We refer to
L here as the context of the judgment. Differences
between the old and new versions of Abella arise only when the
derivation of G depends on backchaining on some clause in
the context. Thus, if the old proof script does not involve reasoning
in a situation where the context is non-empty, it should work
immediately with Abella 2.0.0. Otherwise, it will have to be updated. In
explaining how it should be updated, we use the proof script for
type uniqueness of the simply typed lambda calculus as an example.
If you are not familiar with this example, it is perhaps best if you
first read the proof for it in the distribution of Abella 1.3.5 (in
'examples/lambda-calculus/type-uniq/type-uniq.thm') and in the advanced walkthrough.
The typing rules for simply-typed lambda calculus is encoded in Abella as follows:
of (abs T R) (arrow T U) :- pi x\ (of x T => of (R x) U). % for abstraction of (app M N) T :- of M (arrow U T), of N U. % for applicationThe type uniqueness theorem looks like
Theorem type_uniq : forall L E T1 T2,
ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.
It is stated relative to the following context definition:
Define ctx : olist -> prop by ctx nil ; nabla x, ctx (of x T :: L) := ctx L.
The proof for type_uniq starts with an induction on the judgment {L |-
of E T1} and then a case analysis on it.
induction on 2. intros. case H2.The judgment
{L |- of E T1} can be derived by
backchaining on the program clause for abstraction, for application
or in the context L.
The result of executing the tactics above in Abella 1.3.5 looks like
Subgoal 1:
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
Subgoal 2 is:
arrow T U = T2
Subgoal 3 is:
T1 = T2
The subgoal 1,2,3 correspond to cases for deriving the goal formula from the
context, from the abstraction clause and from the application clause, respectively.
If the same same tactics are executed in Abella 2.0.0, the proof state looks like:
Subgoal 1:
Variables: L, E, T1, T2, U, R, T
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H3 : {L |- of (abs T R) T2}
H4 : {L, of n1 T |- of (R n1) U}*
============================
arrow T U = T2
Subgoal 2 is:
T1 = T2
Subgoal 3 is:
T1 = T2
The subgoal 1,2,3 correspond to cases for deriving the goal formula
from the abstraction clause, from the application clause and from the
context, respectively. Note that in Abella 2.0.0, the subgoal for
deriving goal formulas from the context is presented last, because its
proof becomes non-trivial and sometimes very complicated.
Thus the first step for updating the scripts is to rearrange the script so that the segments for proving cases that judgments are derived by backchaining on the context come last. Those cases are abbreviated as backchaining-on-context cases in the following discussion.
After the previous step, we need to update the proof segments for
backchaining-on-context cases. In Abella 1.3.5 the proof state for the
case that {L |- of E T1} is derived by backchaining on
the context looks like:
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
Since the context L may only contain atomic formulas in Abella 1.3.5,
of E T1 is derived by backchaining on some clause
in L if and only if it is a member
of L; thus the hypothesis member (of E T1)
L. The proof state for the same case in Abella 2.0.0 looks like:
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 a single judgment member (of E T1) L, we get
{L, [F] |- of E T1} and member F L. The
judgment {L, [F] |- of E T1} is called a backchaining
judgment which asserts that of E T1 is derived by
backchaining on some formula F. The
hypothesis member F L indicates that F is a
clause in the context L. The two judgments together
assert that of E T1 is derived by backchaining on some
clause F in L, where F can be
an arbitrary complex program clause in Abella 2.0.0.
Before we can perform case analysis on {L, [F] |- of E
T1}, we first need to reveal the structure
of F. The following theorem comes to help, whose proof is
quite straightforward.
Theorem ctx_mem : forall L E, ctx L -> member E L -> exists N X, E = of X N /\ name X.It is basically an "inversion" (or "inspection") of the context definition. Applying it to
H1 and H5
unifies F with of X N, resulting in:
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
Then we can perform case analysis on H4, resulting in
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
At this point, the proof state looks almost like what we got in Abella
1.3.5, except we have an extra hypothesis name E. In fact, the next step
in the script for Abella 1.3.5 is to apply the following lemma
Theorem of_name : forall L E T, ctx L -> member (of E T) L -> name E.to get the hypothesis
name E. Thus the proof states in
Abella 1.3.5 and 2.0.0 converge at this point. Then both proofs
proceed by a symmetric case analysis on {L |- of E T2}
before their states converge again. The rest proofs for both are
almost the same.
In summary, in Abella 2.0.0, every time a judgment {L |-
G} is derived by backchaining on the context, a
judgment {L, [F] |- G} and a hypothesis member F
L are produced. To get to the same state resulting from the
same backchaing in previous versions of Abella, we need to
L and use it to reveal the
form of F;
{L, [F] |- G}.
It is relatively easy to update the old scripts to Abella 2.0.0 by following the instructions above, since contexts only contain atomic formulas in old proofs. If you encounter any difficulties in updating your scripts, please contact us at the Abella mailing list. You can find some examples for reasoning about higher-order specifications that use full power of Abella 2.0.0 here.