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.