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 , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , MulOneClass , AddMonoidWithOne , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , AddMonoid , One , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , PartialOrder , Preorder , LE , LT : Type u

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

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

theorem IdemSemiring.bot_le {α : Type u} [self : IdemSemiring α] (a : α) : IdemSemiring.bot ≤ a

class IdemCommSemiring (α : Type u) extends CommSemiring , IdemSemiring , Semiring , CommMonoid , SemilatticeSup , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , CommSemigroup , MulOneClass , AddMonoidWithOne , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , AddMonoid , One , AddCommSemigroup , AddSemigroup , AddZeroClass , CommMagma , Mul , Zero , AddCommMagma , Add , PartialOrder , Preorder , LE , LT : Type u

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

class KStar (α : Type u_5) : Type u_5

Notation typeclass for the Kleene star ∗.

• kstar : α → α

  The Kleene star operator on a Kleene algebra

def Computability.«term_∗» : Lean.TrailingParserDescr

The Kleene star operator on a Kleene algebra

Equations

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

class KleeneAlgebra (α : Type u_5) extends IdemSemiring , KStar , Semiring , SemilatticeSup , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , MulOneClass , AddMonoidWithOne , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , AddMonoid , One , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , PartialOrder , Preorder , LE , LT : 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

theorem KleeneAlgebra.one_le_kstar {α : Type u_5} [self : KleeneAlgebra α] (a : α) : 1 ≤ KStar.kstar a

theorem KleeneAlgebra.mul_kstar_le_kstar {α : Type u_5} [self : KleeneAlgebra α] (a : α) : a * KStar.kstar a ≤ KStar.kstar a

theorem KleeneAlgebra.kstar_mul_le_kstar {α : Type u_5} [self : KleeneAlgebra α] (a : α) : KStar.kstar a * a ≤ KStar.kstar a

theorem KleeneAlgebra.mul_kstar_le_self {α : Type u_5} [self : KleeneAlgebra α] (a : α) (b : α) : b * a ≤ b → b * KStar.kstar a ≤ b

theorem KleeneAlgebra.kstar_mul_le_self {α : Type u_5} [self : KleeneAlgebra α] (a : α) (b : α) : a * b ≤ b → KStar.kstar a * b ≤ b

@[instance 100]

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

Equations

• IdemSemiring.toOrderBot = OrderBot.mk ⋯

@[reducible, inline]

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

Construct an idempotent semiring from an idempotent addition.

Equations

• IdemSemiring.ofSemiring h = 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 100]

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

Equations

• IdemSemiring.toCanonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

@[instance 100]

instance IdemSemiring.toMulLeftMono {α : Type u_1} [IdemSemiring α] : MulLeftMono α

Equations

• ⋯ = ⋯

@[instance 100]

instance IdemSemiring.toMulRightMono {α : Type u_1} [IdemSemiring α] : MulRightMono α

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 = IdemSemiring.mk ⋯ ⊥ ⋯

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

Equations

• Prod.instIdemCommSemiring = IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯

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

Equations

• Prod.instKleeneAlgebra = 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 = IdemSemiring.mk ⋯ ⊥ ⋯

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

Equations

• Pi.instIdemCommSemiringForall = IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯

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

Equations

• Pi.instKleeneAlgebraForall = 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, inline]

abbrev Function.Injective.idemSemiring {α : Type u_1} {β : Type u_2} [IdemSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [Max β] [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 : ∀ (n : ℕ) (x : β), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (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

• Function.Injective.idemSemiring f hf zero one add mul nsmul npow natCast sup bot = IdemSemiring.mk ⋯ ⊥ ⋯

@[reducible, inline]

abbrev Function.Injective.idemCommSemiring {α : Type u_1} {β : Type u_2} [IdemCommSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [Max β] [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 : ∀ (n : ℕ) (x : β), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (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

• Function.Injective.idemCommSemiring f hf zero one add mul nsmul npow natCast sup bot = IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯

@[reducible, inline]

abbrev Function.Injective.kleeneAlgebra {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [Zero β] [One β] [Add β] [Mul β] [Pow β ℕ] [SMul ℕ β] [NatCast β] [Max β] [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 : ∀ (n : ℕ) (x : β), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (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

• Function.Injective.kleeneAlgebra f hf zero one add mul nsmul npow natCast sup bot kstar = KleeneAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