Skip to main content
Version: 2.1.0-dev

Command reference

This page lists every command accepted at the top level of Abella 2.1.0-dev. 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. 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. The name may be qualified when it belongs to a module, as in Show M.lemma. It does not print definitions.

Show eval_det.

Show Module​

Show Module <MODULE>.
Show Module "<FILE>".

Prints a summary of a module: its kinds, types, definitions, axioms, and theorem statements, without proofs. The argument may be an in-scope module, an imported instance, or a quoted .thmod file without its extension:

Show Module Counter.
Show Module C.
Show Module "List".

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.

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, and they are applied simultaneously.

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

Import Module​

Import Module [<ALIAS> =] "<FILE>"[<TYPE>, ...] with <KEY> := <VALUE>, ... .
Import Module [<ALIAS> =] <MODULE>.

Loads a reasoning-level module from a .thmod file, a nested module, or an existing module instance. A quoted target omits the .thmod extension. A parameterized module requires a type argument list in parameter order.

The alias becomes the prefix for the imported items. Without an alias, the target module's name is used. A with clause maps declared predicates and axiom items to local predicates and theorems or axioms:

Import Module N = "List"[nat].
Import Module E = "Eq"[nat] with eq := nat_eq, refl := nat_eq_refl.

See Reasoning-level modules for the full syntax and restrictions.

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.

Axiom​

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

Declares the formula as an axiom without requiring a proof. The axiom may be used like a theorem. Abella records that it is axiomatic, and Split propagates that status. In batch mode, the axioms used in the development are listed at the end of the run.

Axiom fun_ext : forall (F G : tm -> tm),
  (forall (x : tm), F x = G x) -> F = G.

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. By default a failed check produces a warning; with --strict-stratification it is an error, and inside a reasoning-level module it is always 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.

Module and End​

Module <NAME>[<PARAM>, ...].
  <DECLARATIONS>
End <NAME>.

Opens and closes a reasoning-level module. In a .thmod file there must be exactly one top-level block, and its name must match the file base name. In a .thm file modules may be defined inline; they are local to the development. The parameters are schematic type variables. Nested modules use the same form.

Module List[T].
  Kind lst type.
  Type lnil lst.
  Type lcons T -> lst -> lst.
End List.

Inside a module, Specification, ordinary Import, Close, Suspend, Quit, and Abort are not allowed. A .thmod file may not use specification-level sequents. See Reasoning-level modules.

Suspend​

Suspend <HEAD>.
Suspend <HEAD> := <VAR>, ... .

Declares a guard for the compute tactic. When computation encounters a predicate matching HEAD and the listed variables are still uninstantiated, it suspends instead of unfolding further. If := is omitted, every variable in HEAD is a suspension condition.

Suspend nat X.
Suspend plus X _ Z := X, Z.

See Computation.

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. The name may be qualified when the theorem belongs to a module. Splitting an axiom produces axioms, and splitting a theorem whose proof used skip keeps the unfinished status.

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 or .thmod file in batch mode and from standard input in interactive mode. The interactive-only commands #back and #reset fail in batch mode. In batch mode, the axioms used in the development are listed at the end of the run. Quit stops reading the file early, which is useful in scripts but leaves the development incomplete.