Ordered rings and semirings #
This file develops the basics of ordered (semi)rings.
Each typeclass here comprises
- an algebraic class (
Semiring
,CommSemiring
,Ring
,CommRing
) - an order class (
PartialOrder
,LinearOrder
) - assumptions on how both interact ((strict) monotonicity, canonicity)
For short,
- "
+
respects≤
" means "monotonicity of addition" - "
+
respects<
" means "strict monotonicity of addition" - "
*
respects≤
" means "monotonicity of multiplication by a nonnegative number". - "
*
respects<
" means "strict monotonicity of multiplication by a positive number".
Typeclasses #
OrderedSemiring
: Semiring with a partial order such that+
and*
respect≤
.StrictOrderedSemiring
: Nontrivial semiring with a partial order such that+
and*
respects<
.OrderedCommSemiring
: Commutative semiring with a partial order such that+
and*
respect≤
.StrictOrderedCommSemiring
: Nontrivial commutative semiring with a partial order such that+
and*
respect<
.OrderedRing
: Ring with a partial order such that+
respects≤
and*
respects<
.OrderedCommRing
: Commutative ring with a partial order such that+
respects≤
and*
respects<
.LinearOrderedSemiring
: Nontrivial semiring with a linear order such that+
respects≤
and*
respects<
.LinearOrderedCommSemiring
: Nontrivial commutative semiring with a linear order such that+
respects≤
and*
respects<
.LinearOrderedRing
: Nontrivial ring with a linear order such that+
respects≤
and*
respects<
.LinearOrderedCommRing
: Nontrivial commutative ring with a linear order such that+
respects≤
and*
respects<
.CanonicallyOrderedCommSemiring
: Commutative semiring with a partial order such that+
respects≤
,*
respects<
, anda ≤ b ↔ ∃ c, b = a + c
.
Hierarchy #
The hardest part of proving order lemmas might be to figure out the correct generality and its corresponding typeclass. Here's an attempt at demystifying it. For each typeclass, we list its immediate predecessors and what conditions are added to each of them.
OrderedSemiring
OrderedAddCommMonoid
& multiplication &*
respects≤
Semiring
& partial order structure &+
respects≤
&*
respects≤
StrictOrderedSemiring
OrderedCancelAddCommMonoid
& multiplication &*
respects<
& nontrivialityOrderedSemiring
&+
respects<
&*
respects<
& nontriviality
OrderedCommSemiring
OrderedSemiring
& commutativity of multiplicationCommSemiring
& partial order structure &+
respects≤
&*
respects<
StrictOrderedCommSemiring
StrictOrderedSemiring
& commutativity of multiplicationOrderedCommSemiring
&+
respects<
&*
respects<
& nontriviality
OrderedRing
OrderedSemiring
& additive inversesOrderedAddCommGroup
& multiplication &*
respects<
Ring
& partial order structure &+
respects≤
&*
respects<
StrictOrderedRing
StrictOrderedSemiring
& additive inversesOrderedSemiring
&+
respects<
&*
respects<
& nontriviality
OrderedCommRing
OrderedRing
& commutativity of multiplicationOrderedCommSemiring
& additive inversesCommRing
& partial order structure &+
respects≤
&*
respects<
StrictOrderedCommRing
StrictOrderedCommSemiring
& additive inversesStrictOrderedRing
& commutativity of multiplicationOrderedCommRing
&+
respects<
&*
respects<
& nontriviality
LinearOrderedSemiring
StrictOrderedSemiring
& totality of the orderLinearOrderedAddCommMonoid
& multiplication & nontriviality &*
respects<
LinearOrderedCommSemiring
StrictOrderedCommSemiring
& totality of the orderLinearOrderedSemiring
& commutativity of multiplication
LinearOrderedRing
StrictOrderedRing
& totality of the orderLinearOrderedSemiring
& additive inversesLinearOrderedAddCommGroup
& multiplication &*
respects<
Domain
& linear order structure
LinearOrderedCommRing
StrictOrderedCommRing
& totality of the orderLinearOrderedRing
& commutativity of multiplicationLinearOrderedCommSemiring
& additive inversesIsDomain
& linear order structure
Note that OrderDual
does not satisfy any of the ordered ring typeclasses due to the
zero_le_one
field.
Addition is monotone in an
OrderedAddCommMonoid
.0 ≤ 1
in any ordered semiring.zero_le_one : 0 ≤ 1In an ordered semiring, we can multiply an inequality
a ≤ b
on the left by a non-negative element0 ≤ c
to obtainc * a ≤ c * b
.In an ordered semiring, we can multiply an inequality
a ≤ b
on the right by a non-negative element0 ≤ c
to obtaina * c ≤ b * c
.
An OrderedSemiring
is a semiring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone.
Instances
Multiplication is commutative in a commutative semigroup.
An OrderedCommSemiring
is a commutative semiring with a partial order such that addition is
monotone and multiplication by a nonnegative number is monotone.
Instances
Addition is monotone in a ordered additive commutative group.
0 ≤ 1
in any ordered ring.zero_le_one : 0 ≤ 1The product of non-negative elements is non-negative.
An OrderedRing
is a ring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone.
Instances
Multiplication is commutative in a commutative semigroup.
An OrderedCommRing
is a commutative ring with a partial order such that addition is monotone
and multiplication by a nonnegative number is monotone.
Instances
Additive cancellation is compatible with the order in an ordered cancellative additive commutative monoid.
- toNontrivial : Nontrivial α
In a strict ordered semiring,
0 ≤ 1
.zero_le_one : 0 ≤ 1Left multiplication by a positive element is strictly monotone.
Right multiplication by a positive element is strictly monotone.
A StrictOrderedSemiring
is a nontrivial semiring with a partial order such that addition is
strictly monotone and multiplication by a positive number is strictly monotone.
Instances
Multiplication is commutative in a commutative semigroup.
A StrictOrderedCommSemiring
is a commutative semiring with a partial order such that
addition is strictly monotone and multiplication by a positive number is strictly monotone.
Instances
- toNontrivial : Nontrivial α
In a strict ordered ring,
0 ≤ 1
.zero_le_one : 0 ≤ 1The product of two positive elements is positive.
A StrictOrderedRing
is a ring with a partial order such that addition is strictly monotone
and multiplication by a positive number is strictly monotone.
Instances
Multiplication is commutative in a commutative semigroup.
A StrictOrderedCommRing
is a commutative ring with a partial order such that addition is
strictly monotone and multiplication by a positive number is strictly monotone.
Instances
A linear order is total.
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq αIn a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1The minimum function is equivalent to the one you get from
minOfLe
.The minimum function is equivalent to the one you get from
maxOfLe
.Comparison via
compare
is equal to the canonical comparison given decidable<
and=
.compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝
A LinearOrderedSemiring
is a nontrivial semiring with a linear order such that
addition is monotone and multiplication by a positive number is strictly monotone.
Instances
A linear order is total.
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq αIn a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1The minimum function is equivalent to the one you get from
minOfLe
.The minimum function is equivalent to the one you get from
maxOfLe
.Comparison via
compare
is equal to the canonical comparison given decidable<
and=
.compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝
A LinearOrderedCommSemiring
is a nontrivial commutative semiring with a linear order such
that addition is monotone and multiplication by a positive number is strictly monotone.
Instances
A linear order is total.
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq αIn a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1The minimum function is equivalent to the one you get from
minOfLe
.The minimum function is equivalent to the one you get from
maxOfLe
.Comparison via
compare
is equal to the canonical comparison given decidable<
and=
.compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝
A LinearOrderedRing
is a ring with a linear order such that addition is monotone and
multiplication by a positive number is strictly monotone.
Instances
Multiplication is commutative in a commutative semigroup.
A LinearOrderedCommRing
is a commutative ring with a linear order such that addition is
monotone and multiplication by a positive number is strictly monotone.
Instances
Alias of one_lt_mul_of_le_of_lt
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderedCommRing.toOrderedCommSemiring = let src := OrderedRing.toOrderedSemiring; let src_1 := inst; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
A choice-free version of StrictOrderedSemiring.toOrderedSemiring
to avoid using choice in
basic Nat
lemmas.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A choice-free version of StrictOrderedCommSemiring.toOrderedCommSemiring'
to avoid using
choice in basic Nat
lemmas.
Equations
- StrictOrderedCommSemiring.toOrderedCommSemiring' = let src := inst; let src_1 := StrictOrderedSemiring.toOrderedSemiring'; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- StrictOrderedCommSemiring.toOrderedCommSemiring = let src := inst; let src_1 := StrictOrderedSemiring.toOrderedSemiring; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- One or more equations did not get rendered due to their size.
A choice-free version of StrictOrderedRing.toOrderedRing
to avoid using choice in basic
Int
lemmas.
Equations
- One or more equations did not get rendered due to their size.
A choice-free version of StrictOrderedCommRing.toOrderedCommRing
to avoid using
choice in basic Int
lemmas.
Equations
- StrictOrderedCommRing.toOrderedCommRing' = let src := inst; let src_1 := StrictOrderedRing.toOrderedRing'; OrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- StrictOrderedCommRing.toStrictOrderedCommSemiring = let src := inst; let src_1 := StrictOrderedRing.toStrictOrderedSemiring; StrictOrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- StrictOrderedCommRing.toOrderedCommRing = let src := inst; let src_1 := StrictOrderedRing.toOrderedRing; OrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Out of three elements of a LinearOrderedRing
, two must have the same sign.
Equations
- LinearOrderedCommRing.toStrictOrderedCommRing = StrictOrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
- One or more equations did not get rendered due to their size.