Top-level declarations

A development is built by issuing commands at the top level of Abella, either interactively or from a .thm file. This page explains what each command is for and how the commands fit together. The command reference gives the complete syntax and all options.

Types and constants

The reasoning logic is simply typed. Declarations extend the current signature.

Kind

Kind introduces atomic types and their arity:

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

The right-hand side is type, or type -> ... -> type for a type constructor of higher arity. The types o, prop, and list are built in and cannot be redeclared.

Type

Type introduces constants:

Type app  tm -> tm -> tm.
Type abs  (tm -> tm) -> tm.
Type unit tm.

Symbols that were introduced by the current specification are already available; Type and Kind add declarations at the reasoning level. A name may be declared only once, and the built-in constants nil, ::, and member cannot be redeclared.

Definitions

Define and CoDefine introduce predicates with a fixed set of clauses. They are the main way to state properties of the object system that are computed rather than proved by induction on a specification derivation.

Define

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

The predicate name and type are given before by, separated from the clauses by a semicolon. Each clause is either a fact or a rule with := separating the head from the body. A nabla binder may appear in the head of a clause, which is how definitions express freshness:

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

Definitions are inductive. The system checks a simple stratification condition. By default it warns if the check fails; with --strict-stratification the finding is an error, and inside a reasoning-level module it is always an error.

CoDefine

CoDefine has the same syntax and introduces co-inductively defined predicates:

CoDefine sim : tm -> tm -> 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 used with the coinduction tactic. See Reasoning logic.

Theorems

Theorem

Theorem starts a proof. It takes a name, an optional list of type parameters in brackets, a colon, and a formula:

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

The optional type parameters support schematic polymorphism:

Theorem member_prune[A] : forall (L : list A) X,
  member X L -> member X (X :: L).

After the command, Abella is in proving mode and accepts tactics until the proof is complete, aborted with abort, or left with skip.

Axiom

Axiom has the same syntax as Theorem but declares the formula without requiring a proof:

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

An axiom may be used like a theorem. Abella records that it is axiomatic, and Split propagates that status to the generated theorems. In batch mode, the axioms used in the development are listed at the end of the run.

Split

A theorem may be a conjunction of several statements proved by mutual induction. Split separates such a theorem into independently named theorems:

Split even_odd_nat as even_nat, odd_nat.

Without as, Abella generates names. Splitting does not re-run the proof: it records each conjunct as a theorem with the same proof. The theorem name may be qualified when it belongs to a module. Splitting an axiom produces axioms, and a proof that used skip keeps its unfinished status.

Specifications and imports

Specification

Specification "name". loads the .sig and .mod files with the given base name. It must be the first command in the development. See File structure.

Import

Import "name". loads a compiled .thc development. It can also rename predicates with a with clause:

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

The replacements must be pairwise distinct, and they are applied simultaneously. See File structure for the compatibility rules.

Import Module

Import Module loads a reasoning-level module from a .thmod file, a nested module, or an existing module instance. A quoted name is a .thmod file without its extension; an unquoted name refers to a module already in scope:

Import Module N = "List"[nat].
Import Module B = "List"[bool].
Import Module C = Counter.

The optional alias before = becomes the prefix for the imported items. A type argument list is required for a parameterized module, in the order of its parameters. A with clause maps declared predicates and axiom items:

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

See Reasoning-level modules for the full syntax.

Reasoning modules

Module and End

A .thmod file contains one top-level Module/End block. The module name must match the file base name:

List.thmod

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

Nested modules use the same form with their own parameters. A .thm file may also define modules inline; those modules are local to the development and are not exported by its .thc artifact. See Reasoning-level modules for the restrictions that apply inside a module.

Inspection and control

Show

Show name. prints a previously proved theorem:

Show eval_det.

It may be used during a proof as well as at the top level.

Show Module

Show Module prints a summary of a module. The argument may be an in-scope module, an imported instance, or a quoted .thmod file:

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

The summary prints the module's kinds, types, definitions, axioms, and theorem statements without proofs.

Suspend

Suspend declares a guard for the compute tactic. A suspension may name all variables in the head, or only some of them:

Suspend $nat X.
Suspend leq X Y := X.

When compute encounters a predicate matching the head and the listed variables are still uninstantiated, it suspends computation on that hypothesis instead of unfolding further. If the := part is omitted, every variable in the head must be uninstantiated for the guard to apply. See Computation for compute and for examples.

Query

Query formula. searches for a proof of the formula using the specification and the current definitions. Free uppercase variables are treated as existentially quantified, and the answers are printed:

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

Query is an animation and testing tool. Failure to find a proof does not mean that the formula is unprovable, because the search is bounded and incomplete.

Close

Close tm, ty. declares the listed atomic types, together with all types subordinate to them, to be closed. Closing a type tells Abella that no new constants can produce a term of that type inside another type, which makes some dependency information vacuous. See Subordination.

Set

Set changes an option at run time. Options may be set at the top level or during a proof:

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

The available options are subgoals, instantiations, types, search_depth, witnesses, and load_path.

Quit

Quit. exits Abella, including from the middle of a proof. In interactive mode, the commands #back and #reset undo the previous command and reset the development, respectively.