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 and warns if it fails, but it does not reject the definition.

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.

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.

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.

See File structure for the compatibility rules.

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.

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.