Reference Guide

Extensibella is an interactive proof assistant based on Abella. Much of the language will look familiar to those familiar with Abella.

Syntax

The syntax of formulas in Extensibella includes the following constructs:

forall A B C, ...	universal quantification
exists A B C, ...	existential quantification
F1 /\ F2	and
F1 \/ F2	or
F1 -> F2	implies
true	true
false	false
t1 = t2	equality
t1, t2, t3 |{ty}- t ~~> t'	projection
rel t1 t2 t3	relation
<rel {ES}> t1 t2 t3	extension size of a derivation
<rel {T}> t1 t2 t3	projection version of a relation

Additionally, we have infix binary operations for several types (e.g. t1 + t2 = t3):

Integers:	+, -, *, /, mod, <, >, <=, >=
Booleans:	&&, ||
Lists and Strings:	++

We also have unary integer negation (- t1 = t2) and unary Boolean negation (!t1 = t2).

The syntax of terms in Extensibella includes the following constructs:

<var>	variable
c t1 t2 t3	constructor application
t1::t2	cons list
nil	empty list
[]	empty list
[t1, t2, t3]	list literal
(t1, t2, t3)	tuple literal
"string"	string literal
<integer>	integer literal
true	Boolean true
false	Boolean false

Identifiers (variables, theorem names, relations, etc.) may begin with a letter or one of -^=`'? followed by any letters, digits, symbols from the previous list, or _*@+#!~/. Note that this also means spaces in operations can be important. For example, a + b = c is an integer addition formula, but a+b=c is a single identifier.

Anywhere the short name of a construct can be used, the qualified name can also be used. For example, if module mo:du:le contains a relation rel, both rel x y z and mo:du:le:rel x y z may be used interchangeably, as long as there is not another relation named rel available in the current module.

Single-line comments start with % and may begin anywhere in a line. Multi-line comments are demarcated by /* and */.

Module Declaration

Each Extensibella interaction begins with a module declaration:

Module mo:du:le.

This tells Extensibella which language specification to use, namely the one for the module named mo:du:le. This is the language module about which the session will reason.

Top-Level Commands

Top-level commands are commands that may be used outside of a proof.

Basic Top-Level Commands

We take our basic top-level commands from Abella:

Theorem <name> : <formula>.

Declares a (non-extensible) theorem, causing Extensibella to enter its proof mode for the user to prove it

Define <pred> : <type>, <pred> : <type>, ... by <clause>; ... <clause>.

Inductively defines a set of non-extensible fixed-point relations at the proof level

Split <name> as <name>, ... <name>.

Splits a theorem with top-level conjunctions into separate theorems. For example, Split thm as a, b, c. where thm refers to the formula f1 /\ f2 /\ f3 will create three new theorems, f1 named a, f2 named b, and f3 named c.

Kind <name> <kind>.

Declares a new proof-level type

Type <name> <type>.

Declares a new proof-level constructor with the given type. The type must be a proof-level type, not a type in the language or a built-in type.

Extensible Declarations

Extensibella has top-level commands for declaring extensible proof objects:

Extensible_Theorem <name> : forall <bindings>, <hyp name> : <formula> -> <hyp name> : <formula> -> ... <conclusion> on <hyp name>.

Declares an extensible theorem to be proven, using induction and case analysis on the premise given in the on clause, which must be an atomic formula built by an extensible relation with a variable for the primary component

Multiple extensible theorems can be declared together and proven using mutual induction by repeating the theorem declaration part (everything after Extensible_Theorem), comma separating each theorem

Non-extensible theorems may be added, for purposes of mutual induction, after all extensible theorems in a group with the also keyword, repeating the theorem declaration part after the also keyword. The also keyword needs to be given only once, with each non-extensible theorem comma-separated after it

The induction hypothesis may be given a descriptive name by adding as <IH name> after the on clause of a theorem declaration

Multiple inductions may be declared by repeating the on clause, with or without a name for the induction hypothesis. All theorems declared together must have the same number of inductions. If multiple are given, the key relation for the top-level case analysis must be marked by * (e.g. on A, on B *, on C to analyze B); note there must be a space separating * from the name as * can be part of names (B* is interpreted as a single name rather than as B plus a mark)

Projection_Constraint <name> : forall <bindings>, <hyp name> : <args> |{<ty>}- <original> ~~> <projection> -> <hyp name> : <formula> -> <conclusion>.

Declares a projection constraints to be proven using case analysis on the projection

Ext_Size <rel> <args>.

Declares the extension size version of <rel>, which adds an integer argument counting up the number of rules introduced by extensions used in the derivation

Multiple relations can have their extension size versions declared together by repeating the <rel> <args> part, comma separating each relation

This also introduces three lemmas the user does not need to prove but can use. For a relation rel, we have ext_size_is_int_rel, that the extension size has the is_integer relation hold for it ext_size_pos_rel, that the extension size is greater than or equal to zero drop_ext_size_rel, that the extension size version of the relation implies the relation itself add_ext_size_rel, that the relation implies the extension size version of itself

Proj_Rel <rel> <args>.

Declares the projection version of <rel>, which adds the premises of the stand-in rule to rules introduced by extension modules

Multiple relations can have their projection versions declared together by repeating the <rel> <args> part, comma separating each relation

This also introduces a lemma the user does not need to prove but can use. For a relation R, we have drop_proj_rel_R, that the projection version of the relation implies the relation itself

Ext_Ind forall <bindings>, <rel> <rel args> with <hyp name> : <formula>, ..., <hyp name> : <formula> as <IH name>, <IH name>.

Declares a requirement for modules to show the projection version of the relation follows from the relation itself; this allows extension to build arguments for new properties using the extensible relation <rel> for induction. Because this uses the projection version of the relation, that must be declared before this.

Multiple relations can be proven together by repeating the bindings, relation, and extra premises (everything after Ext_Ind), semicolon separating each relation

Uses the extension size version of <rel> for the proof if it is declared, or <rel> itself if it is not declared

The with clause adds extra assumptions to be used in the proof; if there are none, the with keyword is dropped

The as clause gives names for the induction hypotheses; if no names are given, the as keyword is dropped and the induction hypotheses have automatically-generated names

Arbitrary theorems can be proven mutually by adding and <theorem statement> for extensible theorems and also <theorem statement> for non-extensible theorems, where the theorem statements take the form expected for Extensible_Theorem

This also introduces a lemma based on what the user has proven. For a relation R declared with extra premise formulas A and B, we have add_proj_rel_R, that the projection version of the relation implies the relation itself: forall <args>, R <args> -> A -> B -> <R {P}> <args>

Each of these extensible top-level commands also has a Prove version, used for adding to its proof in modules that build on the module introducing it. They are Prove_Theorem, Prove_Constraint, Add_Ext_Size, Add_Proj_Rel, and Prove_Ext_Ind, respectively. Each of these takes a list of qualified names (not short names) for the theorems or relations to which it is adding, and presents the user with the new cases to prove in the current module, if any exist.

Some of these allow new additions in their Prove versions:

• Prove <existing thm names> with <new thm statements> also <new also thm statements>.

  Adds new mutually-inductive theorems to the set to prove

• Add_Ext_Size <existing rels> with <new rels>.

  Adds new relations, which must be introduced by the current module, to the set of relations defined together for the extension size

• Add_Proj_Rel <existing rels> with <new rels>.

  Adds new relations, which must be introduced by the current module, to the set of relations defined together for the projection versions of all

• Prove_Ext_Ind <existing rels> and_thms <existing mutual theorem names> with <new rels and premises>.

  Adds new relations to the set for which we are proving the projection version follows from the basic relations; can add new theorems by adding and and also as with Ext_Ind

Tactics

Tactics are the commands used within a proof to advance the proof state. We borrow our tactics from Abella.

Abella Tactics

Several tactics operate in the same way in Extensibella as in Abella:

induction on <num>.
For a goal of the form forall A B C, H1 -> H2 -> H3 -> G, the induction tactic permits induction on one of H1, H2, and H3 (e.g. induction on 2 for H2). Mutual induction across a conjunction can be declared with multiple numbers.
intros <names>.
For a goal of the form forall A B C, H1 -> H2 -> H3 -> G, the intros tactic introduces new eigenvariables A, B, and C and new hypotheses H1, H2, and H3. Giving names to the tactic gives those names to the introduced hypotheses.
apply <thm> to <hyps> with <var> = <tm>, ....
Applies a formula, referenced by name, to the given hypotheses, giving specific instantiations of the variables listed at the end, adding the conclusion to the context as a hypothesis. The hypotheses to which it is applied may also include underscores, in which case Extensibella searches for a formula to fill them. Any not found are added as subgoals for the user to prove. Variable instantiations are usually not needed and may be left off; they are helpful in conjunction with underscores to fill in terms that are otherwise not known.
backchain <thm> with <var> = <tm>, ....
Unifies the conclusion of the formula with the current goal and searches for solutions to the premises. If premises are not found, they are added as subgoals for the user to prove. As with applications, variable instantiations are optional, but are helpful if some of the bound variables in the formula do not appear in its conclusion. This is similar to apply but works backward instead of forward.
assert <formula>.
Extensibella searches for a proof of the formula; if one is not found, the formula is added as a subgoal for the user to prove. Once the formula is proven, it is added to the context as a hypothesis.
exists <tm>.
For a goal of the form exists <var>, <formula>, replaces occurrences of <var> with <tm>.
search <depth>.
Searches for a way to prove the current goal, using rules to the given depth. If no depth is given, this uses the default depth.
split.
For a goal of the form A /\ B, splits it into separate subgoals A and B.
left.
For a goal of the form A \/ B, chooses to prove A.
right.
For a goal of the form A \/ B, chooses to prove B.

Restricted Tactics

Some tactics have specific restrictions not seen in Abella that are necessary because we are reasoning in an extensible setting:

case <hyp>.
Analyze the ways in which the formula in the hypothesis named <hyp> might have been derived. If <hyp> is not built by a relation or the relation is not an extensible relation, case analysis has no extra restrictions.
If <hyp> has the form rel t1 ... tn and rel is an extensible relation in the language, then case analysis is allowed if its primary component is built by a known constructor or its primary component is the explicit unknown constructor and rel is introduced by the current extension.
unfold.
For a goal of the form rel t1 ... tn, if there is only one rule for the goal that could prove it, replaces the goal with the body of the rule. If rel is an extensible relation, its primary component must be built by a known constructor, not a variable on the explicit unknown constructor.

Proof State Manipulation Tactics

There are also tactics that don't move the proof forward, but may be useful while working:

skip.
Skips the current subgoal, moving to the next one. This treats the subgoal as if it were truly solved.
admit.
Skip all remaining subgoals, completing the current theorem. This treats the theorem as if it were truly solved.
abort.
Aborts the current theorem without adding it to the set of known theorems.
undo
Undoes the effect of the last tactic.
clear <hyp>.
Removes the given hypothesis from the context.
rename <name> to <name>.
Changes the name of one hypothesis or variable to another.

Common Commands

Common commands do not affect the state of the prover and can be used in either the proof mode or the top mode.

Set <option> <value>.
Set the value of various runtime options: display_width Set the attempted maximum width for lines in the proof state display (default value is 80) Values: any positive integer search_depth Set the depth which search and other tactics use (default value is 5) Values: any positive integer debug Set whether to display information about communication with Abella for debugging the behind-the-scenes Abella interaction Values: on or off
Show <name>.
Display a previously-proven theorem. The name may either be a qualified name or a short name, with short names only working if there is only one known theorem with that name.
Quit.
Exits Extensibella

Typing

All terms and formulas in Extensibella must be well-typed. Extensibella includes several built-in types:

• integer
• string
• bool
• list (kind type -> type, written list A)
• pair (kind type -> type -> type, written pair A B)

Definitions and non-extensible theorems may be defined as polymorphic. For definitions, any capitalized names in the definition will be treated as variables. For example,

Define rel : A -> list (pair A B) -> prop by ...

will define a relation with two variables, A and B. Non-extensible theorems must declare their type variables. For example,

Theorem thm[A, B] : forall (L : pair A B) X Y, ...

Some bound variables need to be annotated with types so Extensibella can determine the correct types.

Extensibella differentiates between language-level types and proof-level types in defining new constructors with the Type top-level command, but does not differentiate between them in typing.

Inductive Restrictions

As in Abella, the application of inductive hypotheses in Extensibella is guarded by inductive restrictions. These are * for smaller and @ for equal. The induction tactic adds the @ restriction to the induction measure premise and creates the inductive hypothesis with the * restriction. For example, induction on 1 with

============================
 forall A B C, rel A B -> rel B C -> rel A C 

as the proof state creates

IH : forall A B C, rel A B * -> rel B C -> rel A C
============================
 forall A B C, rel A B @ -> rel B C -> rel A C 

The inductive hypothesis having the * restriction means it can only be used with an argument that also has the * restriction. Such a hypothesis can be obtained by case analysis on a premise with the @ restriction, meaning it is equal to the current derivation size we are attempting to prove.

Running Extensibella

Extensibella can be run interactively to build proofs. The best way to do this is using Proof General, where one writes commands into a file in Emacs and runs them as they are written. Alternatively, proofs may be written directly into Extensibella by running it as

extensibella

Note this will not save the proofs written. Writing proofs directly into the Extensibella command line also requires saving the commands elsewhere. When running interactively, Extensibella waits for a command, processes it, and displays the proof state after the command has run.

To check an Extensibella file thms.xthm that has already been written, run

extensibella --check thms.xthm

This will check all the proofs are correct, and that all proof obligations have been fulfilled.

Because the Extensibella file for a module may be anywhere, a file must be compiled before proofs can be written for modules building on it. This takes the relevant information modules building on it must know and places it in Extensibella's generated directory. To compile a file thms.xthm, run

extensibella --compile thms.xthm

The best practice is to combine this with the --check flag, as the proofs being compiled are not checked by default, to ensure the properties being compiled are true. Note --compile by itself can be quite a bit faster than combining it with --check, however, which is why the combination is not the default.

In addition to its use in writing modular proofs, Extensibella also provides a facility for combining them into a single Abella proof. The existence of modular proofs acceptable to Extensibella is sufficient evidence a single Abella proof of the properties for the language exists, but this allows skeptics, or the curious, to check the proof for themselves. To compose a set of modular proofs for the language of a module mo:du:le into an Abella proof out.thm, run

extensibella --compose out.thm mo:du:le file_1.xthm file_2.xthm ... file_n.xthm

where the listed files are the proof files for all modules included in the composition. A few notes:

• Each module file included in the composition must be able to be checked, so the specification of each module must be compiled for Extensibella and the proofs of all properties in the modules completed.
• The module defining the language being composed, module mo:du:le in our example command, must be compiled for an Extensibella full language; this has slightly different requirements than the modular compiled format, so both will be needed.
• If you are using Sterling for your language specifications, the list of proof files must include the one for the Sterling standard library as well.

Emacs Support

Extensibella has a mode written for Proof General, found in the Extensibella GitHub repository. The mode has only been tested with the Abella fork of Proof General and is not guaranteed to work with other versions.

To install the Extensibella Proof General instance, copy the Extensibella Proof General files to a directory named Extensibella in the Proof General directory. You also need to add the following line to the generic/proof-site.el file in the Proof General directory, in the proof-assistant-table-default:

(extensibella "Extensibella" "xthm")

This makes Proof General and Emacs know to open Extensibella .xthm files using this mode automatically.