Skip to main content
Version: 2.0.8

Command reference

This page lists every command accepted at the top level of Abella 2.0.8. Commands that can also be used during a proof are marked anywhere.

Most commands end with a period. Names are unquoted; file names are given as double-quoted strings. Whitespace and comments may appear between tokens.

Commands usable anywhere​

Set​

Set <KEY> <VALUE>.

Changes a run-time option. The command may be used at the top level or in the middle of a proof. The following keys are supported.

  • subgoals: on, off, a non-negative integer, or a depth specification. Controls how much of the subgoal tree is printed.
  • instantiations: on or off. Shows the terms assigned to logic variables.
  • types: on or off. Shows the types of quantified variables.
  • search_depth: a non-negative integer. Sets the default depth for search and tactics that use it. The initial value is 5.
  • witnesses: on or off. Prints a search witness after a successful search.
  • load_path: a quoted string. Sets the load path. In 2.0.8 a relative name is still resolved against the directory of the development; see File structure.

subgoals accepts a depth specification instead of a single number. The specification is a semicolon-separated list of entries, each either n or n[m], where n is the goal-tree depth and m is the number of subgoals to show at that depth:

Set subgoals "1;2[3]".

The integer form is a shorthand for showing that many levels:

Set subgoals 2.

Examples:

Set search_depth 10.
Set witnesses on.
Set types on.
Set load_path "lib".

Show​

Show <THEOREM-NAME>.

Prints a previously proved theorem, including its type parameters and its formula. It does not print definitions.

Show eval_det.

Quit​

Quit.

Exits Abella from the top level or from a proof.

#back​

#back.

Undoes the previous command in interactive mode. It is not available in batch mode. Repeated use walks backwards through the session.

#reset​

#reset.

Resets the session to its initial state in interactive mode. It is not available in batch mode.

Top-level commands​

Specification​

Specification "<NAME>".

Reads the specification with the given base name. Abella adds .sig and .mod and reads both. The name is resolved relative to the current .thm file, then against the load path.

Specification must be the first command in the development. It may appear only once.

Specification "eval".

Import​

Import "<NAME>".
Import "<NAME>" with <P> = <Q>, ..., <P> = <Q>.

Loads a compiled development, adding .thc to the name. If the .thc file is missing or stale, Abella compiles it first, unless --non-recursive was given.

The with clause renames predicates from the imported development to predicates already present in the importing one. The replacements must be pairwise distinct.

Import "util".
Import "util" with helper = local_helper.

Theorem​

Theorem <NAME> : <FORMULA>.
Theorem <NAME>[<TYVAR>, ...] : <FORMULA>.

Starts a proof of the formula. The optional type parameters give the theorem a schematic polymorphic type; they are instantiated at each use.

Theorem eval_det : forall E V1 V2,
  {eval E V1} -> {eval E V2} -> V1 = V2.

Proof commands follow until the proof is completed with search or another tactic that closes the goal, or abandoned with abort or skip.

Define​

Define <P> : <TYPE>, ..., <P> : <TYPE> by
  <CLAUSE> ; ... ; <CLAUSE>.

Introduces inductively defined predicates. Each clause is a fact or a rule with := between the head and the body:

Define append : olist -> olist -> olist -> prop by
  append nil L L ;
  append (X :: L1) L2 (X :: L3) := append L1 L2 L3.

A clause head may begin with nabla:

Define name : tm -> prop by
  nabla x, name x.

A leading semicolon after by is permitted. Definitions are checked for stratification; a failed check produces a warning rather than an error.

CoDefine​

CoDefine <P> : <TYPE>, ..., <P> : <TYPE> by
  <CLAUSE> ; ... ; <CLAUSE>.

Introduces co-inductively defined predicates using the same clause syntax as Define:

CoDefine sim : state -> state -> prop by
  sim P Q := forall A P',
    step P A P' -> exists Q', step Q A Q' /\ sim P' Q'.

Co-inductive predicates are discharged with the coinduction tactic.

Query​

Query <FORMULA>.

Searches for solutions of the formula and prints each one. Free uppercase names are treated as existentially quantified:

Query eval (app (abs R) M) V.

After the first solution, the search continues until no more solutions are found. The search is bounded, so No more solutions means only that the search strategy is exhausted, not that the formula is unprovable.

Kind​

Kind <TYPE>, ..., <TYPE> <KIND>.

Declares atomic types or type constructors. The kind is type, or a chain of arrows ending in type:

Kind tm, ty type.
Kind env type -> type.

A name can be declared only once.

Type​

Type <CONST>, ..., <CONST> <TYPE>.

Declares constants at the reasoning level:

Type z nat.
Type s nat -> nat.

A name can be declared only once. Constants declared by the current specification are already in scope.

Close​

Close <TYPE>, ..., <TYPE>.

Closes the named atomic types and all of their subordinates. Closing a type tells Abella that no future declaration can put a term of that type inside another type, which makes dependency information vacuous.

Close tm, ty.

The types o, olist, and prop cannot be closed.

Split​

Split <THEOREM-NAME>.
Split <THEOREM-NAME> as <NAME>, ..., <NAME>.

Splits a theorem whose conclusion is a conjunction into separate theorems. The original theorem is a proof of mutually recursive statements, so each conjunct is recorded with the same proof.

Split even_odd_nat as even_nat, odd_nat.

Without as, names are generated by appending an index to the original name, starting at 1. Splitting a theorem that is not a conjunction is an error.

Batch-mode note​

Top-level commands are read from a .thm file in batch mode and from standard input in interactive mode. The interactive-only commands #back and #reset fail in batch mode. Quit stops reading the file early, which is useful in scripts but leaves the development incomplete.