Weighted semirings

We introduces weighted versions of nessesaray semiring and order instances with custom notation that mirror the Mathlib definitions almost one-to-one.

The reason for this is to simplify the instantiation of weighted version of already existing structures. One such example is the Tropical semiring which works over ENat. ENat already has instances for (almost) everything we need, however, the existing definitons are (ENat, 0, 1, +, *, ≤) while we need (ENat, ⊤, 0, min, +, ≥). One could create new instances for these that shadow the previous, but suddenly one has to proof goals that look like 0 + 1 ≤ 1 where 0 can be either 0 or ⊤ and the ones can be 1 or 0 independently and ≤ can be either ≤ or ≥.

To simplify these, the new notation makes it very clear for the reader to see which is which, and equally as important, makes it easier to simp away the weighted notation and get to the meat of the proof.

Previous versions tried the prior approach; for some instances it took hundreds of lines and much turmoil, and some we deemed too complicated just because of the sheer confusion when mixing semirings.

Instances with this new approach are significantly shorter and lends themselves much more to automation.

class WAdd (α : Type u_1) : Type u_1

Weighted variant of [Add]

• wadd : α → α → α

class WMul (α : Type u_1) : Type u_1

Weighted variant of [Mul]

• wmul : α → α → α

class WKStar (α : Type u_1) : Type u_1

Weighted variant of [KStar]

• wkstar : α → α

  Weighted variant of [KStar]

class WZero (α : Type u_1) : Type u_1

Weighted variant of [Zero]

• wzero : α

class WOne (α : Type u_1) : Type u_1

Weighted variant of [One]

• wone : α

class WLE (α : Type u_1) : Type u_1

Weighted variant of [LE]

• wle : α → α → Prop

class WLT (α : Type u_1) : Type u_1

Weighted variant of [LT]

• wlt : α → α → Prop

def WKStar.«term_⍟» : Lean.TrailingParserDescr

Weighted variant of [KStar]

Equations

• WKStar.«term_⍟» = Lean.ParserDescr.trailingNode `WKStar.«term_⍟» 1024 1024 (Lean.ParserDescr.symbol "⍟")

def «term𝟘» : Lean.ParserDescr

Equations

• «term𝟘» = Lean.ParserDescr.node `«term𝟘» 1024 (Lean.ParserDescr.symbol "𝟘")

def «term𝟙» : Lean.ParserDescr

Equations

• «term𝟙» = Lean.ParserDescr.node `«term𝟙» 1024 (Lean.ParserDescr.symbol "𝟙")

def «term_⨁_» : Lean.TrailingParserDescr

Equations

• «term_⨁_» = Lean.ParserDescr.trailingNode `«term_⨁_» 68 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨁ ") (Lean.ParserDescr.cat `term 69))

def «term_⨀_» : Lean.TrailingParserDescr

Equations

• «term_⨀_» = Lean.ParserDescr.trailingNode `«term_⨀_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨀ ") (Lean.ParserDescr.cat `term 71))

def «term_≼_» : Lean.TrailingParserDescr

Equations

• «term_≼_» = Lean.ParserDescr.trailingNode `«term_≼_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼ ") (Lean.ParserDescr.cat `term 51))

def «term_≺_» : Lean.TrailingParserDescr

Equations

• «term_≺_» = Lean.ParserDescr.trailingNode `«term_≺_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺ ") (Lean.ParserDescr.cat `term 51))

@[reducible, inline]

abbrev WKStar.toKStar (α : Type u_1) [WKStar α] : KStar α

Equations

• WKStar.toKStar α = { kstar := wkstar }

class WSemiring (α : Type u_1) extends WAdd α, WMul α, WOne α, WZero α : Type u_1

Weighted variant of [Semiring]

• wadd : α → α → α
• wmul : α → α → α
• wone : α
• wzero : α
• wadd_wzero (a : α) : a ⨁ 𝟘 = a
• wadd_assoc (a b c : α) : a ⨁ b ⨁ c = a ⨁ (b ⨁ c)
• wzero_wadd (a : α) : 𝟘 ⨁ a = a
• wnsmul : ℕ → α → α
• wadd_comm (a b : α) : a ⨁ b = b ⨁ a
• left_distrib (a b c : α) : a ⨀ (b ⨁ c) = a ⨀ b ⨁ a ⨀ c
• right_distrib (a b c : α) : (a ⨁ b) ⨀ c = a ⨀ c ⨁ b ⨀ c
• wzero_wmul (a : α) : 𝟘 ⨀ a = 𝟘
• wmul_wzero (a : α) : a ⨀ 𝟘 = 𝟘
• wmul_assoc (a b c : α) : a ⨀ b ⨀ c = a ⨀ (b ⨀ c)
• wone_wmul (a : α) : 𝟙 ⨀ a = a
• wmul_wone (a : α) : a ⨀ 𝟙 = a
• wnsmul_zero (x : α) : wnsmul 0 x = 𝟘
• wnsmul_succ (n : ℕ) (x : α) : wnsmul (n + 1) x = wnsmul n x ⨁ x

