backchain tactics now
produce witnesses when the witnesses option is enabled.
unfold tactic applied using a definition with
nabla in the head will now use "dummy nominals" in case the nabla
bound variables are not used.
/ can no longer begin a name.
- Underscore can now be used to represent anonymous variables in
- Fixed a bug when using
apply with no arguments.
- Fixed a bug in the normalization of binder names
- Added subordination
and the Close command. This makes many pruning lemmas
unnecessary, such as showing that a term of type
cannot appear inside a term of type
- Added case analysis on flex-rigid equalities. For example, one can
perform case analysis on an equality like
R N = plus A
B. The result is that one step of Huet's algorithm is
performed (computing the possible imitation and projections) and
for each result the standard pattern unification code is
- Fixed a unification issue involving the occurs check.
- Optimized the handling of state information. Based on the
developments included in the distribution, Version 1.3.3 is 150%
faster than Version 1.3.2.
- Added evaluation
by explicit substitution development contributed by J. Todd
- Added Show command to
display previously proved theorems.
- Added Split command to
easily separate mutually inductive theorems.
- Fixed an issue with subgoal numbering.
apply tactic no longer requires "dummy nominals"
when nabla bound variables in a lemma are not used.
search tactic now backtracks over equalities.
search tactic now properly considers all nominal
constants when trying to instantiate an existential.
cut tactic can now be used without a
with' argument in which case the
tactic is used to find possible hypotheses to cut from a
specification modularity via
- Loosened the
conditions on importing developments to allow greater use of
- Reorganized the examples directory to have a hierarchical
- Added the
-M flag which can be used to generate
makefile style dependency lists for developments. Also
examples/makefile which demonstrates a typical
makefile for a development.
search tactic now descends underneath forall and
implication. It now embodies every right rule of the logic.
- A 'witnesses' option has been added to
the Set command which
causes search witnesses to be displayed after successful uses
- A warning is now issued when Teyjus keywords (which are not used
in Abella) are used in a specification. In all other respects,
specifications in Abella should now be a proper subset of those in
- Fixed a variable capture bug when using
This version of Abella is aimed at supporting larger developments.
Most notably, it introduces a way to compile and import developments.
This requires a change to way specifications are associated with
developments which is not backwards compatible.
Specifications are now explicitly loaded into a development via
Specification command as
Developments may now be compiled and imported into other
Query command allows the animation of definitions
as described here.
Command line options have been reorganized. Run
--help to find out more.
Some run-time options may be configured via the
Set command as described
Subgoals now use hierarchical numbering.
Large hypotheses may now be abbreviated using
unabbrev commands as
Multi-line comments are now supported via
*/. These comments may be nested.
The annotations for co-induction now use # and + to avoid confusion
with the annotations for induction (@ and *).
split tactic now operates on n-ary
- Tactic names no longer conflict with terms during parsing
- Added the monotone
tactic which explicitly realizes the monotonicity property of
specification logic contexts
- Fixed a couple unification bugs
- New examples
- Abella now
induction over specification judgments
- Abella will now issue a warning if a definition might not be
- Better handling of specification contexts when
search tactic now takes an optional natural
number argument specifying the maximum depth of searching (default
- New examples
- Added coinductive definitions and coinduction. These are used
through the top-level command
CoDefine, which works much
Define, and the tactic
which is similar to
induction but takes no arguments. A
brief example of these features is discussed in the Abella reference
guide in the section on
restrictions. The following examples are now included in the
distribution of Abella.
Note: The formal meta-logic underlying Abella with
coinduction is still being developed. A paper with the full logic is
- Definitions now support an arbitrary number of nablas in the
- The example copy has been
updated to show the equivalence of single and double variable
definitions of a copy predicate.
right tactics for
selecting the left or right side when the current goal is a
- Fixed a bug when case-analysis on a definition with nabla in the
head was used multiple times.
- Fixed a bug in the
exists tactic where nominal
constants were being treated as regular constants.
- Changed the emacs highlighting for Abella. The goal is to
highlight the theorems and definitions in a file while downplaying the
tactics. Hopefully this makes it easier to skim a file.
- Added more checks to definitions such as preventing the use of
undefined predicates and requiring all clauses for a particular
predicate to occur together.
- Removed the
Axiom command since it can be replaced with a
theorem which uses only the
search tactic now does a better job of
backtracking. In particular, each instantiatable variable is now
unbound when the event which caused it to be bound is backtracked
search tactic now delays conflict pairs which
fall outside of the pattern unification fragment. Thus this tactic
is now more robust.
apply tactic now allows specific instantiations
for variables. The general form is
apply <HYP-NAME> to <HYP-NAMES> with X1 = T1,
..., Xn = Tn.
Xn are the variables to
be instantiated with
- Randy Pollack has contributed a formalization of
theorem using Takahashi's proof based on complete
- Slightly extended the ability of the
search tactic by
adding some corner cases of unification.
- Added definedness and arity checks on the usages of
search tactic now uses iterative deepening
depth-first search instead of simply depth-first search.
- Fixed some font-locking issues in the emacs files.
- First public release of Abella