Semirings with monus

This file defines semirings with monus and introduces their main properties.

Many semirings relevant for provenance can be equipped with a monus - operator, resulting in what is called a semiring with monus, or m-semiring. This is standard in semiring theory [Ame84] and was introduced in the setting of provenance semirings by Geerts and Poggi [GP10]. The class is the algebraic structure underlying the annotated query semantics of Section IV-A of Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data (Definition 5).

References

• Amer, Equationally complete classes of commutative monoids with monus
• Geerts & Poggi, On database query languages for K-relations
• Sen, Maniu & Senellart, ProvSQL (Definition 5)

Definition of a SemiringWithMonus

class SemiringWithMonus (α : Type) extends Semiring α, PartialOrder α, IsOrderedAddMonoid α, CanonicallyOrderedAdd α, Sub α : Type

A SemiringWithMonus is a naturally ordered semiring with a monus operation that is compatible with the natural order. We do not require the semiring to be necessarily commutative.

In addition to monus, the class carries a δ : α → α operator subject to three axioms (delta_zero, delta_natCast_pos, and delta_absorb). This is the duplicate-eliminating support operator used to interpret aggregation in the framework of Amsterdamer, Deutch & Tannen, Provenance for aggregate queries, mirroring ProvSQL's Semiring::delta.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : α) : (n + 1) • x = n • x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• npow : ℕ → α → α
• npow_zero (x : α) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : α) : x ^ (n + 1) = x ^ n * x
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c
• le_add_self (a b : α) : a ≤ b + a
• le_self_add (a b : α) : a ≤ a + b
• sub : α → α → α
• monus_spec (a b c : α) : a - b ≤ c ↔ a ≤ b + c
• delta : α → α

  Duplicate-eliminating support operator. Sends 0 to 0 and any positive integer iterate of 1 to 1.

• delta_zero : delta 0 = 0

  δ sends 0 to 0.

• delta_natCast_pos {n : ℕ} : 0 < n → delta ↑n = 1

  δ sends every positive integer iterate of 1 (i.e., every positive natural-number cast) to 1.

• delta_absorb (a b : α) : a * delta (a + b) = a

  A δ-guard is absorbed by any multiple of one of its summands: a ⊗ δ(a ⊕ b) = a. This is what makes a group-existence factor redundant next to any provenance that already contains an occurrence of the group: δ really acts as “the group exists” and nothing more. Both usual choices of δ satisfy it in their natural habitat: the indicator (δ x = 𝟙 for x ≠ 𝟘) in any canonically ordered semiring (delta_absorb_indicator), and the identity in lattice-like semirings, where it is absorption a ⊓ (a ⊔ b) = a.

Main properties

theorem monus_smallest {α : Type} [K : SemiringWithMonus α] (a b : α) : a ≤ b + (a - b) ∧ ∀ (c : α), a ≤ b + c → a - b ≤ c

In a SemiringWithMonus, a - b is the smallest element c satisfying a ≤ b + c.

theorem monus_unique {α : Type} [K : SemiringWithMonus α] (s : α → α → α) (hs : ∀ (a b c : α), s a b ≤ c ↔ a ≤ b + c) (a b : α) : s a b = a - b

Uniqueness of monus. The monus operation is determined by its adjunction property: any binary operation s satisfying s a b ≤ c ↔ a ≤ b + c coincides with ⊖. Consequently, a naturally ordered semiring admits at most one monus operation.

theorem delta_one {α : Type} [K : SemiringWithMonus α] : SemiringWithMonus.delta 1 = 1

In a SemiringWithMonus, δ 1 = 1.

theorem monus_self {α : Type} [K : SemiringWithMonus α] (a : α) : a - a = 0

In a SemiringWithMonus, a - a = 0.

theorem zero_monus {α : Type} [K : SemiringWithMonus α] (a : α) : 0 - a = 0

In a SemiringWithMonus, 0 - a = 0.

