Introduction

Aufbau is a verifier and compiler for Metamath Zero (MM0), a language for formally checked mathematics. An MM0 theory declares its sorts, term constructors, and axioms. Proofs state what follows from that theory, and a small verification kernel checks each result.

This manual is interactive. Each editable example, or proof cell, runs the Aufbau compiler in your browser using WebAssembly. It checks your edits as you type; no installation is needed. The opening chapters cover proof lines, built-in search, and larger proofs. The next two parts describe MM0, the theory language, and .auf, Aufbau’s proof language. Later parts explain theory design, develop several worked theories, and document the command-line and embedding tools.

Your first proof

This chapter introduces theories and proofs through two axioms: weakening and modus ponens. We use them to prove that, if p holds, then q -> p holds for any proposition q.

The theory

The theory sits in its own editable cell.

Here wff is the sort of propositions, short for well-formed formula. provable permits proofs to assert expressions of this sort. imp builds an implication from two propositions, and infixr lets us write it as a -> b. The delimiter declaration lets parentheses separate tokens without spaces.

The first axiom, h1, asserts every proposition of the form a -> (b -> a). This is an axiom scheme: a and b may stand for any propositions. The second axiom is mp: given a proof of a and a proof of a -> b, you may conclude b. In a declaration, > separates hypotheses from what follows, so mp has two hypotheses and the conclusion b. The binder list (a b: wff) states the axiom for any two propositions.

Using it

A lemma is a named result with a proof. This lemma proves q -> p from the hypothesis p: first apply h1, then mp.

Two kinds of reference appear on the last line. #1 is the lemma’s first hypothesis, the incoming proof of p. l1 is the previous line. The brackets supply them to mp in the order its hypotheses were declared: first the proof of a, then the proof of a -> b.

Applying mp here requires a := p and b := q -> p; applying h1 requires bindings for its a and b as well. The compiler infers them from the formulas on the proof lines. Focus the cell and hover over a line to see the inferred bindings.

Spelling it out

You can make binding choices explicit with named bindings in parentheses. This is the same lemma with nothing left to inference:

Explicit bindings are rarely needed. Use them when the goal and hypotheses do not determine a rule’s variables.

Edits to the theory cell cause the proof cells to be checked again immediately.

The parts of a proof line

Proof lines look like this:

label: $ GOAL $ by rule (bindings) [references]

The label names the line. The goal, between $ signs, is what the line asserts. Everything after by is the justification for the line: the rule being applied, optional bindings in parentheses that assign expressions to the rule’s variables, and optional references in brackets that supply the rule’s hypotheses.

We’ll work in the Hilbert system from the last chapter, extended with the distribution axiom h2:

Three kinds of reference

A reference is a proof of one of the rule’s hypotheses. References can be supplied three ways:

• #1, #2, … indicate the hypotheses of the lemma or theorem being proved, in the order they were declared;
• a label like l1 indicates an earlier line of the same proof;
• an inline application is a rule applied on the spot, inside the brackets, without a line of its own.

As a running example, here’s the usual proof that p -> p, which needs instances of h1, an instance of h2, and two applications of mp.

It checks, but l3 transcribes an axiom instance that the compiler can infer.

Inline applications

When a premise needs only one rule application, you can write that application directly in the reference list. For example:

The second reference, h1 [], applies the axiom in place. The empty brackets say it has no hypotheses of its own. A bare name in a reference list means a line label, so without the brackets h1 would look for a line named h1 rather than the axiom.

Inline applications can be nested, and mixed freely with the other reference kinds. Here is imp_refl again, with the h2 instance and the inner mp folded into the final line:

This version omits the explicit h2 line from the first proof.

When chaining fails

Combining every application into one line can remove formulas that the compiler needs in order to infer bindings. The following cell is intentionally invalid:

The diagnostic says one of h1’s variables could not be determined. Aufbau can only infer what is forced by the goal and the references, and nothing here forces a choice of instance for the first h1 [].

If a variable cannot be determined, you can give the premise its own labeled line, as in imp_refl_chained above, or state the instances yourself with bindings, which work on inline applications the same way they work after by. The single-line proof checks when both h1 applications have explicit bindings:

l1: $ p -> p $ by mp [h1 (a := $ p $, b := $ p $) [],
                      mp [h1 (a := $ p $, b := $ p -> p $) [], h2 []]]

Packing and unpacking

Chains can be unpacked. Place the text cursor on the last line of imp_refl_chained and pause: the lightbulb offers an unpack action that rewrites the line as separate labeled lines, one per inline application, with each goal filled in by the compiler.

Proof search

A search placeholder can replace a rule name and ask the language server to find a justification:

l2: $ a ∧ b ⊢ b $ by exact?

The four placeholders serve different purposes: exact? closes a step from available facts, apply? lists rules that could produce the goal, auto? performs backward search, and conversion? looks for a chain of equalities or equivalences.

Example: search over natural deduction

exact? matches rule conclusions against a goal. auto? can also work backward from that goal, treating a rule’s premises as new goals to prove.

For this chapter, we switch to natural deduction. Each connective has introduction rules that produce it and elimination rules that consume it. Introduction rules often work well for backward search because the goal determines their premises.

Here are the rules we will use. The sorts, notation, and rules that let us treat contexts as unordered collections are already loaded. These shared declarations form a prelude.

axiom ax (g: ctx) (a: wff): $ g , a ⊢ a $;

axiom imp_intro (g: ctx) (a b: wff): $ g , a ⊢ b $ > $ g ⊢ a → b $;
axiom imp_elim (g h: ctx) (a b: wff): $ g ⊢ a → b $ > $ h ⊢ a $ > $ g , h ⊢ b $;

axiom and_intro (g: ctx) (a b: wff): $ g ⊢ a $ > $ g ⊢ b $ > $ g ⊢ a ∧ b $;
axiom and_elim_l (g: ctx) (a b: wff): $ g ⊢ a ∧ b $ > $ g ⊢ a $;
axiom and_elim_r (g: ctx) (a b: wff): $ g ⊢ a ∧ b $ > $ g ⊢ b $;

axiom or_intro_l (g: ctx) (a b: wff): $ g ⊢ a $ > $ g ⊢ a ∨ b $;
axiom or_intro_r (g: ctx) (a b: wff): $ g ⊢ b $ > $ g ⊢ a ∨ b $;
axiom or_elim (g h i: ctx) (a b c: wff):
  $ g ⊢ a ∨ b $ > $ h , a ⊢ c $ > $ i , b ⊢ c $ > $ g , h , i ⊢ c $;

axiom not_intro (g: ctx) (a: wff): $ g , a ⊢ ⊥ $ > $ g ⊢ ¬ a $;
axiom not_elim (g h: ctx) (a: wff): $ g ⊢ ¬ a $ > $ h ⊢ a $ > $ g , h ⊢ ⊥ $;
axiom bot_elim (g: ctx) (a: wff): $ g ⊢ ⊥ $ > $ g ⊢ a $;

A sequent g ⊢ a says that a follows from the hypotheses in g. The context is built with ,, and an empty context is written _. A formula standing alone is a one-element context. If you would rather not hunt for the symbols, ->, /\, \/, ~, and |- are accepted as alternative notation for →, ∧, ∨, ¬, and ⊢.

Finishing a step: exact?

Place the text cursor on the exact? line below and wait a moment. Open the lightbulb menu and choose “Replace exact? with and_elim_r [l1]”. The editor replaces the placeholder with that justification.

