1
$\begingroup$

I miraculously found this https://leanprover-community.github.io/extras/simp.html (which I think was for lean 3?) and it said:

The simplifier is what is known as a conditional term rewriting system: all it does is repeatedly replace (or rewrite) subterms of the form A by B (B->A), for all applicable facts of the form A = B or A ↔ B. The simplifier mindlessly rewrites until it can rewrite no more. The simp lemmas are all oriented, with left-hand sides always being replaced by right-hand sides, and never vice versa. we would like the database of facts to be confluent, meaning the order in which the simplifier considers rewrites does not matter. Again, we aim to be close to confluent where possibl

Then it suggested to do:

set_option trace.simplify.rewrite true

then it should show the rewrite rules simp did. Using the docs wording:

if you add set_option trace.simplify.rewrite true above the example, then a squiggly blue underline will appear under simp (in VS Code) and clicking on this will show you the sequence of rewrites that simp performed

but that doesn't work anymore, error:

unknown option 'trace.simplify.rewrite'

How do I force Lean 4 to show me the rewrite rules?

$\endgroup$

1 Answer 1

2
$\begingroup$

I believe it is the following:

set_option trace.Meta.Tactic.simp true

Then you get messages like the following:

example : 1 + 0 = 1 * 1 := by
  simp
  /-
  [Meta.Tactic.simp.rewrite] Nat.add_zero:1000, 1 + 0 ==> 1 
  
  [Meta.Tactic.simp.rewrite] Nat.mul_one:1000, 1 * 1 ==> 1 
  
  [Meta.Tactic.simp.rewrite] @eq_self:1000, 1 = 1 ==> True 
  -/

You may also be interested in the tactic simp? which tells you what exact simp lemmas to use. (In Lean 4, there are many similar question mark tactics, exact?, rw?, apply?, aesop?, etc. which search the library and output a proof or proof step which replaces the tactic.).

example : 1 + 0 = 1 * 1 := by
  simp?
  /-
  Try this: simp only [Nat.add_zero, Nat.mul_one]
  -/

There is also rw_search which is like a more powerful version of simp?.


In general, to find options for set_options, you can use #help option as follows:

import Mathlib

#help option

and search through the (many) available options. That is how I found trace.Meta.Tactic.simp.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.