Proposed change to simplifier: don't simplify instances

Stream: mathlib4

[Kim Morrison]

In lean4#3151 Leo is proposing modifying the simplifier so that it does not visit instance implicit arguments by default, although this can be turned back on via (config := { instances := true }).

I've checked that it is possible to compile Mathlib, although quite a few changes are needed. The PR is at #9572, although this is stacked on top of another larger adaptation PR: the relevant diff is: https://github.com/leanprover-community/mathlib4/compare/lean-pr-testing-3124...lean-pr-testing-3151

There are many cases where it's "obvious" from looking at the simp set that the calling is trying to simplify instances (e.g. there is a HSMul.hSMul in the simp set, or a (· • ·)). However often it looks a bit surprising when (config := { instances := true }) is needed, so there's a concern about users getting stuck on this.

Pros and cons:

• It will presumably be faster (I'd like to benchmark, but this will need to wait for some dust to settle).
• There's a lot of abuse of instances in Mathlib, and I suspect that places where (config := { instances := true }) is necessary correlates with this, so perhaps it is good for visibility.
• Users will get confused, and may not realise when they are in a situation where they need (config := { instances := true }).

The most useful response to this post would be if anyone is interested in looking at the examples from the diffs above, and deciding how unobvious the need to instances := true is, and/or thinking about whether there would have been a better proof that didn't need it.

[Johan Commelin]

@Scott Morrison A lot of the example in the diff above are when a new structure/instance is being defined. Do you agree that this is a legitimate use case of the config option.

Put differently: do you think it makes sense to mainly investigate the other examples that occur in the middle of "regular" proofs?

[Kim Morrison]

Yes, that's a good way of thinking about it!