refactor(*): drop decidable_linear_order, switch to Lean 3.22.0 (#4762

)

The main non-bc change in Lean 3.22.0 is leanprover-community/lean#484 which merges `linear_order`
with `decidable_linear_order`. This is the `mathlib` part of this PR.

## List of API changes

* All `*linear_order*` typeclasses now imply decidability of `(≤)`, `(<)`, and `(=)`.
* Drop `classical.DLO`.
* Drop `discrete_linear_ordered_field`, use `linear_ordered_field` instead.
* Drop `decidable_linear_ordered_semiring`, use `linear_ordered_semiring` instead.
* Drop `decidable_linear_ordered_comm_ring`, use `linear_ordered_comm_ring` instead;
* Rename `decidable_linear_ordered_cancel_add_comm_monoid` to `linear_ordered_cancel_add_comm_monoid`.
* Rename `decidable_linear_ordered_add_comm_group` to `linear_ordered_add_comm_group`.
* Modify some lemmas to use weaker typeclass assumptions.
* Add more lemmas about `ordering.compares`, including `linear_order_of_compares` which
  constructs a `linear_order` instance from `cmp` function.



Co-authored-by: Johan Commelin <johan@commelin.net>

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -26,7 +26,7 @@ variable {n : ℕ}
   neither endpoint of `J` coincides with an endpoint of `I`, `¬ (K ⊆ J)` and
   `K` does not lie completely to the left nor completely to the right of `J`.
   Then `I ∩ K \ J` is nonempty. -/
-lemma Ico_lemma {α} [decidable_linear_order α] {x₁ x₂ y₁ y₂ z₁ z₂ w : α}
+lemma Ico_lemma {α} [linear_order α] {x₁ x₂ y₁ y₂ z₁ z₂ w : α}
   (h₁ : x₁ < y₁) (hy : y₁ < y₂) (h₂ : y₂ < x₂)
   (hz₁ : z₁ ≤ y₂) (hz₂ : y₁ ≤ z₂) (hw : w ∉ Ico y₁ y₂ ∧ w ∈ Ico z₁ z₂) :
   ∃w, w ∈ Ico x₁ x₂ ∧ w ∉ Ico y₁ y₂ ∧ w ∈ Ico z₁ z₂ :=

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.21.0"
+lean_version = "leanprover-community/lean:3.22.0"
 path = "src"
 
 [dependencies]

src/algebra/archimedean.lean

@@ -15,8 +15,8 @@ such that `0 < y` there exists a natural number `n` such that `x ≤ n •ℕ y`
 class archimedean (α) [ordered_add_comm_monoid α] : Prop :=
 (arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n •ℕ y)
 
-namespace decidable_linear_ordered_add_comm_group
-variables [decidable_linear_ordered_add_comm_group α] [archimedean α]
+namespace linear_ordered_add_comm_group
+variables [linear_ordered_add_comm_group α] [archimedean α]
 
 /-- An archimedean decidable linearly ordered `add_comm_group` has a version of the floor: for
 `a > 0`, any `g` in the group lies between some two consecutive multiples of `a`. -/
