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

[timotree3]

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. leanprover-community/mathlib4#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:

lean4/src/Lean/Meta/DiscrTree.lean

Lines 167 to 173 in 8cfcf7c

	/--
	Return true if `e` is one of the following
	- A nat literal (numeral)
	- `Nat.zero`
	- `Nat.succ x` where `isNumeral x`
	- `OfNat.ofNat _ x _` where `isNumeral x` -/
	private partial def isNumeral (e : Expr) : Bool :=

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.

[eric-wieser]

Regarding option B, I'm not sure the raw literals are allowed to exist without an OfNat "event horizon" in the first place; so I think the challenge is only with handling succ and zero, and even then it's not clear to me whether they actually should be treated as literals.

[timotree3]

Unfortunately there are some automatically-generated simp lemmas with raw nat literals that we expect to work with OfNat literals:

lean4/tests/lean/run/bugNatLitDiscrTree.lean

Lines 1 to 14 in e29c323

	def f' (n : Nat) : Option { r : Nat // r ≤ n } :=
	match n with
	| 0 => some ⟨0, Nat.le_refl _⟩
	| n+1 => match f' n with
	| some ⟨m, h₁⟩ =>
	have : m < n+1 := Nat.lt_of_le_of_lt h₁ (Nat.lt_succ_self _)
	match f' m with
	| some ⟨r, h₂⟩ => some ⟨r, Nat.le_trans h₂ (Nat.le_trans h₁ (Nat.le_succ _))⟩
	| none => none
	| none => none
	theorem f'_ne_none (n : Nat) : f' n ≠ none := by
	match n with
	| 0 => simp (config := { decide := false }) [f']; done

In this test case, the lemma f'._eq_1 for the 0 => case of a function defined via a match and well-founded recursion has nat_lit 0 in its LHS.

I have a branch implementing option B, but I don't know how to address this issue properly. Ideally nat_lit n would be its own normal form, but to make this equation lemma work, I had to add a hack where nat_lit n is normalized to OfNat.ofNat (nat_lit n) except if it is already nested inside of an OfNat.ofNat (to prevent infinite recursion). This is annoying because it requires keeping extra state in the DiscrTree traversal loop. Once I have tests I will make a PR for this, but in the long run it would be preferable to avoid having nat_lits in our theorem statements entirely.

[eric-wieser]

That sounds like a bug in the generated lemmas to me

[timotree3]

Equation lemmas sometimes end up with unenclosed nat_lit 0 in them and sometimes don't. For example, if f' is changed above to return Option Nat or any other type which doesn't depend on n, then the generated equation lemma has OfNat.ofNat as desired:

@[simp] def nondep (n : Nat) : Option Nat :=
  match n with
  | 0   => some 0
  | n+1 => match nondep n with
    | some m =>
      have : m < n+1 := sorry
      match nondep m with
      | some r => some r
      | none => none
    | none => none

#check nondep._eq_1 -- nondep._eq_1 : nondep (OfNat.ofNat (nat_lit 0)) = some 0`

I've done a bit of investigating, and it looks like what's happening is:

1. The match is elaborated into a matcher with an argument of type motive (nat_lit 0), because the pattern 0 denotes nat_lit 0.
2. In order to determine the equation lemmas, split is used to split the match. A case for n = nat_lit 0 is created
3. Before finalizing the lemma, its statement is passed through simp. simp has code for nat_lit n -> OfNat.ofNat (nat_lit n), but dsimp doesn't, so the rule can't apply when nat_lit 0 is in a position with forward dependencies. Furthermore, even if dsimp had a rule for this (which it probably should), it wouldn't apply, because the invocation of simp used for normalizing these lemma statements has cfg.dsimp := false. This was done for performance reasons in f1d84a5.

example : nat_lit 2 = sorry := by
  simp only
  -- ⊢ 2 = sorryAx ℕ

example : nat_lit 2 = sorry := by
  dsimp only -- dsimp made no progress

It would be easy enough to add the logic for nat_lits to dsimp and re-enable dsimp in computing these lemma statements, but it would presumably come with some perf cost. Is it worth it? It seems like a good idea to consistently follow the rule that nat_lit should not appear outside of OfNat.ofNat.

[girving]

What’s the status of this issue? There have been a few recent commits, but no_index is still required on OfNat lemmas as of v4.11.0-rc2.

[eric-wieser]

I think all the commits are in the unmerged #3684, which is awaiting someone to prove that mathlib can be adapted to work with it.