Break down simp tactics into all tactics used

[realharryhero]

A lot of theorems use the tactic "simp," which is a tactic that uses many trivial tactics to "simplify" the problem down to an easier version quickly (using identities like a * 1 = a, 1 + 0 = 1, etc). When analyzing the tactics used to solve a particular problem, for example when using thm.get_traced_tactics() in LeanDojo, the list of tactics sometimes includes a simp tactic. But no info is given to what theorems the simp tactic actually uses.

Maybe (maybe) it'd be a good idea to have an option to include what the simp tactic uses? Certainly one can figure out a superset of the set of tactics simp uses by seeing all tactics simp is able to use, but simp only uses a subset of those tactics, and that subset probably cannot be checked in LeanDojo itself, as the only way to do so at the highlighted text here requires something beyond just typing lean tactics to interact with the state. Thank you!

[yangky11]

I would favour leaving simp as is rather than breaking it into a sequence of rw. Tactics in Lean are just meta-programs, and you can easily define new tactics that use existing tactics in the same way simp use rw. If we choose to break simp into rw, then we should probably also try to break all tactics into the most atomic ones, which is infeasible.

[realharryhero]

I see, fair point. Thank you!