working

Mathlib/Data/Rat/Floor.lean

@@ -68,16 +68,46 @@ 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)]
   push_cast
   exact floor_intCast_div_natCast n d
 
+theorem _root_.Int.sign_eq_abs_ediv (b : ℤ) : b.sign = |b| / b := by
+  obtain rfl | hbz := Decidable.eq_or_ne b 0
+  · simp
+  obtain ⟨hb', hb⟩ | ⟨hb', hb⟩ := abs_cases b <;> rw [hb']
+  · replace hb := lt_of_le_of_ne' hb hbz
+    rw [Int.ediv_self hbz, Int.sign_eq_one_of_pos hb]
+  · rw [Int.sign_eq_neg_one_of_neg hb, Int.ediv_eq_of_eq_mul_left hbz]
+    rw [neg_one_mul]
+
+/-- Like `Int.ediv_emod_unique`, but permitting negative `b`. -/
+theorem _root_.Int.ediv_emod_unique' {a b r q : Int} (h : b ≠ 0) :
+  a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b| := by
+  constructor
+  · intro ⟨rfl, rfl⟩
+    exact ⟨emod_add_ediv a b, emod_nonneg _ h, emod_lt _ h⟩
+  · intro ⟨rfl, hz, hb⟩
+    constructor
+    · rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]
+      simp [Int.zero_add]
+    · rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]
+
 @[deprecated (since := "2024-07-23")] alias floor_int_div_nat_eq_div := floor_intCast_div_natCast
 
 @[simp, norm_cast]
@@ -148,7 +178,7 @@ theorem isInt_intCeil_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
   rintro ⟨inv, rfl⟩
   constructor
   simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
-  rw [← floor_intCast_div_natCast n d, ← floor_cast (α := α), Rat.cast_div,
+  rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div,
     cast_intCast, cast_natCast]
 
 /-- `norm_num` extension for `Int.ceil` -/
@@ -168,9 +198,9 @@ def evalIntCeil : NormNumExt where eval {u αZ} e := do
     | .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)
+      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

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