Commit 2022-10-08 09:14 f5a600f8
View on Github →feat(algebra/order/ring): Non-cancellative ordered semirings (#16172)
Historical background
This tackles a problem that we have had for six years (#2697 for its move to mathlib, before it was in core): ordered_semiring
assumes that addition and multiplication are strictly monotone.
This led to weirdness within the algebraic order hierarchy:
ennreal
/ereal
/enat
needed custom lemmas (∞ + 0 = ∞ = ∞ + 1
,1 * ∞ = ∞ = 2 * ∞
).- A
canonically_ordered_comm_semiring
was not anordered_comm_semiring
!
What this PR does
This PR solves the problem minimally by renaming ordered_(comm_)semiring
to strict_ordered_(comm_)semiring
and adding a new class ordered_(comm_)semiring
that doesn't assume strict monotonicity of addition and multiplication but only monotonicity:
class ordered_semiring (α : Type*) extends semiring α, ordered_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_le_mul_of_nonneg_left : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b)
(mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c)
class ordered_comm_semiring (α : Type*) extends ordered_semiring α, comm_semiring α
class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b)
class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α
class strict_ordered_semiring (α : Type*) extends semiring α, ordered_cancel_add_comm_monoid α :=
(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)
class strict_ordered_comm_semiring (α : Type*) extends strict_ordered_semiring α, comm_semiring α
class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
class strict_ordered_comm_ring (α : Type*) extends strict_ordered_ring α, comm_ring α
Whatever happened to the decidable
lemmas?
Scrolling through the diff, you will see that only one lemma in the decidable
namespace out of many survives this PR. Those lemmas were originally meant to avoid using choice in the proof of nat
and int
lemmas.
The need for decidability originated from the proofs of mul_le_mul_of_nonneg_left
/mul_le_mul_of_nonneg_right
.
protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)]
(h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
begin
by_cases ba : b ≤ a, { simp [ba.antisymm h₁] },
by_cases c0 : c ≤ 0, { simp [c0.antisymm h₂] },
exact (mul_lt_mul_of_pos_left (h₁.lt_of_not_le ba) (h₂.lt_of_not_le c0)).le,
end
Now that these are fields to ordered_semiring
, they are already choice-free. Instead, choice is now used in showing that an ordered_cancel_semiring
is an ordered_semiring
.
@[priority 100] -- see Note [lower instance priority]
instance ordered_cancel_semiring.to_ordered_semiring : ordered_semiring α :=
{ mul_le_mul_of_nonneg_left := λ a b c hab hc, begin
obtain rfl | hab := hab.eq_or_lt,
{ refl },
obtain rfl | hc := hc.eq_or_lt,
{ simp },
{ exact (mul_lt_mul_of_pos_left hab hc).le }
end,
mul_le_mul_of_nonneg_right := λ a b c hab hc, begin
obtain rfl | hab := hab.eq_or_lt,
{ refl },
obtain rfl | hc := hc.eq_or_lt,
{ simp },
{ exact (mul_lt_mul_of_pos_right hab hc).le }
end,
..‹ordered_cancel_semiring α› }
It seems unreasonable to make that instance depend on @decidable_rel α (≤)
even though it's only needed for the proofs.
Other changes
To have some lemmas in the generality of the new ordered_semiring
, I needed a few new lemmas:
bit0_mono
bit0_strict_mono
It was also simpler to golfanalysis.special_functions.stirling
usingpositivity
rather than fixing it so I introduce the following (simple)positivity
extensions:positivity_succ
positivity_factorial
positivity_asc_factorial