@@ -44,7 +44,7 @@ begin
   simpa [sub_lt_iff_lt_add']
 end
 
-end decidable_linear_ordered_add_comm_group
+end linear_ordered_add_comm_group
 
 theorem exists_nat_gt [linear_ordered_semiring α] [archimedean α]
   (x : α) : ∃ n : ℕ, x < n :=
@@ -113,7 +113,7 @@ section linear_ordered_field
 /-- Every positive x is between two successive integer powers of
 another y greater than one. This is the same as `exists_int_pow_near'`,
 but with ≤ and < the other way around. -/
-lemma exists_int_pow_near [discrete_linear_ordered_field α] [archimedean α]
+lemma exists_int_pow_near [linear_ordered_field α] [archimedean α]
   {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
   ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
 by classical; exact
@@ -131,7 +131,7 @@ let ⟨n, hn₁, hn₂⟩ := int.exists_greatest_of_bdd hb he in
 /-- Every positive x is between two successive integer powers of
 another y greater than one. This is the same as `exists_int_pow_near`,
 but with ≤ and < the other way around. -/
-lemma exists_int_pow_near' [discrete_linear_ordered_field α] [archimedean α]
+lemma exists_int_pow_near' [linear_ordered_field α] [archimedean α]
   {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
   ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) :=
 let ⟨m, hle, hlt⟩ := exists_int_pow_near (inv_pos.2 hx) hy in
@@ -263,7 +263,7 @@ end
 end linear_ordered_field
 
 section
-variables [discrete_linear_ordered_field α]
+variables [linear_ordered_field α]
 
 /-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
 def round [floor_ring α] (x : α) : ℤ := ⌊x + 1 / 2⌋

src/algebra/big_operators/order.lean

@@ -31,7 +31,7 @@ begin
   refl
 end
 
-lemma abs_sum_le_sum_abs [discrete_linear_ordered_field α] {f : β → α} {s : finset β} :
+lemma abs_sum_le_sum_abs [linear_ordered_field α] {f : β → α} {s : finset β} :
   abs (∑ x in s, f x) ≤ ∑ x in s, abs (f x) :=
 le_sum_of_subadditive _ abs_zero abs_add s f
 
@@ -195,9 +195,9 @@ end
 
 end ordered_cancel_comm_monoid
 
-section decidable_linear_ordered_cancel_comm_monoid
+section linear_ordered_cancel_comm_monoid
 
-variables [decidable_linear_ordered_cancel_add_comm_monoid β]
+variables [linear_ordered_cancel_add_comm_monoid β]
 
 theorem exists_lt_of_sum_lt (Hlt : (∑ x in s, f x) < ∑ x in s, g x) :
   ∃ i ∈ s, f i < g i :=
@@ -225,7 +225,7 @@ begin
                  ... = 0           : by rw [finset.sum_const, nsmul_zero],
 end
 
-end decidable_linear_ordered_cancel_comm_monoid
+end linear_ordered_cancel_comm_monoid
 
 section linear_ordered_comm_ring
 variables [linear_ordered_comm_ring β]

src/algebra/continued_fractions/computation/approximations.lean

@@ -33,7 +33,7 @@ for the values involved in the continued fractions computation `gcf.of`.
 namespace generalized_continued_fraction
 open generalized_continued_fraction as gcf
 
-variables {K : Type*} {v : K} {n : ℕ} [discrete_linear_ordered_field K] [floor_ring K]
+variables {K : Type*} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K]
 
 /-
 We begin with some lemmas about the stream of `int_fract_pair`s, which presumably are not

src/algebra/continued_fractions/computation/basic.lean

@@ -100,10 +100,10 @@ rfl
 
 end coe
 
--- Note: this could be relaxed to something like `discrete_linear_ordered_division_ring` in the
+-- Note: this could be relaxed to something like `linear_ordered_division_ring` in the
 -- future.
 /- Fix a discrete linear ordered field with `floor` function. -/
-variables [discrete_linear_ordered_field K] [floor_ring K]
+variables [linear_ordered_field K] [floor_ring K]
 
 /-- Creates the integer and fractional part of a value `v`, i.e. `⟨⌊v⌋, v - ⌊v⌋⟩`. -/
 protected def of (v : K) : int_fract_pair K := ⟨⌊v⌋, fract v⟩
@@ -167,7 +167,7 @@ process stops when the fractional part `v- ⌊v⌋` hits 0 at some step.
 The implementation uses `int_fract_pair.stream` to obtain the partial denominators of the continued
 fraction. Refer to said function for more details about the computation process.
 -/
-protected def of [discrete_linear_ordered_field K] [floor_ring K] (v : K) : gcf K :=
+protected def of [linear_ordered_field K] [floor_ring K] (v : K) : gcf K :=
 let ⟨h, s⟩ := int_fract_pair.seq1 v in -- get the sequence of integer and fractional parts.
 ⟨ h.b, -- the head is just the first integer part
   s.map (λ p, ⟨1, p.b⟩) ⟩ -- the sequence consists of the remaining integer parts as the partial

src/algebra/continued_fractions/computation/correctness_terminating.lean

@@ -40,7 +40,7 @@ information about the computation process, refer to `algebra.continued_fraction.
 namespace generalized_continued_fraction
 open generalized_continued_fraction as gcf
 
-variables {K : Type*} [discrete_linear_ordered_field K] {v : K} {n : ℕ}
+variables {K : Type*} [linear_ordered_field K] {v : K} {n : ℕ}
 
 /--
 Given two continuants `pconts` and `conts` and a value `fr`, this function returns

src/algebra/continued_fractions/computation/translations.lean

@@ -38,7 +38,7 @@ namespace generalized_continued_fraction
 open generalized_continued_fraction as gcf
 
 /- Fix a discrete linear ordered floor field and a value `v`. -/
-variables {K : Type*} [discrete_linear_ordered_field K] [floor_ring K] {v : K}
+variables {K : Type*} [linear_ordered_field K] [floor_ring K] {v : K}
 
 namespace int_fract_pair
 /-!

src/algebra/field_power.lean

@@ -25,7 +25,7 @@ by rw [fpow_bit1', fpow_bit1', neg_mul_neg, neg_mul_eq_mul_neg]
 section ordered_field_power
 open int
 
-variables {K : Type u} [discrete_linear_ordered_field K]
+variables {K : Type u} [linear_ordered_field K]
 
 lemma fpow_nonneg_of_nonneg {a : K} (ha : 0 ≤ a) : ∀ (z : ℤ), 0 ≤ a ^ z
 | (of_nat n) := pow_nonneg ha _
@@ -91,13 +91,13 @@ lemma one_lt_pow {K} [linear_ordered_semiring K] {p : K} (hp : 1 < p) : ∀ {n :
 
 section
 local attribute [semireducible] int.nonneg
-lemma one_lt_fpow {K}  [discrete_linear_ordered_field K] {p : K} (hp : 1 < p) :
+lemma one_lt_fpow {K}  [linear_ordered_field K] {p : K} (hp : 1 < p) :
   ∀ z : ℤ, 0 < z → 1 < p ^ z
 | (int.of_nat n) h := one_lt_pow hp (nat.succ_le_of_lt (int.lt_of_coe_nat_lt_coe_nat h))
 end
 
 section ordered
-variables  {K : Type*} [discrete_linear_ordered_field K]
+variables  {K : Type*} [linear_ordered_field K]
 
 lemma nat.fpow_pos_of_pos {p : ℕ} (h : 0 < p) (n:ℤ) : 0 < (p:K)^n :=
 by { apply fpow_pos_of_pos, exact_mod_cast h }

src/algebra/floor.lean

@@ -92,7 +92,7 @@ eq_of_forall_le_iff $ λ a, by rw [le_floor,
 theorem floor_sub_int (x : α) (z : ℤ) : ⌊x - z⌋ = ⌊x⌋ - z :=
 eq.trans (by rw [int.cast_neg]; refl) (floor_add_int _ _)
 
-lemma abs_sub_lt_one_of_floor_eq_floor {α : Type*} [decidable_linear_ordered_comm_ring α]
+lemma abs_sub_lt_one_of_floor_eq_floor {α : Type*} [linear_ordered_comm_ring α]
   [floor_ring α] {x y : α} (h : ⌊x⌋ = ⌊y⌋) : abs (x - y) < 1 :=
 begin
   have : x < ⌊x⌋ + 1         := lt_floor_add_one x,

src/algebra/group_power/basic.lean

@@ -432,11 +432,11 @@ end
   {a : R} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 mt pow_eq_zero h
 
-lemma pow_abs [decidable_linear_ordered_comm_ring R] (a : R) (n : ℕ) : (abs a)^n = abs (a^n) :=
+lemma pow_abs [linear_ordered_comm_ring R] (a : R) (n : ℕ) : (abs a)^n = abs (a^n) :=
 by induction n with n ih; [exact (abs_one).symm,
   rw [pow_succ, pow_succ, ih, abs_mul]]
 
-lemma abs_neg_one_pow [decidable_linear_ordered_comm_ring R] (n : ℕ) : abs ((-1 : R)^n) = 1 :=
+lemma abs_neg_one_pow [linear_ordered_comm_ring R] (n : ℕ) : abs ((-1 : R)^n) = 1 :=
 by rw [←pow_abs, abs_neg, abs_one, one_pow]
 
 section add_monoid

src/algebra/group_power/lemmas.lean

@@ -184,8 +184,8 @@ calc n •ℤ a = n •ℤ a + 0 : (add_zero _).symm
 
 end ordered_add_comm_group
 
-section decidable_linear_ordered_add_comm_group
-variable [decidable_linear_ordered_add_comm_group A]
+section linear_ordered_add_comm_group
+variable [linear_ordered_add_comm_group A]
 
 theorem gsmul_le_gsmul_iff {a : A} {n m : ℤ} (ha : 0 < a) : n •ℤ a ≤ m •ℤ a ↔ n ≤ m :=
 begin
@@ -215,7 +215,7 @@ begin
   exact lt_irrefl _ (lt_of_le_of_lt (nsmul_le_nsmul (le_of_lt ha) $ not_lt.mp H) h)
 end
 
-end decidable_linear_ordered_add_comm_group
+end linear_ordered_add_comm_group
 
 @[simp] lemma with_bot.coe_nsmul [add_monoid A] (a : A) (n : ℕ) :
   ((nsmul n a : A) : with_bot A) = nsmul n a :=

src/algebra/order.lean

@@ -225,12 +225,12 @@ calc  c
 namespace decidable
 
 -- See Note [decidable namespace]
-lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [decidable_linear_order β]
+lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [linear_order β]
   {a b : α} {c d : β} : (a ≤ b → c ≤ d) ↔ (d < c → b < a) :=
 ⟨lt_imp_lt_of_le_imp_le, le_imp_le_of_lt_imp_lt⟩
 
 -- See Note [decidable namespace]
-lemma le_iff_le_iff_lt_iff_lt {β} [decidable_linear_order α] [decidable_linear_order β]
+lemma le_iff_le_iff_lt_iff_lt {β} [linear_order α] [linear_order β]
   {a b : α} {c d : β} : (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
 ⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ (not_congr H).trans $ not_lt⟩
 
@@ -245,23 +245,50 @@ namespace ordering
 | eq a b := a = b
 | gt a b := a > b
 
+theorem compares_swap [has_lt α] {a b : α} {o : ordering} :
+  o.swap.compares a b ↔ o.compares b a :=
+by { cases o, exacts [iff.rfl, eq_comm, iff.rfl] }
+
+alias compares_swap ↔ ordering.compares.of_swap ordering.compares.swap
+
+theorem swap_eq_iff_eq_swap {o o' : ordering} : o.swap = o' ↔ o = o'.swap :=
+⟨λ h, by rw [← swap_swap o, h], λ h, by rw [← swap_swap o', h]⟩
+
 theorem compares.eq_lt [preorder α] :
   ∀ {o} {a b : α}, compares o a b → (o = lt ↔ a < b)
 | lt a b h := ⟨λ _, h, λ _, rfl⟩
 | eq a b h := ⟨λ h, by injection h, λ h', (ne_of_lt h' h).elim⟩
 | gt a b h := ⟨λ h, by injection h, λ h', (lt_asymm h h').elim⟩
 
+theorem compares.ne_lt [preorder α] :
+  ∀ {o} {a b : α}, compares o a b → (o ≠ lt ↔ b ≤ a)
+| lt a b h := ⟨absurd rfl, λ h', (not_le_of_lt h h').elim⟩
+| eq a b h := ⟨λ _, ge_of_eq h, λ _ h, by injection h⟩
+| gt a b h := ⟨λ _, le_of_lt h, λ _ h, by injection h⟩
+
 theorem compares.eq_eq [preorder α] :
   ∀ {o} {a b : α}, compares o a b → (o = eq ↔ a = b)
 | lt a b h := ⟨λ h, by injection h, λ h', (ne_of_lt h h').elim⟩
 | eq a b h := ⟨λ _, h, λ _, rfl⟩
 | gt a b h := ⟨λ h, by injection h, λ h', (ne_of_gt h h').elim⟩
 
-theorem compares.eq_gt [preorder α] :
-  ∀ {o} {a b : α}, compares o a b → (o = gt ↔ b < a)
-| lt a b h := ⟨λ h, by injection h, λ h', (lt_asymm h h').elim⟩
-| eq a b h := ⟨λ h, by injection h, λ h', (ne_of_gt h' h).elim⟩
-| gt a b h := ⟨λ _, h, λ _, rfl⟩
+theorem compares.eq_gt [preorder α] {o} {a b : α} (h : compares o a b) : (o = gt ↔ b < a) :=
+swap_eq_iff_eq_swap.symm.trans h.swap.eq_lt
+
+theorem compares.ne_gt [preorder α] {o} {a b : α} (h : compares o a b) : (o ≠ gt ↔ a ≤ b) :=
+(not_congr swap_eq_iff_eq_swap.symm).trans h.swap.ne_lt
+
+theorem compares.le_total [preorder α] {a b : α} :
+  ∀ {o}, compares o a b → a ≤ b ∨ b ≤ a
+| lt h := or.inl (le_of_lt h)
+| eq h := or.inl (le_of_eq h)
+| gt h := or.inr (le_of_lt h)
+
+theorem compares.le_antisymm [preorder α] {a b : α} :
+  ∀ {o}, compares o a b → a ≤ b → b ≤ a → a = b
+| lt h _ hba := (not_le_of_lt h hba).elim
+| eq h _ _   := h
+| gt h hab _ := (not_le_of_lt h hab).elim
 
 theorem compares.inj [preorder α] {o₁} :
   ∀ {o₂} {a b : α}, compares o₁ a b → compares o₂ a b → o₁ = o₂
@@ -292,7 +319,7 @@ by cases o₁; cases o₂; exact dec_trivial
 
 end ordering
 
-theorem cmp_compares [decidable_linear_order α] (a b : α) : (cmp a b).compares a b :=
+theorem cmp_compares [linear_order α] (a b : α) : (cmp a b).compares a b :=
 begin
   unfold cmp cmp_using,
   by_cases a < b; simp [h],
@@ -306,3 +333,14 @@ begin
   by_cases a < b; by_cases h₂ : b < a; simp [h, h₂, gt, ordering.swap],
   exact lt_asymm h h₂
 end
+
+/-- Generate a linear order structure from a preorder and `cmp` function. -/
+def linear_order_of_compares [preorder α] (cmp : α → α → ordering)
+  (h : ∀ a b, (cmp a b).compares a b) :
+  linear_order α :=
+{ le_antisymm := λ a b, (h a b).le_antisymm,
+  le_total := λ a b, (h a b).le_total,
+  decidable_le := λ a b, decidable_of_iff _ (h a b).ne_gt,
+  decidable_lt := λ a b, decidable_of_iff _ (h a b).eq_lt,
+  decidable_eq := λ a b, decidable_of_iff _ (h a b).eq_eq,
+  .. ‹preorder α› }

src/algebra/order_functions.lean

@@ -9,7 +9,7 @@ import order.lattice
 /-!
 # `max` and `min`
 
-This file proves basic properties about maxima and minima on a `decidable_linear_order`.
+This file proves basic properties about maxima and minima on a `linear_order`.
 
 ## Tags
 
@@ -22,7 +22,7 @@ variables {α : Type u} {β : Type v}
 attribute [simp] max_eq_left max_eq_right min_eq_left min_eq_right
 
 section
-variables [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b c d : α}
+variables [linear_order α] [linear_order β] {f : α → β} {a b c d : α}
 
 -- translate from lattices to linear orders (sup → max, inf → min)
 @[simp] lemma le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b := le_inf_iff

src/algebra/ordered_field.lean

@@ -14,8 +14,6 @@ import algebra.field
 
   ### Main Definitions
   * `linear_ordered_field`: the class of linear ordered fields.
-  * `discrete_linear_ordered_field`: the class of linear ordered fields where the inequality is
-    decidable.
 -/
 
 set_option old_structure_cmd true
@@ -593,16 +591,6 @@ lemma mul_self_inj_of_nonneg (a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a
 mul_self_eq_mul_self_iff.trans $ or_iff_left_of_imp $
   λ h, by { subst a, have : b = 0 := le_antisymm (neg_nonneg.1 a0) b0, rw [this, neg_zero] }
 
-end linear_ordered_field
-
-/-- A discrete linear ordered field is a field with a decidable linear order respecting the
-  operations. -/
-@[protect_proj] class discrete_linear_ordered_field (α : Type*)
-  extends linear_ordered_field α, decidable_linear_ordered_comm_ring α
-
-section discrete_linear_ordered_field
-variables [discrete_linear_ordered_field α]
-
 lemma min_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : min (a / c) (b / c) = (min a b) / c :=
 eq.symm $ monotone.map_min (λ x y, div_le_div_of_le hc)
 
@@ -626,4 +614,4 @@ by rw [abs_div, abs_of_nonneg (zero_le_one : 1 ≥ (0 : α))]
 lemma abs_inv (a : α) : abs a⁻¹ = (abs a)⁻¹ :=
 by rw [inv_eq_one_div, abs_one_div, inv_eq_one_div]
 
-end discrete_linear_ordered_field
+end linear_ordered_field