refactor(algebra/order/ring): Make strict_ordered_semirings nontriv…

…ial (#17394)

`strict_ordered_semiring` + `nontrivial` implies `char_zero`, but this can't be instance because `char_zero` implies `nontrivial`

Instead of waiting for Lean 4, where such looping instances are possible, we make all `strict_ordered_semiring`s nontrivial, because we don't care about types with one element being`strict_ordered_semiring`s.

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

@@ -140,7 +140,8 @@ instance socsN2 : strict_ordered_comm_semiring (ℕ × zmod 2) :=
   mul_lt_mul_of_pos_right := mul_lt_mul_of_pos_right,
   ..Nxzmod_2.csrN2_1,
   ..(infer_instance : partial_order (ℕ × zmod 2)),
-  ..(infer_instance : comm_semiring (ℕ × zmod 2)) }
+  ..(infer_instance : comm_semiring (ℕ × zmod 2)),
+  ..pullback_nonzero prod.fst prod.fst_zero prod.fst_one }
 
 end Nxzmod_2
 

src/algebra/geom_sum.lean

@@ -409,7 +409,7 @@ section order
 
 variables {n : ℕ} {x : α}
 
-lemma geom_sum_pos [strict_ordered_semiring α] [nontrivial α] (hx : 0 ≤ x) (hn : n ≠ 0) :
+lemma geom_sum_pos [strict_ordered_semiring α] (hx : 0 ≤ x) (hn : n ≠ 0) :
   0 < ∑ i in range n, x ^ i :=
 sum_pos' (λ k hk, pow_nonneg hx _) ⟨0, mem_range.2 hn.bot_lt, by simp⟩
 

src/algebra/order/archimedean.lean

@@ -83,8 +83,7 @@ lemma exists_unique_add_zsmul_mem_Ioc {a : α} (ha : 0 < a) (b c : α) :
 
 end linear_ordered_add_comm_group
 
-theorem exists_nat_gt [strict_ordered_semiring α] [nontrivial α] [archimedean α]
-  (x : α) : ∃ n : ℕ, x < n :=
+theorem exists_nat_gt [strict_ordered_semiring α] [archimedean α] (x : α) : ∃ n : ℕ, x < n :=
 let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
 ⟨n+1, lt_of_le_of_lt (by rwa ← nsmul_one)
   (nat.cast_lt.2 (nat.lt_succ_self _))⟩
@@ -96,8 +95,8 @@ begin
   exact (exists_nat_gt x).imp (λ n, le_of_lt)
 end
 
-lemma add_one_pow_unbounded_of_pos [strict_ordered_semiring α] [nontrivial α] [archimedean α]
-  (x : α) {y : α} (hy : 0 < y) :
+lemma add_one_pow_unbounded_of_pos [strict_ordered_semiring α] [archimedean α] (x : α) {y : α}
+  (hy : 0 < y) :
   ∃ n : ℕ, x < (y + 1) ^ n :=
 have 0 ≤ 1 + y, from add_nonneg zero_le_one hy.le,
 let ⟨n, h⟩ := archimedean.arch x hy in
@@ -109,7 +108,7 @@ let ⟨n, h⟩ := archimedean.arch x hy in
        ... = (y + 1) ^ n : by rw [add_comm]⟩
 
 section strict_ordered_ring
-variables [strict_ordered_ring α] [nontrivial α] [archimedean α]
+variables [strict_ordered_ring α] [archimedean α]
 
 lemma pow_unbounded_of_one_lt (x : α) {y : α} (hy1 : 1 < y) :
   ∃ n : ℕ, x < y ^ n :=
@@ -270,7 +269,7 @@ section linear_ordered_field
 variables [linear_ordered_field α]
 
 lemma archimedean_iff_nat_lt : archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
-⟨@exists_nat_gt α _ _, λ H, ⟨λ x y y0,
+⟨@exists_nat_gt α _, λ H, ⟨λ x y y0,
   (H (x / y)).imp $ λ n h, le_of_lt $
   by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩
 
@@ -281,7 +280,7 @@ archimedean_iff_nat_lt.trans
    lt_of_le_of_lt h (nat.cast_lt.2 (lt_add_one _))⟩⟩
 
 lemma archimedean_iff_int_lt : archimedean α ↔ ∀ x : α, ∃ n : ℤ, x < n :=
-⟨@exists_int_gt α _ _,
+⟨@exists_int_gt α _,
 begin
   rw archimedean_iff_nat_lt,
   intros h x,

