Did norm_num just get weaker?

Stream: mathlib4

[Bhavik Mehta]

import Mathlib

example : 3 ∣ 9 := by norm_num

I'm pretty sure this worked on mathlib head a week ago, but it fails today. Has something changed?

[Bhavik Mehta]

To be specific, this succeeds for me on mathlib4 commit aa0957f (from 13th Nov) and fails for me on 778f663 (from 19th Nov)

[David Renshaw]

Yes, see mathlib4#8366.

[David Renshaw]

My understanding is that the main difference is that simp no longer uses decide := true by default

[Bhavik Mehta]

Right I'm aware of this change, but that's not enough to justify this example breaking. For instance, simp in mathlib3 doesn't use decide either (and so it fails on this example) but norm_num in mathlib3 can do it

[David Renshaw]

Perhaps decide was masking other deficiencies in mathlib4 norm_num.

[David Renshaw]

fwiw, this works

example : 3 ∣ 9 := by decide

[Bhavik Mehta]

Sure decide works but my actual case is a more complex expression where I'd like this to be normalised away! So perhaps to be more specific, the issue is that norm_num1 fails on this.

[Bhavik Mehta]

Ah, and all the tests for norm_num1 with divisibility are commented out...

[David Renshaw]

curiously, this fails, even though Mathlib.Tactic.NormNum.Prime exists and purports to be able to handle it

example : Prime 3 := by norm_num

[David Renshaw]

Ah, wait, no, it does work with Nat.Prime

[Bhavik Mehta]

It seems like the divisibility extension to norm_num was just never ported, and it wasn't noticed because decide was picking up the slack.

[Thomas Murrills]

Note issue #2136! (I’m not entirely sure it’s up to date)

[Bhavik Mehta]

Ah great to know, thank you!

[Thomas Murrills]

We should probably add the facts that an extension exists for Nat.Prime and that one doesn’t for the generic Prime; I’m on mobile at the moment, however.

[David Renshaw]

Note also that #7112 would allow you to re-enable decide in norm_num.

[Patrick Massot]

@Mario Carneiro is there any reason this wasn't labelled as awaiting review? I delegated it anyway since it looks fine to me.

[Eric Rodriguez]

For Prime it should be really easy to write an extension I guess? I can give it a crack to learn metaprogramming I guess

[Eric Rodriguez]

Where is the guide again?

[Mario Carneiro]

#8534 implements a norm_num extension for Nat.dvd, Int.dvd, Int.div

[Gareth Ma]

Hi, is the following example also related to the simp-decide change?

lemma works (n : ℕ) : 2 * n + 1 + 1 = 2 * n + 2 := by norm_num
lemma fails (n : ℕ) : (2 * n + 1 + 1) / 2 = (2 * n + 2) / 2 := by norm_num

Here's the trace:

▶ 13:67-13:75: information:
[Tactic.norm_num] (2 * n + 1 + 1) / 2 failed: not a division ring
[Tactic.norm_num] Mathlib.Meta.NormNum.evalOfNat:
    2 ==> isNat 2 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
[Tactic.norm_num] 2 * n failed: n: no norm_nums apply
[Tactic.norm_num] 2 * n + 1 failed: 2 * n: no norm_nums apply
[Tactic.norm_num] 2 * n + 1 + 1 failed: 2 * n + 1: no norm_nums apply
[Tactic.norm_num] (2 * n + 1 + 1) / 2 failed: 2 * n + 1 + 1: no norm_nums apply
...

The final line is weird.

[Anne Baanen]

I don't think norm_num is supposed to work on either of these goals anyway, since it's supposed to work on concrete numerals, not variables. Does simp work on either goal? (What are you importing?)

[Ruben Van de Velde]

Wouldn't you expect norm_num to combine the +1 +1?

[Gareth Ma]

^

[Ruben Van de Velde]

Though I can see the argument about that being out of scope too

[Gareth Ma]

Anne Baanen said:

I don't think norm_num is supposed to work on either of these goals anyway, since it's supposed to work on concrete numerals, not variables. Does simp work on either goal? (What are you importing?)

I'm importing Mathlib.Tactic, I can switch to Mathlib and try. ring_nf normalises it to (2 + k * 2) / 2, simp does nothing.

[Mauricio Collares]

