Explode command #
This file contains the main code behind the #explode
command.
If you have a theorem with a name hi
, #explode hi
will display a Fitch table.
Pretty print a const expression using delabConst
and generate terminfo.
This function avoids inserting @
if the constant is for a function whose first
argument is implicit, which is what the default toMessageData
for Expr
does.
Panics if e
is not a constant.
Instances For
Core explode
algorithm.
select
is a condition for which expressions to processincludeAllDeps
is whether to include dependencies even if they were filtered out. IfTrue
, thennone
is inserted for omitted dependenciese
is the expression to processdepth
is the current abstraction depthentries
is the table so farstart
is whether we are at the toplevel of the expression, which causes lambdas to useStatus.sintro
to prevent a layer of nesting.
Prepend the line
of the Entry
to deps
if it's not none
, but if the entry isn't marked
with useAsDep
then it's not added to the list at all.
Instances For
Main definition behind #explode
command.
Instances For
#explode expr
displays a proof term in a linebyline format somewhat akin to a Fitchstyle
proof or the Metamath proof style.
For example, exploding the following theorem:
#explode iff_of_true
produces:
iff_of_true : ∀ {a b : Prop}, a → b → (a ↔ b)
0│ │ a ├ Prop
1│ │ b ├ Prop
2│ │ ha ├ a
3│ │ hb ├ b
4│ │ x✝ │ ┌ a
5│4,3 │ ∀I │ a → b
6│ │ x✝ │ ┌ b
7│6,2 │ ∀I │ b → a
8│5,7 │ Iff.intro │ a ↔ b
9│0,1,2,3,8│ ∀I │ ∀ {a b : Prop}, a → b → (a ↔ b)
Overview #
The #explode
command takes the body of the theorem and decomposes it into its parts,
displaying each expression constructor one at a time. The constructor is indicated
in some way in column 3, and its dependencies are recorded in column 2.
These are the main constructor types:

Lambda expressions (
Expr.lam
). The expressionfun (h : p) => s
is displayed as0│ │ h │ ┌ p 1│** │ ** │ │ q 2│1,2 │ ∀I │ ∀ (h : p), q
with
**
a wildcard, and there can be intervening steps between 0 and 1. Nested lambda expressions can be merged, and∀I
can depend on a whole list of arguments. 
Applications (
Expr.app
). The expressionf a b c
is displayed as0│** │ f │ A → B → C → D 1│** │ a │ A 2│** │ b │ B 3│** │ c │ C 1│0,1,2,3 │ ∀E │ D
There can be intervening steps between each of these. As a special case, if
f
is a constant it can be omitted and the display instead looks like0│** │ a │ A 1│** │ b │ B 2│** │ c │ C 3│1,2,3 │ f │ D

Let expressions (
Expr.letE
) do not display in any special way, but they do ensure that inlet x := v; b
thatv
is processed first and thenb
, rather than first doing zeta reduction. This keeps lambda merging and application merging from making proofs withlet
confusing to interpret. 
Everything else (constants, fvars, etc.) display
x : X
as0│ │ x │ X
In more detail #
The output of #explode
is a Fitchstyle proof in a fourcolumn 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 for each row in the proof, used in the Hyp fields.
 Hyp: The direct children of the current step. These are step numbers for the subexpressions for this step's expression. For theorem applications, it's the theorem arguments, and for foralls it is all the bound variables and the conclusion.
 Ref: The name of the theorem being applied. This is welldefined 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
foo
, x
andy
will be suppressed, because term construction is not interesting, and the Hyp field will reference steps proving
A x
andB y
. This corresponds to a proof term like@foo x y pA pB
wherepA
andpB
are subproofs.  In the Hyp column, suppressed terms are omitted, including terms that ought to be
suppressed but are not (in particular lambda arguments).
TODO: implement a configuration option to enable representing suppressed terms using
an
_
rather than a step number.
 the Ref field will contain
 If the head of the proof term is a local constant or lambda, then in this case the Ref will
say
∀E
for forallelimination. This happens when you have for exampleh : A > B
andha : A
and proveb
byh ha
; we reinterpret this as if it said∀E h ha
where∀E
is (nary) modus ponens.  If the proof term is a lambda, we will also use
∀I
for forallintroduction, 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∀I
step. Metamath doesn't have steps like this, but the style is based on Fitch proofs in firstorder logic.
 If the theorem is
 Type: This contains the type of the proof term, the theorem being proven at the current step.
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.)