src/algebra/order/ring/cone.lean

@@ -14,6 +14,8 @@ import algebra.order.ring.defs
 
 set_option old_structure_cmd true
 
+variables {α : Type*} [ring α] [nontrivial α]
+
 namespace ring
 
 /-- A positive cone in a ring consists of a positive cone in underlying `add_comm_group`,
@@ -26,27 +28,28 @@ structure positive_cone (α : Type*) [ring α] extends add_comm_group.positive_c
 /-- Forget that a positive cone in a ring respects the multiplicative structure. -/
 add_decl_doc positive_cone.to_positive_cone
 
-/-- A positive cone in a ring induces a linear order if `1` is a positive element. -/
+/-- A total positive cone in a nontrivial ring induces a linear order. -/
 @[nolint has_nonempty_instance]
 structure total_positive_cone (α : Type*) [ring α]
-  extends positive_cone α, add_comm_group.total_positive_cone α :=
-(one_pos : pos 1)
+  extends positive_cone α, add_comm_group.total_positive_cone α
 
 /-- Forget that a `total_positive_cone` in a ring is total. -/
 add_decl_doc total_positive_cone.to_positive_cone
 
 /-- Forget that a `total_positive_cone` in a ring respects the multiplicative structure. -/
 add_decl_doc total_positive_cone.to_total_positive_cone
 
-end ring
+lemma positive_cone.one_pos (C : positive_cone α) : C.pos 1 :=
+(C.pos_iff _).2 ⟨C.one_nonneg, λ h, one_ne_zero $ C.nonneg_antisymm C.one_nonneg h⟩
 
-namespace strict_ordered_ring
+end ring
 
 open ring
 
 /-- Construct a `strict_ordered_ring` by designating a positive cone in an existing `ring`. -/
