Possibly breaking changes
abella command has slightly
changed.
-v option is removed; use
--version instead.-nr option is removed; use
--non-recursive instead.file.thc from
file.thm.-a) now produces annotations
in JSON format instead of in HTML fragments. The JSON schema should be
seen as experimental for now and subject to change in the future.-M) has now been
moved to a separate program (see “Additions” below).Additions
Documentation Generation
(abella_doc): There is now a special program
called abella_doc that can be used to convert a collection
of Abella sources into HTML pages that resemble the official
Abella examples.
Run abella_doc --help for usage instructions.
Dependency Generation (abella_dep):
There is now a special program called abella_dep that can
be used to generate a Makefile-based dependency graph.
Executing make on that Makefile will recompile
all the Abella sources specified to abella_dep. This
Makefile can be used in parallel (i.e.,
make -j) mode.
Mention that a proof contained “skip” during interactive mode,
and a summary of skipped theorems in batch mode.
(#137, reported by Farah Al Wardani)
The types flag when set to on will now
print the types of quantified variables as well.
Bugfixes
Import statements now does not
clobber existing partial compilation results. This improves the support
for multiple runs of Abella in parallel using the same source
files.false. SOUNDNESS BUG (#147,
discovered by Sebastiaan Joosten, reported by Gopalan Nadathur)This release adds no functionality, but fixes a number of minor bugs. It also makes Abella compilable with OCaml versions 4.08.0 and higher.
Bugfixes
Additions
The schematic polymorphism branch has been merged. You can read more about it schematic polymorphism tutorial.
Tweaks to existing functionality
Bugfixes
(pi x\ p x).Additions
Added support for (first-order) polymorphic definitions. Definitions such as the following are now accepted.
Define fresh : A -> B -> prop by
nabla x, fresh x M.In every use of the definition, the type arguments are implicitly instantiated. The type-checking for such definitions is identical to taking all the unbound variable names and quantifying them on the outside. In other words, for the above definition, the behavior of type -checking is the same as if there were:
Kind A,B type
Define fresh : A -> B -> prop by
nabla x, fresh x M.Once such a definition is type-checked, the defined symbols are added to the signature as new polymorphic constants, in a vein similar to the pi constant. Whenever it is used, the type arguments are implicitly instantiated based on the types of the arguments.
Added support for (first-order) polymorphic theorems. A theorem such as the following is now accepted.
Theorem prune[A] : forall E L, nabla (x:A), member (E x) L ->
exists F, E = x\ F.The A here is a type parameter, which must be distinct from the other basic types in scope. To use such a theorem, you must supply enough arguments. An example:
Theorem bar : forall E G, nabla (x:tm) (y:ty),
member (E x y) G -> exists F, E = x\ y\ F.
intros.
apply prune[tm] to H1.
apply prune[ty] to H1.
search.Tweaks to existing functionality
The syntax for quantifiers now allows for multiple bound variables of the same type. Example:
/* Type p i -> i -> prop. */
forall (x y : i) (f g : i -> i), p (f (g y)) (g (f x))The apply tactic now takes an optional numerical argument that defines the search depth for automatic searches performed for omitted arguments. A bound of 0 means that no searches are attempted.
The abbrev and unabbrev tactics now both take a list of hypotheses to (un)abbreviate. The display of abbreviations has also been compressed.
Error messages in interactive mode are printed to stderr in addition to any other output file specified with -o.
The monotone tactic now accepts hypothesis naming hints. (#91)
Bugfixes
abbrev and unabbrev correctly.apply tactic was invalidly raising guessed instances over nominal constants that already occur in the body of the lemma.Possibly breaking changes
search tactic has the same error handling behavior in interactive and non-interactive modes, functioning like a failed tactic in both cases if no subgoals were closed.& can no longer appear inside the names of identifiers.Additions
Added support for specification-level conjunction, written using &.
Added a new tactic form:
search with <witness>.This tactic runs the search command with a given search witness. To see these witnesses, run any of the other search forms with:
Set witnesses on.The witness string that is printed can then be used to replay the exact same search. There is no backtracking involved with witness strings. Hence, the replay will tend to be a lot faster.
Witnesses have the following grammar:
witness ::= true | =
| left witness | right witness
| split(witness,witness)
| apply hyp
| intros[id1, ..., idn] witness
| exists[id1=term1, ..., idn=termn] witness
| unfold(id,n,witness1,...,witnessn)
| (witness)
| *The last witness form stands for a place-holder so you can give partial witnesses to search. In fact, the default search tactic is identical to:
search with *.Please use this feature sparingly, and only when building proofs. After you are done with the proof, delete the "with" statements. These witnesses will NOT be portable across different versions of Abella, as they are very particular to the "search" tactic implementation.
Added a new tactic form for backchain and `assert:
backchain <num> <hyp_or_lemma>.
assert <num> <formula>.where the <num>, which is optional, can give a depth bound to the search that is automatically attempted on generated goals. Give it a depth of 0 if you want to prevent searching. The default value is the value of the search_depth flag.
-f that takes a comma-separated list of key=value pairs and initializes the flags based on them. For flags that can be set to on/off, you can just use the key and it means to set them to on. For example, -f subgoals=off,witnesses sets subgoals to off and witnesses to on.Tweaks to existing functionality
exists and witness tactics now take a comma-separated list of existential witnesses. Each witness can also be of the form <id> = <term> which selects a particular existential variable to instantiate. Without the <id> = part it always instantiates the first variables.induction tactic can now traverse an arbitrary sequence of forall, nabla, and -> connectives when finding the induction argument.search tactic now does a small amount of asynchronous reasoning for newly created hypotheses (e.g., reducing pattern equations).Experimental changes (may be changed or removed in the future)
Added support for (first-order) polymorphic definitions. Definitions such as the following are now accepted.
Define fresh : A -> B -> prop by
nabla x, fresh x M.In every use of the definition, the type arguments are implicitly instantiated. The type-checking for such definitions is identical to taking all the unbound variable names and quantifying them on the outside. In other words, for the above definition, the behavior of type-checking is the same as if there were:
Kind A,B type
Define fresh : A -> B -> prop by
nabla x, fresh x M.Once such a definition is type-checked, the defined symbols are added to the signature as new polymorphic constants, in a vein similar to the pi constant. Whenever it is used, the type arguments are implicitly instantiated based on the types of the arguments.
Added support for (first-order) polymorphic theorems. A theorem such as the following is now accepted.
Theorem prune_arg[A] : forall E L, nabla (x:A), member (E x) L ->
exists F, E = x\ F.The A here is a type parameter, which must be distinct from the other basic types in scope. To use such a theorem, you must supply enough arguments. An example:
Theorem bar : forall E G, nabla (x:tm) (y:ty),
member (E x y) G -> exists F, E = x\ y\ F.
intros.
apply prune_arg[tm] to H1.
apply prune_arg[ty] to H1.
search.Added limited support for predicate instantiation during import. The form
Import "thmfile" with id1 := defid1, ..., idn := defidn.performs an import as usual, but any undefined predicates id in "thmfile" are instantiated with defined predicates defid. An undefined predicate is declared as usual with:
Type id T1 -> T2 -> ... -> Tn -> prop.It remains illegal to import a thm with undefined predicates without giving the predicate instantiations.
Added a new "extrusive" tactic form clear -> that can be used to do the opposite of the intros tactic, i.e., intros H1 ... Hn is opposite to clear -> Hn ... H1. Variables can also be extruded in this form and they universally close the goal with respect to the variable if the variable is not free in any hypothesis.
Extended the subgoals flag to take a subgoal specification string argument that can be used to fine tune the subgoals to display. As an example, the invocation:
Set subgoals "0[0];1[2];2[3];3;4[10]".instructs Abella to show 0 additinoal subgoals at depth 0, max 2 additional subgoals at 1, max 3 additional subgoals at depth 2, all subgoals at depth 3, and max 10 subgoals at depth 4. The depths need not be given in order, and any omitted depths display the default number of subgoals. The default flags on, off, and an unquoted number have the following meanings:
on : the same as "0[∞];1[∞];…"off : the same as "0[0];1[0];…"n : the same as "0[0];̣…;n-1[0];n[∞];n+1[0];…"Bugfixes
New examples
Potentially breaking changes
~ and != notations (undocumented introduction in 2.0.2). A general notation support may be considered for Abella in the future. Meanwhile, we prefer simplicity and predictability.Additions
The following tactic forms have been added:
apply *H to ...
apply ... to ... *H ...
backchain *H
cut *H ...
cut ... with *H
inst *H with ...
monotone *H with ...In each case, if H names a hypothesis, then the tactic consumes the hypothesis (like the clear tactic). Note that if hypothesis hints are given, then these hints are used after consuming the hypotheses. Thus, if one writes:
foo : apply lem to *foo bar baz.then the hypothesis named foo is effectively replaced with a new hypothesis named foo that is the result of applying the lem to the old foo and the other arguments.
clear tactic can also remove instantiated variables.Internal changes
Bugfixes
New examples
Potentially breaking changes.
exists now has a synonym: witness. This adds
witness to the list of keywords.Additions
<= in addition to =>unfold n.%:nm: on a line by itself right
before the clause. There must be a single Abella identifier and no
spaces between the two :s.nm of a specification using
unfold nm.~ F for F -> false.Internal changes
Bug fixes
New examples
This is a minor bugfix release for 2.0.0
src/version.mlapply and 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.apply with no arguments.tm
cannot appear inside a term of type nat.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
called.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 search
tactic is used to find possible hypotheses to cut from a
specification judgment.accum_sig
and accumulate.
-M flag which can be used to generate
makefile style dependency lists for developments. Also
added 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.
search tactic.
apply.backchain tactic which is in some sense
dual to the apply tactic. The backchain
tactic applies a lemma (or hypothesis) to the current goal and
produces new subgoals for each of the hypotheses to the lemma.
permute tactic which permutes the nominal
constants in a hypothesis or goal.Quit command.Specification command as
described here.
Query command allows the animation of definitions
as described here.
abella
--help to find out more.
Set command as described
here.
abbrev and unabbrev commands as
described here.
/*
... */. These comments may be nested.
split tactic now operates on n-ary
conjunctionsapplysearch tactic now takes an optional natural
number argument specifying the maximum depth of searching (default
5)CoDefine, which works much
like Define, and the tactic coinduction,
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
coinductive
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
forthcoming.
left and right tactics for
selecting the left or right side when the current goal is a
disjunction.exists tactic where nominal
constants were being treated as regular constants.Axiom command since it can be replaced with a
theorem which uses only the skip tactic.
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
over.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.
where the X1 ... Xn are the variables to
be instantiated with T1 ... Tn.
search tactic by
adding some corner cases of unification.search tactic now uses iterative deepening
depth-first search instead of simply depth-first search.