theorem monus_zero {α : Type} [K : SemiringWithMonus α] (a : α) : a - 0 = a

In a SemiringWithMonus, a - 0 = a.

theorem add_monus {α : Type} [K : SemiringWithMonus α] (a b : α) : a + (b - a) = b + (a - b)

In a SemiringWithMonus, a + (b -a) = b + (a - b).

theorem monus_add {α : Type} [K : SemiringWithMonus α] (a b c : α) : a - (b + c) = a - b - c

In a SemiringWithMonus, monus is left-distributive over plus.

Additional properties

The following properties do not always hold in an arbitrary m-semiring.

@[reducible, inline]

abbrev idempotent (α : Type u_1) [Semiring α] : Prop

A Semiring is idempotent if a + a = a.

Equations

• idempotent α = ∀ (a : α), a + a = a

@[reducible, inline]

abbrev absorptive (α : Type u_1) [Semiring α] : Prop

A Semiring is absorptive (also called 0-closed or 0-bounded) if 1 + a = a.

Equations

• absorptive α = ∀ (a : α), 1 + a = 1

@[reducible, inline]

abbrev mul_sub_left_distributive (α : Type) [SemiringWithMonus α] : Prop

We define left-distributivity of times over monus in a SemiringWithMonus.

Equations

• mul_sub_left_distributive α = ∀ (a b c : α), a * (b - c) = a * b - a * c

theorem idempotent_of_absorptive {α : Type u_1} [K : Semiring α] : absorptive α → idempotent α

Absorptivity implies idempotence

theorem le_iff_add_eq {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b : α) : a ≤ b ↔ a + b = b

In an idempotent SemiringWithMonus, a ≤ b iff a + b = b.

theorem plus_is_join {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b : α) : (a ≤ a + b ∧ b ≤ a + b) ∧ ∀ (u : α), a ≤ u ∧ b ≤ u → a + b ≤ u

In an idempotent SemiringWithMonus, plus is the join of the semilattice

theorem idempotent_of_add_monus {α : Type} [K : SemiringWithMonus α] (h : ∀ (a b c : α), a + b - c = a - c + (b - c)) : idempotent α

In a SemiringWithMonus, right-distributivity of monus over plus implies idempotence.

theorem add_monus_of_idempotent {α : Type} [K : SemiringWithMonus α] (h : idempotent α) (a b c : α) : a + b - c = a - c + (b - c)

In a SemiringWithMonus, idempotence implies right-distributivity of monus over plus.

theorem idempotent_iff_add_monus {α : Type} [SemiringWithMonus α] : idempotent α ↔ ∀ (a b c : α), a + b - c = a - c + (b - c)

A SemiringWithMonus is idempotent iff monus is right-distributive over plus.

theorem add_monus_of_idempotent_multiset {α : Type} [SemiringWithMonus α] (h : idempotent α) (s : Multiset α) (c : α) : s.sum - c = (Multiset.map (fun (x : α) => x - c) s).sum

Finite-family version of add_monus_of_idempotent: in an idempotent SemiringWithMonus, monus distributes over the sum of any multiset of annotations, (⨁ᵢ aᵢ) ⊖ c = ⨁ᵢ (aᵢ ⊖ c).

theorem monus_le {α : Type} [SemiringWithMonus α] (a b : α) : a - b ≤ a

theorem le_plus_monus {α : Type} [SemiringWithMonus α] (a b : α) : a ≤ b + (a - b)

theorem monus_antitone {α : Type} [SemiringWithMonus α] {b b' : α} (h : b ≤ b') (a : α) : a - b' ≤ a - b

Monus is antitone in its second argument: subtracting more leaves less. Together with monus_le this is what lets a subtrahend be replaced by a larger one inside an upper bound.

Characteristic of idempotent semirings

In an idempotent semiring (a + a = a), every positive natural-number cast collapses to 1. With 1 ≠ 0 this yields CharP K 0. Note that this is strictly weaker than CharZero K, which fails for idempotent semirings since the cast ℕ → K is not injective.

