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.ml
apply
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
conjunctionsapply
search
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.