Possibly breaking changes
searchtactic 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.
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>.
<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.
-fthat takes a comma-separated list of key=value pairs and initializes the flags based on them. For flags that can be set to
off, you can just use the key and it means to set them to
on. For example,
Tweaks to existing functionality
witnesstactics 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.
inductiontactic can now traverse an arbitrary sequence of
->connectives when finding the induction argument.
searchtactic 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.
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.
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;1;2;3;4".
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
off, and an unquoted number have the following meanings:
on: the same as
off: the same as
n: the same as
Potentially breaking changes
!=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.
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.
cleartactic can also remove instantiated variables.
Potentially breaking changes.
existsnow has a synonym:
witness. This adds
witnessto the list of keywords.
<=in addition to
%:nm:on a line by itself right before the clause. There must be a single Abella identifier and no spaces between the two :s.
nmof a specification using
F -> false.
This is a minor bugfix release for 2.0.0
backchaintactics now produce witnesses when the witnesses option is enabled.
unfoldtactic 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.
applywith no arguments.
tmcannot appear inside a term of type
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.
applytactic no longer requires "dummy nominals" when nabla bound variables in a lemma are not used.
searchtactic now backtracks over equalities.
searchtactic now properly considers all nominal constants when trying to instantiate an existential.
cuttactic can now be used without a '
with' argument in which case the
searchtactic is used to find possible hypotheses to cut from a specification judgment.
-Mflag which can be used to generate makefile style dependency lists for developments. Also added
examples/makefilewhich demonstrates a typical makefile for a development.
searchtactic now descends underneath forall and implication. It now embodies every right rule of the logic.
backchaintactic which is in some sense dual to the
backchaintactic applies a lemma (or hypothesis) to the current goal and produces new subgoals for each of the hypotheses to the lemma.
permutetactic which permutes the nominal constants in a hypothesis or goal.
Specificationcommand as described here.
Querycommand allows the animation of definitions as described here.
abella --helpto find out more.
Setcommand as described here.
unabbrevcommands as described here.
*/. These comments may be nested.
splittactic now operates on n-ary conjunctions
searchtactic 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
inductionbut 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.
righttactics for selecting the left or right side when the current goal is a disjunction.
existstactic where nominal constants were being treated as regular constants.
Axiomcommand since it can be replaced with a theorem which uses only the
searchtactic 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.
searchtactic now delays conflict pairs which fall outside of the pattern unification fragment. Thus this tactic is now more robust.
applytactic now allows specific instantiations for variables. The general form is
apply <HYP-NAME> to <HYP-NAMES> with X1 = T1, ..., Xn = Tn.
Xnare the variables to be instantiated with
searchtactic by adding some corner cases of unification.
searchtactic now uses iterative deepening depth-first search instead of simply depth-first search.