Skip to content

feat: weaken assumptions on lemmas about FloorRing #37582

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mortarsanjaya wants to merge 1 commit into
base: master
Choose a base branch
from
+31 −35
Open

feat: weaken assumptions on lemmas about FloorRing #37582

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions Mathlib/Algebra/Order/Floor/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ instance : FloorRing ℤ where

/-- A `FloorRing` constructor from the `floor` function alone. -/
@[implicit_reducible]
def FloorRing.ofFloor (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (floor : α → ℤ)
def FloorRing.ofFloor (α) [Ring α] [LinearOrder α] [IsOrderedRing α] (floor : α → ℤ)
(gc_coe_floor : GaloisConnection (↑) floor) : FloorRing α :=
{ floor
ceil := fun a => -floor (-a)
Expand All @@ -179,7 +179,7 @@ def FloorRing.ofFloor (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (

/-- A `FloorRing` constructor from the `ceil` function alone. -/
@[implicit_reducible]
def FloorRing.ofCeil (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (ceil : α → ℤ)
def FloorRing.ofCeil (α) [Ring α] [LinearOrder α] [IsOrderedRing α] (ceil : α → ℤ)
(gc_ceil_coe : GaloisConnection ceil (↑)) : FloorRing α :=
{ floor := fun a => -ceil (-a)
ceil
Expand Down Expand Up @@ -286,7 +286,7 @@ theorem floor_le (a : α) : (⌊a⌋ : α) ≤ a :=
theorem floor_nonneg : 0 ≤ ⌊a⌋ ↔ 0 ≤ a := by rw [le_floor, Int.cast_zero]

@[bound]
theorem floor_nonpos [IsStrictOrderedRing α] (ha : a ≤ 0) : ⌊a⌋ ≤ 0 := by
theorem floor_nonpos [IsOrderedRing α] (ha : a ≤ 0) : ⌊a⌋ ≤ 0 := by
rw [← @cast_le α, Int.cast_zero]
exact (floor_le a).trans ha

Expand All @@ -306,7 +306,7 @@ theorem le_ceil (a : α) : a ≤ ⌈a⌉ :=
gc_ceil_coe.le_u_l a

@[bound]
theorem ceil_nonneg [IsStrictOrderedRing α] (ha : 0 ≤ a) : 0 ≤ ⌈a⌉ := mod_cast ha.trans (le_ceil a)
theorem ceil_nonneg [IsOrderedRing α] (ha : 0 ≤ a) : 0 ≤ ⌈a⌉ := mod_cast ha.trans (le_ceil a)

@[simp]
theorem ceil_pos : 0 < ⌈a⌉ ↔ 0 < a := by rw [lt_ceil, cast_zero]
Expand All @@ -315,7 +315,7 @@ end Int

section FloorRingToSemiring

variable [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α]
variable [Ring α] [LinearOrder α] [IsOrderedRing α] [FloorRing α]

/-! #### A floor ring as a floor semiring -/

Expand Down
47 changes: 22 additions & 25 deletions Mathlib/Algebra/Order/Floor/Ring.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ theorem floor_eq_on_Ico' (n : ℤ) : ∀ a ∈ Set.Ico (n : R) (n + 1), (⌊a⌋
theorem preimage_floor_singleton (m : ℤ) : (floor : R → ℤ) ⁻¹' {m} = Ico (m : R) (m + 1) :=
ext fun _ => floor_eq_iff

variable [IsStrictOrderedRing R]
variable [IsOrderedRing R]

@[simp, bound]
theorem sub_one_lt_floor (a : R) : a - 1 < ⌊a⌋ :=
Expand Down Expand Up @@ -276,21 +276,16 @@ theorem mul_fract_eq_one_iff_exists_int {x : R} {k : R} (hk : 1 < k) :
rw [floor_eq_iff, ← mul_le_mul_iff_right₀ hk0, ← mul_lt_mul_iff_right₀ hk0, hn]
simp [mul_add, hk]

end LinearOrderedRing

section LinearOrderedCommRing
variable {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R}

theorem cast_mul_floor_div_cancel_of_pos {n : ℤ} (hn : 0 < n) (a : R) : ⌊n * a⌋ / n = ⌊a⌋ := by
rw [mul_comm, mul_cast_floor_div_cancel_of_pos hn]
rw [Commute.intCast_left, mul_cast_floor_div_cancel_of_pos hn]

theorem natCast_mul_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : R) : ⌊n * a⌋ / n = ⌊a⌋ := by
rw [mul_comm, mul_natCast_floor_div_cancel hn]
rw [Nat.cast_comm, mul_natCast_floor_div_cancel hn]

end LinearOrderedCommRing
end LinearOrderedRing

section LinearOrderedField
variable {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a b : k}
variable {k : Type*} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k}

theorem floor_div_cast_of_nonneg {n : ℤ} (hn : 0 ≤ n) (a : k) : ⌊a / n⌋ = ⌊a⌋ / n := by
obtain rfl | hn := hn.eq_or_lt
Expand Down Expand Up @@ -332,7 +327,7 @@ theorem fract_sub_self (a : R) : fract a - a = -⌊a⌋ :=
theorem fract_add (a b : R) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by unfold fract; grind⟩

variable [IsStrictOrderedRing R]
variable [IsOrderedRing R]

@[simp]
theorem fract_add_intCast (a : R) (m : ℤ) : fract (a + m) = fract a := by
Expand Down Expand Up @@ -441,8 +436,9 @@ theorem fract_eq_iff {a b : R} : fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z :
exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩,
by
rintro ⟨h₀, h₁, z, hz⟩
rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz,
Int.cast_inj, floor_eq_iff, ← hz]
rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz]
refine congrArg Int.cast ?_
rw [floor_eq_iff, ← hz]
constructor <;> simpa [sub_eq_add_neg, add_assoc] ⟩

theorem fract_eq_fract {a b : R} : fract a = fract b ↔ ∃ z : ℤ, a - b = z :=
Expand Down Expand Up @@ -513,13 +509,13 @@ theorem image_fract (s : Set R) : fract '' s = ⋃ m : ℤ, (fun x : R => x - m)

section LinearOrderedField

variable {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {b : k}
variable {k : Type*} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {b : k}

theorem fract_div_mul_self_mem_Ico (a b : k) (ha : 0 < a) : fract (b / a) * a ∈ Ico 0 a :=
⟨(mul_nonneg_iff_of_pos_right ha).2 (fract_nonneg (b / a)),
(mul_lt_iff_lt_one_left ha).2 (fract_lt_one (b / a))⟩

omit [IsStrictOrderedRing k] in
omit [IsOrderedRing k] in
theorem fract_div_mul_self_add_zsmul_eq (a b : k) (ha : a ≠ 0) :
fract (b / a) * a + ⌊b / a⌋ • a = b := by
rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]
Expand Down Expand Up @@ -619,7 +615,7 @@ theorem ceil_eq_on_Ioc (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, ⌈a⌉ = z
theorem preimage_ceil_singleton (m : ℤ) : (ceil : R → ℤ) ⁻¹' {m} = Ioc ((m : R) - 1) m :=
ext fun _ => ceil_eq_iff

variable [IsStrictOrderedRing R]
variable [IsOrderedRing R]

theorem floor_neg : ⌊-a⌋ = -⌈a⌉ :=
eq_of_forall_le_iff fun z => by rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]
Expand Down Expand Up @@ -713,8 +709,9 @@ theorem ceil_zero : ⌈(0 : R)⌉ = 0 := by rw [← cast_zero, ceil_intCast]
@[simp]
theorem ceil_one : ⌈(1 : R)⌉ = 1 := by rw [← cast_one, ceil_intCast]

theorem ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, (⌈a⌉ : R) = z := fun a ha =>
mod_cast ceil_eq_on_Ioc z a ha
omit [IsOrderedRing R] in
theorem ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, (⌈a⌉ : R) = z :=
fun a ha => congrArg Int.cast (ceil_eq_on_Ioc z a ha)

lemma ceil_eq_self_iff_mem (a : R) : ⌈a⌉ = a ↔ a ∈ Set.range Int.cast := by
aesop
Expand All @@ -729,8 +726,9 @@ theorem floor_lt_ceil_of_lt {a b : R} (h : a < b) : ⌊a⌋ < ⌈b⌉ :=

lemma ceil_eq_floor_add_one_iff_notMem (a : R) : ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast := by
refine ⟨fun h ht => ?_, fun h => ?_⟩
· have := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
linarith [Int.cast_inj.mp this]
· have h0 := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
rw [h, cast_add, cast_one, left_eq_add] at h0
exact one_ne_zero h0
· apply le_antisymm (Int.ceil_le_floor_add_one _)
rw [add_one_le_iff, lt_ceil]
exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))
Expand All @@ -742,9 +740,8 @@ theorem fract_eq_zero_or_add_one_sub_ceil (a : R) : fract a = 0 ∨ fract a = a
suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
rw [this, ← self_sub_fract]
abel
norm_cast
rw [ceil_eq_iff]
refine ⟨?_, _root_.le_of_lt <| by simp⟩
rw [← Int.cast_one, ← Int.cast_add]
refine congrArg Int.cast (ceil_eq_iff.mpr ⟨?_, _root_.le_of_lt <| by simp⟩)
rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
exact ha.symm.lt_of_le (fract_nonneg a)

