Simplify assumptions by reversing `extends`

Stream: mathlib4

[Josha Dekker]

I was curious about the following: currently Lean can pick up if an assumption is not used in a result (we get a nice squiggly line in VS-code for example). Do we have something that tries to see if an assumption is overkill (for the given proof)?

E.g. suppose I wrote down as an assumption [Group G], but in fact I only need [Mul G].
Do we have something/would it be programmatically straightforward to iteratively try and replace every assumption by (one of) its direct parents and check if the proof still works? Possibly it might also want to try aesop or exact? to see if it can still close the goal if the modified assumption gives an error.

In my example, it would thus do:

1. Check that the proof works for [Group G]
2. Check that the proof works for [SemiGroup G], replace the assumption
3. Check that the proof works for [Mul G], replace the assumption

[Ruben Van de Velde]

This existed in lean 3, you can probably find references if you search zulip. We're hoping someone(TM) will port it

[Josha Dekker]

learning Lean for programming is on my (very) long to-do list, I'm afraid I certainly won't be able to be that someone(TM) for a few months.

[Josha Dekker]

How was the experience with this, did it often manage to generalise results nicely?

[Johan Commelin]

@Alex J. Best wrote that tool. It would be awesome if it can be ported to Lean 4 at some point.

[Alex J. Best]

Yeah I agree it would be awesome, and it seems like there is certainly demand for it again! It may well be a bit easier to implement now that we have a lot more computational code written in lean itself.
I think it was fairly successful though sometimes had some annoying false positives due to the fact it was trying to be perhaps too general, which meant that it never made it to mathlib