Kleene Algebras

This file defines idempotent semirings and Kleene algebras, which are used extensively in the theory of computation.

An idempotent semiring is a semiring whose addition is idempotent. An idempotent semiring is naturally a semilattice by setting a ≤ b if a + b = b.

A Kleene algebra is an idempotent semiring equipped with an additional unary operator ∗, the Kleene star.

Main declarations

• IdemSemiring: Idempotent semiring
• IdemCommSemiring: Idempotent commutative semiring
• KleeneAlgebra: Kleene algebra

Notation

a∗ is notation for kstar a in locale Computability.

References

• [D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events] [kozen1994]
• https://planetmath.org/idempotentsemiring
• https://encyclopediaofmath.org/wiki/Idempotent_semi-ring
• https://planetmath.org/kleene_algebra

TODO

Instances for AddOpposite, MulOpposite, ULift, Subsemiring, Subring, Subalgebra.

Tags

kleene algebra, idempotent semiring

class IdemSemiring (α : Type u) extends Semiring , SemilatticeSup : Type u

An idempotent semiring is a semiring with the additional property that addition is idempotent.

• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n x
• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• add_eq_sup : ∀ (a b : α), a + b = a ⊔ b
• bot : α
• bot_le : ∀ (a : α), IdemSemiring.bot ≤ a

class IdemCommSemiring (α : Type u) extends CommSemiring , SemilatticeSup : Type u

An idempotent commutative semiring is a commutative semiring with the additional property that addition is idempotent.

• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n x
• mul_comm : ∀ (a b : α), a * b = b * a
• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• add_eq_sup : ∀ (a b : α), a + b = a ⊔ b
• bot : α
• bot_le : ∀ (a : α), IdemCommSemiring.bot ≤ a

class KStar (α : Type u_5) : Type u_5

Notation typeclass for the Kleene star ∗.

• kstar : α → α

def Computability.«term_∗» : Lean.TrailingParserDescr

Equations