Expand All @@ -759,7 +756,7 @@ theorem ceil_sub_self_eq (ha : fract a ≠ 0) : (⌈a⌉ : R) - a = 1 - fract a
end ceil

section LinearOrderedField
variable {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a b : k}
variable {k : Type*} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k}

lemma mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉ ≤ a) : b * a < ⌊a⌋ := by
calc
Expand Down Expand Up @@ -889,7 +886,7 @@ end Nat

section FloorRingToSemiring

variable [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
variable [Ring R] [LinearOrder R] [IsOrderedRing R] [FloorRing R]

/-! #### A floor ring as a floor semiring -/

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Order/Floor/Semifield.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ theorem floor_div_eq_div (m n : ℕ) : ⌊(m : K) / n⌋₊ = m / n := by
end LinearOrderedSemifield

section LinearOrderedField
variable [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K}
variable [Field K] [LinearOrder K] [IsOrderedRing K] [FloorSemiring K] {a b : K}

lemma mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉₊ ≤ a) : b * a < ⌊a⌋₊ := by
calc
Expand Down
7 changes: 3 additions & 4 deletions Mathlib/Algebra/Order/Floor/Semiring.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,10 +157,9 @@ theorem mul_cast_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : R) : ⌊a * n⌋
rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]

theorem cast_mul_floor_div_cancel {R : Type*} [CommSemiring R] [LinearOrder R]
[IsStrictOrderedRing R] [FloorSemiring R] {n : ℕ} (hn : n ≠ 0) (a : R) :
theorem cast_mul_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : R) :
⌊n * a⌋₊ / n = ⌊a⌋₊ := by
rw [mul_comm, mul_cast_floor_div_cancel hn]
rw [Nat.cast_comm, mul_cast_floor_div_cancel hn]

end floor

Expand Down Expand Up @@ -207,7 +206,7 @@ theorem ceil_le_floor_add_one (a : R) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1 := by
exact (lt_floor_add_one a).le

@[simp]
theorem ceil_intCast {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R]
theorem ceil_intCast {R : Type*} [Ring R] [LinearOrder R] [IsOrderedRing R]
[FloorSemiring R] (z : ℤ) :
⌈(z : R)⌉₊ = z.toNat :=
eq_of_forall_ge_iff fun a => by
Expand Down
Loading