Invalid proofs from simp Int.reduceMod

Stream: mathlib4

[David A]

The two different definitions of (a : Int) % (b : Int) available in Mathlib are causing Int.reduceMod to produce invalid proofs:

import Mathlib.Tactic
#eval (-1 : ℤ) % 4 -- => 3
example : (-1 % 4) = -1 := by simp only [Int.reduceMod]
/-
(kernel) declaration type mismatch, '_example' has type
  -1 = -1
but it is expected to have type
  -1 % 4 = -1
-/

It would be nice to have a flag to turn on simproc proof checking, as I've added checking manually to all my simprocs. Also idk what to do about the specific situation above.

[David A]

To be clear, the above example is false but simp "proves" it, producing an error in the kernel.
A goal of (-1%4) = 3 is proved by rfl but simp converts it into the false goal -1 = 3.

[David A]

Actually this might not be Mathlib's fault. I think it's related to https://github.com/leanprover/lean4/issues/2330; which seems to point to a bug in the extern implementation of the modulo operation. I'm getting the same "application type mismatch" from the bug even when I use Int.mod.

[David A]

Oh, ffs. It's the Int.mod documentation which is wrong. It claims that (-12 : Int).mod 7 = 2 when in fact it evaluates to -5. I still suspect the native code is going by the documented behavior rather than the implemented semantics or something like that, but the lesson is to explicitly use Int.emod everywhere.

[Kevin Buzzard]

Thanks for this careful diagnosis!

[Kim Morrison]

Documentation PR very welcome!