Release 2.0.4

Changes in 2.0.4 from 2.0.3

Possibly breaking changes

• The 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.
• The character & 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.

• Added a new command line 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

• Import declarations automatically compile if needed. An explicit Makefile
  is very rarely needed any more.
• The 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.
• The induction tactic can now traverse an arbitrary sequence of forall,
  nabla, and -> connectives when finding the induction argument.
• The 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

• Annotation mode (-a) output is no longer printed in other modes
• Import statements can now be undone as well from ProofGeneral
• Importing .thcs made with a different Abella binary will now print an
  error message instead of causing a segmentation fault (#39)
• Importing from different directories now works correctly
• Multiple occurrences of a single variable in a binding list is now
  correctly rejected. (#56)
• Better error messages. (#64)

New examples

• Bisimulations relating the π-calculus and the λ-calculus
  (contributed by Horace Blanc and Beniamino Accattoli)
• Type-preservation of Curry-style System F
  (contributed by Ahn Ki Yung)