Regression in cutsat

Stream: lean4

[Bhavik Mehta]

example {m n : Nat} : (4 ^ (m + 1) * n) % 4 = 0 := by cutsat

This works in Lean 4.25.1 but fails in Lean 4.26.0-rc2 (and lia and grind also fail on 4.26.0-rc2). Does anyone know what changed that could have caused this?

(lean4#11515)

[Robin Arnez]

Well, 4 ^ (m + 1) used to be normalized to 4 ^ m * 4, however that caused lean4#10661, so that normalizer got replaced by a propagator which is less powerful -- instead of 4 being a nice constant, it is hidden behind an equality and then grind fails for the same reason that grind can't do:

example (m n : Nat) (h : 4 ∣ m) : 4 ∣ m * n := by
  grind

which is that grind or more specifically the cutsat module works with linear integer arithmetic, and multiplying two variables is well ... not linear

[Bhavik Mehta]

Bah, so this is all my fault! It's annoying though that we can't solve both of these goals simultaneously...

[Bhavik Mehta]

One thing which isn't clear to me is why grind [Nat.pow_succ] also doesn't work, since now it should be explicitly using this lemma instead of (or as well as) the propagator. But grind [Nat.pow_succ, = Nat.mul_assoc] does work, even though the ring module should already know about associativity?

[Bhavik Mehta]

Huh, and grind [= Nat.mul_assoc] solves my original goal... That's surprising to me, but it's a short fix at least

[Bhavik Mehta]

Solved in lean4#11519