chore rename Int.div/mod to tdiv/tmod

src/Init/Data/Int/DivMod.lean

@@ -16,83 +16,99 @@ There are three main conventions for integer division,
 referred here as the E, F, T rounding conventions.
 All three pairs satisfy the identity `x % y + (x / y) * y = x` unconditionally,
 and satisfy `x / 0 = 0` and `x % 0 = x`.
+
+### Historical notes
+In early versions of Lean, the typeclasses provided by `/` and `%`
+were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
+
+However we decided it was better to use `ediv` and `emod`,
+as they are consistent with the conventions used in SMTLib, Mathlib,
+and often mathematical reasoning is easier with these conventions.
+
+At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
+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.
 -/
 
 /-! ### T-rounding division -/
 
 /--
-`div` uses the [*"T-rounding"*][t-rounding]
+`tdiv` uses the [*"T-rounding"*][t-rounding]
 (**T**runcation-rounding) convention, meaning that it rounds toward
 zero. Also note that division by zero is defined to equal zero.
 
   The relation between integer division and modulo is found in
-  `Int.mod_add_div` which states that
-  `a % b + b * (a / b) = a`, unconditionally.
+  `Int.tmod_add_tdiv` which states that
+  `tmod a b + b * (tdiv a b) = a`, unconditionally.
 
-  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862 [theo
-  mod_add_div]:
-  https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+  [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
 
   Examples:
 
   ```
-  #eval (7 : Int).div (0 : Int) -- 0
-  #eval (0 : Int).div (7 : Int) -- 0
-
-  #eval (12 : Int).div (6 : Int) -- 2
-  #eval (12 : Int).div (-6 : Int) -- -2
-  #eval (-12 : Int).div (6 : Int) -- -2
-  #eval (-12 : Int).div (-6 : Int) -- 2
-
-  #eval (12 : Int).div (7 : Int) -- 1
-  #eval (12 : Int).div (-7 : Int) -- -1
-  #eval (-12 : Int).div (7 : Int) -- -1
-  #eval (-12 : Int).div (-7 : Int) -- 1
+  #eval (7 : Int).tdiv (0 : Int) -- 0
+  #eval (0 : Int).tdiv (7 : Int) -- 0
+
+  #eval (12 : Int).tdiv (6 : Int) -- 2
+  #eval (12 : Int).tdiv (-6 : Int) -- -2
+  #eval (-12 : Int).tdiv (6 : Int) -- -2
+  #eval (-12 : Int).tdiv (-6 : Int) -- 2
+
+  #eval (12 : Int).tdiv (7 : Int) -- 1
+  #eval (12 : Int).tdiv (-7 : Int) -- -1
+  #eval (-12 : Int).tdiv (7 : Int) -- -1
+  #eval (-12 : Int).tdiv (-7 : Int) -- 1
   ```
 
   Implemented by efficient native code.
 -/
 @[extern "lean_int_div"]
-def div : (@& Int) → (@& Int) → Int
+def tdiv : (@& Int) → (@& Int) → Int
   | ofNat m, ofNat n =>  ofNat (m / n)
   | ofNat m, -[n +1] => -ofNat (m / succ n)
   | -[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.div`, meaning that `a % b + b * (a / b) = a`
-  unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
+  to pair with `Int.tdiv`, meaning that `tmod a b + b * (tdiv a b) = a`
+  unconditionally (see [`Int.tmod_add_tdiv`][theo tmod_add_tdiv]). In
   particular, `a % 0 = a`.
 
   [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
-  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+  [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
 
   Examples:
 
   ```
-  #eval (7 : Int).mod (0 : Int) -- 7
-  #eval (0 : Int).mod (7 : Int) -- 0
-
-  #eval (12 : Int).mod (6 : Int) -- 0
-  #eval (12 : Int).mod (-6 : Int) -- 0
-  #eval (-12 : Int).mod (6 : Int) -- 0
-  #eval (-12 : Int).mod (-6 : Int) -- 0
-
-  #eval (12 : Int).mod (7 : Int) -- 5
-  #eval (12 : Int).mod (-7 : Int) -- 5
-  #eval (-12 : Int).mod (7 : Int) -- -5
-  #eval (-12 : Int).mod (-7 : Int) -- -5
+  #eval (7 : Int).tmod (0 : Int) -- 7
+  #eval (0 : Int).tmod (7 : Int) -- 0
+
+  #eval (12 : Int).tmod (6 : Int) -- 0
+  #eval (12 : Int).tmod (-6 : Int) -- 0
+  #eval (-12 : Int).tmod (6 : Int) -- 0
+  #eval (-12 : Int).tmod (-6 : Int) -- 0
+
+  #eval (12 : Int).tmod (7 : Int) -- 5
+  #eval (12 : Int).tmod (-7 : Int) -- 5
+  #eval (-12 : Int).tmod (7 : Int) -- -5
+  #eval (-12 : Int).tmod (-7 : Int) -- -5
   ```
 
   Implemented by efficient native code. -/
 @[extern "lean_int_mod"]
-def mod : (@& Int) → (@& Int) → Int
+def tmod : (@& Int) → (@& Int) → Int
   | ofNat m, ofNat n =>  ofNat (m % n)
   | ofNat m, -[n +1] =>  ofNat (m % succ n)
   | -[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)`.
 -/
@@ -233,7 +249,9 @@ instance : Mod Int where
 
 @[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
-theorem ofNat_div (m n : Nat) : ↑(m / n) = div ↑m ↑n := rfl
+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]