feat: add a FloorSemiring instance to NNRat (#13548)

Also some missing `norm_cast` lemmas for inequalities of casts between different types.

Mathlib.lean

@@ -2396,6 +2396,7 @@ import Mathlib.Data.Multiset.Sum
 import Mathlib.Data.Multiset.Sym
 import Mathlib.Data.NNRat.BigOperators
 import Mathlib.Data.NNRat.Defs
+import Mathlib.Data.NNRat.Floor
 import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Data.NNRat.Order
 import Mathlib.Data.NNReal.Basic

Mathlib/Data/NNRat/Defs.lean

@@ -106,8 +106,12 @@ theorem coe_nonneg (q : ℚ≥0) : (0 : ℚ) ≤ q :=
   q.2
 
 @[simp, norm_cast] lemma coe_zero : ((0 : ℚ≥0) : ℚ) = 0 := rfl
+@[simp] lemma num_zero : num 0 = 0 := rfl
+@[simp] lemma den_zero : den 0 = 1 := rfl
 
 @[simp, norm_cast] lemma coe_one : ((1 : ℚ≥0) : ℚ) = 1 := rfl
+@[simp] lemma num_one : num 1 = 1 := rfl
+@[simp] lemma den_one : den 1 = 1 := rfl
 
 @[simp, norm_cast]
 theorem coe_add (p q : ℚ≥0) : ((p + q : ℚ≥0) : ℚ) = p + q :=

Mathlib/Data/NNRat/Floor.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Data.Rat.Floor
+
+/-!
+# Floor Function for Non-negative Rational Numbers
+
+## Summary
+
+We define the `FloorSemiring` instance on `ℚ≥0`, and relate its operators to `NNRat.cast`.
+
+Note that we cannot talk about `Int.fract`, which currently only works for rings.
+
+## Tags
+
+nnrat, rationals, ℚ≥0, floor
+-/
+
+namespace NNRat
+
+instance : FloorSemiring ℚ≥0 where
+  floor q := ⌊q.val⌋₊
+  ceil q := ⌈q.val⌉₊
+  floor_of_neg h := by simpa using h.trans zero_lt_one
+  gc_floor {a n} h := by rw [← NNRat.coe_le_coe, Nat.le_floor_iff] <;> norm_cast
+  gc_ceil {a b} := by rw [← NNRat.coe_le_coe, Nat.ceil_le]; norm_cast
+
+@[simp, norm_cast]
+theorem floor_coe (q : ℚ≥0) : ⌊(q : ℚ)⌋₊ = ⌊q⌋₊ := rfl
+
+@[simp, norm_cast]
+theorem ceil_coe (q : ℚ≥0) : ⌈(q : ℚ)⌉₊ = ⌈q⌉₊ := rfl
+
+@[simp, norm_cast]
+theorem coe_floor (q : ℚ≥0) : ↑⌊q⌋₊ = ⌊(q : ℚ)⌋ := Int.ofNat_floor_eq_floor q.coe_nonneg
+
+@[simp, norm_cast]
+theorem coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈(q : ℚ)⌉ := Int.ofNat_ceil_eq_ceil q.coe_nonneg
+
+protected theorem floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den := by
+  rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def, Int.ofNat_ediv, den_coe, num_coe]
+
+section Semifield
+
+variable {K} [LinearOrderedSemifield K] [FloorSemiring K]
+
+@[simp, norm_cast]
+theorem floor_cast (x : ℚ≥0) : ⌊(x : K)⌋₊ = ⌊x⌋₊ :=
+  (Nat.floor_eq_iff x.cast_nonneg).2 (mod_cast (Nat.floor_eq_iff x.cast_nonneg).1 (Eq.refl ⌊x⌋₊))
+
+@[simp, norm_cast]
+theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ := by
+  obtain rfl | hx := eq_or_ne x 0
+  · simp
+  · refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa
+
+end Semifield
+
+section Field
+
+variable {K} [LinearOrderedField K] [FloorRing K]
+
+@[simp, norm_cast]
+theorem intFloor_cast (x : ℚ≥0) : ⌊(x : K)⌋ = ⌊(x : ℚ)⌋ := by
+  rw [Int.floor_eq_iff (α := K), ← coe_floor]
+  norm_cast
+  norm_cast
+  rw [Nat.cast_add_one, ← Nat.floor_eq_iff (zero_le _)]
+
+@[simp, norm_cast]
+theorem intCeil_cast (x : ℚ≥0) : ⌈(x : K)⌉ = ⌈(x : ℚ)⌉ := by
+  rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
+  constructor
+  · have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x
+    rw [NNRat.cast_add, NNRat.cast_one] at this
+    refine Eq.trans_lt ?_ this
+    norm_cast
+  · rw [Int.cast_natCast, NNRat.cast_le_natCast]
+    exact Nat.le_ceil _
+
+end Field
+
+@[norm_cast]
+theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ≥0)⌋₊ = n / d :=
+  Rat.natFloor_natCast_div_natCast n d
+
+end NNRat

