feat: test for simp problem

[kim-em]

This will fail unless we have a fix!

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 61a84c96db4ef76ebcd7b1510c5b7c7f1cf81212 --onto 91244b2dd9d223006227648659203373f5a46b0b. (2024-05-15 05:39:22)

[leodemoura]

Copying my Zulip message here to make sure we find it in the future.

I investigated the examples in this issue, and I now understand what is going on. It is ugly :( Here are my findings:

• The issue lies in the discrimination tree. foo is not even tried when using simp [foo].

• simp treats non-constant arguments differently. When processing a non-constant, simp will index function arguments as wildcards, mimicking Lean 3's behavior. This approach was motivated by issue Simp regressions probably related to transparency #2670. The idea is that a non-constant is essentially a "local theorem," and its arguments may be messy. For example, given (h : f (a,b) (a,b).2 = (a,b).2), if we use simp [h] and index the argument (a,b).2, it will produce a bad index.

• simp has special support for identifiers that correspond to constants. simp [foo] is shorthand for simp [@foo]. Thus, the left-hand-side arguments of foo are indexed. The following index is added to the discrimination tree: [Quiver.Hom.unop, *, *, *, *, Opposite.op, Quiver.Hom, *, *, Opposite.0, *, Opposite.0, *, *].

• In simp [(foo)], metavariables are created for foo's implicit arguments, and it is not elaborated as a constant, but as a local theorem. Thus, the index generated is: [Quiver.Hom.unop, *, *, *, *, *].

• In simp [foo'], foo' is processed as a constant, but the theorem statement for foo' uses a no_index, resulting again in the index is: [Quiver.Hom.unop, *, *, *, *, *].

• In simp [foo.{v+1}], foo.{v+1} is not an identifier, and simp's support for treating it as @foo.{v+1} does not kick in. Metavariables for implicit arguments are again added, the result is not a constant, and again the index [Quiver.Hom.unop, *, *, *, *, *] is generated. Note that simp [@foo.{v+1}] fails, as it is elaborated as a constant. Providing the universe is not directly helping; it just disables the code that treats identifiers like foo as @foo in simp arguments. I acknowledge this is horrible and counterintuitive.

This is all quite messy, and it is not clear how to proceed. I see the some options:

• Create a new diagnostic section for simp arguments that were never used, and show their index.

• Allow users to instruct simp to use Lean 3 style indexing for constants such as foo. This would result in the simpler index [Quiver.Hom.unop, *, *, *, *, *]. We could even suggest this option for arguments that have a non-trivial index and were not used. Right now, simp [(foo)] is a very contrived way to accomplish that, but binder annotations are lost in the process.

[nomeata]

Create a new diagnostic section for simp arguments that were never used, and show their index.

Related: Just yesterday I was wondering if we could have a linter that warns about unused simp arguments. I assume it has to be a linter, and not a warning that simp can emit, in case the simp invocation is used multi times (e.g. after <;>). (I'd guess that simp can put in the info tree whether it used the argument, or even how often, and then the linter can aggregate over multiple entries from multiple runs of the tactic.)