feat: parity between Int.ediv/tdiv/fdiv theorems (#7358)

This PR fills further gaps in the integer division API, and mostly
achieves parity between the three variants of integer division. There
are still some inequality lemmas about `tdiv` and `fdiv` that are
missing, but as they would have quite awkward statements I'm hoping that
for now no one is going to miss them.

src/Init/Data/BitVec/Lemmas.lean

@@ -3202,6 +3202,7 @@ then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
 theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
     (x / y).toInt = x.toNat / y.toNat := by
   simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
+  norm_cast
 
 /-! ### umod -/
 

src/Init/Data/Int/Bitwise/Lemmas.lean

@@ -27,7 +27,7 @@ theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
     m >>> n = m / ((2 ^ n) : Nat) := by
   simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]
   split
-  · simp
+  · simp; norm_cast
   · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
     rfl
 

src/Init/Data/Int/DivMod/Basic.lean

@@ -40,7 +40,9 @@ This pair satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`.
 /--
 Integer division. This version of integer division uses the E-rounding convention
 (euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
-and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
+and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x` for `y ≠ 0`.
+
+This means that `Int.ediv x y = floor (x / y)` when `y > 0` and `Int.ediv x y = ceil (x / y)` when `y < 0`.
 
 This is the function powering the `/` notation on integers.
 
@@ -109,7 +111,7 @@ instance : Div Int where
 instance : Mod Int where
   mod := Int.emod
 