exact? looks for a single rule whose conclusion matches the goal and whose hypotheses are supplied by available assertions: the lemma’s own hypotheses (#1, #2, …) and earlier proof lines. This collection is the reference pool.

apply? lists rules whose conclusions match the goal, even if the reference pool does not supply all their hypotheses.

Finding a chain: auto?

exact? stops when no single rule proves the goal from the reference pool. auto? goes further: if the pool cannot supply a hypothesis, it tries to prove that hypothesis too. For example, it can find this entire proof:

The suggested justification uses nested inline applications:

imp_intro [and_intro [and_elim_r (a := $ a $) [ax []],
                      and_elim_l (b := $ b $) [ax []]]]

Working backward, imp_intro moves the antecedent into the context. ax proves it from that context, the two elimination rules extract its conjuncts, and and_intro combines them in the opposite order. These six rule applications prove the goal without additional references. The explicit bindings supply variables that cannot be inferred, as in the previous chapter. If you would rather read the result as separate lines, accept it and use the unpack action.

auto?’s search runs under a work budget and a depth limit, so it always stops. Its results are deterministic — the same goal, theory, and pool always produce the same suggestions in the same order.

Placeholders in argument slots

exact?, apply?, and auto? can also appear in reference slots. conversion? requires a whole proof line with a fully specified goal. For example:

The compiler infers the slot’s goal from the outer rule and the rest of the line. Here and_intro needs proofs of a ∧ b ⊢ b and a ∧ b ⊢ a. and_elim_l [l1] supplies the second; exact? searches for the first. Use placeholders in reference slots to guide a search: specify the rule you want and leave only the missing premises to search.

Search failure diagnostics

When a search fails, the diagnostic explains why it stopped. Exhausted means it finished exploring the candidates available to its search strategies at the configured depth. It does not mean that the goal is unprovable. Try a greater depth, add useful references, or adjust the theory’s search annotations. If search ran out of budget or fuel, it stopped before finishing that exploration. The report also lists the most-tried rules, which can reveal repeated unsuccessful attempts.

You can allow more search work on a single line by passing parameters to that call:

l4: $ a → b , ¬ b ⊢ ¬ a $ by auto? (depth: 8, budget: 13)

Computation as search: conversion?

conversion? looks for a rewrite chain from the goal to a member of the reference pool or, for an equation, between its two sides. A theory can register rules for general conversion or directed computation. General conversion repeatedly applies rules to discover more equivalent expressions, a process called saturation. Computation applies reductions in a fixed order to simplify expressions.

Here is a small lambda calculus with explicit substitution and addition on numerals. Beta reduction, the substitution equations, and the addition table are enrolled as computation rules. The substitution equations carry a second annotation, @rewrite, which lets the compiler apply them while checking ordinary proof lines and avoids explicit substitution steps:

-- `a` replaces `x`, so it may mention it. The one denial that carries weight is
-- `a`'s lack of `y` in `sb_lam`: that is what blocks capture.

--| @compute ltr
axiom beta {x: tm} (e: tm x) (a: tm x): $ (λ x. e) · a = [x := a] e $;
--| @compute ltr
--| @rewrite
axiom sb_var {x: tm} (a: tm x): $ [x := a] x = a $;
--| @compute ltr
--| @rewrite
axiom sb_vac {x: tm} (e: tm) (a: tm x): $ [x := a] e = e $;
--| @compute ltr
--| @rewrite
axiom sb_app {x: tm} (f g: tm x) (a: tm x): $ [x := a] (f · g) = ([x := a] f) · ([x := a] g) $;
--| @compute ltr
--| @rewrite
axiom sb_suc {x: tm} (e: tm x) (a: tm x): $ [x := a] (S e) = S ([x := a] e) $;
--| @compute ltr
--| @rewrite
axiom sb_add {x: tm} (f g: tm x) (a: tm x): $ [x := a] (f + g) = ([x := a] f) + ([x := a] g) $;
--| @compute ltr
--| @rewrite
axiom sb_lam {x y: tm} (e: tm x y) (a: tm x): $ [x := a] (λ y. e) = (λ y. [x := a] e) $;
--| @compute ltr
axiom add_z (n: tm): $ 0 + n = n $;
--| @compute ltr
axiom add_s (m n: tm): $ S m + n = S (m + n) $;

· is application, [x := a] e is substitution, and the numerals are unary: 0, S0, SS0. Substitution is not built into MM0: [x := a] e is an ordinary term whose behavior is specified by the equations above. We can now state a lemma in this theory.

The goal says that applying (λ x. λ y. (x + y)) to 1 and 2 gives 3. conversion? applies β-reduction twice, carries out the substitutions through +, and applies the addition rules. Both sides reduce to SSS0.

Rewriting respects variable dependencies: it does not apply a reduction that would capture a variable. If search finds no connection, the diagnostic explains why it stopped. Full saturation rules out a chain using the registered conversion rules, not every possible proof of the goal. A search stopped by a limit is inconclusive. Failure with computation rules is also inconclusive because those rules follow only one reduction order.

Holes

A proof line often contains subexpressions already determined by its rule, references, and remaining text. A hole omits such a subexpression and asks the compiler to recover it.

Holes are opt-in per sort. A @hole annotation on a sort declaration registers one token for it:

--| @hole _wff
sort wff;
--| @hole _ctx
sort ctx;

The natural deduction theory from the last chapter includes both of these annotations. So _wff stands for an omitted formula and _ctx for an omitted context. Contexts can be long and repetitive. Holes let you omit them when the rest of the line determines them.

Each hole is filled from the rule application on its own line. and_elim_l carries the context of l1 down to l2, not_elim joins the contexts of its two premises, and or_elim joins three contexts. You can hover a hole to see what it was filled with: the _ctx on l9 should become a ∨ b , ¬ a ∧ ¬ b , ¬ a ∧ ¬ b.

Line l2 shows that a line may have more than one hole, and that holes are not restricted to contexts. Each occurrence of a hole token is a separate hole, so $ _wff → _wff $ indicates two holes rather than one used twice; there is no way to require that two positions be filled the same way.

When the rule and the references do not determine what belongs in a hole, the line fails:

l1: $ _ctx ⊢ _wff $ by ax []

ax concludes g , a ⊢ a, and with nothing cited there is nothing to fix g. The diagnostic reports the undetermined variable, exactly as it would for a line whose bindings could not be inferred for any other reason.

Holes are allowed only in the assertion of a proof line. They are rejected in .mm0 files, in reference lists, in explicit bindings, and in the bound-variable position of a binder.

Chains of equations

Holes are useful for equational reasoning. A chain of eq_trans steps, for example, keeps its left-hand side fixed. A hole avoids repeating that side on every line.

Here is a step-by-step proof of the lambda-calculus equation that conversion? proved in the previous chapter. beta and add_s are rules listed in that chapter; eq_trans and the congruence rules that lift an equality into a surrounding term come from the theory’s equality bundle.

The s lines prove individual equalities. The last four chain them together, with each line extending by one step and stating only the new right-hand side. Every _tm is the goal’s left-hand side, (λ x. λ y. (x + y)) · S0 · SS0. The compiler infers it from app_congr on c1 and from the preceding equality on each eq_trans line.

Substitution stays out of the proof entirely, although beta produces it: s1 cites a rule concluding [x := S0] (λ y. (x + y)) but states the result of carrying that substitution out. The substitution equations are registered as rewrites, so the compiler applies them itself when it checks the line against the rule.

This resembles a calc block in a proof assistant like Lean, but requires no separate construct: these are ordinary proof lines using the same holes as the context example above.

Sorts and terms

An .mm0 file declares a theory: the syntax of its expressions, its axioms, and the theorems to be proved. A verifier checks the compiled .mmb proof against this declaration. The .mm0 file is the specification that an .auf proof development must satisfy.

An .mm0 file contains a sequence of statements, each ending in a semicolon. This chapter explains the statements that declare a theory’s syntax.

Sorts

A sort is a syntactic category, declared with sort:

sort tm;

Every expression belongs to exactly one sort.

Sort declarations can carry modifiers. The most common is provable:

provable sort wff;

provable means expressions of this sort can be asserted: they may appear between $ signs as an axiom’s conclusion, a theorem’s statement, or a proof line’s goal. Most theories have exactly one provable sort. The opening Hilbert theory used wff as its only sort. The natural deduction examples also used sorts for contexts and sequents.

Term constructors

A term statement declares a way to build expressions.

term imp (a b: wff): wff;

imp takes two expressions of sort wff and produces another wff. Within a math string (text between $ signs), write the constructor before its arguments. Parenthesize any argument that is itself an application:

$ imp a (imp b a) $

Constructors and variables are the only syntactic forms that MM0 supports. The -> in earlier chapters was notation for the imp constructor. Here is the implication fragment from earlier chapters without that notation.

Proofs using the notation-free syntax differ only in how their formulas are written.

Argument names are used only for dependencies between binders (the subject of the next chapter). A constructor whose argument names are never referred to can be declared with an arrow type instead:

term imp: wff > wff > wff;

Delimiters

Theories generally open with something like this:

delimiter $ ( ) $;

The parser normally splits math strings into tokens at whitespace. Characters listed in this form of delimiter also create token boundaries wherever they occur. Without this declaration, (imp is one unknown token rather than ( followed by imp. Notation explains the other delimiter options.

Several sorts

A theory can declare as many sorts as it needs. A first-order theory usually has two: one for the objects it talks about and one for the statements it makes about them.

tm is not provable, which is why a numeral is not a valid assertion. Add axiom bare (n: tm): $ suc n $; to the theory cell and it reports that the math string does not have a provable sort. In this theory the only assertions available are equations.

Sorts also provide the signatures for constructors. For example eq takes two tms, so eq a (eq a a) is rejected — the inner equation is a wff, and a wff is never a tm.

Coercions

A coercion lets the parser convert an expression from one sort to another. It names a one-argument constructor that the parser inserts when the surrounding expression requires the target sort.

hyp turns a formula into a one-element context. The coercion lets us omit it: ax is written nd a a, although nd requires a ctx as its first argument. After the parser inserts the coercion, this is nd (hyp a) a. Writing the constructor out gives the same expression:

These declarations make a formula by itself denote a one-element context in the natural-deduction theory used in Proof search.

A coercion may also be what makes a sort assertable. If the arithmetic theory above declared term holds (t: tm): wff; and coerced tm > wff, then $ suc zero $ would be a statement after all, meaning holds (suc zero).

The parser can chain coercions when several conversions are needed. To prevent ambiguity, there must be at most one path between any two sorts, even when the direction of each coercion is ignored.

Sort modifiers

MM0 provides three other sort modifiers.

Modifiers are written before sort and can be combined. Most theories need only provable. The other three govern how the sort interacts with variables; Variables, binders, and dependencies gives the details.

Variables, binders, and dependencies

A binder declares a variable and its sort. Declarations use binder lists such as (a b: wff), {x: tm}, and (e: tm x). Parentheses and braces distinguish the kinds of variable; variable names after the sort (as in tm x) specify dependencies.

Regular variables

A binder in parentheses declares a regular variable, standing for an arbitrary expression of its sort.

axiom h1 (a b: wff): $ imp a (imp b a) $;

Bound variables

A binder in braces declares a bound variable. This is MM0’s terminology for a variable that must be instantiated with another bound variable, (for example, a bound variable from the theorem declaration or one designated with the @var annotation) not an arbitrary expression. It need not occur under a binding operator.

Bound variables let a theory declare binding constructors, such as lambda abstraction:

term lam {x: tm} (e: tm x): tm;

lam takes a variable x and a body e, both of sort tm, with the curly braces indicating that x is a variable. A bound variable slot can only ever be filled by a bound variable: lam (app u u) e is not well formed. An abstraction is therefore never over a compound term.

These variables are also the object language’s variables. A theory needs no separate constructor for a variable standing as a term: in lam x x the body is the bound variable itself.

Dependencies

The sort in a regular binder may be followed by the names of bound variables.

axiom sb_lam {x y: tm} (e: tm x y) (a: tm x):
  $ eq (sb x (lam y e) a) (lam y (sb x e a)) $;

sb x e a substitutes a for x in e; this axiom pushes that substitution under a lambda. e: tm x y says that the body may mention either variable. a: tm x says that a may mention x but not y.

More generally, if a bound binder is absent from a regular binder’s dependency list, the expression assigned to the regular binder must not mention the variable assigned to the bound binder. Dependency lists encode side conditions such as freshness and capture avoidance.

The rule applies because u is a different variable from y. Substituting x itself would be accepted too, since a: tm x allows it. Replace the two us on the proof line with y, though, so that the term being substituted in is the lambda’s own variable, and the line fails:

dependency violation: the rule does not allow a to mention the variable
assigned to y

This is the capture that the rule must exclude. Substituting y for x in lam y x should leave y free, but the right-hand side places it under the binder. MM0 does not rename variables automatically, so the binder list states the restriction and the verifier enforces it. Aufbau can perform selected alpha-renaming through annotations described in Ergonomics.

Distinct bound binders must stand for distinct variables. A rule declaring {x y: tm}, as sb_lam does, cannot be applied with both slots filled by one variable, and reports that x and y must be assigned distinct variables.

A constructor’s result sort can carry dependencies as well: term fresh {x: tm} (e: tm): tm x; declares that fresh x e mentions x however e is instantiated. This dependency matters when checking the free variables in a definition’s body, as explained in Definition checking.

Dummy variables

A dummy variable appears in a definition’s body, or in a proof, without being one of the arguments. In a binder list a dot marks it:

def uniq {x .y: tm} (p: wff x): wff = $ ex y (all x (iff p (eq x y))) $;

uniq takes two arguments, x and p. Its y is internal to the body, and a proof that unfolds uniq is free to instantiate it with any variable that does not clash. Proofs introduce dummies of their own in the same way.

Definitions are covered in Axioms, theorems, and definitions. For now, dummy variables are the third way that variables enter declarations. The free sort modifier forbids dummies of that sort. The strict modifier forbids bound binders, dummies, and appearances in dependency lists.

Notation

The last two chapters wrote expressions by applying constructors, as in imp a (imp b a). A notation declaration lets that same expression be written a -> (b -> a).

The parser uses notation to read expressions. Aufbau also uses it to format expressions for display. It changes how a math string may be written, but the result is still a tree of term constructors. In a theory that declares a notation, the notation and constructor-application forms are interchangeable everywhere.

Infix operators

infixl and infixr make a two-argument constructor into an infix operator at a given precedence.

A higher precedence binds more tightly, so /\ at 30 groups before -> at 25. infixr associates to the right and infixl to the left. Each lemma below states one spelling against the other and closes with iff_refl, which succeeds only if the two are the same expression.

An infix precedence must be below max, and a token may be declared at only one precedence. If two infix operators have the same precedence, they must associate the same way. An infixl and an infixr declared at the same precedence will be rejected. Operators sharing an associativity and precedence level can be mixed freely, so with /\ and \/ both infixl at 30, a /\ b \/ c is (a /\ b) \/ c.

Prefix operators

prefix creates an operator written before its argument. Prefix operators also have a precedence: ~ at 40 binds more tightly than /\ at 30, so ~ a /\ b means (~ a) /\ b.

Precedence also decides whether a prefix operator’s argument needs parentheses around it. Repeated application of a prefix operator never needs parentheses.

Delimiters

Sorts and terms introduced delimiters. Math strings are split on whitespace first; delimiter characters then split the pieces further. The characters can be given as one list or as separate left and right lists.

delimiter $ ( ) $;          -- both
delimiter $ ( $ $ ) $;      -- left, then right

A left delimiter splits after itself and a right delimiter before itself; a character in the one-list form does both. Grouping therefore needs ( on the left and ) on the right. Declaring them the other way round leaves something like (imp a single token.

Delimiters must be a single byte. delimiter $ ( ) λ $; is rejected, which is why a lambda is written λ x. e and not λx. e — λ cannot be declared a delimiter to separate it from adjacent text.

Notation for everything else

notation covers constants, binders, and mixfix operators, whose notation places fixed tokens before, between, or after arguments. It lists the declaration’s variables interleaved with constants, each constant written (token:prec).

The first literal must be a constant, and it may not be shared with any other notation. . is listed as a delimiter so that x. splits into two tokens.

When a string parses as something else

A binder notation’s trailing slot is parsed with the precedence declared on the leading constant, so λ x. x + x is (λ x. x) + x in the small theory above:

+ has precedence 30, which is less than the leading constant’s 41, so the body is just x and the sum is formed around the lambda rather than inside it. The ($.$:0) in the declaration is the precedence of the . token and does not extend the body past +. Parentheses give the intended reading:

Alternative notations

A constructor can carry more than one notation. The theories in this manual declare an ASCII and a Unicode form of each operator at the same precedence:

infixr imp: $->$ prec 25;
infixr imp: $→$ prec 25;

Both parse to imp, so a proof may use whichever reads better or is easier to type. A rule stated with one applies to a goal written with the other.

Axioms, theorems, and definitions

Besides declaring a theory’s syntax, an .mm0 file states its axioms and theorems and introduces definitions.

Axioms

An axiom states a rule that the theory accepts without proof.

axiom ax_k (a b: wff): $ a -> b -> a $;

Hypotheses go ahead of the conclusion, separated by >:

axiom mp (a b: wff): $ a $ > $ a -> b $ > $ b $;

The last formula is the conclusion and every formula before it is a hypothesis, so mp says b is derivable whenever a and a -> b are. Every formula in an axiom must have a provable sort.

An axiom’s binder list gives the sorts with which the rule may be instantiated and any restrictions described in Variables, binders, and dependencies.

Hypotheses as binders

A hypothesis can also be written as a binder with a formula for its sort.

axiom mp (a b: wff) (h1: $ a $) (h2: $ a -> b $): $ b $;

This declares the same rule as the arrow form above. The two can be combined, and hypotheses are taken in the order they appear either way.

Ordinary binders may follow a hypothesis binder, but a hypothesis can only mention variables already declared to its left, so in practice the variables come first.

Proof lines cite hypotheses with a # reference: positionally as #1 and #2 under either spelling, or by name as #h1 and #h2 when the hypothesis is a named binder.

Theorems

A theorem is written like an axiom.

theorem id (a: wff): $ a -> a $;

Unlike an axiom, a theorem requires a proof block in the .auf file.

The .mm0 file gives a human-readable specification of what the compiled .mmb file must prove. The verifier checks the binary proof against that specification.

Definitions

A def introduces a new constructor that abbreviates a different expression.

A defined term such as not is still a constructor and can carry notation. Definitions are conservative: replacing each defined term with its body removes the definitions without changing what is provable.

Definitions are transparent at rule applications. The folded and unfolded forms are the same expression as far as matching is concerned, so each line can be written in whichever form is clearer.

weaken_not is ax_k instantiated at a -> F., unfolded on the left of the arrow and folded on the right. not_elim gives mp the folded term ~ a for its second, implication-shaped hypothesis; it unfolds automatically.

Dummy variables

A definition’s body may use variables that are not among its arguments. A dot in the binder list indicates that the variable is hidden and not among the required arguments of the definition.

uniq takes x and p. Its y is internal to the body. A proof that unfolds uniq may instantiate it with any variable that does not clash. The free sort modifier described in Sorts and terms forbids hidden dummies of a sort.

Definition checking

A definition’s result type must declare every variable that remains free in its body: that is, every variable not captured by a binder in the body.

definition body has free variables that the result type does not declare

The body eq x x has x free, and the bare sort wff does not declare any dependencies. The fix is to declare the dependency the body really has. A def may carry dependencies on its result type in the same way as a term.

Here’s the fixed version:

def refl_of {x: tm}: wff x = $ eq x x $;

Every refl_of x now counts as having x free — as it must, since unfolding it produces eq x x.

Binders inside the body capture free variables. uniq from the previous section is accepted with a bare wff because ex y and all x between them capture everything:

FV(eq x y)                        = {x, y}
FV(iff p (eq x y))                = {x, y}
FV(all x (iff p (eq x y)))        = {y}
FV(ex y (all x (iff p (eq x y)))) = {}

FV(p) is {x} because uniq declares p as wff x. What makes all x subtract that x again is all’s declaration, term all {x: tm} (p: wff x): wff: the x on the argument p says that this constructor binds x within that argument. If you declare it as (p: wff) then all does not bind anything.

This free-variable computation occurs only during definition checking. At rule applications, the restrictions from Variables, binders, and dependencies use plain occurrence: an expression counts as mentioning a variable if the variable appears anywhere in it, even under a binder. all x (eq x y) cannot instantiate an argument whose dependency list excludes x, although x is not free in it. Binding structure counts when a definition is checked, and never when a rule is applied.

Definitions without a body

The body of a definition may be omitted.

def nand (a b: wff): wff;

The .mm0 interface declares that the connective exists without specifying its body. Theorems about the connective can specify its required properties. The proof file must supply a body and prove those theorems, as described in Lemmas and definitions in proofs.

Proof blocks and lines

An .auf file supplies the proofs for the theorems declared in an .mm0 file. The Proving chapters introduced proof scripts by example; this part of the manual describes the format itself. An .auf file is a sequence of top-level items: proof blocks, which prove the declared theorems, plus the lemma blocks and def items described in Lemmas and definitions in proofs. This chapter covers proof blocks and the exact form of a proof line.

Declaration and proof ordering

The compiler reads the .mm0 and .auf files together, in statement order. Each theorem declaration in the .mm0 file must be proved by the next theorem proof block in the .auf file.

Proof blocks must appear in the same order as the corresponding theorem declarations. If the two blocks above are swapped, the compiler finds weaken_twice where it expects weaken and rejects the file.

Declaration order also determines what a proof may cite: any axiom, any public theorem already proved, and any earlier lemma or proof-local definition. weaken_twice cites weaken this way. Later declarations in either file are not visible, so forward references are rejected.

Proof blocks

A proof block is the theorem’s name, an underline, and the proof lines. The underline appears on the line immediately after the name and consists of at least three dashes, with nothing else on it. The block extends to the next top-level item or to the end of the file. Blank lines within a block are ignored.

Proof lines

Each line has the form introduced in The parts of a proof line:

label: $ GOAL $ by rule (bindings) [references]

Lines are checked in order. Each line is an application of the cited rule. Once a line checks, its label names the proved goal for the rest of the block. Labels must be unique within their block.

Each rule must be an axiom, public theorem, or lemma in scope, and the bracketed list must supply exactly as many references as the rule has hypotheses — omitting the brackets is the same as writing []. Rule references and bindings are the subject of the next chapter.

Admitting a line

A line may be justified by sorry! instead of a rule. The goal is accepted without proof, and the block is otherwise checked as usual: later lines may cite the admitted line, and the last line must still match the declared conclusion.

The compiler reports a warning at each sorry! and, from the command line, exits with status 3 after writing the output. The MMB carries a Sorry instruction at that line only, so the verifier checks every other step; it names each admitted theorem and exits with status 3 as well. sorry! takes no bindings or references, and its goal may not contain holes.

Layout and comments

Within a proof line, line breaks may fall before or after by, inside binding and reference lists, or inside math strings. A new proof line must begin on a fresh line with its label.

A -- comment runs to the end of the line. Comments may stand alone between blocks and between proof lines, follow a header or a proof line, and interrupt a line that spans several physical lines. The underline is the exception: it must include nothing but dashes.

Comments beginning with --| are annotation comments. They can be used to attach rule metadata — @rewrite, @view, and the annotations in the annotation reference — to the item that follows, just as in an .mm0 file. In an .auf file they may only precede lemma blocks; a public theorem’s metadata belongs on its .mm0 declaration, not on its proof block. A --| line that does not start with @ is a doc comment, shown when the item’s name is hovered; those may precede any item. A standalone --| line also ends the current block, so it may be written directly after the last line of the preceding proof.

Proof conclusions

A block is accepted only if its final line proves the theorem’s declared conclusion. Proving that conclusion on an earlier line is not enough. The final line need not use exactly the same expression as the declaration: the compiler can expand definitions and apply registered normalization rules to match them. It includes the necessary conversion steps in the binary proof. Lemma blocks are checked against their headers in the same way.

References and bindings

Everything after by in a proof line is a rule application:

rule (bindings) [references]

The references supply proofs of the cited rule’s hypotheses, and the bindings instantiate its variables. This chapter describes both references and bindings, ending with inline applications — rule applications used as references.

The reference list

The brackets hold one reference per hypothesis of the cited rule, in the order the rule declares its hypotheses; a mismatched count is an error. Each reference is either:

• a hypothesis reference #n or #name, citing a hypothesis of the theorem or lemma being proved;
• a line reference, a bare label citing an earlier line of the same block; or
• an inline application, a rule applied on the spot (described below).

A bare identifier is always read as a line reference, even when a rule has the same name. Writing h1 in a block with no line labeled h1 reports an unknown label; applying the axiom in place requires the inline-application syntax, at minimum h1 [].

Labels are local to their block. A proof cannot refer to a line in another block.

Hypothesis references

Hypotheses are numbered #1, #2, … in the order they appear in the theorem’s header. A hypothesis declared as a named binder may also be cited by name.

#hab and #hbc cite the two named hypotheses; #1 and #2 would be another way of referring to those hypotheses. The arrow-form hypothesis $ a $ has no name and can only be cited as #3. A # name that matches no hypothesis binder is an error.

Bindings

A binding assigns an expression to one of the cited rule’s binders:

(name := $ expr $, ...)

Each name must be a binder of the rule, and each expression is written like any other math string, using the variables of the current block. The order of the bindings does not matter, but assigning the same binder twice or naming a binder the rule does not have is an error.

Bound binders are assigned the same way, but a {x} binder stands for a variable, so it must be given a bare variable, not a compound expression.

Instantiations remain subject to the occurrence-based restrictions described in Variables, binders, and dependencies.

Omitted bindings

Bindings are usually omitted. The compiler infers each missing binder by matching the stated goal against the rule’s conclusion and the references against the rule’s hypotheses. Both proofs above check with their binding lists deleted, so you can hover a line once its cell checks to see what was inferred.

When the goal is written out and every reference is a hypothesis or an earlier line, the compiler matches complete formulas. This usually determines every variable the rule mentions. Undetermined binders arise mainly with inline applications, whose goals are not explicitly written down.

Inline applications

A reference may itself be a rule application, written with the same syntax that follows by. It behaves like an anonymous proof line inserted just before the line that uses it: the rule is applied, and its conclusion becomes the reference expression. The hidden line has no label and cannot be cited later; a result needed more than once should get a labeled line of its own.

Because a bare identifier is always a line reference, an inline application must carry a reference list or a binding list. A rule with no hypotheses is applied as h1 []; when a binding list is present, an empty reference list may be dropped.

This is weaken from above with the h1 instance applied in place. Inline applications nest, and mix freely with the other reference kinds.

An inline application has no written goal, so the compiler must infer its entire conclusion. The enclosing application supplies the expected conclusion from the stated goal, explicit bindings, and other references. In weaken_inline, the goal and #1 fix both variables of mp, so h1 is asked to prove p -> (q -> p) and its own variables are forced.

The expected conclusion need not be complete. A variable of the enclosing rule that is still unknown is left open in the hint, to be settled by the inline application’s own conclusion or by another reference — including one further to the right. Every variable must be determined somewhere in the line. If one remains unknown, the compiler rejects the line. Supply the missing value with a binding list on the inline application:

The compiler must resolve every binding in an inline application before it can finish checking the enclosing application. It does not try several possible values for an unresolved binder.

The unpack action described in The parts of a proof line reverses this notation. It creates one labeled line per inline application and fills each new goal from the checked conclusion.

Lemmas and definitions in proofs

An .auf file is a sequence of top-level items: proof blocks, lemma blocks, and def items. Proof blocks prove the theorems declared in the .mm0 file. lemma and def items extend the theory without adding unproved assumptions.

Proof blocks

A theorem declared in the .mm0 file is proved by a block consisting of the name of the theorem, an underline of at least three dashes, and the proof lines.

Theorem proof blocks appear in the same order as their declarations. The compiler reads the .mm0 and .auf files together, so a proof can cite only declarations already in scope. Forward references are rejected.

Lemma blocks

A lemma block declares a proof-local rule. It carries its own signature, written like an MM0 axiom:

lemma NAME (binders): $ hypothesis $ > $ conclusion $
----
proof lines

Once proved, a lemma is cited exactly like an axiom or a public theorem: by name, with its hypotheses in brackets and its variables inferred from the goal and the references.

and_comm is a derived rule: from a proof of g ⊢ a ∧ b it produces one of g ⊢ b ∧ a, for any context and any two formulas. Line l2 of and_comm_imp applies it with g bound to a ∧ b.

Lemmas are not part of the theory’s .mm0 interface, and nothing outside the proof file can cite them. In the compiled .mmb binary they are emitted as local theorems.

Definitions with hidden bodies

A definition declared in the .mm0 file may omit its body. An omitted body can then be supplied by the proof file:

This form is called a body filler. It has no return sort, unlike a proof-local definition. It must appear where the compiler reaches the corresponding bodyless declaration. The definition it fills is public: it is emitted as an ordinary term definition and checked against the .mm0 declaration, so it can carry notation, and a ⊼ b is available in proofs.

Leaving the body out of the .mm0 file means that the interface commits only to the connective’s existence. The file may still declare theorems involving the defined term. This supports constructive implicit definitions: the interface specifies a term through properties that must be proved, while the proof development supplies a concrete definition satisfying them.

Proof-local definitions

A def item with a return sort declares a definition local to the proof file:

def NAME (binders): sort = $ body $

Like a lemma, it is a top-level item rather than a proof line. It takes no underline, and is available to later proof lines, lemmas, and definitions but not before its own declaration. The .mm0 file may not mention it: the theory must stand on its own for any MM0 verifier, and nothing there declares the name. A statement in the .mm0 file that names a proof-local definition is an error.

Proof-local definitions take the same --| annotations as an .mm0 term, so a local operator can be declared @acui with its laws proved as lemmas alongside it (see the annotation reference).

Local notation

A proof-local definition may be given notation in the proof file. The declaration is written exactly as it would be in the .mm0 file, semicolon included, and follows the definition it names:

prefix, infixl, infixr, and general notation declarations are accepted; coercion and delimiter are not. The notation is visible to later proof lines, lemmas, and definitions, and hovers and goal displays use it. Only a proof-local definition may be named: notation for a term the .mm0 file declares belongs in the .mm0 file. The token, precedence, and associativity tables are shared with the theory, so a local token should not be one the .mm0 file also declares.

Like ordinary definitions, proof-local definitions are transparent at rule applications: the folded and unfolded forms are interchangeable, and each line can be stated in whichever form is clearer. A defined connective can be introduced and its rules derived without writing the expanded form anywhere but the definition itself.

Equality and normalization

Theories in earlier chapters used annotations to reorder contexts, normalize substitutions, and reconcile concrete proof lines with the rules they cite. This part explains how to add those features to a theory.

Annotations belong to the compiler frontend and do not extend the trusted kernel. The compiler emits their effects as ordinary rule applications, which the verifier checks against the unannotated MM0 theory. Annotations change how the compiler constructs a binary proof certificate, not what the verifier accepts.

This chapter covers @relation, @congr, @rewrite, and @acui. Each may be attached to an .mm0 declaration or, except for @acui, to a lemma block in the .auf file, where it takes effect once the lemma is proved.

Relation bundles

When a rule’s instantiated conclusion differs from the written goal, the compiler can prove that the two are equivalent. It needs an equivalence relation for the sort and rules for reflexivity, transitivity, symmetry, and transport. Transport uses an equivalence to turn a proof of one expression into a proof of the other. A @relation annotation registers this group of rules, called a relation bundle:

--| @relation <sort> <relation-term> <refl> <trans> <symm> <transport>

The natural deduction theory of the Proving chapters proves sequents, and registers ⟚ as the equivalence on them:

--| @relation seq seq_eq seq_refl seq_trans seq_sym seq_mp
axiom seq_refl (s: seq): $ s ⟚ s $;
axiom seq_trans (s t u: seq): $ s ⟚ t $ > $ t ⟚ u $ > $ s ⟚ u $;
axiom seq_sym (s t: seq): $ s ⟚ t $ > $ t ⟚ s $;
axiom seq_mp (s t: seq): $ s ⟚ t $ > $ s $ > $ t $;

The transport rule seq_mp is what makes the bundle useful on a provable sort. After normalization by rewrite rules (see below), the compiler holds a proof of the raw conclusion and a proof that the raw conclusion is equivalent to the user’s assertion; transport combines them into a proof of the assertion itself.

For a non-provable sort there is no such thing as a proof of the sort’s expressions, so no transport rule is necessary. Write _ in its place. The same theory does this for its equivalences on formulas and on contexts:

--| @relation wff iff iff_refl iff_trans iff_sym _
--| @relation ctx ctx_eq ctx_refl ctx_trans ctx_sym _

The four bundle rules must not have bound binders, since the compiler instantiates them with arbitrary subexpressions when assembling a proof.

Congruence rules

An equivalence can be discovered deep inside an expression (by rewrite rules or proof search), and the compiler then needs to lift the resulting equivalence through each surrounding constructor. A @congr annotation marks the rule that justifies this for one constructor:

--| @congr
axiom nd_congr (g h: ctx) (a b: wff):
  $ ctx_eq g h $ > $ a ↔ b $ > $ (g ⊢ a) ⟚ (h ⊢ b) $;

The binder layout follows a fixed convention: for each regular argument of the constructor, a before and an after variable, in argument order, with one hypothesis relating each pair. When an argument is unchanged the compiler supplies a reflexivity proof itself, so one congruence rule per constructor suffices.

Congruence rules may cross sorts. nd_congr lifts a context equivalence and a formula equivalence into a sequent equivalence; in the lambda calculus theory, eq_congr lifts two term equations into ↔:

--| @congr
axiom eq_congr (a b c d: tm) (h1: $ a = b $) (h2: $ c = d $):
  $ iff (a = c) (b = d) $;

The compiler picks the right relation for each hypothesis from the sort of the corresponding argument. A sort with no registered relation is simply left alone: children of that sort are never rewritten, and no congruence proof is required for them.

For a binding constructor, the bound argument appears once and stays unchanged. Each before/after pair of regular arguments must declare every dependency the constructor permits:

--| @congr
axiom lam_congr {x: tm} (a b: tm x) (h: $ a = b $): $ (λ x. a) = (λ x. b) $;

Declaring (a b: tm) instead would reject the annotation: a congruence lift plugs in arbitrary bodies, which may mention x.

Rewrite rules

@rewrite marks an axiom or theorem as an oriented rewrite equation. The conclusion must have the form rel lhs rhs for a registered relation. The compiler applies the equation from left to right, replacing a matching expression with the corresponding instance of the right-hand side. The substitution equations of the lambda calculus chapter are an example of a useful set of rewrite rules:

--| @rewrite
axiom sb_var {x: tm} (a: tm x): $ [x := a] x = a $;
--| @rewrite
axiom sb_vac {x: tm} (e: tm) (a: tm x): $ [x := a] e = e $;
--| @rewrite
axiom sb_add {x: tm} (f g: tm x) (a: tm x):
  $ [x := a] (f + g) = ([x := a] f) + ([x := a] g) $;

These rules apply during ordinary line checking. When a rule application’s instantiated conclusion or hypothesis does not match the corresponding expression exactly, the compiler normalizes both sides with the registered rewrites and compares the results, emitting every step it takes. That is why a line can cite beta — whose right-hand side is a substitution term — and state the substituted result:

The raw right-hand side is [x := S0] (S (x + 0)). The compiler reduces it with sb_suc, sb_add, sb_var, and sb_vac, lifts the steps through S and + with the congruence rules, joins them with transitivity, and transports the raw conclusion to the stated one. The binary proof records each of these steps as an ordinary rule application.

When choosing rewrite rules, keep these constraints in mind:

• Rules are indexed by the head constructor of their left-hand side. When several rules share a head, they are tried in declaration order and the first matching rule applies, with no backtracking. Put specific rules before general ones.
• Rules that undo one another can cause normalization to loop. A step limit stops the loop, after which the line fails with a mismatch.
• Matching works on visible syntax. A rewrite does not apply inside a folded definition; transparent definitions are a separate mechanism.

Orientation matters: a rewrite set should reduce toward a normal form. Equations such as commutativity do not give a useful left-to-right normal form. Register them for conversion? instead, as described in Computation.

Substitution

The beta example above cited a rule whose conclusion contains a substitution term:

axiom beta {x: tm} (e: tm x) (a: tm x): $ (λ x. e) · a = [x := a] e $;

The proof line states the reduced result

(λ x. S (x + 0)) · S0 = S (S0 + 0)

instead of the literal instance

(λ x. S (x + 0)) · S0 = [x := S0] (S (x + 0))

Rewrite rules perform the reduction between these forms.

MM0 has built-in substitution only for a rule’s binders: applying a rule assigns one expression to each binder and uses it at every occurrence. It has no built-in operation for replacing x with t inside an arbitrary expression p. Rules such as β-reduction, quantifier instantiation, and induction still need to express this operation.

Following Metamath, an MM0 theory that needs substitution defines it within the logic. The fol-base prelude extends the natural-deduction theory with quantifiers and declares a substitution operator for formulas:

term sb {x: obj} (t: obj x) (p: wff x): wff;
notation sb {x: obj} (t: obj x) (p: wff x): wff =
  ($[$:41) x ($:=$:0) t ($]$:0) p;

sb is an ordinary term constructor, not a built-in compiler operation: `[x

= y] (P x)andP y` are distinct expressions. The substitution relation is axiomatized:

--| @rewrite
axiom sb_vac {x: obj} (t: obj x) (p: wff): $ [x := t] p ↔ p $;
--| @rewrite
axiom sb_P {x: obj} (t: obj x): $ [x := t] (P x) ↔ P t $;
--| @rewrite
axiom sb_imp {x: obj} (t: obj x) (p q: wff x):
  $ [x := t] (p → q) ↔ ([x := t] p → [x := t] q) $;
--| @rewrite
axiom sb_all {x y: obj} (t: obj x) (p: wff x y):
  $ [x := t] (∀ y p) ↔ ∀ y ([x := t] p) $;

Registering the substitution axioms as rewrite rules makes the operator practical to use. Read together, the rules define its behavior:

• sb_vac: a vacuous substitution vanishes. The declaration (p: wff) excludes x from p’s dependencies. This requires that p not mention x at all, even under a binder.
• sb_P: at an atom, the replacement actually happens: assign y to t and the right-hand side reads P y. Each atomic predicate gets one such equation.
• sb_imp: substitution distributes through a constructor.
• sb_all: the substitution moves under another binder. The dependency list prevents capture: (t: obj x) permits t to mention x but not y, so moving it under ∀ y cannot bind a variable in t.

With the operator and its equations in place, quantifier rules can be stated, and (as with beta) used without sb ever needing to be written explicitly. The compiler normalizes the instantiated conclusion before comparing it against what the author wrote:

The raw conclusion of l2 is ∀ x (P x → P x) ⊢ [x := y] (P x → P x): sb_imp splits the substitution, sb_P finishes each side, congruence lifts the steps through → and ⊢, and transport produces the stated conclusion. A complete equation set keeps sb confined to rule statements this way, with proof lines stating only substituted results.¹

The lambda calculus equations earlier in the chapter use the same approach for substituting a term into a term: sb_var handles the variable itself in place of the per-atom equations, and sb_lam plays sb_all’s role, blocking capture the same way, by omitting y from the dependency list of the replacement a.

Structural combiners

The context , of the natural deduction theory is not governed by oriented rewrites but by an @acui annotation on the combiner itself:

--| @acui ctx_assoc ctx_comm emp ctx_idem
term join (g h: ctx): ctx; infixl join: $,$ prec 5;

The four fields are the associativity axiom, the commutativity axiom (or _), the unit term, and the idempotence axiom (or _). The compiler canonicalizes any expression built from the combiner (flattening nested joins, dropping units, sorting members when commutativity is declared, merging duplicates when idempotence is) and proves the canonical form equal to the original using exactly the cited axioms. With all four properties registered, contexts containing the same formulas are interchangeable regardless of order, grouping, or duplicates:

ax concludes g , a ⊢ a; the compiler splits the stated context into g := c , a and the principal formula b even though b sits in the middle. Without the annotation the same theory rejects the line:

Here g , a can only match the raw tree (c , b) , a, so the rule proves c , b , a ⊢ a and the line fails with a conclusion mismatch.

Associativity is mandatory; the other properties are independent. A non-commutative monoid like function composition declares --| @acui comp_assoc _ id _ and gets flattening and unit elimination while preserving order. Unit elimination also requires the matching unit laws to be in scope, such as ctx_eq (emp , g) g in the natural deduction theory. Each removed unit needs a proof.

An @acui combiner needs its companions: a @relation bundle for its sort, and a @congr rule for the combiner, so the structural steps can be proved and lifted like any other rewrite.

1. The compiler recovers y as the substituted term through the @view annotations described in Views and recovery. ↩

Ergonomics: variables, freshness, holes, fallbacks

This chapter covers four annotation families that help make proofs easier to write: hole tokens, variable pools, renaming to avoid variable clashes, and alternative rules to try when an application fails.

As a running example we extend the natural deduction theory with quantifiers. The extension lives in two prelude files, fol-base (syntax, substitution, and equality metadata) and fol-rules (the quantifier rules), loaded on top of the propositional theory. This chapter uses the first file and one rule from the second.

delimiter $ [ ] $;

--| @vars u v w
sort obj;

term all {x: obj} (p: wff x): wff;
prefix all: $∀$ prec 41;
prefix all: $A.$ prec 41;
term ex {x: obj} (p: wff x): wff;
prefix ex: $∃$ prec 41;
prefix ex: $E.$ prec 41;

term P (t: obj): wff;
prefix P: $P$ prec 50;

term sb {x: obj} (t: obj x) (p: wff x): wff;
notation sb {x: obj} (t: obj x) (p: wff x): wff =
  ($[$:41) x ($:=$:0) t ($]$:0) p;

--| @congr
axiom imp_congr (a b c d: wff):
  $ a ↔ b $ > $ c ↔ d $ > $ (a → c) ↔ (b → d) $;
--| @congr
axiom and_congr (a b c d: wff):
  $ a ↔ b $ > $ c ↔ d $ > $ (a ∧ c) ↔ (b ∧ d) $;
--| @congr
axiom or_congr (a b c d: wff):
  $ a ↔ b $ > $ c ↔ d $ > $ (a ∨ c) ↔ (b ∨ d) $;
--| @congr
axiom not_congr (a b: wff): $ a ↔ b $ > $ ¬ a ↔ ¬ b $;
--| @congr
axiom all_congr {x: obj} (p q: wff x): $ p ↔ q $ > $ ∀ x p ↔ ∀ x q $;
--| @congr
axiom ex_congr {x: obj} (p q: wff x): $ p ↔ q $ > $ ∃ x p ↔ ∃ x q $;

--| @rewrite
axiom sb_vac {x: obj} (t: obj x) (p: wff): $ [x := t] p ↔ p $;
--| @rewrite
axiom sb_P {x: obj} (t: obj x): $ [x := t] (P x) ↔ P t $;
--| @rewrite
axiom sb_imp {x: obj} (t: obj x) (p q: wff x):
  $ [x := t] (p → q) ↔ ([x := t] p → [x := t] q) $;
--| @rewrite
axiom sb_and {x: obj} (t: obj x) (p q: wff x):
  $ [x := t] (p ∧ q) ↔ ([x := t] p ∧ [x := t] q) $;
--| @rewrite
axiom sb_or {x: obj} (t: obj x) (p q: wff x):
  $ [x := t] (p ∨ q) ↔ ([x := t] p ∨ [x := t] q) $;
--| @rewrite
axiom sb_not {x: obj} (t: obj x) (p: wff x):
  $ [x := t] (¬ p) ↔ ¬ ([x := t] p) $;
--| @rewrite
axiom sb_all {x y: obj} (t: obj x) (p: wff x y):
  $ [x := t] (∀ y p) ↔ ∀ y ([x := t] p) $;
--| @rewrite
axiom sb_ex {x y: obj} (t: obj x) (p: wff x y):
  $ [x := t] (∃ y p) ↔ ∃ y ([x := t] p) $;

--| @alpha x y
axiom all_alpha {x y: obj} (p: wff x y): $ ∀ x p ↔ ∀ y ([x := y] p) $;
--| @alpha x y
axiom ex_alpha {x y: obj} (p: wff x y): $ ∃ x p ↔ ∃ y ([x := y] p) $;

The second half of the file uses the substitution operator [x := t] p from the previous chapter. Its @congr and @rewrite annotations let the compiler normalize substitutions. This chapter introduces @vars and @alpha, which support variable selection and renaming.

Hole tokens

@hole attaches to a sort. It registers a token that proof lines may use for an omitted subexpression of that sort:

--| @hole _wff
sort wff;
--| @hole _ctx
sort ctx;

Register holes for sorts whose expressions are routinely determined by the rest of a proof line. In the natural-deduction theory, ctx is a good candidate because contexts are large, repetitive, and usually fixed by the cited rule.

A hole token may use any otherwise available token, including Unicode. This manual follows the _sort convention.

Variable pools

A @vars annotation on a sort registers tokens that proof lines may use as variables.

--| @vars u v w
sort obj;

When one of these tokens appears in proof math and is not otherwise known, the compiler creates a theorem-local dummy variable of the annotated sort.

The proof needs a name for the witness to ex_intro. The variable u comes from the @vars pool.

Pool tokens work in proof line math only. Statement headers, including lemma headers, must declare their variables as binders, and a pool token appearing there is an unknown token. The annotation is rejected on strict and free sorts, which forbid theorem-local dummies. A token that collides with another pool, a term name, or a notation token is also rejected.

The compiler also uses @vars pools when it needs a variable that the proof does not specify. For example, unfolding a definition may require a dummy variable that the target expression does not determine. A sort whose rules use these features needs a @vars pool even if proof authors never write the tokens themselves.

Freshness: @freshen and @alpha

Variables, binders, and dependencies introduced the dependency check: if a rule declares {x: obj} and an argument (g: ctx) without x in its dependency list, then whatever is substituted for g may not mention the variable assigned to x anywhere, even bound by a quantifier. For ∀-introduction this is stricter than the textbook side condition. The rule

axiom all_intro (g: ctx) {x: obj} (p: wff x):
  $ g ⊢ p $ > $ g ⊢ ∀ x p $;

demands that the context not mention x at all, while the textbook only forbids free occurrences. A context that merely quantifies over the same letter is rejected:

The generalization here is vacuous. P b does not mention a — and the a inside the context is bound by its own ∀. On paper this is fine. The line still fails:

dependency violation: the rule does not allow g to mention the variable
assigned to x

Alpha-renaming repairs this case: ∀ a (P a) and ∀ u (P u) denote the same hypothesis. MM0 has no built-in alpha-conversion, but the theory can prove a renaming principle:

--| @alpha x y
axiom all_alpha {x y: obj} (p: wff x y): $ ∀ x p ↔ ∀ y ([x := y] p) $;

--| @freshen g x
axiom all_intro (g: ctx) {x: obj} (p: wff x):
  $ g ⊢ p $ > $ g ⊢ ∀ x p $;

@alpha old new registers a proved renaming equivalence for one binding constructor. @freshen g x allows the compiler to try renaming when the value of g violates the dependency restriction for x. It uses a registered @alpha rule and a fresh variable from the @vars pool to rename the conflicting bound occurrence, then retries the application. The renamed application then proves an alpha-variant of the user’s line, and the ordinary congruence and transport machinery returns it to the stated form. With the annotated rule from fol-rules, the same proof checks:

The repair applies only to the declared argument pair. It chooses one fresh variable and tries the registered alpha rules for that constructor. This handles some cases where MM0’s occurrence check is stricter than a free-variable check. It does not make matching generally ignore bound variable names.

A @freshen repair requires: a @vars pool on the binder’s sort, an @alpha rule for each binding constructor that may head the offending subexpression, and the substitution rewrites that reduce the renamed body.

Fallbacks: @fallback

Some rules form families that should share one user-facing name. For example, a theory may expose one and_elim rather than separate left and right elimination names. @fallback connects the members of such a family:

--| @fallback and_elim_r
axiom and_elim (g: ctx) (a b: wff): $ g ⊢ a ∧ b $ > $ g ⊢ a $;

If a proof line cites and_elim and the application fails, the compiler retries the same line with and_elim_r.

l2 is an ordinary and_elim application. l1 checks through the fallback: matching and_elim’s conclusion against the line determines a := b, after which #1 cannot supply the premise, so the attempt fails and the retry with and_elim_r proves the line.

Fallbacks chain: the target rule may carry a @fallback of its own. The candidates are tried in chain order. When every candidate fails, the current diagnostic comes from the first attempted rule, keeping the error anchored to the rule name the line actually cites. A rule takes at most one @fallback; the target must be declared earlier in the file.

Views and recovery

A proof line may state a rule’s result in a different form from its declaration. For example, the declaration may contain a substitution term while the line states the result of that substitution. Rewrite rules can check that the two forms agree, but in order to apply rewrites the compiler must first infer the rule’s bindings.

This chapter explains three annotations that help with binder inference. @view describes the form used in proof lines. @recover extracts a substituted expression, and @abstract recovers the surrounding expression into which a substitution was made.

The problem

Consider ∃-introduction:

axiom ex_intro {x: obj} (g: ctx) (t: obj x) (p: wff x):
  $ g ⊢ [x := t] p $ > $ g ⊢ ∃ x p $;

To conclude g ⊢ ∃ x p, cite a proof of p with the witness t substituted for x. Without annotations, this cell fails:

the statement and cited premises could not be matched against this rule
first unsolved binder: x

The goal determines p := P x. But the witness t occurs inside [x := t] p, which doesn’t occur in the written line (instead, the cited line shows the substitution already carried out: P y). The line does check with the bindings spelled out, (x := $ x $, t := $ y $, p := $ P x $), but repeating these bindings is unnecessary work: the cited line already shows the witness y.

@view: an alternative signature

A @view annotation gives the compiler an alternative signature that matches the form used in proof lines:

--| @view {x: obj} (g: ctx) (t: obj x) (p: wff x) (q: wff): $ g ⊢ q $ > $ g ⊢ ∃ x p $
--| @recover t q p x
--| @freshen g x
axiom ex_intro {x: obj} (g: ctx) (t: obj x) (p: wff x):
  $ g ⊢ [x := t] p $ > $ g ⊢ ∃ x p $;

The text after @view is a theorem-like signature. Keep the entire annotation on one line. It must declare exactly as many hypotheses as the rule. The compiler matches the view’s conclusion against the proof line and its hypotheses against the cited references, getting bindings from the user-supplied line.

View binders are matched to rule binders by name. x, g, t, and p name real rule binders, so solving them in the view solves the rule. q names no rule binder: it is a phantom binder, local to the view. Here it captures what the cited line proves (P y). Recovery annotations can then use these extra bindings to solve the remaining rule variables.

@recover: extracting a buried witness

The view solves p := P x and q := P y, but nothing yet solves t. That’s what @recover is for:

--| @recover <target> <source> <pattern> <hole>

The four names should be view binders, read as: to solve target, walk source and pattern in parallel, and wherever pattern reaches the value of hole, take the corresponding subtree of source. For ex_intro, @recover t q p x walks P y against P x; the hole x sits under P, the corresponding subtree of the source is y, so t := y.

With t recovered, the compiler instantiates the raw rule, normalizes [x := y] (P x) to P y with the substitution rewrites, and the application closes.

Recovery compares the structure of the two expressions. If the hole occurs several times, every extracted candidate must agree. It skips unchanged occurrences in bound argument slots, so it does not mistake a substitution operator’s binder for its witness.

If source and pattern are identical, recovery assigns the hole itself to the target: substituting a variable for itself leaves the expression unchanged. Any other structural mismatch makes recovery fail.

∀-elimination is the same pattern on the conclusion side:

--| @view {x: obj} (g: ctx x) (t: obj x) (p: wff x) (q: wff): $ g ⊢ ∀ x p $ > $ g ⊢ q $
--| @recover t q p x
axiom all_elim {x: obj} (g: ctx x) (t: obj x) (p: wff x):
  $ g ⊢ ∀ x p $ > $ g ⊢ [x := t] p $;

Here the phantom q captures the stated goal, and the witness is recovered from what the user wants to conclude:

@abstract: recovering a context

@recover extracts a subexpression. @abstract recovers the surrounding structure shared by two expressions, with a variable marking the positions to replace. This is useful for a rule that replaces a with b inside a formula, given a ↔ b:

This is a self-contained theory: sb t x r substitutes a formula for a formula variable, and replace is substitution of equivalent formulas. As with the quantifier rules, proof lines should not need to mention the substitution operator. Here the view already determines the formulas being substituted, but not their surrounding structure. We recover that structure with:

--| @abstract <target> <left> <right> <hole> <left-plug> <right-plug>

The names are view binders: walk left and right in parallel, and wherever the pair is exactly (left-plug, right-plug), put hole; everything else must agree on both sides and is kept. In repl_demo the walk of a → ⊤ against b → ⊤ finds the plug pair on the left-hand side of the arrow and recovers r := x → ⊤. Several occurrences of the pair are fine. repl_two recovers r := x → x, replacing both at once.

Plugs as patterns

replace reads its plugs off the premise a ↔ b. A rule without such a premise has nothing to read them off. For example, De Morgan’s law might rewrite ¬ (A ∧ B) to ¬ A ∨ ¬ B anywhere in a formula, and A and B are only known once the site is found. In this situation, a plug can be a pattern in $ … $ over the view binders:

The walk now looks for a position where the left side matches ¬ (A ∧ B) and the right side matches ¬ A ∨ ¬ B. Subtrees that are identical on both sides are never sites, the outermost matching position wins, and one assignment of A and B serves every site. A and B are declared in the @view line so that the walk’s solution reaches the rule binders of the same name. DeM_rev is the other direction, reached through @fallback. Search does not use @abstract, so a rule like DeM is only applied when a line cites it.

@fresh, completing the picture

One binder in replace is still unaccounted for: the substitution variable x itself. It appears nowhere in the written proof, so comparison cannot recover it. Luckily, the compiler can choose an arbitrary fresh variable instead.

The @fresh annotation handles this case. --| @fresh x fills the binder from the sort’s @vars pool (here, the z registered at the top of the theory) before matching the view. The fol-rules examples do not need it because their bound binder is visible in the line’s ∀ or ∃.

How a line is elaborated

With all the annotations in play, the compiler determines a rule application’s arguments in a fixed order:

1. explicit bindings from the line, which nothing may override;
2. @fresh binders, filled from their pools;
3. @view matching against the line and the cited references;
4. @recover and @abstract, run to a fixed point over the view state;
5. ordinary unification against the raw rule, starting from what the view solved;
6. validation of every binding, then instantiation and normalization.

A rule binder still unsolved after all of this is an error.

Powering search

Proof search introduced auto? and conversion?. This chapter describes the @auto annotations that control auto?. Unannotated rules remain searchable; annotations opt particular rules into additional, more expensive strategies.

What the search does on its own

Ordinary auto? applies rules whose conclusions match the goal, discharges their hypotheses from the reference pool if possible, and recursively proves the remaining unsolved hypotheses. The search solves rule binders by matching. This handles many cases, including nested eliminations on premises already in scope:

The suggestion is and_elim_r (a := $ b $) [and_elim_r [#1]].

• Matching and_elim_r’s conclusion g ⊢ b against the goal determines `g

  = andb := c. Its premise becomes ⊢ ?t ∧ c, where ?tstands for the still-unknown conjuncta`.

• The pattern becomes a sub-goal.
• The inner and_elim_r, applied to #1, concludes _ ⊢ b ∧ c: it fits the pattern, and matching determines a := b.

Ordinary search prefers applications whose bindings it can determine immediately. If those candidates fail, it may leave a binder unresolved while searching for a premise. A metavariable, such as ?t, represents that unknown expression. The annotations below control when search uses this strategy.

@auto backward: witnesses as metavariables

Ordinary search handles rules such as ∃-introduction poorly. The witness may be determined several steps below the introduction, so search must carry it as a metavariable. Because unannotated search defers that strategy, earlier attempts may consume the work budget first. Mark rules that normally require such witnesses with @auto backward:

--| @auto backward
axiom ex_intro {x: obj} (g: ctx) (t: obj x) (p: wff x):
  $ g ⊢ [x := t] p $ > $ g ⊢ ∃ x p $;

For an annotated rule, metavariable propagation becomes an ordinary search step rather than a last resort. Several metavariables may coexist, and any still undetermined after a proof is found receive witnesses from the @vars pool. The latter case occurs when a witness is introduced and eliminated entirely within the proof.

Scheduling

Search runs in phases that use increasingly expensive strategies. Each phase searches for a proof sequentially at increasing depths, iteratively deepening the search space and caching partial results for future phases. For unannotated rules, introducing metavariables is a last resort, available only in a late phase.

@auto backward makes metavariable introduction available in earlier phases. At each depth, search still tries cheaper candidates first: unannotated rules, then annotated rules whose conclusions determine all their binders, then annotated rules with unresolved binders.

Nested deferrals

Backward searches with metavariables may nest. Two @auto backward rules can occur on one path while both metavariables remain open in the sub-goal pattern.

The suggestion is

ex_intro (t := $ c $, p := $ E. y (P x /\ Q y) $)
  [ex_intro (x := $ y $, g := $ _ $, t := $ d $, p := $ P c /\ Q y $)
    [and_intro [#1, #2]]]

Here’s how we get there:

The outer ex_intro creates a metavariable ?s and the subgoal _ ⊢ ∃ y (P ?s ∧ Q y). The inner ex_intro creates another metavariable, ?t, leaving _ ⊢ P ?s ∧ Q ?t. Then and_intro splits the conjunction. Matching #1 determines ?s := c, and matching #2 determines ?t := d. Search uses these values to complete both ex_intro applications.

Opening ?t with ?s unsolved required @auto backward. Without the annotation the proof hits the search limit, trying rules other than ex_intro for the inner search.

Choosing an arbitrary witness

Sometimes the proof does not determine a witness because any variable will do.

The suggestion is

ex_intro (t := $ u $, p := $ P x -> P x $) [imp_intro [ax []]]

The search created a metavariable ?t, proved the tautology P ?t → P ?t, and took the pool variable u as the witness for ?t. Without the annotation, the same search fails:

auto? search failed: no proof found within depth 6. The search space was
exhausted (25 applications validated: 0 accepted, 25 rejected), so only a
deeper proof can exist — try 'auto? (depth: 8)'. Most-tried rules: ax
(25 tried, 0 accepted).

Use @auto backward for introduction and witness rules that build a goal from sub-goals while leaving part of a hypothesis undetermined. Existential introduction and similar generalization rules with a @view are typical.

Using @auto backward on a rule that matches very broadly can be harmful, especially if the conclusion of that rule leaves its premises undetermined. Consider

axiom or_elim (g h i: ctx) (a b c: wff):
  $ g ⊢ a ∨ b $ > $ h , a ⊢ c $ > $ i , b ⊢ c $ > $ g , h , i ⊢ c $;

Any sequent goal can match … ⊢ c, but the goal does not determine a or b. Applying this rule backward can create three poorly constrained subgoals. Exploring them may use the budget before search reaches rules better suited to the goal.

@auto forward: enrich the pool first

Use @auto forward for elimination rules and other rules that extract simpler facts from known ones. Before backward search begins, the engine repeatedly applies these rules to the reference pool and adds the derived facts as extra references, subject to its search limits.

A forward rule need not determine its entire output. Applying ∀-elimination to ∀ x p produces an instance of p, but the premise does not determine the substituted term t. Rather than guess, search records ?t as a universal metavariable: it represents a family of instances. Another rule can combine this family with a known fact to determine the needed instance. This matching operation is called a join.

A Hilbert-style quantifier theory shows how it works:

The useful route to the existential goal is to derive Q c from ∀ x (P x → Q x) and P c. Forward saturation can find that route: all_elim turns #1 into the family P ?t → Q ?t, and mp (enrolled forward as well as backward) joins the family with P c, instantiating t := c. The derived Q c determines the metavariable introduced by backward ex_intro. Search suggests a three-step chain:

ex_intro [mp (a := $ P c $, b := $ Q c $)
             [all_elim (x := $ x $, t := $ c $, p := $ P x → Q x $) [#1], #2]]

If you delete the two @auto forward lines, the same search reports an exhausted space at depth 6 even though the proof we’re looking for is only three applications deep. Backward search reaches mp with two unresolved premises, ?a → Q ?t and ?a. These patterns do not constrain the search enough to find t := c. Forward search instead matches the derived implication family against the known fact P c, which determines the bindings.

By contrast, ∀ x (P x) > ∃ y (P y) needs no join: any instance proves the goal. Backward search alone can prove it by choosing a witness from the sort’s @vars pool. Joins help when the proof needs a specific instance determined by another fact in the pool.

@auto forward does not belong on most introduction rules, since backward search uses them more effectively and indiscriminate application wastes budget and introduces noise into the reference pool.

@auto eager: invertible rules

Some rules are invertible: their conclusion is provable exactly when their premises are. Applying such a rule backward loses no search-relevant information, so doing it immediately avoids repeating the decomposition on several branches. @auto eager declares this strategy for tableau and sequent-style theories. For example, in a one-sided Tait calculus:

--| @auto eager
axiom rim (d: ctx) (a b: wff):
  $ ⊢ (¬ a) , b , d $ > $ ⊢ (a → b) , d $;

--| @auto eager 2
axiom rand (d: ctx) (a b: wff):
  $ ⊢ a , d $ > $ ⊢ b , d $ > $ ⊢ (a ∧ b) , d $;

An eager rule also has the effect of @auto backward. It is tried before other registered rules, in priority order. Priority 1 is the default and runs first.

Once an eager rule applies, search commits to it: if its premises cannot be proved, search does not try non-eager alternatives at that node. Eager applications do not count toward the search depth limit, so a long sequence of these steps does not require a greater depth setting. So eager rules should generally be “invertible” rules that can safely be applied without producing unprovable goals.

The compiler cannot prove that a rule is invertible; the annotation is the theory author’s choice. It does reject @auto eager if a premise mentions a binder absent from the conclusion. If search fails without reaching its budget, it also retries once without committing to eager rules. Priority ordering and the depth exemption still apply on that retry.

@auto trigger: seed leaf facts

Some proofs need a leaf fact backward search cannot easily discover, typically an axiom instance like p ⊢ p for some subformula p of the goal. @auto trigger applies to hypothesis-free rules and takes a pattern over term names, the rule’s binders, and _:

--| @auto trigger (hyp a)
axiom ax (g: ctx) (a: wff): $ g , a ⊢ a $;

When search would otherwise fail, the engine matches each trigger pattern against the goal’s subterms. It creates a rule instance for each match and retries with those facts in the reference pool. The pattern has to name every binder of the rule except those that default to the unit of an @acui combiner. g above defaults to the empty context, and the annotation is rejected if a binder is unresolvable.

Computation: conversion? and folding

conversion? searches for a proof that can be constructed from a chain of equalities or equivalences. For a general goal, the chain must reach an earlier line or hypothesis. For an equation, it may instead connect the equation’s two sides. The search stores expressions in an e-graph, a data structure that groups expressions known to be equivalent. It repeatedly applies rules to find more equivalences, a process called saturation. This chapter explains saturation and an alternative mode for directed computation.

Reading the suggested proof

The clearest way to see what conversion? does is to read the proof output. In the lambda calculus theory:

Accepting the suggestion replaces l1 with three lines:

l1_1: $ S a = S b $ by suc_congr [#1]
l1_2: $ S a = S a $ by eq_refl
l1: $ S a = S b $ by eq_trans [l1_2, l1_1]

The proof uses the rules introduced in Equality and normalization: the hypothesis rewrites a to b under S through a congruence rule, and reflexivity and transitivity restate the goal from the chain. The goal above is itself an equation, so once its two sides meet in the search space the chain between them is the proof. A goal of any other shape instead has to convert to a hypothesis or an earlier line, and the emitted chain ends with a transport along the sort’s relation, citing that reference. The theory therefore needs the relevant @relation bundle and a @congr rule for each constructor a rewrite must pass through. Converting a goal to an existing reference also requires transport for the goal’s sort.

A reference of the form rel lhs rhs, for a registered relation, can rewrite between its two sides without an annotation. The emitted proof cites the reference directly, as in suc_congr [#1] above. With relation and congruence rules in place, conversion? can therefore use local equations even when no general conversion rules are registered.

Enrolling rewrite schemas: @conversion

Theorems join the rewrite set with @conversion. They carry a direction token:

--| @conversion ltr
axiom contract (a: wff): $ (a ∧ a) ↔ a $;

The direction is ltr (left to right), rtl (right to left), or both. It controls which side search matches and which expressions it creates. For example, applying (a ∧ a) ↔ a left to right removes duplication. More generally, rules that expand expressions can make search explore many unnecessary terms. Prefer simplifying directions where possible.

The compiler checks the annotation when it registers the rule. The conclusion must be rel lhs rhs for the operand sort’s registered relation. The matched side must be a term application that determines every binder used on the other side. Rules may have bound binders and dependency restrictions; search checks those restrictions before applying them.

A rule may have hypotheses. For example, a / a = 1 might require a ≠ 0. Search applies such a rule only when the e-graph already establishes every hypothesis. An equation is established when its sides belong to the same equivalence class. Any other formula must be equivalent to a theorem hypothesis or an earlier proof line.

Search retries a match on later iterations if its hypotheses are not yet established. The matched side must determine every binder used in a hypothesis.

Associativity and commutativity: role certificates

The two structural laws from associativity and commutativity get special treatment, again for efficiency. Instead of a direction, you annotate the law itself:

With both annotations and a @congr rule, search treats nested applications of the operator as a multiset: an unordered collection that keeps duplicates. This avoids exploring each ordering and grouping separately. With only one of the two annotations, search instead applies that law in both directions during ordinary saturation.

This is related to but not the same as @acui. @acui drives the normalizer’s canonical forms during ordinary line checking, while the conversion annotations drive the term representation during search. The natural deduction context carries both kinds of metadata for exactly that reason.

Definitions

A def can enroll its own defining equation, with an orientation:

unfold replaces the defined term with its body. fold matches the body and replaces it with the defined term. both allows either direction. An unannotated definition is not expanded or folded by conversion?. Here saturation unfolds double 0 to 0 + 0, the addition rules finish, and the emitted chain crosses the definition with a single reflexivity line (the $ double 0 = 0 + 0 $ by eq_refl) which the checker closes through ordinary transparent unfolding.

For a def with hidden dummy binders only fold is legal: unfolding would have to invent a variable, which would complicate search significantly. The fold direction binds the dummy to a variable already present in the matched term.

Computation rules: @compute

For computation, applying reductions in a fixed order can be much cheaper than exploring all application orders. @compute registers a rule for this directed process, called folding, instead of general saturation. The lambda-calculus theory uses it for beta, substitution equations, and addition rules.

This works particularly well for terminating, confluent rule sets: reduction stops, and the result does not depend on the order of steps. Untyped β-reduction is not always terminating, so computation still needs search limits. For example:

--| @compute ltr
axiom beta {x: tm} (e: tm x) (a: tm x): $ (λ x. e) · a = [x := a] e $;

Choose one direction, ltr or rtl, to identify the expression to reduce, called the redex. Folding tries rules in declaration order, applies the first new match at each node, and continues reducing the results. Put specific computation rules before general simplification rules.

Goals may contain theorem variables. conversion? leaves those variables unchanged: for example, a zero law can reduce 0 + a to a just as it reduces 0 + S0 to S0.

A rule can be registered for saturation or computation, but not both. Both modes record justifications in the e-graph and emit ordinary proof steps.

Reading a miss

A failed conversion? says how it failed, which sometimes conveys useful information. This cell asks for a conversion that does not exist; put the cursor on the conversion? to run the search, and the report appears under the placeholder:

conversion? search failed: the egraph saturated (8 e-classes, 8 e-nodes,
1 iterations, 0 rule orientations, 0 local equations): no chain of the
enrolled @conversion rewrites connects this goal to any of the 1 pool
references.

A fully saturated search has reached a fixed point: its rules produce no new equivalences. Failure then means that no chain of the registered conversion rules connects the goal’s sides or reaches a reference. It does not establish that the goal is unprovable. Add relevant equations or a useful reference if the search lacks a needed connection.

Failure caused by an iteration or node limit is inconclusive. Try raising the limits for that call, for example with conversion? (iters: 32, nodes: 20000).

The diagnostic also notes when saturation was approximate. In particular, failure with @compute rules is inconclusive: computation follows one reduction order rather than exploring every possible chain.

A Hilbert calculus

Each chapter in this part develops a theory, alternating declarations and proofs with explanations. Cells with the same document name share one theory: theory cells add MM0 declarations, and proof cells add theorems and proofs. Editing a cell rechecks its document. Later cells can use earlier declarations in that document.

We start with a small classical system: a Hilbert calculus for propositional logic.

The signature

Two connectives suffice, implication and negation:

Each connective registers its notation twice, giving every Unicode token an ASCII alias that can be typed easily. Negation binds tighter than implication, and implication associates to the right.

The axioms

A Hilbert calculus uses axiom schemes with few inference rules. This theory has three schemes with no hypotheses and one inference rule:

h1 and h2 are the K and S schemes, and h3 is classical contraposition. Modus ponens is the only inference rule. MM0 represents it as an axiom with hypotheses.

Implication is reflexive

Here’s a classic proof of a simple tautology:

Hypothetical syllogism

A theorem’s hypotheses are cited as #1, #2, … like any other reference:

Negation

To shorten the double-negation proofs, we add one more axiom scheme:

con2 is derivable from the three schemes above, but this small development assumes it to keep the example short. Double-negation introduction then takes three lines:

The first line cites imp_refl from earlier on the page. Elimination uses the same pattern with h3:

The whole page

The index lists every statement the page has built, in order, with a marker for each proof obligation. The document behind it is an ordinary .mm0/.auf pair, and everything on the page is live, so you can edit any of the theorems, axioms, or proofs.

Natural deduction

This chapter builds a sequent-style natural deduction system for intuitionistic logic, with quantifiers. Each annotation that appears here was introduced in one of the design chapters.

Formulas

This theory has three sorts. Only seq, the sort of sequents, is provable. Formulas and contexts are syntax, not assertions: a proof cannot assert a bare wff. The sort system also rejects combinations such as a conjunction of two sequents. Each connective carries an ASCII alias alongside its Unicode notation.

Sequents and contexts

This cell declares judgment forms. A sequent like g ⊢ a is what deduction rules actually derive. The other three judgments express equivalence: ↔ for formulas, ctx_eq for contexts, and ⟚ for sequents. The compiler uses them to justify normalization. Because ↔ produces a seq, not a wff, this theory cannot place an equivalence inside a formula such as a conjunction or implication.

Contexts are built from single formulas (hence the coercion from wff to ctx) with the join ,, whose @acui annotation makes them behave as sets: order, grouping, and duplication are normalized when lines are checked. The empty context is written _.

The equational layer

This follows the pattern of the Equality and normalization chapter: a @relation bundle for each equivalence judgment, plus the context laws the @acui annotation cited. Only the sequent bundle carries a transport member, since seq is the only provable sort. The @congr axioms assist with deeply nested rewrites: a rewrite inside a formula lifts through hyp_congr and nd_congr to a ⟚ that the transport can use.

The rules

The system is intuitionistic. Rules such as imp_elim combine the contexts of their premises; and_intro uses the same context for both. ax is the only deduction rule with no hypotheses. Its arbitrary context g permits extra assumptions, so proofs do not need a separate weakening step.

A first proof, elimination followed by re-introduction:

The currying proof illustrates context handling. Lines l2 and l3 use ax with extra assumptions. imp_elim combines contexts on l5, then each imp_intro step moves one assumption into the conclusion:

Excluded middle is not provable here, but its double negation is. Note l7: not_elim concludes g , h ⊢ ⊥ where g and h are the same hypothesis. Idempotence collapses the join, so the line can state the context once:

Quantifiers

The quantifier layer adds a sort of objects, with a variable pool, and the binding syntax:

The substitution operator [x := t] p is an ordinary term with no built-in meaning. Designated @rewrite equations push it through each connective and discharge it at atoms, allowing the normalizer to compute substitutions during rule applications. The @alpha axioms at the end prove the renaming principles used by the freshness machinery described in Ergonomics.

The four quantifier rules have several additional annotations: @freshen repairs from Ergonomics, @view/@recover pairs from Views and recovery, and @auto enrollments from Powering search. Plain --| lines are doc comments; hover a rule’s name to read them:

Here all_elim’s conclusion is [x := u] (P x), but l2 states the normalized form P u, with a witness u from the @vars pool:

Existential elimination can use the bound x itself as the fresh name. The rule’s dependency constraints ensure that neither the conclusion c nor the side context h mentions that variable. If x occurs bound in h or c, alpha-freshening renames it before applying the rule and restores the original form afterward.

The whole page

Peano arithmetic

This chapter develops a small first-order arithmetic theory. We add equality, successor, quantifiers, substitution, and induction to classical propositional logic, then prove an addition law and a concrete sum. Unlike the sequent system of the previous chapter, this theory uses Hilbert style: formulas are themselves assertions, and wff is the provable sort.

The propositional skeleton

This is the same Łukasiewicz system as the Hilbert calculus chapter.

Hilbert-style proofs repeatedly use a few short derived rules. We prove them once so later proofs can cite them.

a1i weakens a theorem with an antecedent, and syl composes two implications.

Numbers

peano1 says zero is not a successor, and peano2 says that successor is injective. Its converse, peano2r, would ordinarily follow from a congruence principle; this small theory assumes it directly. The axioms use object-level implication rather than rule hypotheses, so their use generally requires an ax_mp step:

The equational layer

The theory needs to say how equivalent formulas and equal terms may replace one another, in the format of the Equality and normalization chapter:

A natural question: why introduce nat_eq when the theory already has =? A @relation bundle needs its members in rule form, and the equality axioms above are object-level implications — eq_trans is a formula about →, not a rule the normalizer can chain. Rather than derive rule-form counterparts, the theory keeps a separate judgment for the rewriting machinery; eq_congr connects it back to = formulas.

Quantifiers

For quantifiers, we have generalization, distribution of ∀ over implication, and vacuous quantification (note that ax_5’s p does not depend on x). Generalization is written in rule form: it takes a proof of p and produces a proof of ∀ x p. Here we apply it to an equality proved without hypotheses:

Substitution and instantiation

As in the last chapter, substitution is an ordinary term with @rewrite equations that push it through the syntax. Here it comes in two layers: sb_f substitutes in a formula and normalizes along ↔, while sb_t substitutes in a number term and normalizes along nat_eq:

ax_inst is instantiation. Its raw conclusion sb_f x t p is not intended to be user-facing syntax. Instead, the @view and @recover annotations (from Views and recovery) let a proof state the normalized instance, and let the compiler recover t and p from that shape:

The rewrite rules push sb_f through =, then sb_t through suc and down to the variable, and the emitted proof carries the conversion.

Addition and induction

Addition is defined by recursion on the right argument. peano5 is induction, stated with sb_f explicit in both hypotheses. The @view on the induction axiom uses two phantom binders, base and step, that absorb whatever the hypotheses normalize to: the user supplies the base case and inductive step in their already-substituted forms, and the rewrite rules reconcile them with the sb_f shapes.

The left identity law is a common first induction. Lines l1–l7 build the base case and the generalized step, and l8 closes:

The next theorem has no {x: nat} binder; its proof obtains x from the sort’s @vars pool:

Two plus two

To close, here’s a concrete computation: unfold with add_suc twice and add_0 once, lifting through suc with peano2r at each stage:

Even this small sum needs several congruence and transitivity steps. To automate such proofs, register the recursion equations with @compute and use conversion?. The lambda calculus chapter demonstrates this approach.

The whole page

The lambda calculus

This chapter builds an equational theory of the untyped lambda calculus with unary numerals. It extends the theory used in evaluation examples during the Proof search and Computation chapters. We end with the characteristic equation of the Y combinator.

Syntax

The sort tm contains terms. Its @vars pool supplies variables when a proof needs them. Abstractions are λ x. e, applications are f · a, and explicit substitution is [x := a] e, governed by the reduction rules below. The numerals are unary (0, S0, SS0, with S in the delimiter set so the compact form parses), and + is their addition.

The equational layer

The only judgments are term equations a = b and their iff equivalences, bundled as in the Equality and normalization chapter:

Note lam_congr: it lets an equation proved about a body a, possibly mentioning the bound variable, lift to an equation between abstractions. This is necessary to let rewriting descend under binders.

Reduction

Dependency restrictions prevent variable capture. In sb_lam, the declaration (a: tm x) permits a to mention x but not y. Moving a under the binder for y therefore cannot capture a variable in a.

The substitution rules carry two annotations. @rewrite lets the compiler run substitutions whenever it checks an ordinary line, so a cited rule whose conclusion contains a substitution can be stated in reduced form. @compute enrolls the same equations, plus beta and the addition table, as directed computation rules for conversion? (see Computation).

Single steps

@rewrite normalization alone is enough to make one beta step a one-line proof. The right-hand side of beta’s instantiated conclusion is [x := 0] (S x). The line states the reduced form, and the compiler emits the conversion:

For anything longer than one step, equations are chained by hand with the congruence and transitivity axioms. Here is the K combinator discarding its second argument:

l1 reduces under the binder through sb_lam (legal, since a doesn’t mention y), and l4 discharges [y := b] a by sb_vac. Both capture facts come straight from the binder declarations of the theorem.

Evaluation

A Church numeral represents a number by repeated function application. The numeral for two applies its function twice. Giving it the successor function and 0 therefore produces S S 0:

The goal is an equation, so conversion? only has to join its two sides: the fold reduces the left side to S S 0. Church addition works the same way: plus uses its first numeral to iterate f on top of the second’s result, and 1 + 1 = 2 is just evaluation.

The accepted suggestion expands to a long proof because every conversion step is emitted explicitly.

The Y combinator

The fixed-point combinator Y = λ f. (λ x. f · (x · x)) · (λ x. f · (x · x)) satisfies Y · g = g · (Y · g) for any g. Name it with a definition, whose bound variables become dummy binders:

Writing ω for λ u. g · (u · u), one beta step takes Y · g to ω · ω, and one more takes ω · ω to g · (ω · ω), so both sides of the fixed-point equation reduce to a common term.

On l1, the function being applied is Y, not a visible abstraction. The compiler unfolds Y to find the β-reduction step.

conversion? can find this equation, but only when the definition of Y is used rather than the defined term Y. Only annotated definitions take part in conversion, and a definition with hidden dummy binders can be folded but never unfolded during conversion (see Computation), so Y is opaque to that search method.

The whole page

Programs and correctness

This chapter verifies two small imperative programs: an assignment sequence and a while loop. We build a fragment of dynamic logic, which expresses how programs affect states, then derive rules of Hoare logic for reasoning about preconditions and postconditions.

Registering the Floyd assignment axiom with @rewrite lets the compiler compute assignment preconditions by substitution. The examples prove partial correctness: if a program terminates, its result satisfies the postcondition. They do not prove termination.

Formulas and programs

Two sorts represent data: obj for program-variable values and world for program states. The object syntax has only 0 and pred; this example needs no arithmetic laws. Formulas are a separate syntactic sort form, since the provable sort wff is reserved for judgments about them.

Programs use four constructs. Sequencing a ⨟ b runs a then b. Iteration ⋆ a runs a zero or more times. A test ? p leaves the state unchanged if p holds and cannot proceed otherwise. Assignment ⟨ x ≔ e ⟩ stores the value of e in x.

The formula [ a ] p says that p holds after every terminating run of a.

Judgments

The basic judgment is world-labelled truth: w : p says the formula p holds at state w, and step w a v says program a can move state w to state v. Sequents g ⊢ w : p collect labelled assumptions in a context that behaves as a set, as in Natural deduction. ⊨ p asserts truth at every state. The Hoare triple ⦃ p ⦄ a ⟦ q ⟧ says that every terminating run of a from a state satisfying p ends in a state satisfying q.

Equivalence infrastructure

Each sort gets its equivalence, bundled for the normalizer as in Equality and normalization.

Congruence rules let rewriting pass through the surrounding constructors used in these proofs.

Substitution as computation

The substitution operators get the standard @rewrite annotations, as in the Peano and lambda calculus chapters:

The logic

The propositional core is a labelled natural deduction system. These are the rules of the Natural deduction chapter, with world indices.

pbc makes the base logic classical.

The modality needs only two rules. K and necessitation are derivable:

To prove [ a ] p at w, box_intro assumes that a reaches an arbitrary state v and proves p is true in that state. The bound binder {v: world} makes v an eigenvariable: the rule’s dependency lists keep it out of the other arguments, so the proof cannot depend on a particular choice of destination state.

Reduction axioms

Compound programs reduce to their parts. Sequencing and test are genuine rewrites; the box over a compound program is the simpler formula:

red_assign is the Floyd assignment axiom: the box over an assignment is the substitution instance. Because it is a @rewrite, and the substitution operators push through the formula language by rewrites too, checking any line against a boxed assignment computes the weakest precondition.

Iteration is different: star_fix is not a rewrite. Its right-hand side mentions [ ⋆ a ] again, so normalizing with it would loop. Unfolding a loop is a deliberate proof step. star_ind is the corresponding induction rule.

Validity and Hoare triples

valid_intro proves validity by proving the formula at an arbitrary state from an empty context. The two ht rules convert between a Hoare triple ⦃ p ⦄ a ⟦ q ⟧ and ⊨ (p → ([ a ] q)). The while loop is a definition, not a primitive: iterate the guarded body, then exit through the failed guard.

The modal toolkit

A few validity-level lemmas are useful. box_k is the K axiom.

The reduction axioms rewrite left to right, so proofs that need to build a box (introducing [ a ⨟ b ] p from its reduct) cite these symmetric forms through at_mp.

Note the pool worlds: imp_refl_valid has no world binder of its own, so u and v come from the sort’s @vars pool and become the eigenstates that valid_intro and box_intro discharge.

Hoare logic, derived

We can now derive Hoare rules for consequence, sequencing, assignment, and while loops.

Assignment comes in two forms. The Floyd–Hoare assignment rule follows from red_assign:

The @view described in Views and recovery lets proof lines omit the explicit substitution ⌊ x / e ⌋ p. Its phantom binder q occupies the precondition, while the assignment and postcondition determine x, e, and p. The rewrite rules then compute the substitution ⌊ x / e ⌋ p.

hoare_assign_wp builds in precondition strengthening. Read its hypothesis as “q implies the weakest precondition”. Its view again lets us lean on the rewrite rules to handle substitutions. The phantom r stands where ⌊ x / e ⌋ p sits in the raw rule, so the cited verification condition can be written with the substitutions fully evaluated.

The last line states the triple with while b a; the compiler matches it against l20’s unfolded form through the definition.

Verified programs

The first program assigns a to x, then overwrites it with b. The first assignment has no effect on the final result. Its verification condition reduces to the reflexive equality b = b:

The final program repeatedly assigns pred x to x while x ≠ 0. Its loop invariant is ⊤, which holds in every state. hoare_while proves that, on exit, the invariant holds and the guard is false: ⊤ ∧ ¬ ¬ (x = 0). hoare_conseq then uses classical double-negation elimination to obtain x = 0.

This does not show that the loop reaches zero. We have given pred no arithmetic axioms, and the proof establishes only the state on termination.

The whole page

Install and run

You do not need to install Aufbau to work through the opening chapters. The interactive cells run the compiler and language server in your browser. Install the native tools when you want to work with files on disk, script a build, or verify an MMB file independently.

With Nix

With Nix and flakes enabled, you can let Nix obtain or build the tools. Open a shell with both commands on your PATH:

nix shell github:gleachkr/Aufbau

or install them into your profile:

nix profile install github:gleachkr/Aufbau

Either way you get the abc and mm0-zig commands directly — where the rest of this chapter writes zig-out/bin/abc, just type abc. The repository’s flake also provides a development shell (nix develop) with the required Zig version and other build tools. Use it if you prefer to build from source, as described below.

Requirements

Building Aufbau requires:

• Git
• Zig 0.15.2

Clone the repository, including its submodules, and make a release build:

git clone --recurse-submodules https://github.com/gleachkr/Aufbau.git
cd Aufbau
zig build -Doptimize=ReleaseFast

The build installs two programs under zig-out/bin/: abc compiles an MM0 theory and an Aufbau proof script to MMB; mm0-zig verifies an MMB file against its MM0 source. Check that both programs run:

zig-out/bin/abc --version
zig-out/bin/mm0-zig --version

Compile a proof

An Aufbau project has two source files. The .mm0 file declares the theory and the statements to prove. The .auf file gives their proofs.

Create hello.mm0:

delimiter $ ( ) $;
provable sort wff;
term imp (a b: wff): wff; infixr imp: $->$ prec 25;
axiom h1 (a b: wff): $ a -> (b -> a) $;
theorem weaken (p q: wff): $ p -> (q -> p) $;

This declares a provable sort of propositions, an implication constructor written infix as ->, the weakening axiom h1, and a theorem to prove — weakening restated for the propositions p and q.

Create hello.auf:

weaken
------
l1: $ p -> (q -> p) $ by h1

The block named weaken supplies the proof of the corresponding theorem in the MM0 file. Its only line states the goal and cites the axiom; the compiler infers the instantiation.

Compile the pair:

zig-out/bin/abc compile hello.mm0 hello.auf hello.mmb

A successful compile writes hello.mmb and prints nothing. The MMB file is the compact binary proof consumed by the verifier.

Verify the result

Run the verifier separately:

zig-out/bin/mm0-zig hello.mmb < hello.mm0

It should print:

Verification successful!

mm0-zig takes the MMB path as its argument and reads the matching MM0 source from standard input.

Command-line help

The compiler also exposes the language server used by editor integrations:

zig-out/bin/abc lsp

For the complete current options, including diagnostic debugging and treating warnings as errors, use:

zig-out/bin/abc --help
zig-out/bin/mm0-zig --help

The command-line compiler requires finished proofs. Search placeholders like auto? are an editor feature: in a cell or an LSP-connected editor they run the search and offer a concrete proof to accept, but abc compile rejects a proof script that still contains one.

Embedding the editor

Every proof cell in this manual is an instance of @aufbau/editor, a set of web components that run the Aufbau compiler in the reader’s browser using WebAssembly. You can put the same live, checked proofs on any static website, using an import map and one module import.

A complete page

Save this as an .html file and serve it from any static host (or open it through a local web server — module scripts don’t load from file: URLs):

<!doctype html>
<html>
<head>
<meta charset="utf-8">
<script type="importmap">
  {
    "imports": {
      "@codemirror/state": "https://esm.sh/@codemirror/state",
      "@codemirror/view": "https://esm.sh/@codemirror/view?external=@codemirror/state",
      "@codemirror/commands": "https://esm.sh/@codemirror/commands?external=@codemirror/state,@codemirror/view",
      "@codemirror/lint": "https://esm.sh/@codemirror/lint?external=@codemirror/state,@codemirror/view",
      "@codemirror/autocomplete": "https://esm.sh/@codemirror/autocomplete?external=@codemirror/state,@codemirror/view",
      "@aufbau/compiler": "https://esm.sh/@aufbau/compiler",
      "@aufbau/lsp": "https://esm.sh/@aufbau/lsp",
      "@aufbau/editor": "https://esm.sh/@aufbau/editor?external=@aufbau/compiler,@aufbau/lsp,@codemirror/state,@codemirror/view,@codemirror/commands,@codemirror/lint,@codemirror/autocomplete"
    }
  }
</script>
<script type="module">
  import "@aufbau/editor";
</script>
</head>
<body>

<aufbau-proof>
  <script type="text/mm0">
    delimiter $ ( ) $;
    provable sort wff;
    term imp (a b: wff): wff; infixr imp: $->$ prec 25;
    axiom h1 (a b: wff): $ a -> (b -> a) $;
  </script>
  <script type="text/auf">
    lemma weaken (p q: wff): $ p -> (q -> p) $
    ----
    l1: $ p -> (q -> p) $ by h1
  </script>
</aufbau-proof>

</body>
</html>

The cell compiles its theory and proof in WebAssembly and shows a live status line.

• Everything loads from esm.sh, which serves npm packages as ES modules and allows browsers to load them from other sites.
• The ?external= parameters ensure that CodeMirror and the Aufbau WebAssembly packages each have one shared instance. Without them, dependencies may load separate copies, which breaks the editor.

Sharing a theory between cells

To share a theory between cells, give the theory its own element and point the proof cells at it.

<aufbau-theory id="hilbert">
  <script type="text/mm0">
    delimiter $ ( ) $;
    provable sort wff;
    term imp (a b: wff): wff; infixr imp: $->$ prec 25;
    axiom h1 (a b: wff): $ a -> (b -> a) $;
    axiom mp (a b: wff): $ a $ > $ a -> b $ > $ b $;
  </script>
</aufbau-theory>

<aufbau-proof theory="hilbert">
  <script type="text/auf">
    lemma weaken_under (p q: wff): $ p $ > $ q -> p $
    ----
    l1: $ p -> (q -> p) $ by h1
    l2: $ q -> p $ by mp [#1, l1]
  </script>
</aufbau-proof>

<aufbau-theory> only holds the shared prelude. Later cells can use anything proved by earlier cells in the same document. A cell reads “verified” only when the entire document checks cleanly.

Sources can also live in separate files instead of inline scripts: <aufbau-theory id="hilbert" src="/hilbert.mm0"> and <aufbau-proof theory="hilbert" src="/proofs.auf">.

If you want the theory itself to be visible and editable, skip <aufbau-theory> and group the cells with a doc attribute instead. A proof cell whose body is only MM0 acts as an editable theory cell:

<aufbau-proof doc="hilbert">
  <script type="text/mm0">
    ...the theory, editable in place...
  </script>
</aufbau-proof>

<aufbau-proof doc="hilbert">
  <script type="text/auf">
    ...a lemma checked against it...
  </script>
</aufbau-proof>

A document can also contain theorem cells (an MM0 theorem declaration plus its proof), definition cells (a bodyless def whose editable content is the definition body), and proof-local definitions. There is also <aufbau-index theory="…">, which provides a live index of every statement in the document.

Cell attributes

The language server is optional

Compiling and verifying need only @aufbau/compiler. The @aufbau/lsp entry adds hover, completion, and proof search, and it runs in a Web Worker. Two things to know:

• Browsers only build workers from same-origin scripts, so when the package is served from a CDN it bootstraps the worker through a blob: URL. If your site sets a Content-Security-Policy, allow worker-src blob: alongside the CDN host.
• If the language server fails to load, the editor still compiles, reports diagnostics, and verifies proofs. To skip it deliberately, drop the @aufbau/lsp and @codemirror/autocomplete lines from the import map.

The npm packages

Aufbau provides four npm packages. The verifier, compiler, and language server use the same Zig code as the command-line tools, compiled to WebAssembly for JavaScript environments. The editor provides browser components built on those packages.

All four use ES modules. The verifier, compiler, and language server work in browsers and Node; the editor requires a browser and the peer dependencies listed below. Browser applications can use a bundler or a content delivery network (CDN) with an import map. See Embedding the editor for the CDN setup.

@aufbau/verifier

import { loadVerifier } from "@aufbau/verifier";

const verifier = await loadVerifier();
const result = verifier.verifyPair(mm0Text, mmbBytes);
if (!result.ok) console.error(result.diagnostics);

mm0Text is a string; mmbBytes is a Uint8Array (or any typed-array view). The result carries ok, diagnostics, verifier metadata, and durationMs.

@aufbau/compiler

import { loadCompiler } from "@aufbau/compiler";

const compiler = await loadCompiler();
const result = compiler.compile(mm0Text, proofText);
if (result.ok) {
  // result.mmbBytes is a Uint8Array, ready for the verifier
}

A browser page can compile a proof script and then pass the output to the independent verifier.

Both loaders locate their .wasm file automatically in browsers and Node. To control loading (offline bundles, custom hosting), pass wasmUrl, wasmBytes, module, or instance to loadVerifier() / loadCompiler().

@aufbau/lsp

The language server speaks JSON-RPC. loadLspServer() runs it synchronously in the calling thread:

import { loadLspServer } from "@aufbau/lsp";

const server = await loadLspServer();
const responses = server.process({
  jsonrpc: "2.0",
  id: 1,
  method: "initialize",
  params: { capabilities: {} },
});

Long proof searches block the calling thread, so browser pages should prefer loadLspServerWorker(), which runs the server in a Web Worker and delivers messages through server.subscribe(callback). The worker transport is browser-only; Node applications should use loadLspServer() directly.

Browsers cannot start a worker directly from a script hosted on another origin. When the package loads from a CDN, loadLspServerWorker() starts the worker through a local blob: URL instead. Pages with a Content-Security-Policy must allow this:

worker-src blob:; script-src 'self' https://esm.sh; connect-src 'self' https://esm.sh

Passing your own options.worker or options.workerUrl bypasses the blob path.

@aufbau/editor

Importing the package registers the custom elements used throughout this manual:

import "@aufbau/editor";

<aufbau-theory id="example" src="/example.mm0"></aufbau-theory>
<aufbau-proof theory="example" src="/example.auf"></aufbau-proof>

It declares peer dependencies on @aufbau/compiler and CodeMirror 6 (@codemirror/view, state, commands, lint), with @aufbau/lsp and @codemirror/autocomplete optional. Without those last two packages, cells still compile and report diagnostics but have no hover, completion, or proof search. See Embedding the editor for the element and attribute reference.

Appendix: annotation reference

Annotations are --| comment lines immediately before a declaration. Each annotation occupies exactly one line, and only one annotation is allowed per line. In .mm0 files they attach to the next statement; in .auf files they may precede a lemma block or a proof-local def, giving the local rule or term the same metadata as an ordinary assertion or term. A public definition’s body filler takes no annotations; they belong on its .mm0 declaration.

A --| line that does not start with @ is a doc comment. Doc lines and annotations may be mixed in any order; consecutive doc lines form one paragraph, and an empty --| line starts a new one. The doc comment is shown when the declaration’s name is hovered, and in completion lists. Backticks mark code spans; other markdown is shown as written.

--| Existential introduction: a formula proved of a particular term
--| `t` holds of something.
--| @auto backward
axiom ex_intro {x: obj} (g: ctx) (t: obj x) (p: wff x):
  $ g ⊢ [x := t] p $ > $ g ⊢ ∃ x p $;

This is the same doc-comment convention as mm0-rs, so tools that read MM0 files without Aufbau’s annotations still show the text.

Equality and normalization

@relation

--| @relation SORT REL REFL TRANS SYMM TRANSPORT

The fields name the sort, relation term, and its reflexivity, transitivity, symmetry, and transport rules, in that order. _ marks a missing symmetry or transport member. The declarative annotation may sit on any assertion; by convention it sits on the reflexivity axiom. Bundle members must use rule-form hypotheses (>, not object-level implications) and have no bound binders.

--| @relation wff bi biid bitr bisym mpbi
--| @relation nat nat_eq nat_eq_refl nat_eq_trans nat_eq_sym _

@rewrite

--| @rewrite

No arguments. The associated assertion’s conclusion must be rel lhs rhs for a registered relation; it is indexed by the head term of lhs and applied left to right during normalization. Rules with the same head are tried in declaration order; the first matching rule applies.

@congr

--| @congr

No arguments. Registers an assertion as the congruence rule for the head term of its conclusion, letting normalization rewrite inside that constructor. Binders must pair up as old new for each regular argument (bound arguments appear once), and the conclusion must relate the two applications.

@acui

--| @acui ASSOC COMM UNIT IDEM

Applied to a term declaration (the combiner). The four positions name the associativity axiom, commutativity axiom, unit term, and idempotence axiom; _ marks an absent law, and the trailing IDEM may be omitted. Arguments of the combiner are flattened, units dropped, sorted (when commutative), deduplicated (when idempotent), and rebuilt, with a relation proof emitted during .auf compilation for every step. Requires a @relation for the result sort and a @congr rule for the combiner.

--| @acui ctx_assoc ctx_comm emp ctx_idem
term join (g h: ctx): ctx;

Computation

@conversion on an assertion

--| @conversion ltr|rtl|both|comm|assoc|alpha

Registers an equation rel lhs rhs for saturation in conversion?. ltr, rtl, and both select the direction of matching. A rule may have hypotheses, which must already be established in the e-graph before it applies. The matched side must determine every binder used in the other side or in a hypothesis.

comm and assoc identify commutativity and associativity laws. With both annotations and a @congr rule, search represents nested applications as multisets rather than exploring each ordering and grouping.

alpha registers a renaming equation such as rel (all x p) (all y (sb x y p)). Search applies it between existing expressions with the same binding constructor, taking the new binder from the other expression. The substitution rules needed to reduce the renamed body must also be registered for conversion. Nested renaming proceeds from the outside inward and needs substitution rules that move under each relevant binder, such as sb x a (all y p) to all y (sb x a p).

A rule cannot carry both @conversion and @compute.

@conversion on a definition

--| @conversion fold|unfold|both

Enrolls the definition’s own equation for conversion?: fold replaces an instance of the body with the defined term; unfold replaces the defined term with its body. Unannotated definitions are invisible to conversion?. A definition with hidden dummy binders may enroll fold only. (Ordinary transparent-def unfolding during line checking needs no annotation at all.)

@compute

--| @compute ltr|rtl

Registers a hypothesis-free equation for directed computation in conversion?. Rules apply in declaration order rather than by general saturation. The annotation does not guarantee termination. This is the appropriate enrollment for recursion equations and arithmetic tables; see the evaluation examples in Computation and The lambda calculus.

Search

@auto

--| @auto forward
--| @auto backward
--| @auto eager      -- optionally: @auto eager N
--| @auto trigger (TERM child ...)

One mode per line; a rule may carry several lines. forward runs the rule over the reference pool before backward search (elimination rules); backward allows unresolved binders to remain as metavariables while search proves premises. If a successful proof still needs an arbitrary witness, search chooses one from the @vars pool.

eager marks a rule as invertible. Search tries it first, commits to it once applied, and does not count its applications toward the depth limit. The optional priority N is at least 1, defaults to 1, and runs earlier when smaller. It implies backward. The compiler checks that premises use only binders present in the conclusion, but cannot verify invertibility.

trigger supplies a parenthesized prefix pattern over term names, rule binders, and _. As a last resort, search matches it against subterms of the goal to create fully instantiated facts from a hypothesis-free rule.

More details are available in Powering search.

Views and binder recovery

@view

--| @view BINDERS : $ HYP $ > ... > $ CONCLUSION $

A theorem-like signature, on one line, declaring an alternative surface shape for the rule: binders in the usual (a: s) / {x: s} forms, hypotheses and conclusion separated by >. Binders whose names match rule arguments map back to the rule arguments; the rest are phantom, view-local slots. At most one @view may appear on a rule.

@recover

--| @recover TARGET SOURCE PATTERN HOLE

Four view-binder names; must follow the @view it refines. Walks SOURCE and PATTERN in parallel and, where PATTERN reaches the resolved HOLE, reads the corresponding SOURCE subtree off as the value of TARGET.

@abstract

--| @abstract TARGET LEFT RIGHT HOLE LEFT-PLUG RIGHT-PLUG

Four view-binder names and two plugs; must follow a @view. Each plug is a view-binder name or a $ … $ pattern over the view binders. Recovers a surrounding expression, or context, with one variable marking replacement positions. It compares LEFT and RIGHT, replaces each occurrence of the plug pair with HOLE, and assigns the result to TARGET; binders solved by a pattern are assigned as well. Several @recover and @abstract lines may follow one @view; they run to a fixed point.

Variables, freshness, and repair

@vars

--| @vars TOKEN TOKEN ...
sort obj;

On a sort declaration. Declares a pool of variable names that proofs may use on demand. These variables are used by @fresh, @freshen, backward-search witness invention, and hidden-dummy matching. Multiple @vars lines accumulate. Not allowed on strict or free sorts.

@fresh

--| @fresh BINDER

BINDER is a bound binder of the rule. When the binder is omitted at a citation, the compiler selects a variable from the binder sort’s @vars pool (preferring one that does not occur in the goal) before inference runs. An explicit binding always overrides it.

@freshen

--| @freshen TARGET-ARG BLOCKER-BINDER

TARGET-ARG is a regular argument and BLOCKER-BINDER is a bound binder of the rule. Marks the pair as eligible for alpha-renaming repair when a dependency (capture) check blocks the application; the repair renames the blocker inside the target via a matching @alpha rule and a @vars pool variable.

@alpha

--| @alpha OLD NEW
axiom all_alpha {x y: obj} (p: wff x y): $ ∀ x p ↔ ∀ y ([x/y] p) $;

OLD and NEW are bound binders of the same sort on a hypothesis-free equivalence. Registers the rule as the alpha-renaming lemma for its head term, consumed only by the @freshen repair path.

Holes and fallbacks

@hole

--| @hole TOKEN
provable sort wff;

Occurs on a sort declaration, at most one per sort. Registers TOKEN as the hole marker for that sort: each occurrence in proof math is a fresh, independent hole that inference must solve. See Holes.

@fallback

--| @fallback RULE

RULE names an earlier rule. At most one @fallback may appear on a rule. If the annotated rule’s application fails, the compiler retries the entire application with the named rule and follows fallback chains recursively. A theory can therefore expose one name for a family of rule variants.

Appendix: search parameters

This appendix lists proof-search commands and their parameters. Proof search explains how to use them; Computation covers conversion? in detail.

The search commands

A search command can be used on a proof line after by, or inside a reference slot (by mp [auto?, #1]). conversion? can only be accepted on top-level proof lines, and only with a concrete goal (no holes).

Search commands run in the editor and language server, which report the found proof as a suggestion. Batch compilation (abc compile) rejects proof scripts that contain unexpanded search commands.

Parameter syntax

Parameters go in the same parenthesized list as explicit bindings, as name: INTEGER entries (a plain colon, rather than := for bindings). The two kinds can be mixed:

l1: $ c $ by auto? (depth: 8, fuel: 8192)
l2: $ c $ by rule1 [auto? (t := $ k $, nodes: 400)]

Unknown names and out-of-range values are reported and skipped. If a name is repeated, the last occurrence wins.

auto? parameters

When auto? fails, the failure report says which limit it hit and suggests a concrete retry, e.g. auto? (depth: 8) — start from that suggestion rather than guessing.

conversion? parameters

nodes has command-specific units: sub-goals for auto?, and e-graph nodes for conversion?.

exact? and apply?

exact? and apply? take no search parameters.

What search reads from the theory

The searches can be controlled by annotations in the .mm0 file: @auto forward / backward / eager / trigger enroll rules for auto? (see Powering search), @conversion and @compute enroll equations for conversion? (see Computation), and @vars supplies a witness pool. The per-invocation parameters above only decide how much work those enrollments are allowed to do.

Appendix: grammar summaries

Condensed grammars for the two source languages. The MM0 grammar is fixed by the upstream Metamath Zero specification; the .auf grammar is this project’s proof-script format.

MM0 lexical structure

file          ::= (lexeme | whitespace)*
line-comment  ::= '--' [^\n]* '\n'
lexeme        ::= symbol | identifier | number | math-string
symbol        ::= '*' | '.' | ':' | ';' | '(' | ')' | '>' | '{' | '}' | '=' | '_'
identifier    ::= [a-zA-Z_][a-zA-Z0-9_]*
number        ::= 0 | [1-9][0-9]*
math-string   ::= '$' [^\$]* '$'

Comments starting --| are annotation comments: Aufbau attaches them to the next statement, as metadata when the line starts with @ (@relation, @rewrite, @auto, …) and as a doc comment otherwise. See the annotation reference.

MM0 statements

mm0-file      ::= (statement)*
statement     ::= sort-stmt | term-stmt | assert-stmt | def-stmt
                | notation-stmt

sort-stmt     ::= ('pure')? ('strict')? ('provable')? ('free')?
                  'sort' identifier ';'

term-stmt     ::= 'term' identifier (type-binder)* ':' arrow-type ';'
type          ::= identifier (identifier)*
type-binder   ::= '{' (identifier)* ':' type '}'
              |   '(' (identifier_)* ':' type ')'
arrow-type    ::= type | type '>' arrow-type

assert-stmt   ::= ('axiom' | 'theorem') identifier
                  (formula-type-binder)* ':' formula-arrow-type ';'
formula-type-binder ::= '{' (identifier)* ':' type '}'
                      | '(' (identifier_)* ':' (type | formula) ')'
formula-arrow-type ::= formula | (type | formula) '>' formula-arrow-type
formula       ::= math-string

def-stmt      ::= 'def' identifier (dummy-binder)* ':' type
                  ('=' formula)? ';'
dummy-binder  ::= '{' (dummy-identifier)* ':' type '}'
              |   '(' (dummy-identifier)* ':' type ')'
dummy-identifier ::= '.' identifier | identifier_

Curly binders {x: s} are bound (binding) variables; parenthesized binders (a: s) are regular variables, with trailing identifiers in the type naming the bound variables the term may depend on. .-prefixed binders on a def are hidden dummy variables. A def without = $ ... $ leaves its body to be supplied by the .auf file. See Sorts and terms and Variables, binders, and dependencies.

notation-stmt        ::= delimiter-stmt | simple-notation-stmt
                       | coercion-stmt | gen-notation-stmt
delimiter-stmt       ::= 'delimiter' math-string math-string? ';'
simple-notation-stmt ::= ('infixl' | 'infixr' | 'prefix') identifier ':'
                         constant 'prec' precedence-lvl ';'
precedence-lvl       ::= number | 'max'
coercion-stmt        ::= 'coercion' identifier ':' identifier '>' identifier ';'
gen-notation-stmt    ::= 'notation' identifier (type-binder)* ':' type '='
                         (notation-literal)+ ';'
notation-literal     ::= '(' constant ':' precedence-lvl ')' | identifier

See Notation for how precedence and delimiters interact.

The .auf language

An Aufbau script is a sequence of theorem blocks, lemma blocks, def items, and notation items, in the same order as the .mm0 declarations they serve (see Proof blocks and lines):

aufbau-script ::= (theorem-block | lemma-block | def-item | notation-item
                  | blank | comment)*

theorem-block ::= theorem-name newline underline newline* proof-line*
underline     ::= '-' '-' '-'* newline          -- at least 3 dashes

lemma-block   ::= annotation-comment* 'lemma' identifier lemma-binders? ':'
                  formula ('>' formula)* newline underline newline*
                  proof-line*

def-item      ::= public-body-filler | local-def
public-body-filler ::= 'def' identifier dummy-group* '=' math-string
dummy-group   ::= '(' ('.' identifier)+ ':' sort ')'
local-def     ::= 'def' identifier binder* ':' sort '=' math-string

notation-item ::= prefix-stmt | infix-stmt | notation-stmt   -- MM0 syntax, ';' included

Lemma binders use the same syntax as MM0 assertions. The presence of a top-level : sort return annotation is what distinguishes a proof-local definition from a public body filler (Lemmas and definitions in proofs). A notation item is an MM0 prefix, infixl, infixr, or notation statement naming a proof-local definition; coercion and delimiter statements are not accepted.

Proof lines

proof-line   ::= label ':' formula 'by' rule-application newline*

rule-application ::= rule-name ('(' arg-bindings ')')? ('[' refs ']')?

arg-bindings ::= empty | arg-binding (',' arg-binding)*
arg-binding  ::= binder-name ':=' formula
             |   param-name ':' number        -- search parameters only

refs         ::= empty | ref (',' ref)*
ref          ::= hyp-ref | line-ref | inline-application
hyp-ref      ::= '#' number | '#' identifier
line-ref     ::= identifier
inline-application ::= rule-application

Notes:

• Whitespace, newlines, and -- comments are interchangeable separators inside a proof line; a new line must still start with its label.
• An omitted [...] is an empty reference list; the reference count must match the cited rule’s hypothesis count.
• A bare identifier in a reference list is always a line reference, so a zero-hypothesis inline application needs its delimiter: keep [top_i []].
• rule-name may also be a search command (exact?, apply?, auto?, conversion?); the name: number parameter form is accepted only there (search parameters).
• On a proof line, rule-name may be sorry!, which admits the goal with no bindings or references (Admitting a line). It is not accepted as an inline application.
• $ ... $ formulas may contain @hole tokens where the theory declares them (Holes).