# Updating Old Proof Scripts to Run on Abella Version 2.0.0

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 Type Uniqueness Example

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 application
```
The 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.
```

# Updating the Script up to the Reordering of Subgoals

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.

# Updating the Script for the Case of Backchaining on Context Clauses

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

• Prove a lemma about the form of clauses in the context `L` and use it to reveal the form of `F`;
• Then perform case analysis on `{L, [F] |- G}`.
After that, the proof in the old script should be followed until a backchaining-on-context case is encountered again.

# Conclusion

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.