• Computability.«term_∗» = Lean.ParserDescr.trailingNode `Computability.term_∗ 1024 1024 (Lean.ParserDescr.symbol "∗")

class KleeneAlgebra (α : Type u_5) extends IdemSemiring , KStar : Type u_5

A Kleene Algebra is an idempotent semiring with an additional unary operator kstar (for Kleene star) that satisfies the following properties:

• 1 + a * a∗ ≤ a∗
• 1 + a∗ * a ≤ a∗
• If a * c + b ≤ c, then a∗ * b ≤ c
• If c * a + b ≤ c, then b * a∗ ≤ c

• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n x
• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• add_eq_sup : ∀ (a b : α), a + b = a ⊔ b
• bot : α
• bot_le : ∀ (a : α), IdemSemiring.bot ≤ a
• kstar : α → α
• one_le_kstar : ∀ (a : α), 1 ≤ KStar.kstar a
• mul_kstar_le_kstar : ∀ (a : α), a * KStar.kstar a ≤ KStar.kstar a
• kstar_mul_le_kstar : ∀ (a : α), KStar.kstar a * a ≤ KStar.kstar a
• mul_kstar_le_self : ∀ (a b : α), b * a ≤ b → b * KStar.kstar a ≤ b
• kstar_mul_le_self : ∀ (a b : α), a * b ≤ b → KStar.kstar a * b ≤ b

instance IdemSemiring.toOrderBot {α : Type u_1} [IdemSemiring α] : OrderBot α

Equations

• IdemSemiring.toOrderBot = let __src := inst; OrderBot.mk ⋯

@[reducible]

def IdemSemiring.ofSemiring {α : Type u_1} [Semiring α] (h : ∀ (a : α), a + a = a) : IdemSemiring α

Construct an idempotent semiring from an idempotent addition.

Equations

• IdemSemiring.ofSemiring h = let __src := inst; IdemSemiring.mk ⋯ 0 ⋯

theorem add_eq_sup {α : Type u_1} [IdemSemiring α] (a : α) (b : α) : a + b = a ⊔ b

theorem add_idem {α : Type u_1} [IdemSemiring α] (a : α) : a + a = a

theorem nsmul_eq_self {α : Type u_1} [IdemSemiring α] {n : ℕ} : n ≠ 0 → ∀ (a : α), n • a = a

theorem add_eq_left_iff_le {α : Type u_1} [IdemSemiring α] {a : α} {b : α} : a + b = a ↔ b ≤ a

theorem add_eq_right_iff_le {α : Type u_1} [IdemSemiring α] {a : α} {b : α} : a + b = b ↔ a ≤ b

theorem LE.le.add_eq_left {α : Type u_1} [IdemSemiring α] {a : α} {b : α} : b ≤ a → a + b = a

Alias of the reverse direction of add_eq_left_iff_le.

theorem LE.le.add_eq_right {α : Type u_1} [IdemSemiring α] {a : α} {b : α} : a ≤ b → a + b = b

Alias of the reverse direction of add_eq_right_iff_le.

theorem add_le_iff {α : Type u_1} [IdemSemiring α] {a : α} {b : α} {c : α} : a + b ≤ c ↔ a ≤ c ∧ b ≤ c

theorem add_le {α : Type u_1} [IdemSemiring α] {a : α} {b : α} {c : α} (ha : a ≤ c) (hb : b ≤ c) : a + b ≤ c

instance IdemSemiring.toCanonicallyOrderedAddCommMonoid {α : Type u_1} [IdemSemiring α] : CanonicallyOrderedAddCommMonoid α

Equations

• IdemSemiring.toCanonicallyOrderedAddCommMonoid = let __src := inst; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

instance IdemSemiring.toCovariantClass_mul_le {α : Type u_1} [IdemSemiring α] : CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1

Equations

• ⋯ = ⋯

instance IdemSemiring.toCovariantClass_swap_mul_le {α : Type u_1} [IdemSemiring α] : CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1

Equations

• ⋯ = ⋯

@[simp]

theorem one_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} : 1 ≤ KStar.kstar a

theorem mul_kstar_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} : a * KStar.kstar a ≤ KStar.kstar a

theorem kstar_mul_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} : KStar.kstar a * a ≤ KStar.kstar a

theorem mul_kstar_le_self {α : Type u_1} [KleeneAlgebra α] {a : α} {b : α} : b * a ≤ b → b * KStar.kstar a ≤ b

theorem kstar_mul_le_self {α : Type u_1} [KleeneAlgebra α] {a : α} {b : α} : a * b ≤ b → KStar.kstar a * b ≤ b

theorem mul_kstar_le {α : Type u_1} [KleeneAlgebra α] {a : α} {b : α} {c : α} (hb : b ≤ c) (ha : c * a ≤ c) : b * KStar.kstar a ≤ c

theorem kstar_mul_le {α : Type u_1} [KleeneAlgebra α] {a : α} {b : α} {c : α} (hb : b ≤ c) (ha : a * c ≤ c) : KStar.kstar a * b ≤ c

theorem kstar_le_of_mul_le_left {α : Type u_1} [KleeneAlgebra α] {a : α} {b : α} (hb : 1 ≤ b) : b * a ≤ b → KStar.kstar a ≤ b

theorem kstar_le_of_mul_le_right {α : Type u_1} [KleeneAlgebra α] {a : α} {b : α} (hb : 1 ≤ b) : a * b ≤ b → KStar.kstar a ≤ b

@[simp]

theorem le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} : a ≤ KStar.kstar a

theorem kstar_mono {α : Type u_1} [KleeneAlgebra α] : Monotone KStar.kstar

@[simp]

theorem kstar_eq_one {α : Type u_1} [KleeneAlgebra α] {a : α} : KStar.kstar a = 1 ↔ a ≤ 1

@[simp]

theorem kstar_zero {α : Type u_1} [KleeneAlgebra α] : KStar.kstar 0 = 1

@[simp]

theorem kstar_one {α : Type u_1} [KleeneAlgebra α] : KStar.kstar 1 = 1

@[simp]

theorem kstar_mul_kstar {α : Type u_1} [KleeneAlgebra α] (a : α) : KStar.kstar a * KStar.kstar a = KStar.kstar a

@[simp]

theorem kstar_eq_self {α : Type u_1} [KleeneAlgebra α] {a : α} : KStar.kstar a = a ↔ a * a = a ∧ 1 ≤ a

@[simp]

theorem kstar_idem {α : Type u_1} [KleeneAlgebra α] (a : α) : KStar.kstar (KStar.kstar a) = KStar.kstar a

@[simp]

theorem pow_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} {n : ℕ} : a ^ n ≤ KStar.kstar a

instance Prod.instIdemSemiring {α : Type u_1} {β : Type u_2} [IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β)

Equations

• Prod.instIdemSemiring = let __src := Prod.instSemiring; let __src_1 := Prod.instSemilatticeSup α β; let __src_2 := Prod.instOrderBot α β; IdemSemiring.mk ⋯ ⊥ ⋯

instance Prod.instIdemCommSemiringProd {α : Type u_1} {β : Type u_2} [IdemCommSemiring α] [IdemCommSemiring β] : IdemCommSemiring (α × β)

Equations

• Prod.instIdemCommSemiringProd = let __src := Prod.instCommSemiring; let __src_1 := Prod.instIdemSemiring; IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯

instance Prod.instKleeneAlgebraProd {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] : KleeneAlgebra (α × β)

Equations

• Prod.instKleeneAlgebraProd = let __src := Prod.instIdemSemiring; KleeneAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯

theorem Prod.kstar_def {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) : KStar.kstar a = (KStar.kstar a.1, KStar.kstar a.2)

@[simp]

theorem Prod.fst_kstar {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) : (KStar.kstar a).1 = KStar.kstar a.1

@[simp]

theorem Prod.snd_kstar {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) : (KStar.kstar a).2 = KStar.kstar a.2

instance Pi.instIdemSemiring {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → IdemSemiring (π i)] : IdemSemiring ((i : ι) → π i)

Equations

• Pi.instIdemSemiring = let __src := Pi.semiring; let __src_1 := Pi.instSemilatticeSup; let __src_2 := Pi.instOrderBot; IdemSemiring.mk ⋯ ⊥ ⋯

instance Pi.instIdemCommSemiringForAll {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → IdemCommSemiring (π i)] : IdemCommSemiring ((i : ι) → π i)

Equations

• Pi.instIdemCommSemiringForAll = let __src := Pi.commSemiring; let __src_1 := Pi.instIdemSemiring; IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯

instance Pi.instKleeneAlgebraForAll {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → KleeneAlgebra (π i)] : KleeneAlgebra ((i : ι) → π i)

Equations

• Pi.instKleeneAlgebraForAll = let __src := Pi.instIdemSemiring; KleeneAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯

theorem Pi.kstar_def {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → KleeneAlgebra (π i)] (a : (i : ι) → π i) : KStar.kstar a = fun (i : ι) => KStar.kstar (a i)

@[simp]

theorem Pi.kstar_apply {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → KleeneAlgebra (π i)] (a : (i : ι) → π i) (i : ι) : KStar.kstar a i = KStar.kstar (a i)

@[reducible]

def Function.Injective.idemSemiring {α : Type u_1} {β : Type u_2} [IdemSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [Sup β] [Bot β] (f : β → α) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) : IdemSemiring β

Pullback an IdemSemiring instance along an injective function.

Equations

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

@[reducible]

def Function.Injective.idemCommSemiring {α : Type u_1} {β : Type u_2} [IdemCommSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [Sup β] [Bot β] (f : β → α) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) : IdemCommSemiring β

Pullback an IdemCommSemiring instance along an injective function.

Equations

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

@[reducible]

def Function.Injective.kleeneAlgebra {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [Sup β] [Bot β] [KStar β] (f : β → α) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) (kstar : ∀ (a : β), f (KStar.kstar a) = KStar.kstar (f a)) : KleeneAlgebra β

Pullback a KleeneAlgebra instance along an injective function.

Equations

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