bdiv and bmod

Stream: Is there code for X?

[Mitchell Lee]

The definition of docs#Int.bdiv has this docstring:

Balanced division. This returns the unique integer so that
b * (Int.bdiv a b) + Int.bmod a b = a.

However, I can't see where the equation b * (Int.bdiv a b) + Int.bmod a b = a is actually proved. Is there something I am missing?

[Ruben Van de Velde]

@loogle Int.bdiv, Int.bmod

[loogle]

:shrug: nothing found

[Ruben Van de Velde]

Apparently not

[Mitchell Lee]

Here's a low-powered proof (only requiring Mathlib.Init). I'm sure it can be improved.

import Mathlib.Init

namespace Int

theorem bdiv_add_bmod (a : Int) (b : Nat) : b * (a.bdiv b) + a.bmod b = a := by
  unfold bdiv bmod
  split
  · simp_all only [Nat.cast_ofNat_Int, Int.mul_zero, emod_zero, Int.zero_add, Int.sub_zero,
      ite_self]
  · dsimp only
    split
    · exact ediv_add_emod a b
    · rw [Int.mul_add, Int.mul_one, Int.add_assoc, Int.add_comm b, Int.sub_add_cancel]
      exact ediv_add_emod a b

theorem bmod_eq (a : Int) (b : Nat) : a.bmod b = a - b * (a.bdiv b) := by
  rw (occs := .pos [2]) [← bdiv_add_bmod a b]
  rw [Int.add_comm, Int.add_sub_cancel]

Where would be the best place for a theorem like this to go? One possibility is Mathlib.Data.Int.DivMod (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Int/DivMod.html) but I am slightly concerned about putting an inessential theorem so early in the import hierarchy.

[Yury G. Kudryashov]

@Kim Morrison Should it go to Mathlib or Lean?

[Yury G. Kudryashov]

Looks like a basic fact about a definition from core which is never used in Mathlib.

[Ruben Van de Velde]

I'm guessing mathlib doesn't care much, so put it in batteries for Kim to upstream into core at their leisure

[Kim Morrison]

Yes, either PR to Batteries or Lean. I can collect it from Batteries when I next return to Int/Nat.

[Mario Carneiro]

yes, this should go in Data.Int.DivMod. I think bdiv did not exist when I wrote most of the theorems in that file (which is now in Init)

[Mitchell Lee]

https://github.com/leanprover/lean4/pull/6494