theorem natCast_pos_eq_one_of_idempotent {K : Type} [Semiring K] (h : idempotent K) {n : ℕ} : 0 < n → ↑n = 1

In a semiring with idempotent addition, the cast of any positive natural number equals 1.

theorem CharP.zero_of_idempotent {K : Type} [Semiring K] [Nontrivial K] (h : idempotent K) : CharP K 0

A nontrivial idempotent semiring has characteristic 0 in the CharP sense. Unlike CharZero, this does not require the natural-number cast to be injective: in an idempotent semiring every positive natural maps to 1, but 1 ≠ 0 still suffices to give CharP K 0.

Generic constructions of δ

In the m-semirings used for provenance the δ operator is invariably realized in one of two ways: as the identity (when the semiring is idempotent, so every positive natural cast already equals 1) or as the indicator-of-nonzero (a ↦ if a = 0 then 0 else 1). The lemmas below package the proofs of the δ axioms for both candidates so each concrete instance can plug them in directly.

theorem delta_natCast_pos_id {K : Type} [Semiring K] (h : idempotent K) {n : ℕ} (hn : 0 < n) : id ↑n = 1

δ := id satisfies delta_natCast_pos in any idempotent semiring: every positive natural-number cast collapses to 1.

structure IsDeltaIndicator {K : Type} [Zero K] [One K] (δ : K → K) : Prop

The “indicator-of-nonzero” recipe: δ a = 0 when a = 0 and δ a = 1 otherwise. Captured abstractly so a single set of axioms can serve all the concrete instances that use it (ℕ, ℕ[X], Tropical, Viterbi, Lukasiewicz).

• zero : δ 0 = 0
• nonzero (a : K) : a ≠ 0 → δ a = 1

theorem delta_natCast_pos_indicator {K : Type} [Semiring K] [Nontrivial K] [CharP K 0] {δ : K → K} (h : IsDeltaIndicator δ) {n : ℕ} (hn : 0 < n) : δ ↑n = 1

Any δ matching the indicator recipe satisfies delta_natCast_pos in a nontrivial semiring of characteristic 0 (in the CharP sense): positive natural-number casts are nonzero, so δ sends them to 1.

theorem delta_absorb_indicator {K : Type} [Semiring K] [PartialOrder K] [IsOrderedAddMonoid K] [CanonicallyOrderedAdd K] {δ : K → K} (h : IsDeltaIndicator δ) (a b : K) : a * δ (a + b) = a

Any δ matching the indicator recipe satisfies delta_absorb in a canonically ordered semiring: if a ⊕ b = 𝟘 then a = 𝟘 by zero-sum freeness, and otherwise δ(a ⊕ b) = 𝟙.

Admissibility of a candidate δ

δ is not determined by the axioms, and the two operators used in practice are the identity and the support indicator. IsDelta states the axioms as a predicate on a candidate operator, so that a semiring can record which of the two it must use: the identity is preferred where it is admissible, and the indicator is forced exactly where ¬ IsDelta id holds. The three not_isDelta_id_of_* lemmas below cover the three ways the identity fails, in increasing order of subtlety.

structure IsDelta {K : Type} [Semiring K] (δ : K → K) : Prop

A candidate operator δ : K → K satisfies the δ-axioms of SemiringWithMonus.

• zero : δ 0 = 0

  δ sends 𝟘 to 𝟘.

• natCast_pos {n : ℕ} : 0 < n → δ ↑n = 1

  δ sends every positive natural-number cast to 𝟙.

• absorb (a b : K) : a * δ (a + b) = a

  A δ-guard is absorbed by any multiple of one of its summands.

theorem isDelta_delta {α : Type} [K : SemiringWithMonus α] : IsDelta SemiringWithMonus.delta

The δ carried by a SemiringWithMonus is admissible, by definition of the class. In particular, in a semiring whose instance takes δ := id this gives IsDelta id for free.

