# 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.

Core `explode`

algorithm.

`select`

is a condition for which expressions to process`includeAllDeps`

is whether to include dependencies even if they were filtered out. If`True`

, then`none`

is inserted for omitted dependencies`e`

is the expression to process`depth`

is the current abstraction depth`entries`

is the table so far`start`

is whether we are at the top-level of the expression, which causes lambdas to use`Status.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.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Main definition behind `#explode`

command.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`#explode expr`

displays a proof term in a line-by-line format somewhat akin to a Fitch-style
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 expression`fun (h : p) => s`

is displayed as`0│ │ 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 expression`f a b c`

is displayed as`0│** │ 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 like`0│** │ 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 in`let x := v; b`

that`v`

is processed first and then`b`

, rather than first doing zeta reduction. This keeps lambda merging and application merging from making proofs with`let`

confusing to interpret.Everything else (constants, fvars, etc.) display

`x : X`

as`0│ │ x │ X`

## 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 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 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
`foo`

, `x`

and`y`

will be suppressed, because term construction is not interesting, and- the Hyp field will reference steps proving
`A x`

and`B y`

. This corresponds to a proof term like`@foo x y pA pB`

where`pA`

and`pB`

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 forall-elimination. This happens when you have for example`h : A -> B`

and`ha : A`

and prove`b`

by`h ha`

; we reinterpret this as if it said`∀E h ha`

where`∀E`

is (n-ary) modus ponens. - If the proof term is a lambda, we will also use
`∀I`

for 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`∀I`

step. 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.

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.)

## Equations

- One or more equations did not get rendered due to their size.