-def mk_of_positive_cone {α : Type*} [ring α] (C : positive_cone α) : strict_ordered_ring α :=
-{ zero_le_one := by { change C.nonneg (1 - 0), convert C.one_nonneg, simp, },
+def strict_ordered_ring.mk_of_positive_cone (C : positive_cone α) : strict_ordered_ring α :=
+{ exists_pair_ne := ⟨0, 1, λ h, by simpa [←h, C.pos_iff] using C.one_pos⟩,
+  zero_le_one := by { change C.nonneg (1 - 0), convert C.one_nonneg, simp, },
   mul_pos := λ x y xp yp, begin
     change C.pos (x*y - 0),
     convert C.mul_pos x y (by { convert xp, simp, }) (by { convert yp, simp, }),
@@ -55,23 +58,8 @@ def mk_of_positive_cone {α : Type*} [ring α] (C : positive_cone α) : strict_o
   ..‹ring α›,
   ..ordered_add_comm_group.mk_of_positive_cone C.to_positive_cone }
 
-end strict_ordered_ring
-
-namespace linear_ordered_ring
-
-open ring
-
 /-- Construct a `linear_ordered_ring` by
 designating a positive cone in an existing `ring`. -/
-def mk_of_positive_cone {α : Type*} [ring α] (C : total_positive_cone α) :
-  linear_ordered_ring α :=
-{ exists_pair_ne := ⟨0, 1, begin
-    intro h,
-    have one_pos := C.one_pos,
-    rw [←h, C.pos_iff] at one_pos,
-    simpa using one_pos,
-  end⟩,
-  ..strict_ordered_ring.mk_of_positive_cone C.to_positive_cone,
+def linear_ordered_ring.mk_of_positive_cone (C : total_positive_cone α) : linear_ordered_ring α :=
+{ ..strict_ordered_ring.mk_of_positive_cone C.to_positive_cone,
   ..linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone, }
-
-end linear_ordered_ring

src/algebra/order/ring/defs.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Yaël Dillies
 -/
 import order.min_max
 import algebra.order.monoid.cancel.defs
@@ -29,21 +29,23 @@ For short,
 ## Typeclasses
 
 * `ordered_semiring`: Semiring with a partial order such that `+` and `*` respect `≤`.
-* `strict_ordered_semiring`: Semiring with a partial order such that `+` and `*` respects `<`.
+* `strict_ordered_semiring`: Nontrivial semiring with a partial order such that `+` and `*` respects
+  `<`.
 * `ordered_comm_semiring`: Commutative semiring with a partial order such that `+` and `*` respect
   `≤`.
-* `strict_ordered_comm_semiring`: Commutative semiring with a partial order such that `+` and `*`
-  respect `<`.
+* `strict_ordered_comm_semiring`: Nontrivial commutative semiring with a partial order such that `+`
+  and `*` respect `<`.
 * `ordered_ring`: Ring with a partial order such that `+` respects `≤` and `*` respects `<`.
 * `ordered_comm_ring`: Commutative ring with a partial order such that `+` respects `≤` and
   `*` respects `<`.
-* `linear_ordered_semiring`: Semiring with a linear order such that `+` respects `≤` and
+* `linear_ordered_semiring`: Nontrivial semiring with a linear order such that `+` respects `≤` and
   `*` respects `<`.
-* `linear_ordered_comm_semiring`: Commutative semiring with a linear order such that `+` respects
+* `linear_ordered_comm_semiring`: Nontrivial commutative semiring with a linear order such that `+`
+  respects `≤` and `*` respects `<`.
+* `linear_ordered_ring`: Nontrivial ring with a linear order such that `+` respects `≤` and `*`
+  respects `<`.
+* `linear_ordered_comm_ring`: Nontrivial commutative ring with a linear order such that `+` respects
   `≤` and `*` respects `<`.
-* `linear_ordered_ring`: Ring with a linear order such that `+` respects `≤` and `*` respects `<`.
-* `linear_ordered_comm_ring`: Commutative ring with a linear order such that `+` respects `≤` and
-  `*` respects `<`.
 * `canonically_ordered_comm_semiring`: Commutative semiring with a partial order such that `+`
   respects `≤`, `*` respects `<`, and `a ≤ b ↔ ∃ c, b = a + c`.
 
@@ -57,35 +59,42 @@ immediate predecessors and what conditions are added to each of them.
   - `ordered_add_comm_monoid` & multiplication & `*` respects `≤`
   - `semiring` & partial order structure & `+` respects `≤` & `*` respects `≤`
 * `strict_ordered_semiring`
-  - `ordered_cancel_add_comm_monoid` & multiplication & `*` respects `<`
-  - `ordered_semiring` & `+` respects `<` & `*` respects `<`
+  - `ordered_cancel_add_comm_monoid` & multiplication & `*` respects `<` & nontriviality
+  - `ordered_semiring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `ordered_comm_semiring`
   - `ordered_semiring` & commutativity of multiplication
   - `comm_semiring` & partial order structure & `+` respects `≤` & `*` respects `<`
 * `strict_ordered_comm_semiring`
   - `strict_ordered_semiring` & commutativity of multiplication
-  - `ordered_comm_semiring` & `+` respects `<` & `*` respects `<`
+  - `ordered_comm_semiring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `ordered_ring`
-  - `strict_ordered_semiring` & additive inverses
+  - `ordered_semiring` & additive inverses
   - `ordered_add_comm_group` & multiplication & `*` respects `<`
   - `ring` & partial order structure & `+` respects `≤` & `*` respects `<`
+* `strict_ordered_ring`
+  - `strict_ordered_semiring` & additive inverses
+  - `ordered_semiring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `ordered_comm_ring`
   - `ordered_ring` & commutativity of multiplication
   - `ordered_comm_semiring` & additive inverses
   - `comm_ring` & partial order structure & `+` respects `≤` & `*` respects `<`
+* `strict_ordered_comm_ring`
+  - `strict_ordered_comm_semiring` & additive inverses
+  - `strict_ordered_ring` & commutativity of multiplication
+  - `ordered_comm_ring` & `+` respects `<` & `*` respects `<` & nontriviality
 * `linear_ordered_semiring`
-  - `strict_ordered_semiring` & totality of the order & nontriviality
+  - `strict_ordered_semiring` & totality of the order
   - `linear_ordered_add_comm_monoid` & multiplication & nontriviality & `*` respects `<`
 * `linear_ordered_comm_semiring`
-  - `strict_ordered_comm_semiring` & totality of the order & nontriviality
+  - `strict_ordered_comm_semiring` & totality of the order
   - `linear_ordered_semiring` & commutativity of multiplication
 * `linear_ordered_ring`
-  - `ordered_ring` & totality of the order & nontriviality
+  - `strict_ordered_ring` & totality of the order
   - `linear_ordered_semiring` & additive inverses
   - `linear_ordered_add_comm_group` & multiplication & `*` respects `<`
   - `domain` & linear order structure
 * `linear_ordered_comm_ring`
-  - `ordered_comm_ring` & totality of the order & nontriviality
+  - `strict_ordered_comm_ring` & totality of the order
   - `linear_ordered_ring` & commutativity of multiplication
   - `linear_ordered_comm_semiring` & additive inverses
   - `is_domain` & linear order structure
@@ -133,10 +142,11 @@ and multiplication by a nonnegative number is monotone. -/
 @[protect_proj, ancestor ordered_ring comm_ring]
 class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α
 
-/-- A `strict_ordered_semiring` is a semiring with a partial order such that addition is strictly
-monotone and multiplication by a positive number is strictly monotone. -/
-@[protect_proj, ancestor semiring ordered_cancel_add_comm_monoid]
-class strict_ordered_semiring (α : Type u) extends semiring α, ordered_cancel_add_comm_monoid α :=
+/-- A `strict_ordered_semiring` is a nontrivial semiring with a partial order such that addition is
+strictly monotone and multiplication by a positive number is strictly monotone. -/
+@[protect_proj, ancestor semiring ordered_cancel_add_comm_monoid nontrivial]
+class strict_ordered_semiring (α : Type u)
+  extends semiring α, ordered_cancel_add_comm_monoid α, nontrivial α :=
 (zero_le_one : (0 : α) ≤ 1)
 (mul_lt_mul_of_pos_left  : ∀ a b c : α, a < b → 0 < c → c * a < c * b)
 (mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
@@ -148,8 +158,8 @@ class strict_ordered_comm_semiring (α : Type u) extends strict_ordered_semiring
 
 /-- A `strict_ordered_ring` is a ring with a partial order such that addition is strictly monotone
 and multiplication by a positive number is strictly monotone. -/
-@[protect_proj, ancestor ring ordered_add_comm_group]
-class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
+@[protect_proj, ancestor ring ordered_add_comm_group nontrivial]
+class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α, nontrivial α :=
 (zero_le_one : 0 ≤ (1 : α))
 (mul_pos     : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
 
@@ -165,7 +175,7 @@ explore changing this, but be warned that the instances involving `domain` may c
 search loops. -/
 @[protect_proj, ancestor strict_ordered_semiring linear_ordered_add_comm_monoid nontrivial]
 class linear_ordered_semiring (α : Type u)
-  extends strict_ordered_semiring α, linear_ordered_add_comm_monoid α, nontrivial α
+  extends strict_ordered_semiring α, linear_ordered_add_comm_monoid α
 
 /-- A `linear_ordered_comm_semiring` is a nontrivial commutative semiring with a linear order such
 that addition is monotone and multiplication by a positive number is strictly monotone. -/
@@ -175,8 +185,8 @@ class linear_ordered_comm_semiring (α : Type*)
 
 /-- A `linear_ordered_ring` is a ring with a linear order such that addition is monotone and
 multiplication by a positive number is strictly monotone. -/
-@[protect_proj, ancestor strict_ordered_ring linear_order nontrivial]
-class linear_ordered_ring (α : Type u) extends strict_ordered_ring α, linear_order α, nontrivial α
+@[protect_proj, ancestor strict_ordered_ring linear_order]
+class linear_ordered_ring (α : Type u) extends strict_ordered_ring α, linear_order α
 
 /-- A `linear_ordered_comm_ring` is a commutative ring with a linear order such that addition is
 monotone and multiplication by a positive number is strictly monotone. -/
@@ -518,29 +528,17 @@ lemma strict_mono.mul (hf : strict_mono f) (hg : strict_mono g) (hf₀ : ∀ x,
 
 end monotone
 
-section nontrivial
-variables [nontrivial α]
-
 lemma lt_one_add (a : α) : a < 1 + a := lt_add_of_pos_left _ zero_lt_one
 lemma lt_add_one (a : α) : a < a + 1 := lt_add_of_pos_right _ zero_lt_one
 
 lemma one_lt_two : (1 : α) < 2 := lt_add_one _
 
 lemma lt_two_mul_self (ha : 0 < a) : a < 2 * a := lt_mul_of_one_lt_left ha one_lt_two
 
-lemma nat.strict_mono_cast : strict_mono (coe : ℕ → α) :=
-strict_mono_nat_of_lt_succ $ λ n, by { rw [nat.cast_succ], apply lt_add_one }
-
-/-- `coe : ℕ → α` as an `order_embedding` -/
-@[simps { fully_applied := ff }] def nat.cast_order_embedding : ℕ ↪o α :=
-order_embedding.of_strict_mono coe nat.strict_mono_cast
-
 @[priority 100] -- see Note [lower instance priority]
 instance strict_ordered_semiring.to_no_max_order : no_max_order α :=
 ⟨λ a, ⟨a + 1, lt_add_of_pos_right _ one_pos⟩⟩
 
-end nontrivial
-
 end strict_ordered_semiring
 
 section strict_ordered_comm_semiring

src/algebra/order/ring/inj_surj.lean

@@ -90,7 +90,8 @@ protected def strict_ordered_semiring [strict_ordered_semiring α] [has_zero β]
   mul_lt_mul_of_pos_right := λ a b c h hc, show f (a * c) < f (b * c),
     by simpa only [mul, zero] using mul_lt_mul_of_pos_right ‹f a < f b› (by rwa ←zero),
   ..hf.ordered_cancel_add_comm_monoid f zero add nsmul,
-  ..hf.ordered_semiring f zero one add mul nsmul npow nat_cast }
+  ..hf.ordered_semiring f zero one add mul nsmul npow nat_cast,
+  ..pullback_nonzero f zero one }
 
 /-- Pullback a `strict_ordered_comm_semiring` under an injective map. -/
 @[reducible] -- See note [reducible non-instances]
@@ -143,7 +144,6 @@ protected def linear_ordered_semiring [linear_ordered_semiring α] [has_zero β]
   (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
   linear_ordered_semiring β :=
 { .. linear_order.lift f hf hsup hinf,
-  .. pullback_nonzero f zero one,
   .. hf.strict_ordered_semiring f zero one add mul nsmul npow nat_cast }
 
 /-- Pullback a `linear_ordered_semiring` under an injective map. -/
@@ -172,7 +172,6 @@ def linear_ordered_ring [linear_ordered_ring α] [has_zero β] [has_one β] [has
   (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
   linear_ordered_ring β :=
 { .. linear_order.lift f hf hsup hinf,
-  .. pullback_nonzero f zero one,
   .. hf.strict_ordered_ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }
 
 /-- Pullback a `linear_ordered_comm_ring` under an injective map. -/
@@ -188,7 +187,6 @@ protected def linear_ordered_comm_ring [linear_ordered_comm_ring α] [has_zero 
   (hsup : ∀ x y, f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ x y, f (x ⊓ y) = min (f x) (f y)) :
   linear_ordered_comm_ring β :=
 { .. linear_order.lift f hf hsup hinf,
-  .. pullback_nonzero f zero one,
   .. hf.strict_ordered_comm_ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }
 
 end function.injective

src/algebra/order/ring/nontrivial.lean

@@ -7,25 +7,12 @@ import algebra.char_zero.defs
 import algebra.order.ring.defs
 
 /-!
-# Nontrivial strict ordered semirings (and hence linear ordered semirings) are characteristic zero.
+# Strict ordered semiring have characteristic zero
 -/
 
 variables {α : Type*}
 
-section strict_ordered_semiring
-variables [strict_ordered_semiring α] [nontrivial α]
-
-/-- Note this is not an instance as `char_zero` implies `nontrivial`, and this would risk forming a
-loop. -/
-lemma strict_ordered_semiring.to_char_zero : char_zero α := ⟨nat.strict_mono_cast.injective⟩
-
-end strict_ordered_semiring
-
-section linear_ordered_semiring
-variables [linear_ordered_semiring α]
-
 @[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_semiring.to_char_zero : char_zero α :=
-strict_ordered_semiring.to_char_zero
-
-end linear_ordered_semiring
+instance strict_ordered_semiring.to_char_zero [strict_ordered_semiring α] : char_zero α :=
+⟨strict_mono.injective $ strict_mono_nat_of_lt_succ $ λ n,
+  by { rw [nat.cast_succ], apply lt_add_one }⟩

src/analysis/box_integral/box/subbox_induction.lean

@@ -147,7 +147,7 @@ begin
   { suffices : tendsto (λ m, (J m).upper - (J m).lower) at_top (𝓝 0), by simpa using hJlz.add this,
     refine tendsto_pi_nhds.2 (λ i, _),
     simpa [hJsub] using tendsto_const_nhds.div_at_top
-      (tendsto_pow_at_top_at_top_of_one_lt (@one_lt_two ℝ _ _)) },
+      (tendsto_pow_at_top_at_top_of_one_lt $ @one_lt_two ℝ _) },
   replace hJlz : tendsto (λ m, (J m).lower) at_top (𝓝[Icc I.lower I.upper] z),
     from tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _ hJlz
       (eventually_of_forall hJl_mem),