how to get all steps of `simp` tactic

Stream: mathlib4

[John Smith]

In Lean 4, many simple proofs can be completed directly using the simp tactic. I am trying to understand how simp works internally and would like to see all the steps it performs during the simplification process.

I know that by enabling the trace option:

lean

set_option trace.Meta.Tactic.simp true

I can see some traces of the simp tactic's behavior. However, the trace only shows part of the process, and many details are still omitted.

For example, consider the following code:

lean

import Mathlib set_option trace.Meta.Tactic.simp true
example : 1 + 0 = 1 * 1 := by   simp

The trace output is:

[Meta.Tactic.simp.rewrite] add_zero:1000, 1 + 0 ==> 1
[Meta.Tactic.simp.rewrite] mul_one:1000, 1 * 1 ==> 1
[Meta.Tactic.simp.rewrite] eq_self:1000, 1 = 1 ==> True

Based on this information, I tried to manually reproduce the proof:

lean

example : 1 + 0 = 1 * 1 := by
rewrite [add_zero]
rewrite [mul_one]
rewrite [eq_self]

However, Lean 4 gives an error:

Basic.lean:7:27
unsolved goals
⊢ True

This is a simple unsolved goal, but the core issue is that I cannot retrieve the complete steps performed by simp. Specifically:

• The trace does not show how simp closes the final goal (e.g., proving ⊢ True).
• Some intermediate steps or implicit reasoning might be missing from the trace.

Questions:

1. Is there a way to get all the steps performed by simp, including the final step that closes the goal?
2. Are there additional debugging options or techniques to fully reconstruct what simp does?

Any guidance or suggestions would be greatly appreciated!

[suhr]

You can just use #print to look inside the generated code:

import Mathlib
set_option trace.Meta.Tactic.simp true

def foo : 1 + 0 = 1 * 1 := by simp

#print foo
#check of_eq_true

[Ruben Van de Velde]

If you want to know how exactly simp does what it does, I guess you should read the implementation

[John Smith]

suhr said:

You can just use #print to look inside the generated code

When I tried using #print to inspect some mathlib lemmas that were proven by simp, I encountered an issue. The output often contains references to _auxLemma. However, when I attempt to check these auxiliary lemmas, Lean 4 responds with unknown constant.

For example:

#print SimpleGraph.isClique_empty

The output is:

theorem SimpleGraph.isClique_empty.{u_1} : ∀ {α : Type u_1} {G : SimpleGraph α}, G.IsClique ∅ := fun {α} {G} ↦ of_eq_true (Mathlib.Data.Set.Pairwise.Basic._auxLemma.1 G.Adj)

But when I try to inspect Mathlib.Data.Set.Pairwise.Basic._auxLemma.1, Lean 4 gives me the error:

unknown identifier 'Mathlib.Data.Set.Pairwise.Basic._auxLemma'

why this happens? Are these _auxLemma definitions inaccessible or intentionally hidden? Is there a way to fully explore the steps used by simp in such cases?

[John Smith]

Ruben Van de Velde said:

If you want to know how exactly simp does what it does, I guess you should read the implementation

Nice suggestion, I will try

[Patrick Massot]

See also https://github.com/nomeata/lean-calcify

[John Smith]

Patrick Massot said:

See also https://github.com/nomeata/lean-calcify

calcify is a useful tactic for breaking down proofs into clear steps.

However, in complex cases, calcify may fail, and in other situations, it can still involve auxLemma.

Is there currently a fully mature explanation tactic or tool that can provide complete transparency into what simp does?

[Kyle Miller]

The step to close the goal is hard-coded. docs#Lean.Meta.simpTargetCore looks to see that the goal is True, and if so, uses of_eq_true to turn the proof generated by simp that p = True into a proof of p. (Or, if the simplification was purely definitional, it uses True.intro directly.)

[Kyle Miller]

It's part of the simp tactic, but not the core simp algorithm.

[Mario Carneiro]

John Smith said:

• The trace does not show how simp closes the final goal (e.g., proving ⊢ True).

simp closes the final goal by proving |- True

[Mario Carneiro]

it always proves goals by reducing them to True