DiscrTree doesn't match lemmas with `OfNat.ofNat *` to nat literal keys

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When a @[simp] lemma is ∀ (n : Nat), P (OfNat.ofNat n), simp fails to apply it to targets like P 2 due to a bug in DiscrTree.

Context

Zulip thread

This has been requiring us to add no_index around every explicit invocation of OfNat.ofNat. e.g. https://github.com/leanprover-community/mathlib4/pull/8317

MWE

def MyProp (n : Nat) : Prop := False

-- DiscrTree key: [MyProp, OfNat.ofNat, Nat, *, *]
theorem myProp_ofNat (n : Nat) : MyProp (OfNat.ofNat n) := sorry

example : MyProp 0 := by simp [myProp_ofNat] -- fails. should succeed
example (n : Nat) : MyProp (OfNat.ofNat n) := by simp [myProp_ofNat] -- succeeds

-- DiscrTree key: [MyProp, *]
theorem myProp_ofNat' (n : Nat) : MyProp (no_index (OfNat.ofNat n)) := sorry
example : MyProp 0 := by simp [myProp_ofNat'] -- succeeds

Expected behavior: simp should be able to solve MyProp 0

Actual behavior: simp makes no progress

Versions

4.3.0-rc1

Additional Information

My diagnosis of the issue is that in DiscrTree, we are stripping off invocations of OfNat.ofNat on numerals, but not on variables.

Code stripping it off of numerals:
https://github.com/leanprover/lean4/blob/8cfcf7ce61bba328ed57d97bb12cf1a0fc40a0b9/src/Lean/Meta/DiscrTree.lean#L167-L173

It seems like the possible solutions are:

• (A) Treat OfNat.ofNat n similarly to n + 1, and convert it to * when inserting in the DiscrTree. (Equivalent to placing no_index around every OfNat.ofNat invocation)
  • This is bad for performance in Mathlib because simp lemmas about (OfNat.ofNat n : R) for an arbitrary ring R will be tried for every single subexpression of the target
• (B) Change the normal form of numerals like (5 : R) in the DiscrTree to [OfNat.ofNat, R, 5, *] rather than simply [5]
  • This would probably require additional handling to convert raw nat literals, Nat.zero, and Nat.succ into this normal form
• (C) Add a special case when doing lookup of an expression whose key is Key.lit (natVal _) to additionally search the tree for Key.const OfNat.ofNat 3 and then traverse next few keys appropriately
  • This seems ugly, and I think it would result in false positives when the OfNat result types are different. e.g. Searching for lemmas about (5 : R) where R is a variable would turn up results for specific rings (5 : Rat)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with src/Lean/Meta/DiscrTree.lean around lines 167–173 and reproduce the minimal example from the issue. Trace how DiscrTree keys are formed and looked up for OfNat.ofNat applied to variables versus literals. Done means simp solves MyProp 0 for the lemma shown without causing the noted false matches.