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.