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.