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.

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