Mathlib/Data/Rat/Cast/Order.lean

@@ -54,6 +54,38 @@ def castOrderEmbedding : ℚ ↪o K :=
 
 @[simp] lemma cast_lt_zero : (q : K) < 0 ↔ q < 0 := by norm_cast
 
+@[simp, norm_cast]
+theorem cast_le_natCast {m : ℚ} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_le_cast {m : ℕ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem cast_le_intCast {m : ℚ} {n : ℤ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by
+  rw [← cast_le (K := K), cast_intCast]
+
+@[simp, norm_cast]
+theorem intCast_le_cast {m : ℤ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n := by
+  rw [← cast_le (K := K), cast_intCast]
+
+@[simp, norm_cast]
+theorem cast_lt_natCast {m : ℚ} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ) := by
+  rw [← cast_lt (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_lt_cast {m : ℕ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n := by
+  rw [← cast_lt (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem cast_lt_intCast {m : ℚ} {n : ℤ} : (m : K) < n ↔ m < (n : ℚ) := by
+  rw [← cast_lt (K := K), cast_intCast]
+
+@[simp, norm_cast]
+theorem intCast_lt_cast {m : ℤ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n := by
+  rw [← cast_lt (K := K), cast_intCast]
+
 @[simp, norm_cast]
 lemma cast_min (p q : ℚ) : (↑(min p q) : K) = min (p : K) (q : K) := (@cast_mono K _).map_min
 
@@ -154,6 +186,22 @@ variable {n : ℕ} [n.AtLeastTwo]
 
 end ofNat
 
+@[simp, norm_cast]
+theorem cast_le_natCast {m : ℚ≥0} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ≥0) := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_le_cast {m : ℕ} {n : ℚ≥0} : (m : K) ≤ n ↔ (m : ℚ≥0) ≤ n := by
+  rw [← cast_le (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem cast_lt_natCast {m : ℚ≥0} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ≥0) := by
+  rw [← cast_lt (K := K), cast_natCast]
+
+@[simp, norm_cast]
+theorem natCast_lt_cast {m : ℕ} {n : ℚ≥0} : (m : K) < n ↔ (m : ℚ≥0) < n := by
+  rw [← cast_lt (K := K), cast_natCast]
+
 @[simp, norm_cast] lemma cast_min (p q : ℚ≥0) : (↑(min p q) : K) = min (p : K) (q : K) :=
   (@cast_mono K _).map_min
 

Mathlib/Data/Rat/Floor.lean

@@ -49,7 +49,8 @@ instance : FloorRing ℚ :=
 
 protected theorem floor_def {q : ℚ} : ⌊q⌋ = q.num / q.den := Rat.floor_def' q
 
-theorem floor_int_div_nat_eq_div (n : ℤ) (d : ℕ) : ⌊(↑n : ℚ) / (↑d : ℚ)⌋ = n / (↑d : ℤ) := by
+@[norm_cast]
+theorem floor_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / (↑d : ℤ) := by
   rw [Rat.floor_def]
   obtain rfl | hd := @eq_zero_or_pos _ _ d
   · simp
@@ -61,6 +62,18 @@ theorem floor_int_div_nat_eq_div (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 floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / d :=
+  floor_intCast_div_natCast n d
+
+@[norm_cast]
+theorem natFloor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋₊ = n / d := by
+  rw [← Int.ofNat_inj, Int.ofNat_floor_eq_floor (by positivity)]
+  push_cast
+  exact floor_intCast_div_natCast n d
+
+@[deprecated (since := "2024-07-23")] alias floor_int_div_nat_eq_div := floor_intCast_div_natCast
+
 @[simp, norm_cast]
 theorem floor_cast (x : ℚ) : ⌊(x : α)⌋ = ⌊x⌋ :=
   floor_eq_iff.2 (mod_cast floor_eq_iff.1 (Eq.refl ⌊x⌋))
@@ -93,7 +106,7 @@ theorem isInt_intFloor_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
   rintro ⟨inv, rfl⟩
   constructor
   simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
-  rw [← floor_int_div_nat_eq_div n d, ← floor_cast (α := α), Rat.cast_div,
+  rw [← floor_intCast_div_natCast n d, ← floor_cast (α := α), Rat.cast_div,
     cast_intCast, cast_natCast]
 
 /-- `norm_num` extension for `Int.floor` -/
@@ -123,7 +136,7 @@ end NormNum
 end Rat
 
 theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} : n % d = n - d * ⌊(n : ℚ) / d⌋ := by
-  rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_int_div_nat_eq_div]
+  rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_intCast_div_natCast]
 
 theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.Coprime d) :
     ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.Coprime d := by