theorem not_isDelta_id_of_absorb_ne {K : Type} [Semiring K] {a b : K} (h : a * (a + b) ≠ a) : ¬IsDelta id

To refute δ := id, exhibit a pair violating the lattice absorption law a ⊗ (a ⊕ b) = a, which is what delta_absorb demands of the identity.

theorem not_isDelta_id_of_not_idempotent {K : Type} [Semiring K] (h : ¬idempotent K) : ¬IsDelta id

δ := id requires the semiring to be idempotent: delta_natCast_pos at n = 2 reads 𝟙 ⊕ 𝟙 = 𝟙, whence a ⊕ a = a ⊗ (𝟙 ⊕ 𝟙) = a. This is the crudest of the three obstructions, and the one that rules the identity out of the counting semirings (ℕ, ℕ[X]).

theorem not_isDelta_id_of_not_mul_idempotent {K : Type} [Semiring K] (hadd : idempotent K) (h : ¬∀ (a : K), a * a = a) : ¬IsDelta id

δ := id requires multiplicative idempotence as soon as addition is idempotent: delta_absorb at b = a reads a ⊗ (a ⊕ a) = a ⊗ a = a. This is the obstruction in the absorptive semirings whose ⊗ is a genuine product (Viterbi, Łukasiewicz), where the two coarser tests below say nothing.

theorem not_isDelta_id_of_not_absorptive {K : Type} [Semiring K] (h : ¬absorptive K) : ¬IsDelta id

δ := id requires absorptivity: delta_absorb at a = 𝟙 reads 𝟙 ⊗ (𝟙 ⊕ b) = 𝟙, i.e., 𝟙 ⊕ b = 𝟙.

Existence of a δ-like operator

This is the abstract counterpart of the SemiringWithMonus δ-axioms: we characterize, in an arbitrary nontrivial semiring (no order assumed), when a function δ : K → K satisfying δ 0 = 0 and δ ((n : K)) = 1 for 0 < n can exist. The class also demands delta_absorb, which the iff below ignores, so it should be read as a statement about how much of the ProvSQL δ interface is consistent with a given characteristic, not as a full existence proof for the class. (Constructing a witness for delta_absorb requires more structure: in a canonically ordered semiring the indicator works, see delta_absorb_indicator.)

theorem delta_exists_iff_charP_zero {K : Type} [Semiring K] [Nontrivial K] : (∃ (δ : K → K), δ 0 = 0 ∧ ∀ {n : ℕ}, 0 < n → δ ↑n = 1) ↔ CharP K 0

In any nontrivial semiring, a function δ : K → K satisfying δ 0 = 0 and δ ((n : K)) = 1 for every positive natural cast n exists if and only if K has characteristic 0 in the CharP sense. The forward direction follows because δ 0 = 0 and δ ((n : K)) = 1 are inconsistent when (n : K) = 0 for some 0 < n (it would force 0 = 1). The backward direction defines δ as the indicator of being nonzero.

Note that the δ operator is not uniquely determined by these axioms: they only pin its values on the image of ℕ. Two typical choices are δ as the indicator of being nonzero (δ x = if x = 0 then 0 else 1, used in the backward direction below) and, in an idempotent semiring, δ as the identity (since every positive natural cast then equals 1, see natCast_pos_eq_one_of_idempotent). Both are idempotent (δ (δ a) = δ a); adding idempotence as a third requirement would leave the statement unchanged, since the forward direction never uses it and the indicator witness satisfies it.