-@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+@[norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
 theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl
 @[norm_cast]
@@ -165,6 +167,9 @@ def tdiv : (@& Int) → (@& Int) → Int
   unconditionally (see [`Int.tmod_add_tdiv`][theo tmod_add_tdiv]). In
   particular, `a % 0 = a`.
 
+  `tmod` satisfies `natAbs (tmod a b) = natAbs a % natAbs b`,
+  and when `b` does not divide `a`, `tmod a b` has the same sign as `a`.
+
   [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
   [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
 

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -53,7 +53,7 @@ protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm .
   constructor <;> exact fun ⟨k, e⟩ =>
     ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
 
-protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
+@[simp] protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
   constructor <;> exact fun ⟨k, e⟩ =>
     ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
 
@@ -121,7 +121,7 @@ theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
 
 /-! ### `/` ediv -/
 
-@[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
+@[simp] theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat _, -[_+1] => (Int.neg_neg _).symm
   | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
@@ -183,8 +183,6 @@ theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a
   match b, h with
   | Int.ofNat (b+1), _ =>
     rcases a with ⟨a⟩ <;> simp [Int.ediv]
-    norm_cast
-    simp
 
 @[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
 abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos

src/Init/Data/Int/Lemmas.lean

@@ -91,7 +91,7 @@ theorem add_neg_one (i : Int) : i + -1 = i - 1 := rfl
 
 /- ## basic properties of subNatNat -/
 
--- @[elabAsElim] -- TODO(Mario): unexpected eliminator resulting type
+@[elab_as_elim]
 theorem subNatNat_elim (m n : Nat) (motive : Nat → Nat → Int → Prop)
     (hp : ∀ i n, motive (n + i) n i)
     (hn : ∀ i m, motive m (m + i + 1) -[i+1]) :
@@ -269,6 +269,17 @@ protected theorem add_left_cancel {a b c : Int} (h : a + b = a + c) : b = c := b
   rw [Int.add_right_neg, Int.add_comm a, ← Int.add_assoc, Int.add_assoc b,
     Int.add_right_neg, Int.add_zero, Int.add_right_neg]
 
+/--
+If a predicate on the integers is invariant under negation,
+then it is sufficient to prove it for the nonnegative integers.
+-/
+theorem wlog_sign {P : Int → Prop} (inv : ∀ a, P a ↔ P (-a)) (w : ∀ n : Nat, P n) (a : Int) : P a := by
+  cases a with
+  | ofNat n => exact w n
+  | negSucc n =>
+    rw [negSucc_eq, ← inv, ← ofNat_succ]
+    apply w
+
 /- ## subtraction -/
 
 @[simp] theorem negSucc_sub_one (n : Nat) : -[n+1] - 1 = -[n + 1 +1] := rfl

src/Init/Data/Int/Linear.lean

@@ -194,7 +194,7 @@ theorem cmod_eq_zero_iff_emod_eq_zero (a b : Int) : cmod a b = 0 ↔ a%b = 0 :=
   unfold cmod
   have := @Int.emod_eq_emod_iff_emod_sub_eq_zero  b b a
   simp at this
-  simp [Int.neg_emod, ← this, Eq.comm]
+  simp [Int.neg_emod_eq_sub_emod, ← this, Eq.comm]
 
 private abbrev div_mul_cancel_of_mod_zero :=
   @Int.ediv_mul_cancel_of_emod_eq_zero

src/Init/Data/Int/Order.lean

@@ -361,6 +361,10 @@ protected theorem sub_lt_self (a : Int) {b : Int} (h : 0 < b) : a - b < a :=
 
 theorem add_one_le_of_lt {a b : Int} (H : a < b) : a + 1 ≤ b := H
 
+protected theorem le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1 := by
+  rw [Int.lt_iff_add_one_le]
+  exact (Int.add_le_add_iff_right 1).symm
+
 /- ### Order properties and multiplication -/
 
 
@@ -428,7 +432,7 @@ protected theorem mul_le_mul_of_nonpos_left {a b c : Int}
 
 /- ## natAbs -/
 
-@[simp] theorem natAbs_ofNat (n : Nat) : natAbs ↑n = n := rfl
+@[simp, norm_cast] theorem natAbs_ofNat (n : Nat) : natAbs ↑n = n := rfl
 @[simp] theorem natAbs_negSucc (n : Nat) : natAbs -[n+1] = n.succ := rfl
 @[simp] theorem natAbs_zero : natAbs (0 : Int) = (0 : Nat) := rfl
 @[simp] theorem natAbs_one : natAbs (1 : Int) = (1 : Nat) := rfl
@@ -473,6 +477,13 @@ theorem natAbs_of_nonneg {a : Int} (H : 0 ≤ a) : (natAbs a : Int) = a :=
 theorem ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : (natAbs a : Int) = -a := by
   rw [← natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]
 
+theorem natAbs_sub_of_nonneg_of_le {a b : Int} (h₁ : 0 ≤ b) (h₂ : b ≤ a) :
+    (a - b).natAbs = a.natAbs - b.natAbs := by
+  rw [← Int.ofNat_inj]
+  rw [natAbs_of_nonneg, ofNat_sub, natAbs_of_nonneg (Int.le_trans h₁ h₂), natAbs_of_nonneg h₁]
+  · rwa [← Int.ofNat_le, natAbs_of_nonneg h₁, natAbs_of_nonneg (Int.le_trans h₁ h₂)]
+  · exact Int.sub_nonneg_of_le h₂
+
 /-! ### toNat -/
 
 theorem toNat_eq_max : ∀ a : Int, (toNat a : Int) = max a 0

src/Init/Data/Nat/Div/Lemmas.lean

@@ -27,8 +27,8 @@ theorem div_le_iff_le_mul (h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1 := b
   omega
 
 -- TODO: reprove `div_eq_of_lt_le` in terms of this:
-protected theorem div_eq_iff (h : 0 < k) : x / k = y ↔ x ≤ y * k + k - 1 ∧ y * k ≤ x := by
-  rw [Nat.eq_iff_le_and_ge, le_div_iff_mul_le h, Nat.div_le_iff_le_mul h]
+protected theorem div_eq_iff (h : 0 < k) : x / k = y ↔ y * k ≤ x ∧ x ≤ y * k + k - 1 := by
+  rw [Nat.eq_iff_le_and_ge, and_comm, le_div_iff_mul_le h, Nat.div_le_iff_le_mul h]
 
 theorem lt_of_div_eq_zero (h : 0 < k) (h' : x / k = 0) : x < k := by
   rw [Nat.div_eq_iff h] at h'
@@ -98,18 +98,34 @@ theorem succ_div_of_not_dvd {a b : Nat} (h : ¬ b ∣ a + 1) :
     rw [eq_comm, Nat.div_eq_iff (by simp)]
     constructor
     · rw [Nat.div_mul_self_eq_mod_sub_self]
-      have : (a + 1) % (b + 1) < b + 1 := Nat.mod_lt _ (by simp)
       omega
     · rw [Nat.div_mul_self_eq_mod_sub_self]
+      have : (a + 1) % (b + 1) < b + 1 := Nat.mod_lt _ (by simp)
       omega
 
 theorem succ_div_of_mod_ne_zero {a b : Nat} (h : (a + 1) % b ≠ 0) :
     (a + 1) / b = a / b := by
   rw [succ_div_of_not_dvd (by rwa [dvd_iff_mod_eq_zero])]
 
-theorem succ_div {a b : Nat} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0 := by
+protected theorem succ_div {a b : Nat} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0 := by
   split <;> rename_i h
   · simp [succ_div_of_dvd h]
   · simp [succ_div_of_not_dvd h]
 
+protected theorem add_div {a b c : Nat} (h : 0 < c) :
+    (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0 := by
+  conv => lhs; rw [← Nat.div_add_mod a c]
+  rw [Nat.add_assoc, mul_add_div h]
+  conv => lhs; rw [← Nat.div_add_mod b c]
+  rw [Nat.add_comm (a % c), Nat.add_assoc, mul_add_div h, ← Nat.add_assoc, Nat.add_comm (b % c)]
+  congr
+  rw [Nat.div_eq_iff h]
+  constructor
+  · split <;> rename_i h
+    · simpa using h
+    · simp
+  · have := mod_lt a h
+    have := mod_lt b h
+    split <;> · simp; omega
+
 end Nat