Displays a proof term in a line by line format somewhat akin to a Fitch style proof or the Metamath proof style.
#explode decl_name displays a proof term in a line-by-line format somewhat akin to a Fitch-style
proof or the Metamath proof style.
#explode_widget decl_name renders a widget that displays an
#explode iff_true_intro produces
In more detail:
The output of
#explode is a Fitch-style proof in a four-column diagram modeled after Metamath
proof displays like this. The headers of the columns are
"Step", "Hyp", "Ref", "Type" (or "Expression" in the case of Metamath):
- Step: An increasing sequence of numbers to number each step in the proof, used in the Hyp field.
- Hyp: The direct children of the current step. Most theorems are implications like
A -> B -> C, and so on the step proving
Cthe Hyp field will refer to the steps that prove
- Ref: The name of the theorem being applied. This is well-defined in Metamath, but in Lean there
are some special steps that may have long names because the structure of proof terms doesn't
exactly match this mold.
- If the theorem is
foo (x y : Z) : A x -> B y -> C x y:
- the Ref field will contain
ywill be suppressed, because term construction is not interesting, and
- the Hyp field will reference steps proving
B y. This corresponds to a proof term like
@foo x y pA pBwhere
- If the head of the proof term is a local constant or lambda, then in this case the Ref will
∀Efor forall-elimination. This happens when you have for example
h : A -> Band
ha : Aand prove
h ha; we reinterpret this as if it said
∀E h hawhere
∀Eis (n-ary) modus ponens.
- If the proof term is a lambda, we will also use
∀Ifor forall-introduction, referencing the body of the lambda. The indentation level will increase, and a bracket will surround the proof of the body of the lambda, starting at a proof step labeled with the name of the lambda variable and its type, and ending with the
∀Istep. Metamath doesn't have steps like this, but the style is based on Fitch proofs in first-order logic.
- If the theorem is
- Type: This contains the type of the proof term, the theorem being proven at the current step.
This proof layout differs from
Also, it is common for a Lean theorem to begin with a sequence of lambdas introducing local
constants of the theorem. In order to minimize the indentation level, the
∀I steps at the end of
the proof will be introduced in a group and the indentation will stay fixed. (The indentation
brackets are only needed in order to delimit the scope of assumptions, and these assumptions
have global scope anyway so detailed tracking is not necessary.)