chore: remove deprecated aliases for Int.tdiv and Int.tmod (#6322)

This PR removes the deprecated aliases `Int.div := Int.tdiv` and
`Int.mod := Int.tmod`. Later we will rename `Int.ediv` to `Int.div` and
`Int.emod` to `Int.mod`.

src/Init/Data/Int/DivMod.lean

@@ -29,6 +29,8 @@ At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with
 In September 2024, we decided to do this rename (with deprecations in place),
 and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
 ever need to use these functions and their associated lemmas.
+
+In December 2024, we removed `tdiv` and `tmod`, but have not yet renamed `ediv` and `emod`.
 -/
 
 /-! ### T-rounding division -/
@@ -71,8 +73,6 @@ def tdiv : (@& Int) → (@& Int) → Int
   | -[m +1], ofNat n => -ofNat (succ m / n)
   | -[m +1], -[n +1] =>  ofNat (succ m / succ n)
 
-@[deprecated tdiv (since := "2024-09-11")] abbrev div := tdiv
-
 /-- Integer modulo. This function uses the
   [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
   to pair with `Int.tdiv`, meaning that `tmod a b + b * (tdiv a b) = a`
@@ -107,8 +107,6 @@ def tmod : (@& Int) → (@& Int) → Int
   | -[m +1], ofNat n => -ofNat (succ m % n)
   | -[m +1], -[n +1] => -ofNat (succ m % succ n)
 
-@[deprecated tmod (since := "2024-09-11")] abbrev mod := tmod
-
 /-! ### F-rounding division
 This pair satisfies `fdiv x y = floor (x / y)`.
 -/
@@ -251,8 +249,6 @@ instance : Mod Int where
 
 theorem ofNat_tdiv (m n : Nat) : ↑(m / n) = tdiv ↑m ↑n := rfl
 
-@[deprecated ofNat_tdiv (since := "2024-09-11")] abbrev ofNat_div := ofNat_tdiv
-
 theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
   | 0, _ => by simp [fdiv]
   | succ _, _ => rfl

src/Init/Data/Int/DivModLemmas.lean

@@ -1315,65 +1315,3 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
           all_goals decide
     · exact ofNat_nonneg x
     · exact succ_ofNat_pos (x + 1)
-
-/-! ### Deprecations -/
-
-@[deprecated Int.zero_tdiv (since := "2024-09-11")] protected abbrev zero_div := @Int.zero_tdiv
-@[deprecated Int.tdiv_zero (since := "2024-09-11")] protected abbrev div_zero := @Int.tdiv_zero
-@[deprecated tdiv_eq_ediv (since := "2024-09-11")] abbrev div_eq_ediv := @tdiv_eq_ediv
-@[deprecated fdiv_eq_tdiv (since := "2024-09-11")] abbrev fdiv_eq_div := @fdiv_eq_tdiv
-@[deprecated zero_tmod (since := "2024-09-11")] abbrev zero_mod := @zero_tmod
-@[deprecated tmod_zero (since := "2024-09-11")] abbrev mod_zero := @tmod_zero
-@[deprecated tmod_add_tdiv (since := "2024-09-11")] abbrev mod_add_div := @tmod_add_tdiv
-@[deprecated tdiv_add_tmod (since := "2024-09-11")] abbrev div_add_mod := @tdiv_add_tmod
-@[deprecated tmod_add_tdiv' (since := "2024-09-11")] abbrev mod_add_div' := @tmod_add_tdiv'
-@[deprecated tdiv_add_tmod' (since := "2024-09-11")] abbrev div_add_mod' := @tdiv_add_tmod'
-@[deprecated tmod_def (since := "2024-09-11")] abbrev mod_def := @tmod_def
-@[deprecated tmod_eq_emod (since := "2024-09-11")] abbrev mod_eq_emod := @tmod_eq_emod
-@[deprecated fmod_eq_tmod (since := "2024-09-11")] abbrev fmod_eq_mod := @fmod_eq_tmod
-@[deprecated Int.tdiv_one (since := "2024-09-11")] protected abbrev div_one := @Int.tdiv_one
-@[deprecated Int.tdiv_neg (since := "2024-09-11")] protected abbrev div_neg := @Int.tdiv_neg
-@[deprecated Int.neg_tdiv (since := "2024-09-11")] protected abbrev neg_div := @Int.neg_tdiv
-@[deprecated Int.neg_tdiv_neg (since := "2024-09-11")] protected abbrev neg_div_neg := @Int.neg_tdiv_neg
-@[deprecated Int.tdiv_nonneg (since := "2024-09-11")] protected abbrev div_nonneg := @Int.tdiv_nonneg
-@[deprecated Int.tdiv_nonpos (since := "2024-09-11")] protected abbrev div_nonpos := @Int.tdiv_nonpos
-@[deprecated Int.tdiv_eq_zero_of_lt (since := "2024-09-11")] abbrev div_eq_zero_of_lt := @Int.tdiv_eq_zero_of_lt
-@[deprecated Int.mul_tdiv_cancel (since := "2024-09-11")] protected abbrev mul_div_cancel := @Int.mul_tdiv_cancel
-@[deprecated Int.mul_tdiv_cancel_left (since := "2024-09-11")] protected abbrev mul_div_cancel_left := @Int.mul_tdiv_cancel_left
-@[deprecated Int.tdiv_self (since := "2024-09-11")] protected abbrev div_self := @Int.tdiv_self
-@[deprecated Int.mul_tdiv_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev mul_div_cancel_of_mod_eq_zero := @Int.mul_tdiv_cancel_of_tmod_eq_zero
-@[deprecated Int.tdiv_mul_cancel_of_tmod_eq_zero (since := "2024-09-11")] abbrev div_mul_cancel_of_mod_eq_zero := @Int.tdiv_mul_cancel_of_tmod_eq_zero
-@[deprecated Int.dvd_of_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_of_mod_eq_zero := @Int.dvd_of_tmod_eq_zero
-@[deprecated Int.mul_tdiv_assoc (since := "2024-09-11")] protected abbrev mul_div_assoc := @Int.mul_tdiv_assoc
-@[deprecated Int.mul_tdiv_assoc' (since := "2024-09-11")] protected abbrev mul_div_assoc' := @Int.mul_tdiv_assoc'
-@[deprecated Int.tdiv_dvd_tdiv (since := "2024-09-11")] abbrev div_dvd_div := @Int.tdiv_dvd_tdiv
-@[deprecated Int.natAbs_tdiv (since := "2024-09-11")] abbrev natAbs_div := @Int.natAbs_tdiv
-@[deprecated Int.tdiv_eq_of_eq_mul_right (since := "2024-09-11")] protected abbrev div_eq_of_eq_mul_right := @Int.tdiv_eq_of_eq_mul_right
-@[deprecated Int.eq_tdiv_of_mul_eq_right (since := "2024-09-11")] protected abbrev eq_div_of_mul_eq_right := @Int.eq_tdiv_of_mul_eq_right
-@[deprecated Int.ofNat_tmod (since := "2024-09-11")] abbrev ofNat_mod := @Int.ofNat_tmod
-@[deprecated Int.tmod_one (since := "2024-09-11")] abbrev mod_one := @Int.tmod_one
-@[deprecated Int.tmod_eq_of_lt (since := "2024-09-11")] abbrev mod_eq_of_lt := @Int.tmod_eq_of_lt
-@[deprecated Int.tmod_lt_of_pos (since := "2024-09-11")] abbrev mod_lt_of_pos := @Int.tmod_lt_of_pos
-@[deprecated Int.tmod_nonneg (since := "2024-09-11")] abbrev mod_nonneg := @Int.tmod_nonneg
-@[deprecated Int.tmod_neg (since := "2024-09-11")] abbrev mod_neg := @Int.tmod_neg
-@[deprecated Int.mul_tmod_left (since := "2024-09-11")] abbrev mul_mod_left := @Int.mul_tmod_left
-@[deprecated Int.mul_tmod_right (since := "2024-09-11")] abbrev mul_mod_right := @Int.mul_tmod_right
-@[deprecated Int.tmod_eq_zero_of_dvd (since := "2024-09-11")] abbrev mod_eq_zero_of_dvd := @Int.tmod_eq_zero_of_dvd
-@[deprecated Int.dvd_iff_tmod_eq_zero (since := "2024-09-11")] abbrev dvd_iff_mod_eq_zero := @Int.dvd_iff_tmod_eq_zero
-@[deprecated Int.neg_mul_tmod_right (since := "2024-09-11")] abbrev neg_mul_mod_right := @Int.neg_mul_tmod_right
-@[deprecated Int.neg_mul_tmod_left (since := "2024-09-11")] abbrev neg_mul_mod_left := @Int.neg_mul_tmod_left
-@[deprecated Int.tdiv_mul_cancel (since := "2024-09-11")] protected abbrev div_mul_cancel := @Int.tdiv_mul_cancel
-@[deprecated Int.mul_tdiv_cancel' (since := "2024-09-11")] protected abbrev mul_div_cancel' := @Int.mul_tdiv_cancel'
-@[deprecated Int.eq_mul_of_tdiv_eq_right (since := "2024-09-11")] protected abbrev eq_mul_of_div_eq_right := @Int.eq_mul_of_tdiv_eq_right
-@[deprecated Int.tmod_self (since := "2024-09-11")] abbrev mod_self := @Int.tmod_self
-@[deprecated Int.neg_tmod_self (since := "2024-09-11")] abbrev neg_mod_self := @Int.neg_tmod_self
-@[deprecated Int.lt_tdiv_add_one_mul_self (since := "2024-09-11")] abbrev lt_div_add_one_mul_self := @Int.lt_tdiv_add_one_mul_self
-@[deprecated Int.tdiv_eq_iff_eq_mul_right (since := "2024-09-11")] protected abbrev div_eq_iff_eq_mul_right := @Int.tdiv_eq_iff_eq_mul_right
-@[deprecated Int.tdiv_eq_iff_eq_mul_left (since := "2024-09-11")] protected abbrev div_eq_iff_eq_mul_left := @Int.tdiv_eq_iff_eq_mul_left
-@[deprecated Int.eq_mul_of_tdiv_eq_left (since := "2024-09-11")] protected abbrev eq_mul_of_div_eq_left := @Int.eq_mul_of_tdiv_eq_left
-@[deprecated Int.tdiv_eq_of_eq_mul_left (since := "2024-09-11")] protected abbrev div_eq_of_eq_mul_left := @Int.tdiv_eq_of_eq_mul_left
-@[deprecated Int.eq_zero_of_tdiv_eq_zero (since := "2024-09-11")] protected abbrev eq_zero_of_div_eq_zero := @Int.eq_zero_of_tdiv_eq_zero
-@[deprecated Int.tdiv_left_inj (since := "2024-09-11")] protected abbrev div_left_inj := @Int.tdiv_left_inj
-@[deprecated Int.tdiv_sign (since := "2024-09-11")] abbrev div_sign := @Int.tdiv_sign
-@[deprecated Int.sign_eq_tdiv_abs (since := "2024-09-11")] protected abbrev sign_eq_div_abs := @Int.sign_eq_tdiv_abs
-@[deprecated Int.tdiv_eq_ediv_of_dvd (since := "2024-09-11")] abbrev div_eq_ediv_of_dvd := @Int.tdiv_eq_ediv_of_dvd

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -71,8 +71,8 @@ builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMu
 builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
 builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
-builtin_dsimproc [simp, seval] reduceTDiv (tdiv  _ _) := reduceBin ``Int.div 2 Int.tdiv
-builtin_dsimproc [simp, seval] reduceTMod (tmod  _ _) := reduceBin ``Int.mod 2 Int.tmod
+builtin_dsimproc [simp, seval] reduceTDiv (tdiv  _ _) := reduceBin ``Int.tdiv 2 Int.tdiv
+builtin_dsimproc [simp, seval] reduceTMod (tmod  _ _) := reduceBin ``Int.tmod 2 Int.tmod
 builtin_dsimproc [simp, seval] reduceFDiv (fdiv _ _) := reduceBin ``Int.fdiv 2 Int.fdiv
 builtin_dsimproc [simp, seval] reduceFMod (fmod _ _) := reduceBin ``Int.fmod 2 Int.fmod
 builtin_dsimproc [simp, seval] reduceBdiv (bdiv _ _) := reduceBinIntNatOp ``bdiv bdiv

tests/bench/liasolver.lean

@@ -170,7 +170,7 @@ namespace Equation
     let (i, c) := e.coeffs.getAny?.get!
     return { e with
       coeffs := e.coeffs.insert i 1
-      const := Int.div e.const c }
+      const := Int.ediv e.const c }
 
   def invert (e : Equation) : Equation :=
     { e with

tests/lean/307.lean

@@ -7,81 +7,61 @@ def INT32_MIN : Int := -0x80000000
 #reduce INT32_MIN % -1
 #eval INT32_MIN % -1
 
-#reduce (Int.mod (-2 : Int) 0)
-#eval (Int.mod (-2 : Int) 0)
+#reduce (Int.emod (-2 : Int) 0)
+#eval (Int.emod (-2 : Int) 0)
 
-#reduce -(Int.mod (-2 : Int) 0)
-#eval -(Int.mod (-2 : Int) 0)
+#reduce -(Int.emod (-2 : Int) 0)
+#eval -(Int.emod (-2 : Int) 0)
 
 @[noinline] def oneU8 : UInt8 := 1
 
 #reduce (UInt8.mod oneU8 0).val.val
 #eval (UInt8.mod oneU8 0)
 
-#reduce (UInt8.modn oneU8 0).val.val
-#eval (UInt8.modn oneU8 0)
+#reduce (UInt8.mod oneU8 0).val.val
+#eval (UInt8.mod oneU8 0)
 
-@[noinline] def int_div x y := Int.div x y
-@[noinline] def int_mod x y := Int.mod x y
+@[noinline] def int_div x y := Int.ediv x y
+@[noinline] def int_mod x y := Int.emod x y
 @[noinline] def uint8_mod x y := UInt8.mod x y
-@[noinline] def uint8_modn x y := UInt8.modn x y
 
 @[noinline] def oneU16 : UInt16 := 1
 
 #reduce (UInt16.mod oneU16 0).val.val
 #eval (UInt16.mod oneU16 0)
 
-#reduce (UInt16.modn oneU16 0).val.val
-#eval (UInt16.modn oneU16 0)
-
 @[noinline] def uint16_mod x y := UInt16.mod x y
-@[noinline] def uint16_modn x y := UInt16.modn x y
 
 @[noinline] def oneU32 : UInt32 := 1
 
 #reduce (UInt32.mod oneU32 0).val.val
 #eval (UInt32.mod oneU32 0)
 
-#reduce (UInt32.modn oneU32 0).val.val
-#eval (UInt32.modn oneU32 0)
-
 @[noinline] def uint32_mod x y := UInt32.mod x y
-@[noinline] def uint32_modn x y := UInt32.modn x y
 
 
 @[noinline] def oneU64 : UInt64 := 1
 
 #reduce (UInt64.mod oneU64 0).val.val
 #eval (UInt64.mod oneU64 0)
 
-#reduce (UInt64.modn oneU64 0).val.val
-#eval (UInt64.modn oneU64 0)
-
 @[noinline] def uint64_mod x y := UInt64.mod x y
-@[noinline] def uint64_modn x y := UInt64.modn x y
 
 @[noinline] def oneUSize : USize := 1
 
 #eval (USize.mod oneUSize 0)
-#eval (USize.modn oneUSize 0)
 
 @[noinline] def usize_mod x y := USize.mod x y
-@[noinline] def usize_modn x y := USize.modn x y
 
 def main : IO Unit := do
   IO.println <| int_div INT32_MIN (-1)
   IO.println <| int_div (-2) 0
   IO.println <| int_mod INT32_MIN (-1)
   IO.println <| int_mod (-2) 0
   IO.println <| uint8_mod 1 0
-  IO.println <| uint8_modn 1 0
   IO.println <| uint16_mod 1 0
-  IO.println <| uint16_modn 1 0
   IO.println <| uint32_mod 1 0
-  IO.println <| uint32_modn 1 0
   IO.println <| uint64_mod 1 0
-  IO.println <| uint64_modn 1 0
   IO.println <| usize_mod 1 0
-  IO.println <| usize_modn 1 0
 
 #eval main

tests/lean/307.lean.expected.out

@@ -19,13 +19,6 @@ Int.ofNat 2
 1
 1
 1
-1
-1
-1
-1
-1
-1
-1
 2147483648
 0
 0
@@ -35,8 +28,3 @@ Int.ofNat 2
 1
 1
 1
-1
-1
-1
-1
-1

tests/lean/matchOfNatIssue.lean

@@ -1,13 +1,13 @@
-example (x : Int) (h : x = 2) : Int.div 2 1 = x := by
-  simp [Int.div]
+example (x : Int) (h : x = 2) : Int.ediv 2 1 = x := by
+  simp [Int.ediv]
   trace_state
   simp (config := { decide := true }) [h]
 
-example (n : Nat) : Int.div (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n / 0) := by
-  simp [Int.div]
+example (n : Nat) : Int.ediv (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n / 0) := by
+  simp [Int.ediv]
 
-example (n : Nat) : Int.div (Int.ofNat n) 0 = Int.ofNat (n / 0) := by
-  simp [Int.div]
+example (n : Nat) : Int.ediv (Int.ofNat n) 0 = Int.ofNat (n / 0) := by
+  simp [Int.ediv]
 
 example (n : Nat) : Int.mul (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n * 0) := by
   simp [Int.mul]