class WPartialOrder (α : Type u_1) extends WLE α, WLT α : Type u_1

Weighted variant of [PartialOrder]

• wle : α → α → Prop
• wlt : α → α → Prop
• wle_refl (a : α) : a ≼ a
• wle_trans {a b c : α} : a ≼ b → b ≼ c → a ≼ c
• wlt_iff_wle_not_wge (a b : α) : a ≺ b ↔ a ≼ b ∧ ¬b ≼ a
• wle_antisymm (a b : α) (hab : a ≼ b) (hba : b ≼ a) : a = b
• decidableWLE : DecidableRel wle

@[reducible, inline]

abbrev WSemiring.toSemiring (α : Type u_1) [WSemiring α] : Semiring α

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev WLE.toLE (α : Type u_1) [WLE α] : LE α

Equations

• WLE.toLE α = { le := wle }

@[reducible, inline]

abbrev WLT.toLT (α : Type u_1) [WLT α] : LT α

Equations

• WLT.toLT α = { lt := wlt }

@[reducible, inline]

abbrev WPartialOrder.toPartialOrder (α : Type u_1) [WPartialOrder α] : PartialOrder α

Equations

• WPartialOrder.toPartialOrder α = { toLE := WLE.toLE α, toLT := WLT.toLT α, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible, inline]

abbrev WPartialOrder.toDecidableLE (α : Type u_1) [inst : WPartialOrder α] : DecidableLE α

Equations

• WPartialOrder.toDecidableLE α = WPartialOrder.decidableWLE

@[implicit_reducible]

instance instWLTOfWLE {α : Type u_1} [WLE α] : WLT α

Equations

• instWLTOfWLE = { wlt := fun (a b : α) => a ≼ b ∧ ¬b ≼ a }

class WOmegaCompletePartialOrder (α : Type u_1) extends WPartialOrder α : Type u_1

• wle : α → α → Prop
• wlt : α → α → Prop
• wle_refl (a : α) : a ≼ a
• wle_trans {a b c : α} : a ≼ b → b ≼ c → a ≼ c
• wlt_iff_wle_not_wge (a b : α) : a ≺ b ↔ a ≼ b ∧ ¬b ≼ a
• wle_antisymm (a b : α) (hab : a ≼ b) (hba : b ≼ a) : a = b
• decidableWLE : DecidableRel wle
• wωSup (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) : α
• wle_wωSup (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) (i : ℕ) : f i ≼ wωSup f ⋯
• wωSup_wle (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) (x : α) : (∀ (i : ℕ), f i ≼ x) → wωSup f ⋯ ≼ x

theorem WOmegaCompletePartialOrder.wωSup_wle_of_wle {α : Type u_1} [WOmegaCompletePartialOrder α] {f : ℕ → α} {h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b} {x : α} (i : ℕ) (hi : x ≼ f i) : x ≼ wωSup f ⋯

@[implicit_reducible]

def instLEOfWLE {α : Type u_1} [WLE α] : LE α

Equations

• instLEOfWLE = WLE.toLE α

@[implicit_reducible]

def instLTOfWLT {α : Type u_1} [WLT α] : LT α

Equations

• instLTOfWLT = WLT.toLT α

@[implicit_reducible]

def instPartialOrderOfWPartialOrder {α : Type u_1} [WPartialOrder α] : PartialOrder α

Equations

• instPartialOrderOfWPartialOrder = WPartialOrder.toPartialOrder α

@[reducible, inline]

abbrev WOmegaCompletePartialOrder.toOmegaCompletePartialOrder (α : Type u_1) [WOmegaCompletePartialOrder α] : OmegaCompletePartialOrder α

Equations

• One or more equations did not get rendered due to their size.

class WOmegaContinuousNonUnitalSemiring (α : Type u_1) extends WSemiring α, WOmegaCompletePartialOrder α : Type u_1

