feat: norm_num for Int.ceil (#19669)

Long ago I tried writing this in leanprover-community/mathlib3#16502 for Lean 3.

Mathlib/Data/Rat/Floor.lean

@@ -50,6 +50,11 @@ instance : FloorRing ℚ :=
 
 protected theorem floor_def {q : ℚ} : ⌊q⌋ = q.num / q.den := Rat.floor_def' q
 
+protected theorem ceil_def (q : ℚ) : ⌈q⌉ = -(-q.num / ↑q.den) := by
+  change -⌊-q⌋ = _
+  rw [Rat.floor_def, num_neg_eq_neg_num, den_neg_eq_den]
+
+
 @[norm_cast]
 theorem floor_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / (↑d : ℤ) := by
   rw [Rat.floor_def]
@@ -63,10 +68,19 @@ theorem floor_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌊(↑n / ↑d : ℚ)
   refine (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left ?_ <| Int.natCast_nonneg q.den).symm
   rwa [← d_eq_c_mul_denom, Int.natCast_pos]
 
+@[norm_cast]
+theorem ceil_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / (↑d : ℤ)) := by
+  conv_lhs => rw [← neg_neg ⌈_⌉, ← floor_neg]
+  rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]
+
 @[norm_cast]
 theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / d :=
   floor_intCast_div_natCast n d
 
+@[norm_cast]
+theorem ceil_natCast_div_natCast (n d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / d) :=
+  ceil_intCast_div_natCast n d
+
 @[norm_cast]
 theorem natFloor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋₊ = n / d := by
   rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]
@@ -128,10 +142,46 @@ def evalIntFloor : NormNumExt where eval {u αZ} e := do
       let _i ← synthInstanceQ q(LinearOrderedField $α)
       assertInstancesCommute
       have z : Q(ℤ) := mkRawIntLit ⌊q⌋
-      letI : $z =Q ⌊$n / $d⌋ := ⟨⟩
+      letI : $z =Q $n / $d := ⟨⟩
       return .isInt q(inferInstance) z ⌊q⌋ q(isInt_intFloor_ofIsRat _ $n $d $h)
   | _, _, _ => failure
 
+theorem isNat_intCeil {R} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℕ) :
+    IsNat r m → IsNat ⌈r⌉ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩
+
+theorem isInt_intCeil {R} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℤ) :
+    IsInt r m → IsInt ⌈r⌉ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩
+
+theorem isInt_intCeil_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
+    IsRat r n d → IsInt ⌈r⌉ (-(-n / d)) := by
+  rintro ⟨inv, rfl⟩
+  constructor
+  simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
+  rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div,
+    cast_intCast, cast_natCast]
+
+/-- `norm_num` extension for `Int.ceil` -/
+@[norm_num ⌈_⌉]
+def evalIntCeil : NormNumExt where eval {u αZ} e := do
+  match u, αZ, e with
+  | 0, ~q(ℤ), ~q(@Int.ceil $α $instR $instF $x) =>
+    match ← derive x with
+    | .isBool .. => failure
+    | .isNat _ _ pb => do
+      assertInstancesCommute
+      return .isNat q(inferInstance) _ q(isNat_intCeil $x _ $pb)
+    | .isNegNat _ _ pb => do
+      assertInstancesCommute
+      -- ceil always keeps naturals negative, so we can shortcut `.isInt`
+      return .isNegNat q(inferInstance) _ q(isInt_intCeil _ _ $pb)
+    | .isRat _ q n d h => do
+      let _i ← synthInstanceQ q(LinearOrderedField $α)
+      assertInstancesCommute
+      have z : Q(ℤ) := mkRawIntLit ⌈q⌉
+      letI : $z =Q (-(-$n / $d)) := ⟨⟩
+      return .isInt q(inferInstance) z ⌈q⌉ q(isInt_intCeil_ofIsRat _ $n $d $h)
+  | _, _, _ => failure
+
 end NormNum
 
 end Rat

MathlibTest/norm_num_ext.lean

@@ -10,6 +10,7 @@ import Mathlib.Tactic.NormNum.DivMod
 import Mathlib.Tactic.NormNum.NatFib
 import Mathlib.Tactic.NormNum.NatSqrt
 import Mathlib.Tactic.NormNum.Prime
+import Mathlib.Data.Rat.Floor
 import Mathlib.Tactic.NormNum.LegendreSymbol
 import Mathlib.Tactic.NormNum.Pow
 
@@ -400,6 +401,11 @@ example : ⌊(2 : R)⌋ = 2 := by norm_num
 example : ⌊(15 / 16 : K)⌋ + 1 = 1 := by norm_num
 example : ⌊(-15 / 16 : K)⌋ + 1 = 0 := by norm_num
 
+example : ⌈(-1 : R)⌉ = -1 := by norm_num
+example : ⌈(2 : R)⌉ = 2 := by norm_num
+example : ⌈(15 / 16 : K)⌉ + 1 = 2 := by norm_num
+example : ⌈(-15 / 16 : K)⌉ + 1 = 1 := by norm_num
+
 end floor
 
 section jacobi