From 67d7502bb773ddf0384a3ac2309b8acd3530bede Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard Date: Sat, 17 Aug 2024 13:18:00 +0000 Subject: [PATCH] chore(Algebra.Order.Ring.Rat): split into unbundled and bundled ordered algebra results (#15071) We split off all but the `LinearOrderedCommRing` and the inferred `OrderedAddCommMonoid` instances on `Rat` into `Algebra.Order.Ring.Unbundled.Rat` as these results do not require bundled ordered algebra classes. --- Mathlib.lean | 1 + Mathlib/Algebra/Order/Ring/Rat.lean | 194 +-------------- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean | 226 ++++++++++++++++++ Mathlib/Data/FP/Basic.lean | 2 +- Mathlib/Data/Int/Star.lean | 1 + Mathlib/Data/NNRat/Defs.lean | 9 +- Mathlib/Data/Rat/Cast/Lemmas.lean | 4 +- 7 files changed, 239 insertions(+), 198 deletions(-) create mode 100644 Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean diff --git a/Mathlib.lean b/Mathlib.lean index dfa5d02698df5..7227416de3c6a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -643,6 +643,7 @@ import Mathlib.Algebra.Order.Ring.Star import Mathlib.Algebra.Order.Ring.Synonym import Mathlib.Algebra.Order.Ring.Unbundled.Basic import Mathlib.Algebra.Order.Ring.Unbundled.Nonneg +import Mathlib.Algebra.Order.Ring.Unbundled.Rat import Mathlib.Algebra.Order.Ring.WithTop import Mathlib.Algebra.Order.Sub.Basic import Mathlib.Algebra.Order.Sub.Defs diff --git a/Mathlib/Algebra/Order/Ring/Rat.lean b/Mathlib/Algebra/Order/Ring/Rat.lean index 00c5c90fcde79..88cca6d79229f 100644 --- a/Mathlib/Algebra/Order/Ring/Rat.lean +++ b/Mathlib/Algebra/Order/Ring/Rat.lean @@ -3,8 +3,8 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro -/ -import Mathlib.Algebra.Order.Ring.Int -import Mathlib.Algebra.Ring.Rat +import Mathlib.Algebra.Order.Ring.Defs +import Mathlib.Algebra.Order.Ring.Unbundled.Rat /-! # The rational numbers form a linear ordered field @@ -27,168 +27,6 @@ assert_not_exists GaloisConnection namespace Rat -variable {a b c p q : ℚ} - -@[simp] lemma divInt_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) : 0 ≤ a /. b ↔ 0 ≤ a := by - cases' hab : a /. b with n d hd hnd - rw [mk'_eq_divInt, divInt_eq_iff hb.ne' (mod_cast hd)] at hab - rw [← num_nonneg, ← mul_nonneg_iff_of_pos_right hb, ← hab, - mul_nonneg_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero hd)] - -@[simp] lemma divInt_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a /. b := by - obtain rfl | hb := hb.eq_or_lt - · simp - rfl - rwa [divInt_nonneg_iff_of_pos_right hb] - -@[simp] lemma mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b := by - simpa using divInt_nonneg ha (Int.natCast_nonneg _) - -theorem ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) : - 0 ≤ Rat.ofScientific m s e := by - rw [Rat.ofScientific] - cases s - · rw [if_neg (by decide)] - refine num_nonneg.mp ?_ - rw [num_natCast] - exact Int.natCast_nonneg _ - · rw [if_pos rfl, normalize_eq_mkRat] - exact Rat.mkRat_nonneg (Int.natCast_nonneg _) _ - -instance _root_.NNRatCast.toOfScientific {K} [NNRatCast K] : OfScientific K where - ofScientific (m : ℕ) (b : Bool) (d : ℕ) := - NNRat.cast ⟨Rat.ofScientific m b d, ofScientific_nonneg m b d⟩ - -/-- Casting a scientific literal via `ℚ≥0` is the same as casting directly. -/ -@[simp, norm_cast] -theorem _root_.NNRat.cast_ofScientific {K} [NNRatCast K] (m : ℕ) (s : Bool) (e : ℕ) : - (OfScientific.ofScientific m s e : ℚ≥0) = (OfScientific.ofScientific m s e : K) := - rfl - -protected lemma add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b := - numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ by - have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁ - have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂ - simp only [d₁0, d₂0, h₁, h₂, mul_pos, divInt_nonneg_iff_of_pos_right, divInt_add_divInt, Ne, - Nat.cast_eq_zero, not_false_iff] - intro n₁0 n₂0 - apply add_nonneg <;> apply mul_nonneg <;> · first |assumption|apply Int.ofNat_zero_le - -protected lemma mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b := - numDenCasesOn' a fun n₁ d₁ h₁ => - numDenCasesOn' b fun n₂ d₂ h₂ => by - have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁ - have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂ - simp only [d₁0, d₂0, mul_pos, divInt_nonneg_iff_of_pos_right, - divInt_mul_divInt _ _ d₁0.ne' d₂0.ne'] - apply mul_nonneg - --- Porting note (#11215): TODO can this be shortened? -protected theorem le_iff_sub_nonneg (a b : ℚ) : a ≤ b ↔ 0 ≤ b - a := - numDenCasesOn'' a fun na da ha hared => - numDenCasesOn'' b fun nb db hb hbred => by - change Rat.blt _ _ = false ↔ _ - unfold Rat.blt - simp only [Bool.and_eq_true, decide_eq_true_eq, Bool.ite_eq_false_distrib, - decide_eq_false_iff_not, not_lt, ite_eq_left_iff, not_and, not_le, ← num_nonneg] - split_ifs with h h' - · rw [Rat.sub_def] - simp only [false_iff, not_le] - simp only [normalize_eq] - apply Int.ediv_neg' - · rw [sub_neg] - apply lt_of_lt_of_le - · apply mul_neg_of_neg_of_pos h.1 - rwa [Int.natCast_pos, Nat.pos_iff_ne_zero] - · apply mul_nonneg h.2 (Int.natCast_nonneg _) - · simp only [Int.natCast_pos, Nat.pos_iff_ne_zero] - exact Nat.gcd_ne_zero_right (Nat.mul_ne_zero hb ha) - · simp only [divInt_ofNat, ← zero_iff_num_zero, mkRat_eq_zero hb] at h' - simp [h'] - · simp only [Rat.sub_def, normalize_eq] - refine ⟨fun H => ?_, fun H _ => ?_⟩ - · refine Int.ediv_nonneg ?_ (Int.natCast_nonneg _) - rw [sub_nonneg] - push_neg at h - obtain hb|hb := Ne.lt_or_lt h' - · apply H - intro H' - exact (hb.trans H').false.elim - · obtain ha|ha := le_or_lt na 0 - · apply le_trans <| mul_nonpos_of_nonpos_of_nonneg ha (Int.natCast_nonneg _) - exact mul_nonneg hb.le (Int.natCast_nonneg _) - · exact H (fun _ => ha) - · rw [← sub_nonneg] - contrapose! H - apply Int.ediv_neg' H - simp only [Int.natCast_pos, Nat.pos_iff_ne_zero] - exact Nat.gcd_ne_zero_right (Nat.mul_ne_zero hb ha) - -protected lemma divInt_le_divInt {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) : - a /. b ≤ c /. d ↔ a * d ≤ c * b := by - rw [Rat.le_iff_sub_nonneg, ← sub_nonneg (α := ℤ)] - simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, mul_pos d0 b0] - -protected lemma le_total : a ≤ b ∨ b ≤ a := by - simpa only [← Rat.le_iff_sub_nonneg, neg_sub] using Rat.nonneg_total (b - a) - -protected theorem not_le {a b : ℚ} : ¬a ≤ b ↔ b < a := (Bool.not_eq_false _).to_iff - -instance linearOrder : LinearOrder ℚ where - le_refl a := by rw [Rat.le_iff_sub_nonneg, ← num_nonneg]; simp - le_trans a b c hab hbc := by - rw [Rat.le_iff_sub_nonneg] at hab hbc - have := Rat.add_nonneg hab hbc - simp_rw [sub_eq_add_neg, add_left_comm (b + -a) c (-b), add_comm (b + -a) (-b), - add_left_comm (-b) b (-a), add_comm (-b) (-a), add_neg_cancel_comm_assoc, - ← sub_eq_add_neg] at this - rwa [Rat.le_iff_sub_nonneg] - le_antisymm a b hab hba := by - rw [Rat.le_iff_sub_nonneg] at hab hba - rw [sub_eq_add_neg] at hba - rw [← neg_sub, sub_eq_add_neg] at hab - have := eq_neg_of_add_eq_zero_left (Rat.nonneg_antisymm hba hab) - rwa [neg_neg] at this - le_total _ _ := Rat.le_total - decidableEq := inferInstance - decidableLE := inferInstance - decidableLT := inferInstance - lt_iff_le_not_le _ _ := by rw [← Rat.not_le, and_iff_right_of_imp Rat.le_total.resolve_left] - -/-! -### Extra instances to short-circuit type class resolution - -These also prevent non-computable instances being used to construct these instances non-computably. --/ - -instance instDistribLattice : DistribLattice ℚ := inferInstance -instance instLattice : Lattice ℚ := inferInstance -instance instSemilatticeInf : SemilatticeInf ℚ := inferInstance -instance instSemilatticeSup : SemilatticeSup ℚ := inferInstance -instance instInf : Inf ℚ := inferInstance -instance instSup : Sup ℚ := inferInstance -instance instPartialOrder : PartialOrder ℚ := inferInstance -instance instPreorder : Preorder ℚ := inferInstance - -/-! ### Miscellaneous lemmas -/ - -protected lemma le_def : p ≤ q ↔ p.num * q.den ≤ q.num * p.den := by - rw [← num_divInt_den q, ← num_divInt_den p] - conv_rhs => simp only [num_divInt_den] - exact Rat.divInt_le_divInt (mod_cast p.pos) (mod_cast q.pos) - -protected lemma lt_def : p < q ↔ p.num * q.den < q.num * p.den := by - rw [lt_iff_le_and_ne, Rat.le_def] - suffices p ≠ q ↔ p.num * q.den ≠ q.num * p.den by - constructor <;> intro h - · exact lt_iff_le_and_ne.mpr ⟨h.left, this.mp h.right⟩ - · have tmp := lt_iff_le_and_ne.mp h - exact ⟨tmp.left, this.mpr tmp.right⟩ - exact not_iff_not.mpr eq_iff_mul_eq_mul - -protected theorem add_le_add_left {a b c : ℚ} : c + a ≤ c + b ↔ a ≤ b := by - rw [Rat.le_iff_sub_nonneg, add_sub_add_left_eq_sub, ← Rat.le_iff_sub_nonneg] - instance instLinearOrderedCommRing : LinearOrderedCommRing ℚ where __ := Rat.linearOrder __ := Rat.commRing @@ -213,32 +51,4 @@ instance : OrderedCancelAddCommMonoid ℚ := by infer_instance instance : OrderedAddCommMonoid ℚ := by infer_instance -@[simp] lemma num_nonpos {a : ℚ} : a.num ≤ 0 ↔ a ≤ 0 := by simpa using @num_nonneg (-a) -@[simp] lemma num_pos {a : ℚ} : 0 < a.num ↔ 0 < a := lt_iff_lt_of_le_iff_le num_nonpos -@[simp] lemma num_neg {a : ℚ} : a.num < 0 ↔ a < 0 := lt_iff_lt_of_le_iff_le num_nonneg - -@[deprecated (since := "2024-02-16")] alias num_nonneg_iff_zero_le := num_nonneg -@[deprecated (since := "2024-02-16")] alias num_pos_iff_pos := num_pos - -theorem div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) : - (a : ℚ) / b < c / d ↔ a * d < c * b := by - simp only [lt_iff_le_not_le] - apply and_congr - · simp [div_def', Rat.divInt_le_divInt b_pos d_pos] - · apply not_congr - simp [div_def', Rat.divInt_le_divInt d_pos b_pos] - -theorem lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.den := by simp [Rat.lt_def] - -theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den := by - rcases le_total q 0 with hq | hq - · rw [abs_of_nonpos hq] - rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt (mod_cast q.pos) zero_lt_one, - mul_one, zero_mul] at hq - rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def] - · rw [abs_of_nonneg hq] - rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt zero_lt_one (mod_cast q.pos), - mul_one, zero_mul] at hq - rw [Int.natAbs_of_nonneg hq, num_divInt_den] - end Rat diff --git a/Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean b/Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean new file mode 100644 index 0000000000000..8b5c91a55c468 --- /dev/null +++ b/Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean @@ -0,0 +1,226 @@ +/- +Copyright (c) 2019 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Mario Carneiro +-/ +import Mathlib.Algebra.Order.Group.Unbundled.Abs +import Mathlib.Algebra.Order.Group.Unbundled.Basic +import Mathlib.Algebra.Ring.Rat +import Mathlib.Init.Data.Int.Order + +/-! +# The rational numbers possess a linear order + +This file constructs the order on `ℚ` and proves various facts relating the order to +ring structure on `ℚ`. This only used unbundled type classes relating the order structure +and algebra structure on `ℚ`. For the bundled `LinearOrderedCommRing` instance on `Q`, +see `Algebra.Order.Ring.Rat`. + +## Tags + +rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering +-/ + +assert_not_exists OrderedCommMonoid +assert_not_exists Field +assert_not_exists Finset +assert_not_exists Set.Icc +assert_not_exists GaloisConnection + +namespace Rat + +variable {a b c p q : ℚ} + +@[simp] lemma divInt_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) : 0 ≤ a /. b ↔ 0 ≤ a := by + cases' hab : a /. b with n d hd hnd + rw [mk'_eq_divInt, divInt_eq_iff hb.ne' (mod_cast hd)] at hab + rw [← num_nonneg, ← Int.mul_nonneg_iff_of_pos_right hb, ← hab, + Int.mul_nonneg_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero hd)] + +@[simp] lemma divInt_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a /. b := by + obtain rfl | hb := hb.eq_or_lt + · simp + rfl + rwa [divInt_nonneg_iff_of_pos_right hb] + +@[simp] lemma mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b := by + simpa using divInt_nonneg ha (Int.natCast_nonneg _) + +theorem ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) : + 0 ≤ Rat.ofScientific m s e := by + rw [Rat.ofScientific] + cases s + · rw [if_neg (by decide)] + refine num_nonneg.mp ?_ + rw [num_natCast] + exact Int.natCast_nonneg _ + · rw [if_pos rfl, normalize_eq_mkRat] + exact Rat.mkRat_nonneg (Int.natCast_nonneg _) _ + +instance _root_.NNRatCast.toOfScientific {K} [NNRatCast K] : OfScientific K where + ofScientific (m : ℕ) (b : Bool) (d : ℕ) := + NNRat.cast ⟨Rat.ofScientific m b d, ofScientific_nonneg m b d⟩ + +/-- Casting a scientific literal via `ℚ≥0` is the same as casting directly. -/ +@[simp, norm_cast] +theorem _root_.NNRat.cast_ofScientific {K} [NNRatCast K] (m : ℕ) (s : Bool) (e : ℕ) : + (OfScientific.ofScientific m s e : ℚ≥0) = (OfScientific.ofScientific m s e : K) := + rfl + +protected lemma add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b := + numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ by + have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁ + have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂ + simp only [d₁0, d₂0, h₁, h₂, Int.mul_pos, divInt_nonneg_iff_of_pos_right, divInt_add_divInt, Ne, + Nat.cast_eq_zero, not_false_iff] + intro n₁0 n₂0 + apply Int.add_nonneg <;> apply Int.mul_nonneg <;> · first | assumption | apply Int.ofNat_zero_le + +protected lemma mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b := + numDenCasesOn' a fun n₁ d₁ h₁ => + numDenCasesOn' b fun n₂ d₂ h₂ => by + have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁ + have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂ + simp only [d₁0, d₂0, Int.mul_pos, divInt_nonneg_iff_of_pos_right, + divInt_mul_divInt _ _ d₁0.ne' d₂0.ne'] + apply Int.mul_nonneg + +-- Porting note (#11215): TODO can this be shortened? +protected theorem le_iff_sub_nonneg (a b : ℚ) : a ≤ b ↔ 0 ≤ b - a := + numDenCasesOn'' a fun na da ha hared => + numDenCasesOn'' b fun nb db hb hbred => by + change Rat.blt _ _ = false ↔ _ + unfold Rat.blt + simp only [Bool.and_eq_true, decide_eq_true_eq, Bool.ite_eq_false_distrib, + decide_eq_false_iff_not, not_lt, ite_eq_left_iff, not_and, not_le, ← num_nonneg] + split_ifs with h h' + · rw [Rat.sub_def] + simp only [false_iff, not_le] + simp only [normalize_eq] + apply Int.ediv_neg' + · rw [sub_neg] + apply lt_of_lt_of_le + · apply Int.mul_neg_of_neg_of_pos h.1 + rwa [Int.natCast_pos, Nat.pos_iff_ne_zero] + · apply Int.mul_nonneg h.2 (Int.natCast_nonneg _) + · simp only [Int.natCast_pos, Nat.pos_iff_ne_zero] + exact Nat.gcd_ne_zero_right (Nat.mul_ne_zero hb ha) + · simp only [divInt_ofNat, ← zero_iff_num_zero, mkRat_eq_zero hb] at h' + simp [h'] + · simp only [Rat.sub_def, normalize_eq] + refine ⟨fun H => ?_, fun H _ => ?_⟩ + · refine Int.ediv_nonneg ?_ (Int.natCast_nonneg _) + rw [Int.sub_nonneg] + push_neg at h + obtain hb|hb := Ne.lt_or_lt h' + · apply H + intro H' + exact (hb.trans H').false.elim + · obtain ha|ha := le_or_lt na 0 + · apply le_trans <| Int.mul_nonpos_of_nonpos_of_nonneg ha (Int.natCast_nonneg _) + exact Int.mul_nonneg hb.le (Int.natCast_nonneg _) + · exact H (fun _ => ha) + · rw [← Int.sub_nonneg] + contrapose! H + apply Int.ediv_neg' H + simp only [Int.natCast_pos, Nat.pos_iff_ne_zero] + exact Nat.gcd_ne_zero_right (Nat.mul_ne_zero hb ha) + +protected lemma divInt_le_divInt {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) : + a /. b ≤ c /. d ↔ a * d ≤ c * b := by + rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg] + simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0] + +protected lemma le_total : a ≤ b ∨ b ≤ a := by + simpa only [← Rat.le_iff_sub_nonneg, neg_sub] using Rat.nonneg_total (b - a) + +protected theorem not_le {a b : ℚ} : ¬a ≤ b ↔ b < a := (Bool.not_eq_false _).to_iff + +instance linearOrder : LinearOrder ℚ where + le_refl a := by rw [Rat.le_iff_sub_nonneg, ← num_nonneg]; simp + le_trans a b c hab hbc := by + rw [Rat.le_iff_sub_nonneg] at hab hbc + have := Rat.add_nonneg hab hbc + simp_rw [sub_eq_add_neg, add_left_comm (b + -a) c (-b), add_comm (b + -a) (-b), + add_left_comm (-b) b (-a), add_comm (-b) (-a), add_neg_cancel_comm_assoc, + ← sub_eq_add_neg] at this + rwa [Rat.le_iff_sub_nonneg] + le_antisymm a b hab hba := by + rw [Rat.le_iff_sub_nonneg] at hab hba + rw [sub_eq_add_neg] at hba + rw [← neg_sub, sub_eq_add_neg] at hab + have := eq_neg_of_add_eq_zero_left (Rat.nonneg_antisymm hba hab) + rwa [neg_neg] at this + le_total _ _ := Rat.le_total + decidableEq := inferInstance + decidableLE := inferInstance + decidableLT := inferInstance + lt_iff_le_not_le _ _ := by rw [← Rat.not_le, and_iff_right_of_imp Rat.le_total.resolve_left] + +/-! +### Extra instances to short-circuit type class resolution + +These also prevent non-computable instances being used to construct these instances non-computably. +-/ + +instance instDistribLattice : DistribLattice ℚ := inferInstance +instance instLattice : Lattice ℚ := inferInstance +instance instSemilatticeInf : SemilatticeInf ℚ := inferInstance +instance instSemilatticeSup : SemilatticeSup ℚ := inferInstance +instance instInf : Inf ℚ := inferInstance +instance instSup : Sup ℚ := inferInstance +instance instPartialOrder : PartialOrder ℚ := inferInstance +instance instPreorder : Preorder ℚ := inferInstance + +/-! ### Miscellaneous lemmas -/ + +protected lemma le_def : p ≤ q ↔ p.num * q.den ≤ q.num * p.den := by + rw [← num_divInt_den q, ← num_divInt_den p] + conv_rhs => simp only [num_divInt_den] + exact Rat.divInt_le_divInt (mod_cast p.pos) (mod_cast q.pos) + +protected lemma lt_def : p < q ↔ p.num * q.den < q.num * p.den := by + rw [lt_iff_le_and_ne, Rat.le_def] + suffices p ≠ q ↔ p.num * q.den ≠ q.num * p.den by + constructor <;> intro h + · exact lt_iff_le_and_ne.mpr ⟨h.left, this.mp h.right⟩ + · have tmp := lt_iff_le_and_ne.mp h + exact ⟨tmp.left, this.mpr tmp.right⟩ + exact not_iff_not.mpr eq_iff_mul_eq_mul + +protected theorem add_le_add_left {a b c : ℚ} : c + a ≤ c + b ↔ a ≤ b := by + rw [Rat.le_iff_sub_nonneg, add_sub_add_left_eq_sub, ← Rat.le_iff_sub_nonneg] + +instance : CovariantClass ℚ ℚ (· + ·) (· ≤ ·) where + elim := fun _ _ _ h => Rat.add_le_add_left.2 h + +@[simp] lemma num_nonpos {a : ℚ} : a.num ≤ 0 ↔ a ≤ 0 := by + simp [Int.le_iff_lt_or_eq, instLE, Rat.blt, Int.not_lt] +@[simp] lemma num_pos {a : ℚ} : 0 < a.num ↔ 0 < a := lt_iff_lt_of_le_iff_le num_nonpos +@[simp] lemma num_neg {a : ℚ} : a.num < 0 ↔ a < 0 := lt_iff_lt_of_le_iff_le num_nonneg + +@[deprecated (since := "2024-02-16")] alias num_nonneg_iff_zero_le := num_nonneg +@[deprecated (since := "2024-02-16")] alias num_pos_iff_pos := num_pos + +theorem div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) : + (a : ℚ) / b < c / d ↔ a * d < c * b := by + simp only [lt_iff_le_not_le] + apply and_congr + · simp [div_def', Rat.divInt_le_divInt b_pos d_pos] + · apply not_congr + simp [div_def', Rat.divInt_le_divInt d_pos b_pos] + +theorem lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.den := by simp [Rat.lt_def] + +theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den := by + rcases le_total q 0 with hq | hq + · rw [abs_of_nonpos hq] + rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt (mod_cast q.pos) Int.zero_lt_one, + mul_one, zero_mul] at hq + rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def] + · rw [abs_of_nonneg hq] + rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt Int.zero_lt_one (mod_cast q.pos), + mul_one, zero_mul] at hq + rw [Int.natAbs_of_nonneg hq, num_divInt_den] + +end Rat diff --git a/Mathlib/Data/FP/Basic.lean b/Mathlib/Data/FP/Basic.lean index 8ba466a35a5cb..c854edb12daef 100644 --- a/Mathlib/Data/FP/Basic.lean +++ b/Mathlib/Data/FP/Basic.lean @@ -86,7 +86,7 @@ theorem Float.Zero.valid : ValidFinite emin 0 := rw [mul_comm] assumption le_trans C.precMax (Nat.le_mul_of_pos_left _ two_pos), - by (rw [max_eq_right]; simp [sub_eq_add_neg])⟩ + by (rw [max_eq_right]; simp [sub_eq_add_neg, Int.ofNat_zero_le])⟩ @[nolint docBlame] def Float.zero (s : Bool) : Float := diff --git a/Mathlib/Data/Int/Star.lean b/Mathlib/Data/Int/Star.lean index 9492664978ba1..1304983eb851c 100644 --- a/Mathlib/Data/Int/Star.lean +++ b/Mathlib/Data/Int/Star.lean @@ -7,6 +7,7 @@ import Mathlib.Algebra.Star.Order import Mathlib.Algebra.Order.Group.Abs import Mathlib.Algebra.Order.Monoid.Submonoid import Mathlib.Algebra.Order.Ring.Basic +import Mathlib.Algebra.Order.Ring.Int /-! # Star ordered ring structure on `ℤ` diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean index dc43e243e47d4..48552f3ade343 100644 --- a/Mathlib/Data/NNRat/Defs.lean +++ b/Mathlib/Data/NNRat/Defs.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies, Bhavik Mehta -/ import Mathlib.Algebra.Order.Nonneg.Ring +import Mathlib.Algebra.Order.Group.Unbundled.Int import Mathlib.Algebra.Order.Ring.Rat +import Mathlib.Algebra.Order.Ring.Unbundled.Rat import Mathlib.Data.Nat.Cast.Order.Ring /-! @@ -296,7 +298,7 @@ namespace NNRat variable {p q : ℚ≥0} @[norm_cast] lemma num_coe (q : ℚ≥0) : (q : ℚ).num = q.num := by - simp [num, abs_of_nonneg, Rat.num_nonneg, q.2] + simp only [num, Int.natCast_natAbs, Rat.num_nonneg, coe_nonneg, abs_of_nonneg] theorem natAbs_num_coe : (q : ℚ).num.natAbs = q.num := rfl @@ -328,14 +330,15 @@ theorem ext_num_den_iff : p = q ↔ p.num = q.num ∧ p.den = q.den := /-- Form the quotient `n / d` where `n d : ℕ`. See also `Rat.divInt` and `mkRat`. -/ -def divNat (n d : ℕ) : ℚ≥0 := ⟨.divInt n d, Rat.divInt_nonneg n.cast_nonneg d.cast_nonneg⟩ +def divNat (n d : ℕ) : ℚ≥0 := + ⟨.divInt n d, Rat.divInt_nonneg (Int.ofNat_zero_le n) (Int.ofNat_zero_le d)⟩ variable {n₁ n₂ d₁ d₂ d : ℕ} @[simp, norm_cast] lemma coe_divNat (n d : ℕ) : (divNat n d : ℚ) = .divInt n d := rfl lemma mk_divInt (n d : ℕ) : - ⟨.divInt n d, Rat.divInt_nonneg n.cast_nonneg d.cast_nonneg⟩ = divNat n d := rfl + ⟨.divInt n d, Rat.divInt_nonneg (Int.ofNat_zero_le n) (Int.ofNat_zero_le d)⟩ = divNat n d := rfl lemma divNat_inj (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁ := by rw [← coe_inj]; simp [Rat.mkRat_eq_iff, h₁, h₂]; norm_cast diff --git a/Mathlib/Data/Rat/Cast/Lemmas.lean b/Mathlib/Data/Rat/Cast/Lemmas.lean index 9dea343405326..4089d6b56d2e4 100644 --- a/Mathlib/Data/Rat/Cast/Lemmas.lean +++ b/Mathlib/Data/Rat/Cast/Lemmas.lean @@ -32,7 +32,7 @@ theorem cast_inv_nat (n : ℕ) : ((n⁻¹ : ℚ) : α) = (n : α)⁻¹ := by cases' n with n · simp rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero, - Int.sign_eq_one_of_pos (Nat.cast_pos.mpr n.succ_pos), Int.cast_one, one_div] + Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div] -- Porting note: proof got a lot easier - is this still the intended statement? @[simp] @@ -47,7 +47,7 @@ theorem cast_nnratCast {K} [DivisionRing K] (q : ℚ≥0) : rw [Rat.cast_def, NNRat.cast_def, NNRat.cast_def] have hn := @num_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den on_goal 1 => have hd := @den_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den - case hdp => simpa only [Nat.cast_pos] using q.den_pos + case hdp => simpa only [Int.ofNat_pos] using q.den_pos simp only [Int.cast_natCast, Nat.cast_inj] at hn hd rw [hn, hd, Int.cast_natCast]