To confirm this is not related to the decide change, you can try norm_num (config := {decide := true}) on the norm_num_cfg branch (#7112). I just did and it fails there too.

[Gareth Ma]

uh
Screenshot-2023-11-21-at-09.17.01.png

[Gareth Ma]

Oh, I need to switch to the branch you mentioned, I see

[Dan Velleman]

The following example worked in v4.2.0, but doesn't work in v4.3.0-rc2:

import Mathlib.Tactic

def f (n : Nat) : Nat := n + 1

example : f 0 = 1 := by
  norm_num

Was this a deliberate change to norm_num, or a side effect of some other change?

[Ruben Van de Velde]

We had a change to make simp not run decide by default, that might be it

[Patrick Massot]

This is not about decide, this is about unfolding the definition of f.

[Kyle Miller]

@Patrick Massot I'm pretty sure this is about decide. The "decision procedure" for Nat equality is to do rfl. This succeeds:

example : f 0 = 1 := by
  decide

[Kyle Miller]

@Dan Velleman You can pass norm_num additional simp lemmas, including functions to unfold.

example : f 0 = 1 := by
  norm_num [f]

If you tag the function with @[simp] to make it auto-unfold, then norm_num succeeds.

@[simp]
def f (n : Nat) : Nat := n + 1

example : f 0 = 1 := by
  norm_num

[Patrick Massot]

I claims that

example : f 0 = 1 := by
  unfold f
  norm_num

should work

[Patrick Massot]

So this is about norm_num no longer unfolding f, right?

[Patrick Massot]

And by norm_num I really mean the simp called by norm_num

[Kyle Miller]

Yeah, that does work, but I think the specific change is that simp doesn't use decide by default anymore, and decide was incidentally unfolding f because it applies rfl.

[Dan Velleman]

If I make it f 0 < 2 rather than f 0 = 1, then rfl is no longer relevant, right? But decide still seems to work. So I think f is still getting unfolded, but not because of a call to rfl.

[Kyle Miller]

Sure, rfl wouldn't be relevant if you change the proposition to something that's not an equality. In the case of f 0 < 2, you can check the term that decide produces, and it uses Nat.decLt (f 0) 2. Inside of this is Nat.ble (f 0 + 1) 2, and the elaborator will unfold f 0 here while it computes whether this is true or false.

[Kyle Miller]

The short version is that decide can incidentally unfold functions because unification/whnf is eager to (efficiently) compute basic Nat functions including Nat.ble.

This is what decide is doing:

theorem foo : f 0 < 2 :=
  Nat.le_of_ble_eq_true (refl true : Nat.ble (f 0 + 1) 2 = true)

[Kyle Miller]

(Here's that list by the way: https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/WHNF.lean#L858-L866)

[Scott Morrison]

I think turning decide back on inside norm_num may be reasonable! Someone should try it, and run !bench.

[Mario Carneiro]

yes, it's supposed to be enabled by default

[Shreyas Srinivas]

Stumbled into this issue with simp. Is there a shortcut to all simp using tactics that use the old configuration ? It breaks quite a few proofs for me (all fixed now, after some effort)

[Scott Morrison]

No, there is not. In future when making significant changes to tactic behaviour like this, we may add a set_option that gives a backwards compatibility mode. But we'll probably set it up to generate many warnings; it won't be an alternative to adapting to the new behaviour, just a helper.

[Scott Morrison]

I do hope someone looks at norm_num. It is probably just a one-liner fix.

[Kyle Miller]

One of the issues with norm_num back when simp was still doing decide was that this could cause norm_num to be slow because it was accidentally using a decide procedure rather than actually normalizing numbers. (And for something like equailty, that means it would be just applying rfl, which might be a heavy one.)

Maybe the fix is that norm_num should have a low-priority norm num extension for propositions that tries doing decide?

[Kyle Miller]

By the way, there's a declare_simp_like_tactic command to make your own simp with your own configuration. I've never used it, but I noticed it the other day.

[Kyle Miller]

That's how tactics like simp_arith are defined.

declare_simp_like_tactic simpArith "simp_arith " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, decide := true }

[Mario Carneiro]

AFAIK norm_num should use its own algorithms by preference to decide when both are applicable. The only reason that situation should happen is if there is no norm_num extension for the function in question