feat: add Simp.Config.index

[leodemoura]

The simp tactic uses a discrimination tree to select candidate theorems that will be used to rewrite an expression. This indexing data structure minimizes the number of theorems that need to be tried and improves performance. However, indexing modulo reducibility is challenging, and a theorem that could be applied, when taking reduction into account, may be missed. For example, suppose we have a simp theorem foo : forall x y, f x (x, y).2 = y, and we are trying to simplify the expression f a b <= b. foo will not be tried by simp because the second argument of f a b is not a projection of a pair. However, f a b is definitionally equal to f a (a, b).2 since we can reduce (a, b).2.

In Lean 3, we had a much simpler indexing data structure where only the head symbol was taken into account. For the theorem foo, the head symbol is f. Thus, the theorem would be considered by simp.

This commit adds the option Simp.Config.index. When simp (config := { index := false }), only the head symbol is considered when retrieving theorems, as in Lean 3. Moreover, if set_option diagnostics true, simp will check whether every applied theorem would also have been applied if index := true, and report them. This feature can help users diagnose tricky issues in code that has been ported from libraries developed using Lean 3 and then ported to Lean 4. In the following example, it will report that foo is a problematic theorem.

opaque f : Nat → Nat → Nat

@[simp] theorem foo : f x (x, y).2 = y := by sorry

example : f a b ≤ b := by
  set_option diagnostics true in
  simp (config := { index := false })

In the example above, the following diagnostic message is produced.

[simp] theorems with bad keys
    foo, key: [f, *, Prod.1, Prod.mk, Nat, Nat, *, *]

With the information above, users can annotate theorems such as foo using no_index for problematic subterms.
Example:

opaque f : Nat → Nat → Nat

@[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry

example : f a b ≤ b := by
  simp -- `foo` is still applied

cc @semorrison
cc @PatrickMassot

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-05-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-05-17 18:09:30)