theorem isDelta_exists_of_natCast_axioms {K : Type} [Semiring K] [PartialOrder K] [IsOrderedAddMonoid K] [CanonicallyOrderedAdd K] [Nontrivial K] {δ : K → K} (h0 : δ 0 = 0) (hpos : ∀ {n : ℕ}, 0 < n → δ ↑n = 1) : ∃ (δ' : K → K), IsDelta δ'

The third axiom is free. In a canonically ordered semiring, a full IsDelta operator exists as soon as some function satisfies the first two axioms: the indicator witnessing delta_exists_iff_charP_zero satisfies delta_absorb as well (delta_absorb_indicator). So the admissibility question for a candidate δ is never one of existence – it is only about whether the preferred candidate, the identity, is among the admissible ones (not_isDelta_id_of_*).

theorem isDelta_exists_iff_charP_zero {K : Type} [Semiring K] [PartialOrder K] [IsOrderedAddMonoid K] [CanonicallyOrderedAdd K] [Nontrivial K] : (∃ (δ : K → K), IsDelta δ) ↔ CharP K 0

The companion of delta_exists_iff_charP_zero for the full axiom set: in a nontrivial canonically ordered semiring, an admissible δ exists if and only if the characteristic is 0.

Commutative SemiringWithMonuss

SemiringWithMonus is intentionally not assumed to be commutative; however, every provenance semiring used in this library is in fact commutative, and the algebraic identities that drive HAVING-style aggregate provenance (see Provenance.Having) require it. CommSemiringWithMonus packages a SemiringWithMonus together with the commutativity axiom, producing a CommMonoid instance whose Mul matches the one already supplied by SemiringWithMonus, so no Mul diamond appears when Finset.prod is used.

class CommSemiringWithMonus (K : Type) extends SemiringWithMonus K : Type

A SemiringWithMonus whose multiplication is commutative.

• add : K → K → K
• add_assoc (a b c : K) : a + b + c = a + (b + c)
• zero : K
• zero_add (a : K) : 0 + a = a
• add_zero (a : K) : a + 0 = a
• nsmul : ℕ → K → K
• nsmul_zero (x : K) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : K) : (n + 1) • x = n • x + x
• add_comm (a b : K) : a + b = b + a
• mul : K → K → K
• mul_assoc (a b c : K) : a * b * c = a * (b * c)
• one : K
• one_mul (a : K) : 1 * a = a
• mul_one (a : K) : a * 1 = a
• npow : ℕ → K → K
• npow_zero (x : K) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : K) : x ^ (n + 1) = x ^ n * x
• zero_mul (a : K) : 0 * a = 0
• mul_zero (a : K) : a * 0 = 0
• left_distrib (a b c : K) : a * (b + c) = a * b + a * c
• right_distrib (a b c : K) : (a + b) * c = a * c + b * c
• natCast : ℕ → K
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• le : K → K → Prop
• lt : K → K → Prop
• le_refl (a : K) : a ≤ a
• le_trans (a b c : K) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : K) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : K) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : K) : a ≤ b → ∀ (c : K), a + c ≤ b + c
• add_le_add_right (a b : K) : a ≤ b → ∀ (c : K), c + a ≤ c + b
• exists_add_of_le {a b : K} : a ≤ b → ∃ (c : K), b = a + c
• le_add_self (a b : K) : a ≤ b + a
• le_self_add (a b : K) : a ≤ a + b
• sub : K → K → K
• monus_spec (a b c : K) : a - b ≤ c ↔ a ≤ b + c
• delta : K → K
• delta_zero : delta 0 = 0
• delta_natCast_pos {n : ℕ} : 0 < n → delta ↑n = 1
• delta_absorb (a b : K) : a * delta (a + b) = a
• mul_comm (a b : K) : a * b = b * a

  Multiplication on K is commutative.

@[instance_reducible, instance 100]

instance instCommMonoidOfCommSemiringWithMonus {K : Type} [h : CommSemiringWithMonus K] : CommMonoid K

A CommSemiringWithMonus is automatically a CommMonoid, sharing its multiplicative structure with the underlying SemiringWithMonus. This makes Finset.prod usable without introducing a separate CommSemiring hypothesis that would cause a Mul diamond.

Equations

