Please report all bugs, feature request, and comments to Andrew Gacek.
This document is not intend to be a tutorial or introduction to Abella. For that, we suggest you read the walkthrough of an example session in Abella. This document is intended as a reference for more details on specific features of Abella.
The syntax of terms in Abella supports the following constructs,
forall A B C, ...exists A B C, ...nabla a b c, ...G1 /\ G2(and) G1 \/ G2(or) H -> G(implies) pred A B C(meta level predicate) {pred A B C}(specification level predicate) {hyp A, hyp B |- pred A B C}(specification level predicate with context)
Nominal constants are denoted by n1, n2, ...
One way to think about the different level of predicates is that
everything inside of {...} is at the specification
level while things outside are at the reasoning level. For typical
reasoning tasks, almost every predicate will be at the specification
level, except for a few reasoning level predicates to describe the
structure of contexts for specification predicates.
Nominal constants and the nabla quantifier can be roughly thought of as representing "names."
There are only three top-level commands in Abella.
Theorem <THM-NAME> : <TERM>.Define <PRED NAME> <PRED ARGS>.Define <PRED NAME> <PRED ARGS> := <PRED BODY>.<PRED NAME>. Multiple calls to define are used to define multiple clauses of a definition.
The define command can be used used with nabla in the definition head. See examples/type_uniq for an example.
The Abella logic requires that all definitions satisfy a stratification condition. Various stratification conditions, all of which ensure the consistency of the Abella logic, are possible. The system does not current enforce any of these conditions since we are still experimenting with the best possible choice. Stratification is only a concern when definitions have an implication in their body. Thus, specific stratification conditions are noted with each such definition in the examples suite accompanying this distribution. The user is encouraged do identify, document, and adhere to such conditions in their own developments. A later version of the system will automate conformity to such conditions.CoDefine <PRED NAME> <PRED ARGS>.CoDefine <PRED NAME> <PRED ARGS> := <PRED BODY>.<PRED NAME>. Multiple calls to codefine are used to define multiple clauses of a definition.
As with the define command, the codefine command can be used with nabla in the definition head and all definitions must be stratified.
Note: The formal meta-logic underlying Abella with coinduction is still being developed. A paper with the full logic is forthcoming.
There are four categories of tactics.
Primary and secondary tactics are distinguished by their overall usefulness. The primary tactics make up over 90% of the tactic usages in the examples distributed with Abella, and they are used in almost every proof.
induction on <NUM>.forall A B C, H1 -> H2 -> H3 -> Gtheinductiontactic allows you to induct on one ofH1,H2, orH3. The hypotheses to be inducted on must be inductively defined. The choice of induction is based on the number<NUM>. Applying theinductiontactic results in an inductive hypothesis being added to the current set of hypotheses. Specifics on this inductive hypothesis and how it relates to the goal are given in the section Inductive Restrictions.Abella supports nested induction through repeated calls to theinductiontactic. See the Inductive Restrictions section for more details.coinduction.forall A B C, H1 -> H2 -> H3 -> Gthecoinductiontactic allows you to use coinduction onG, which must be a coinductively defined predicate. Applying thecoinductiontactic results in a coinductive hypothesis being added to the current set of hypotheses. Specifics on this coinductive hypothesis and how it relates to the goal are given in the section Coinductive Restrictions.
Note: The formal meta-logic underlying Abella with coinduction is still being developed. A paper with the full logic is forthcoming.intros.forall A B C, H1 -> H2 -> Gtheintrostactic introduces three new eigenvariablesA,B, andCand addsH1andH2to the hypotheses. The new goal isG.case <HYP-NAME>.casetactic performs case analysis on a hypothesis. The tactic also removes the hypothesis from the hypothesis list. To keep it, use the keep flag, e.g.case H3 (keep).See examples/pcf for an example of where keeping a hypothesis is convenient.search.search <NUM>.searchtactic tries to prove the current goal by repeatedly unfolding the goal and looking in the list of hypotheses. When the goal is a specification level judgment, this corresponds very much to the executable search semantics of the specification logic. The maximum depth of search is specified by<NUM>and defaults to 5. Thesearchtactic does not unfold goals with a top-level structure of forall or implies.apply <HYP-NAME> to <HYP-NAMES>.apply <HYP-NAME> to <HYP-NAMES> with X1 = T1, ..., Xn = Tn.applytactic applies a hypotheses of the formforall A1 ... Ai, nabla z1 ... zj, H1 -> ... -> Hk -> Gto argument hypotheses which matchH1, ...,Hk. The result is an instantiation ofG. Either or both of i and j may be zero, that is there need not be forall or nabla quantified variables. Thewithclause allows specific instantiations of any of the variablesA1...Aiandz1...zj.
A previously proved theorem can be used instead of the first hypothesis, and then this acts like using a lemma. This tactic also triggers some basic case analysis on the resulting hypotheses.
A useful feature of apply is that not all of its arguments have to be available. See the section Apply with Unknowns for more information.
unfold.unfoldtactic attempts to unfold the current goal by matching it against its possible definitions. The first definition to match is the one used.assert <FORMULA>.asserttactic changes the current goal to the given formula and once that is proven it comes back to the original goal, but with the given formula as a hypothesis. If the asserted formula can be solved by thesearchtactic, this is done so automatically.
This tactic is useful for when the prover is doing a poor job with, for example, thesearchtactic. Using assert allows you to "hold the prover's hand" to get to your desired goal. Future improvements to thesearchtactic will therefore lessen the need for this tactic.exists <TERM>.exists A, ...theexiststactic instantiatesAwith the given term.split.G1 /\ G2thesplittactic creates the two subgoalsG1andG2. Ifsplit*is used instead ofsplit, the second subgoal hasG1as a hypothesis.left.G1 \/ G2thelefttactic changes the goal toG1.right.G1 \/ G2therighttactic changes the goal toG2.
inst <HYP-NAME> with <VAR> = <TERM>.{... <VAR> ...}where<VAR>is a nominal constant, theinsttactic creates the hypothesis{... <TERM> ...}. Thus this tactic implements a meta-level substitution property of the specification logic. See subject reduction in examples/eval for an example.cut <HYP-NAME> with <HYP-NAME>.{L1, A |- C}and{L2 |- A}withL1andL2possibly empty, thecuttactic creates the hypothesis{L1, L2 |- C}. This corresponds to meta-level cut property of the specification logic. See subject reduction in examples/eval for an example.
undo.undotactic undoes the previous tactic. This can be used repeatedly.skip.skiptactic skips the current subgoal completely. This is logically unsound, but very convenient during proof development and exploration.abort.aborttactic gives up on the current theorem and returns the user to the top-level.clear <HYP-NAME> ... <HYP-NAME>.
Inductive restrictions are represented by * (smaller)
and @ (equal). They are used to track the size of
inductive arguments rather than using explicit numeric values. For
example, suppose we apply induction on 1. when trying to
prove the following subject reduction theorem,
============================
forall E V T, {eval E V} -> {of E T} -> {of V T}
We will get the following proof state.
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
============================
forall E V T, {eval E V}@ -> {of E T} -> {of V T}
Here we have an inductive hypothesis where the inductive argument is
flagged with *. This means that we can only apply that
hypothesis to an argument which also has the *.
Because * means smaller, in order to get an argument with
a * we must perform case analysis on an argument that is
"equal" which we denote by @. Thus the above proof
proceeds by first doing "intros." and then case analysis on {eval E
V}@. This will give us two subgoals, one which is trivial
and the other which has hypotheses tagged with * and thus
eligible for use with the inductive hypothesis.
Abella supports nested induction through repeated calls to the
induction tactic. For example, suppose we have a goal
such as
outer -> inner -> result.
If we apply induction on 1 followed by induction
on 2 we get the following proof state.
IH : outer * -> inner -> result IH' : outer @ -> inner ** -> result ============================ outer @ -> inner @@ -> resultThe outer inductive hypothesis
IH can be used like normal.
It ignores the flags @@ and **. The inner
inductive hypothesis IH' checks two things when applied:
that whatever is given for outer has a tag of
@ or *, and whatever is used for inner has a
tag of **.
See examples/cut for a real usage of nested induction.
Coinductive restrictions are used to ensure that a coinductive hypothesis is used correctly. That is, to ensure the coinductive hypothesis can only be used to establish results about recursive calls to the coinductive predicate to which coinduction is applied. This is best understood through an example.
Suppose we want to reason about a labeled transition system. As a simple example, we will take the following system.
We assume that the rules of this system are encoded in a predicate
step P A Q which holds if we can move from
state P to state Q via the
label A. The exact definition is therefore,
Define step p0 a p0. Define step q0 a q0. Define step q0 b q1.Suppose we want to show that the state
q0 can simulate,
or always act like, the state p0. We formalize this
notion in the following coinductive definition of sim P
Q, which holds when P is simulated
by Q.
CoDefine sim P Q := forall A P', step P A P' -> exists Q', step Q A Q' /\ sim P' Q'.Now when we are conducting a proof of
sim p0 q0 we will
begin by applying the coinduction tactic which results in
the following proof state.
CH : sim p0 q0 + ============================ sim p0 q0 @The restriction
+ on CH means that it cannot
match any goal unless that goal also has the +
restriction. The @ on the goal indicates that when this
goal is unfolded, the recursive calls will be tagged
with +. The next step in the proof is to apply
the unfold tactic which results in the following.
CH : sim p0 q0 + ============================ forall A P', step p0 A P' -> exists Q', step q0 A Q' /\ sim P' Q' +Notice that the recursive call
sim P' Q' is tagged
with + thus it will be able to match with CH
when the search tactic is eventually used. Before we can
apply search, however, we must apply
the intros tactic and then consider all possible cases
for step p0 A P'. The only case is when A
is a and P' is p0, which
results in the following state.
Variables: A, P' CH : sim p0 q0 + ============================ exists Q', step q0 a Q' /\ sim p0 Q' +The proof is then finished by the
search tactic which
will pick Q' as q0 and deduce
step q0 a q0 and sim p0 q0, by matching the
latter with CH.
To use a lemma, prove it as a theorem and then refer to it by name in
another proof using the apply tactic. For example,
Theorem my_lemma : ... ... Theorem my_theorem : ... ... apply my_lemma to H3 H5. ...
Abella supports mutual induction on specification judgments. We will illustrate this ability using the following specification.
nat z. nat (s X) :- nat X. even z. even (s X) :- odd X. odd (s X) :- even X.Suppose we want to show that everything recognized by
even is also recognized by nat, and
similarly for odd. Although, in this case, these results
could be established independently, we will use mutual induction. In
order to do this, we state a single theorem which is the conjunction
of the mutually recursive theorems we want to prove.
Theorem even_odd_nat :
(forall X, {even X} -> {nat X}) /\
(forall X, {odd X} -> {nat X}).
We can now call the induction tactic and pass it an
induction argument for each of the mutually recursive theorems. In
this case we have two such theorems and we want to induct on the first
argument in each. Thus we call induction on 1 1. which
results in the following.
IH : forall X, {even X}* -> {nat X}
IH1 : forall X, {odd X}* -> {nat X}
============================
(forall X, {even X}@ -> {nat X}) /\ (forall X, {odd X}@ -> {nat X})
We now have an inductive hypothesis for each of the mutually recursive
theorems, and these inductive hypotheses share the same inductive
restriction. At this point we can call split and proceed
to handle each of the two sub-theorems individually. The complete
proof script is as follows.
induction on 1 1. split.
intros. case H1.
search.
apply IH1 to H2. search.
intros. case H1.
apply IH to H2. search.
The apply tactic allows you to leave some arguments
unspecified by replacing them with an underscore. For example, in examples/type_uniq we at one point
have roughly the proof state,
Variables: L, E, T1, T2, U, R, T, U'
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} ->
T1 = T2
H1 : ctx L
H4 : {L, of n1 T |- of (R n1) U}*
H5 : {L, of n1 T |- of (R n1) U'}
============================
arrow T U = arrow T U'
Now we would like to apply IH to H4 and
H5, but for this we would need a hypothesis which says
ctx (of n1 T :: L). We could assert this hypothesis and
the proof of it would follow from ctx L. Another option
is to say apply IH to _ H4 H5. The prover will then guess
what needs be proved for the unknown hypothesis and attempt to prove
it using search. If this fails, the current subgoal will
be delayed and the unknown hypothesis will become the current goal.
Abella assumes that :: is an infix, two-argument
constructor for lists and that nil denotes the empty
list. Abella also assumes the following definition
of member.
Define member A (A :: L). Define member A (B :: L) := member A L.
The distribution of Abella includes Emacs modes for mod and thm files. You can load these by putting the following into your .emacs file.
(load "/path/to/abella/emacs/lprolog-mod.el") (load "/path/to/abella/emacs/abella.el")Where
/path/to/abella is replaced with the actual
location you have installed Abella.
The mode for editing thm files provides some basic proof navigation
support. To use this, type M-x shell and run Abella in
that shell, passing in the proper mod file to reason over. At this
point it is recommended to do C-x 2 which splits the
emacs buffer into two separate buffers. You can toggle between them
with C-x C-o. My preference is to put the thm file in the
top buffer and the shell in the bottom buffer. Now back in the thm
file there are three proof navigation commands.
C-c C-n will send the next proof step
to the *shell* buffer.
C-c
C-p will go back to the previous proof step.
This command is designed only for within proofs since top-level
commands cannot currently be un-done.
C-c C-e will execute the previously written
proof step. This is useful while writing proofs.
The following list very briefly describes each example included in the distribution of Abella. Clicking on one takes you to the corresponding files.