• wadd : α → α → α
• wmul : α → α → α
• wone : α
• wzero : α
• wadd_wzero (a : α) : a ⨁ 𝟘 = a
• wadd_assoc (a b c : α) : a ⨁ b ⨁ c = a ⨁ (b ⨁ c)
• wzero_wadd (a : α) : 𝟘 ⨁ a = a
• wnsmul : ℕ → α → α
• wadd_comm (a b : α) : a ⨁ b = b ⨁ a
• left_distrib (a b c : α) : a ⨀ (b ⨁ c) = a ⨀ b ⨁ a ⨀ c
• right_distrib (a b c : α) : (a ⨁ b) ⨀ c = a ⨀ c ⨁ b ⨀ c
• wzero_wmul (a : α) : 𝟘 ⨀ a = 𝟘
• wmul_wzero (a : α) : a ⨀ 𝟘 = 𝟘
• wmul_assoc (a b c : α) : a ⨀ b ⨀ c = a ⨀ (b ⨀ c)
• wone_wmul (a : α) : 𝟙 ⨀ a = a
• wmul_wone (a : α) : a ⨀ 𝟙 = a
• wnsmul_zero (x : α) : wnsmul 0 x = 𝟘
• wnsmul_succ (n : ℕ) (x : α) : wnsmul (n + 1) x = wnsmul n x ⨁ x
• wle : α → α → Prop
• wlt : α → α → Prop
• wle_refl (a : α) : a ≼ a
• wle_trans {a b c : α} : a ≼ b → b ≼ c → a ≼ c
• wlt_iff_wle_not_wge (a b : α) : a ≺ b ↔ a ≼ b ∧ ¬b ≼ a
• wle_antisymm (a b : α) (hab : a ≼ b) (hba : b ≼ a) : a = b
• decidableWLE : DecidableRel wle
• wωSup (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) : α
• wle_wωSup (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) (i : ℕ) : f i ≼ wωSup f ⋯
• wωSup_wle (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) (x : α) : (∀ (i : ℕ), f i ≼ x) → wωSup f ⋯ ≼ x
• wbot : α
• wbot_wle (a : α) : wbot ≼ a
• wbot_eq_wzero : wbot = 𝟘
• wadd_left_mono {b c : α} (h : b ≼ c) (a : α) : a ⨁ b ≼ a ⨁ c
• wadd_right_mono {b c : α} (h : b ≼ c) (a : α) : b ⨁ a ≼ c ⨁ a
• wmul_left_mono {b c : α} (h : b ≼ c) (a : α) : a ⨀ b ≼ a ⨀ c
• wmul_right_mono {b c : α} (h : b ≼ c) (a : α) : b ⨀ a ≼ c ⨀ a
• wωScottContinuous_wadd_right (a : α) (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) : WOmegaCompletePartialOrder.wωSup f ⋯ ⨁ a = WOmegaCompletePartialOrder.wωSup (fun (x : ℕ) => f x ⨁ a) ⋯
• wωScottContinuous_wadd_left (a : α) (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) : a ⨁ WOmegaCompletePartialOrder.wωSup f ⋯ = WOmegaCompletePartialOrder.wωSup (fun (x : ℕ) => a ⨁ f x) ⋯
• wωScottContinuous_wmul_right (a : α) (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) : WOmegaCompletePartialOrder.wωSup f ⋯ ⨀ a = WOmegaCompletePartialOrder.wωSup (fun (x : ℕ) => f x ⨀ a) ⋯
• wωScottContinuous_wmul_left (a : α) (f : ℕ → α) (h : ∀ {a b : ℕ}, a ≤ b → f a ≼ f b) : a ⨀ WOmegaCompletePartialOrder.wωSup f ⋯ = WOmegaCompletePartialOrder.wωSup (fun (x : ℕ) => a ⨀ f x) ⋯

@[implicit_reducible]

def instSemiringOfWSemiring {α : Type u_1} [WSemiring α] : Semiring α

Equations

• instSemiringOfWSemiring = WSemiring.toSemiring α

@[implicit_reducible]

def instOmegaCompletePartialOrderOfWOmegaCompletePartialOrder {α : Type u_1} [WOmegaCompletePartialOrder α] : OmegaCompletePartialOrder α

Equations

• instOmegaCompletePartialOrderOfWOmegaCompletePartialOrder = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder α

@[reducible, inline]

abbrev WOmegaContinuousNonUnitalSemiring.toOrderBot (α : Type u_1) [WOmegaContinuousNonUnitalSemiring α] : OrderBot α

Equations

• WOmegaContinuousNonUnitalSemiring.toOrderBot α = { bot := WOmegaContinuousNonUnitalSemiring.wbot, bot_le := ⋯ }

@[reducible, inline]

abbrev WOmegaContinuousNonUnitalSemiring.toMulLeftMono (α : Type u_1) [WOmegaContinuousNonUnitalSemiring α] : MulLeftMono α

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev WOmegaContinuousNonUnitalSemiring.toMulRightMono (α : Type u_1) [WOmegaContinuousNonUnitalSemiring α] : MulRightMono α

Equations

• ⋯ = ⋯

@[implicit_reducible]

def WOmegaContinuousNonUnitalSemiring.instOrderBot {α : Type u_2} [WOmegaContinuousNonUnitalSemiring α] : OrderBot α

