simprocs and norm_num

Stream: mathlib4

[Joe Hendrix]

Hi all. I have an open Lean 4 PR (lean4#3808) that removes some simp annotations using Nat.succ and adds simprocs to more efficiently solve some basic arithmetic normalization problems that Lean currently struggles with such as:

example : 12345678 ≠ 1234567 := by simp
example (x : Nat) : x + 12345678 ≥ 1234567 := by simp

When testing on Mathlib, I noticed that this PR seems to weaken norm_num. That's a Mathlib tactic and out of scope for a Lean PR, but I thought I'd alert folks to the issue in case there are any changes that would help Mathlib.

The simproc approach in that PR has some downsides in complexity, but Lean default simp rules shouldn't struggle with numeric literals either.

[Eric Wieser]

Why does 37 (aka OfNat.ofNat (nat_lit 37)) unify with succ (OfNat.ofNat (nat_lit 36))? To me it seems like the succ lemmas should remain simp, but we should stop allowing succ _ to match with numeric literals?

[Eric Wieser]

(after all, simpProcs can now handle the numeric literals)

[Joe Hendrix]

Changing discriminator trees to not treat offset terms as star would make those lemmas effectively never trigger as simp rules given Nat.succ_eq_add_one is now simp.

My hunch is that dropping support for offset terms is going to lead to a less effective simp for most users, but I also don't have the bandwidth to investigate downstream effects in more detail.

[Eric Wieser]

I've not heard the term "offset term" before; what does it refer to here?

[Eric Wieser]

Your point about Nat.succ_eq_add_one is a good one

[Joe Hendrix]

I should have expanded that a bit. That's a term I was using informally to describe terms that match the isOffset predicate used in the implementation of discriminator trees here.

Discriminator trees are essentially a filter and so if you wanted the discriminator tree to not match the 37 literal against succ x then the first thing to change is probably the definition of shouldAddAsStar in that file.

[Eric Wieser]

I think this is already a painpoint for mathlib, and there's an open lean4 issue about it; due to numeric literals not indexing OfNat in the discrTrees, mathlib is littered with no_index lemmas which are probably bad for performance.

[Kyle Miller]

I this regression to norm_num is just from a changing simp set changing how Nat.succ simplifies, that seems fine to me. I don't think that tactic should rely on those sorts of simp lemmas.

[Kyle Miller]

In particular, they weaken norm_num's ability to efficiently normalize numbers, for the same reason you want the simprocs.

[Timo Carlin-Burns]

Eric Wieser said:

I think this is already a painpoint for mathlib, and there's an open lean4 issue about it; due to numeric literals not indexing OfNat in the discrTrees, mathlib is littered with no_index lemmas which are probably bad for performance.

You're talking about lean4#2867 which is different but related. That issue is about how terms like 5 : Nat appear in the discrtree. isOffset is about how terms like n + 2 appear in the discrtree. My fix for the former leaves the latter unchanged

[Mario Carneiro]

@Kyle Miller said:

I this regression to norm_num is just from a changing simp set changing how Nat.succ simplifies, that seems fine to me. I don't think that tactic should rely on those sorts of simp lemmas.

In particular, they weaken norm_num's ability to efficiently normalize numbers, for the same reason you want the simprocs.

I'm confused, that seems like a big issue? Normalizing numbers is its job, after all (it's right in the name).

Is there an MWE which explains what regression is being talked about here?

[Eric Wieser]

Hi all. I have an open Lean 4 PR (lean4#3808)

Just to note, this is now a merged PR, not an open PR

[Eric Wieser]

Something pretty wonky is going on in https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3808; std is in the lake manifest 5 times!

[Joe Hendrix]

Yes, I've done testing on a local copy of Mathlib and the results seem fairly reasonable. The issue with lake is really strange, but it has to be orthogonal. I'll manually update that manifest.

[Eric Wieser]

Could this instance concern be related to the norm_num issues?

[Joe Hendrix]

Does norm_num automatically use [simp] rules? It's possible that Nat.succ.injEq no longer being simp is impacting norm_num's normalization.

[Mario Carneiro]

Joe Hendrix said:

Does norm_num automatically use [simp] rules? It's possible that Nat.succ.injEq no longer being simp is impacting norm_num's normalization.

norm_num is an extension of simp, and takes all the same options

[Notification Bot]

30 messages were moved from this topic to #mathlib4 > Interfacing with changes to core by Eric Wieser.

[Eric Wieser]

Eric Wieser said:

Could this instance concern be related to the norm_num issues?

I split the thread because I don't want this point to be swamped; matching instances syntactically is IMO pretty much always a bug (and objectively incompatible with the current typeclass design in Mathlib).

[Joe Hendrix]

I picked a conservative approach with that check precisely to avoid the simproc matching unexpected parts of Mathlib. It strictly generalizes the existing simprocs. I think a norm_cast issue if it is using the simp discriminator tree.

[Eric Wieser]

Well, you've removed simp on some lemmas with the claim that the simpproc replaces them, but this is not the case

[Eric Wieser]

The lemmas will fire on any defeq instance, the simp-proc will only match syntactically

[Eric Wieser]

So I think norm_num aside, this has made simp able to work with n + 1 but not n + 1, where the difference is only visible in the infoview.

[Joe Hendrix]

Those lemmas involved Nat.succ. What instance is relevant?

[Eric Wieser]

The succ lemma matches against n + 1 too

[Eric Wieser]

import Mathlib.Data.Nat.Basic

example (n : ℕ) : 1 + n = 1 + 3 := by
  rw [add_comm 1, add_comm 1]
  -- this works, but a simproc looking for `instNatAdd` will fail
  simp only [Nat.succ.injEq]
  sorry

[Joe Hendrix]

Awesome. Thanks I can make a Lean specific one to evaluate.

[Joe Hendrix]

@Eric Wieser Interestingly, the simp only line didn't appear to be succeeding in master due to additional syntacic checks added in an earlier PR. The issue has been added in lean4#3836, and a proposed fix PR is in lean4#3838 that addresses both the isDefEq failure and the new simproc.