Documentation

Mathlib.Tactic.Explode

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.

source
partial def Mathlib.Explode.explodeCore (select : Lean.Expr → Lean.MetaM Bool) (includeAllDeps : Bool) (e : Lean.Expr) (depth : Nat) (entries : Mathlib.Explode.Entries) (start : optParam Bool false) :
Lean.MetaM (Option Mathlib.Explode.Entry × Mathlib.Explode.Entries)

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.
source
def Mathlib.Explode.explodeCore.consDep (includeAllDeps : Bool) (entry? : Option Mathlib.Explode.Entry) (deps : List (Option Nat)) :
List (Option Nat)

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
    source
    def Mathlib.Explode.explode (e : Lean.Expr) (filterProofs : optParam Bool true) :
    Lean.MetaM Mathlib.Explode.Entries

    Main definition behind #explode command.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Mathlib.Explode.«command#explode_» :
      Lean.ParserDescr

      #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.
        • 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.
      • 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.
      Instances For