Equations

• WOmegaContinuousNonUnitalSemiring.instOrderBot = WOmegaContinuousNonUnitalSemiring.toOrderBot α

@[reducible, inline]

abbrev WOmegaContinuousNonUnitalSemiring.toIsPositiveOrderedAddMonoid (α : Type u_1) [WOmegaContinuousNonUnitalSemiring α] : IsPositiveOrderedAddMonoid α

Equations

• ⋯ = ⋯

@[implicit_reducible]

def instOrderBot_weightedNetKAT {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] : OrderBot α

Equations

• instOrderBot_weightedNetKAT = WOmegaContinuousNonUnitalSemiring.toOrderBot α

theorem instMulLeftMono_weightedNetKAT {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] : MulLeftMono α

theorem instMulRightMono_weightedNetKAT {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] : MulRightMono α

theorem instIsPositiveOrderedAddMonoid {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] : IsPositiveOrderedAddMonoid α

@[reducible, inline]

abbrev WOmegaContinuousNonUnitalSemiring.toOmegaContinuousNonUnitalSemiring (α : Type u_1) [WOmegaContinuousNonUnitalSemiring α] : OmegaContinuousNonUnitalSemiring α

Equations

• ⋯ = ⋯

def wstarn {α : Type u_1} [WSemiring α] (a : α) : ℕ → α

Equations

• wstarn a 0 = 𝟘
• wstarn a n.succ = 𝟙 ⨁ a ⨀ wstarn a n

@[simp]

theorem wzero_le {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a : α} : 𝟘 ≼ a

theorem wadd_le_wadd {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a b c d : α} (hac : a ≼ c) (hbd : b ≼ d) : a ⨁ b ≼ c ⨁ d

theorem wmul_le_wmul {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a b c d : α} (hac : a ≼ c) (hbd : b ≼ d) : a ⨀ b ≼ c ⨀ d

@[simp]

theorem wstarn_zero {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a : α} : wstarn a 0 = 𝟘

theorem wstarn_mono_left {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a b : α} {n : ℕ} (h : a ≼ b) : wstarn a n ≼ wstarn b n

theorem wstarn_le_succ {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a : α} {n : ℕ} : wstarn a n ≼ wstarn a (n + 1)

theorem wstarn_mono_right {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a : α} {n m : ℕ} (h : n ≤ m) : wstarn a n ≼ wstarn a m

theorem wstarn_mono {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {a : α} : Monotone (wstarn a)

@[simp]

theorem wstarn_wzero_left {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] {i : ℕ} : wstarn 𝟘 i = if i = 0 then 𝟘 else 𝟙

@[simp]

theorem wωSup_wstarn_wzero_left {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] : WOmegaCompletePartialOrder.wωSup (fun (x : ℕ) => wstarn 𝟘 x) ⋯ = 𝟙

class LawfulWKStar (α : Type u_1) [WKStar α] [WOmegaContinuousNonUnitalSemiring α] : Prop

• wkstar_eq_sum (m : α) : wkstar m = WOmegaCompletePartialOrder.wωSup (fun (n : ℕ) => wstarn m n) ⋯

@[implicit_reducible]

def instSemiringOfWSemiring_1 {α : Type u_1} [WSemiring α] : Semiring α

Equations

• instSemiringOfWSemiring_1 = WSemiring.toSemiring α

@[implicit_reducible]

def instKStarOfWKStar {α : Type u_1} [WKStar α] : KStar α

Equations

• instKStarOfWKStar = WKStar.toKStar α

@[reducible, inline]

abbrev LawfulWKStar.toLawfulKStar (α : Type u_1) [WOmegaContinuousNonUnitalSemiring α] [WKStar α] [LawfulWKStar α] : LawfulKStar α

Equations

• ⋯ = ⋯

theorem instLawfulKStarOfLawfulWKStar {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] [WKStar α] [LawfulWKStar α] : LawfulKStar α

@[implicit_reducible]

def instOmegaCompletePartialOrderOfLawfulWKStar {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] [WKStar α] [LawfulWKStar α] : OmegaCompletePartialOrder α

Equations

• instOmegaCompletePartialOrderOfLawfulWKStar = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder α

theorem instOmegaContinuousNonUnitalSemiring {α : Type u_1} [WOmegaContinuousNonUnitalSemiring α] [WKStar α] [LawfulWKStar α] : OmegaContinuousNonUnitalSemiring α

@[reducible, inline]

abbrev LawfulWKStar.toKStarIter (α : Type u_1) [WOmegaContinuousNonUnitalSemiring α] [WKStar α] [LawfulWKStar α] : KStarIter α

Equations

• ⋯ = ⋯