• instCommMonoidOfCommSemiringWithMonus = { toMonoid := h.toMonoid, mul_comm := ⋯ }

Homomorphisms of SemiringWithMonuss

class SemiringWithMonusHom (α β : Type) [SemiringWithMonus α] [SemiringWithMonus β] extends α →+* β : Type

Definition of a homomorphism of SemiringWithMonuss. Preserves the semiring structure (via RingHom), the monus (map_sub), and the δ operator (map_delta). The latter is required for hom commutation of the aggregation operator, where δ appears on the row-annotation column (Definition 7 / R5 of Sen, Maniu & Senellart).

• toFun : α → β
• map_one' : (↑↑self.toRingHom).toFun 1 = 1
• map_mul' (x y : α) : (↑↑self.toRingHom).toFun (x * y) = (↑↑self.toRingHom).toFun x * (↑↑self.toRingHom).toFun y
• map_zero' : (↑↑self.toRingHom).toFun 0 = 0
• map_add' (x y : α) : (↑↑self.toRingHom).toFun (x + y) = (↑↑self.toRingHom).toFun x + (↑↑self.toRingHom).toFun y
• map_sub (x y : α) : self.toRingHom (x - y) = self.toRingHom x - self.toRingHom y
• map_delta (a : α) : self.toRingHom (SemiringWithMonus.delta a) = SemiringWithMonus.delta (self.toRingHom a)

  The hom preserves δ: h (δ a) = δ (h a).

@[instance_reducible]

instance instCoeFunSemiringWithMonusHomForall (α β : Type) [SemiringWithMonus α] [SemiringWithMonus β] : CoeFun (SemiringWithMonusHom α β) fun (x : SemiringWithMonusHom α β) => α → β

Equations

• instCoeFunSemiringWithMonusHomForall α β = { coe := fun (f : SemiringWithMonusHom α β) (x : α) => f.toRingHom x }

theorem idempotent_of_injective_homomorphism_idempotent {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνi : Function.Injective fun (x : α) => ν.toRingHom x) : idempotent β → idempotent α

If ν is an injective m-semiring homomorphism from α to β, and β is idempotent, so is α.

theorem idempotent_of_surjective_homomorphism_idempotent {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνs : Function.Surjective fun (x : α) => ν.toRingHom x) : idempotent α → idempotent β

If ν is an m-semiring homomorphism from α onto β, and α is idempotent, so is β.

theorem mul_sub_left_of_injective_homomorphism_mul_sub_left {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνi : Function.Injective fun (x : α) => ν.toRingHom x) : mul_sub_left_distributive β → mul_sub_left_distributive α

If ν is an injective m-semiring homomorphism from α to β, and β has left-distributivity of times over monus, so has α.

theorem mul_sub_left_of_surjective_homomorphism_mul_sub_left {α β : Type} [SemiringWithMonus α] [SemiringWithMonus β] (ν : SemiringWithMonusHom α β) (hνs : Function.Surjective fun (x : α) => ν.toRingHom x) : mul_sub_left_distributive α → mul_sub_left_distributive β

If ν is an m-semiring homomorphism from α onto β, and α has left-distributivity of times over monus, so has β.

Miscellaneous

theorem natural_preorder_not_antisymm : ∃ (a : ℤ), ∃ (b : ℤ), (∃ (c : ℤ), b = a + c) ∧ (∃ (c : ℤ), a = b + c) ∧ a ≠ b

On an arbitrary semiring the natural relation a ≼ b ↔ ∃ c, b = a + c is always a preorder (reflexive by c = 0, transitive by adding witnesses) but not always antisymmetric: on ℤ, any two elements are related in both directions, e.g., 0 ≼ 1 ≼ 0 with 0 ≠ 1. This is why SemiringWithMonus assumes the canonically ordered structure instead of deriving an order from +.

class HasAltLinearOrder (α : Type u) : Type u

• altOrder : LinearOrder α

Home · Documentation · Publications · Contributors · Source · Cite