Index of simprocs?

Stream: lean4

[Alex Meiburg]

I happened upon the Lean v4.6.0 release notes, where simprocs were first announced. It suggested the advent of

Simplification procedures for custom theories, such as using ring axioms or performing polynomial factorization
And I mean, that sounds great! I could imagine a world where simp turns (x + y) * a + (z - a * x) into y * a + z using some ring-based simproc that says, I'll cancel out terms when it definitely leaves the whole thing strictly simpler, but leave other terms unchanged. (So, less aggressive that ring_nf, which we definitely would not want being a default simproc.)

But I'm not aware of any such simproc existing. Has anyone looked at making such powerful simprocs? What simprocs even _exist_? I realized I have no idea!

So, is there a list/guide of simprocs somewhere?

[Alex Meiburg]

There's three in Mathlib/Tactics/Simproc, I don't know where to find them in core Lean or Batteries... but anyway, since there's now so much ring-y type typeclasses in core lean because of grind, I could see such a simproc even existing in core

[Chris Henson]

Via a mix of loogle and grep, I see for Nat there is in core src/Init/Data/Nat/Simproc.lean that is then used for simprocs in src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean, not sure exactly what is all there.

[Chris Henson]

Oh I see it says rings in the quote, sorry. Not sure about that.

[David Thrane Christiansen]

A simproc index would be a nice thing to have in the language reference. I've created an issue to track it.

This is not at the top of the priority list right now, but it's good to track these things!

[Paul Lezeau]

Somewhat related: I implemented a command to list simprocs that match against a given pattern here: #27392