# 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.

## TODO #

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

## Tags #

kleene algebra, idempotent semiring

class IdemSemiring (α : Type u) extends , :

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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + 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_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• sup : ααα
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• add_eq_sup : ∀ (a b : α), a + b = a b
• bot : α

The bottom element of an idempotent semiring: 0 by default

• bot_le : ∀ (a : α), IdemSemiring.bot a
Instances
theorem IdemSemiring.add_eq_sup {α : Type u} [self : ] (a : α) (b : α) :
a + b = a b
theorem IdemSemiring.bot_le {α : Type u} [self : ] (a : α) :
IdemSemiring.bot a
class IdemCommSemiring (α : Type u) extends , :

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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + 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_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * 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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• add_eq_sup : ∀ (a b : α), a + b = a b
• bot : α

The bottom element of an idempotent semiring: 0 by default

• bot_le : ∀ (a : α), IdemCommSemiring.bot a
Instances
class KStar (α : Type u_5) :
Type u_5

Notation typeclass for the Kleene star ∗.

• kstar : αα

The Kleene star operator on a Kleene algebra

Instances

The Kleene star operator on a Kleene algebra

Equations
Instances For
class KleeneAlgebra (α : Type u_5) extends , :
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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + 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_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• sup : ααα
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• add_eq_sup : ∀ (a b : α), a + b = a b
• bot : α
• bot_le : ∀ (a : α), IdemSemiring.bot a
• kstar : αα
• one_le_kstar : ∀ (a : α), 1
• mul_kstar_le_kstar : ∀ (a : α), a *
• kstar_mul_le_kstar : ∀ (a : α), * a
• mul_kstar_le_self : ∀ (a b : α), b * a bb * b
• kstar_mul_le_self : ∀ (a b : α), a * b b * b b
Instances
theorem KleeneAlgebra.one_le_kstar {α : Type u_5} [self : ] (a : α) :
1
theorem KleeneAlgebra.mul_kstar_le_kstar {α : Type u_5} [self : ] (a : α) :
a *
theorem KleeneAlgebra.kstar_mul_le_kstar {α : Type u_5} [self : ] (a : α) :
* a
theorem KleeneAlgebra.mul_kstar_le_self {α : Type u_5} [self : ] (a : α) (b : α) :
b * a bb * b
theorem KleeneAlgebra.kstar_mul_le_self {α : Type u_5} [self : ] (a : α) (b : α) :
a * b b * b b
@[instance 100]
instance IdemSemiring.toOrderBot {α : Type u_1} [] :
Equations
• IdemSemiring.toOrderBot = let __src := inst;
@[reducible, inline]
abbrev IdemSemiring.ofSemiring {α : Type u_1} [] (h : ∀ (a : α), a + a = a) :

Construct an idempotent semiring from an idempotent addition.

Equations
• = let __src := inst;
Instances For
theorem add_eq_sup {α : Type u_1} [] (a : α) (b : α) :
a + b = a b
theorem add_idem {α : Type u_1} [] (a : α) :
a + a = a
theorem nsmul_eq_self {α : Type u_1} [] {n : } :
n 0∀ (a : α), n a = a
theorem add_eq_left_iff_le {α : Type u_1} [] {a : α} {b : α} :
a + b = a b a
theorem add_eq_right_iff_le {α : Type u_1} [] {a : α} {b : α} :
a + b = b a b
theorem LE.le.add_eq_left {α : Type u_1} [] {a : α} {b : α} :
b aa + b = a

Alias of the reverse direction of add_eq_left_iff_le.

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

Alias of the reverse direction of add_eq_right_iff_le.

theorem add_le_iff {α : Type u_1} [] {a : α} {b : α} {c : α} :
a + b c a c b c
theorem add_le {α : Type u_1} [] {a : α} {b : α} {c : α} (ha : a c) (hb : b c) :
a + b c
@[instance 100]
Equations
• IdemSemiring.toCanonicallyOrderedAddCommMonoid = let __src := inst;
@[instance 100]
instance IdemSemiring.toCovariantClass_mul_le {α : Type u_1} [] :
CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
Equations
• =
@[instance 100]
instance IdemSemiring.toCovariantClass_swap_mul_le {α : Type u_1} [] :
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} [] {a : α} :
1
theorem mul_kstar_le_kstar {α : Type u_1} [] {a : α} :
a *
theorem kstar_mul_le_kstar {α : Type u_1} [] {a : α} :
* a
theorem mul_kstar_le_self {α : Type u_1} [] {a : α} {b : α} :
b * a bb * b
theorem kstar_mul_le_self {α : Type u_1} [] {a : α} {b : α} :
a * b b * b b
theorem mul_kstar_le {α : Type u_1} [] {a : α} {b : α} {c : α} (hb : b c) (ha : c * a c) :
b * c
theorem kstar_mul_le {α : Type u_1} [] {a : α} {b : α} {c : α} (hb : b c) (ha : a * c c) :
* b c
theorem kstar_le_of_mul_le_left {α : Type u_1} [] {a : α} {b : α} (hb : 1 b) :
b * a b b
theorem kstar_le_of_mul_le_right {α : Type u_1} [] {a : α} {b : α} (hb : 1 b) :
a * b b b
@[simp]
theorem le_kstar {α : Type u_1} [] {a : α} :
a
theorem kstar_mono {α : Type u_1} [] :
Monotone KStar.kstar
@[simp]
theorem kstar_eq_one {α : Type u_1} [] {a : α} :
= 1 a 1
@[simp]
theorem kstar_zero {α : Type u_1} [] :
= 1
@[simp]
theorem kstar_one {α : Type u_1} [] :
= 1
@[simp]
theorem kstar_mul_kstar {α : Type u_1} [] (a : α) :
@[simp]
theorem kstar_eq_self {α : Type u_1} [] {a : α} :
= a a * a = a 1 a
@[simp]
theorem kstar_idem {α : Type u_1} [] (a : α) :
@[simp]
theorem pow_le_kstar {α : Type u_1} [] {a : α} {n : } :
a ^ n
instance Prod.instIdemSemiring {α : Type u_1} {β : Type u_2} [] [] :
Equations
• Prod.instIdemSemiring = let __src := Prod.instSemiring; let __src_1 := ; let __src_2 := ;
instance Prod.instIdemCommSemiring {α : Type u_1} {β : Type u_2} [] [] :
Equations
• Prod.instIdemCommSemiring = let __src := Prod.instCommSemiring; let __src_1 := Prod.instIdemSemiring; IdemCommSemiring.mk IdemSemiring.bot
instance Prod.instKleeneAlgebra {α : Type u_1} {β : Type u_2} [] [] :
Equations
• Prod.instKleeneAlgebra = let __src := Prod.instIdemSemiring; KleeneAlgebra.mk
theorem Prod.kstar_def {α : Type u_1} {β : Type u_2} [] [] (a : α × β) :
@[simp]
theorem Prod.fst_kstar {α : Type u_1} {β : Type u_2} [] [] (a : α × β) :
().1 = KStar.kstar a.1
@[simp]
theorem Prod.snd_kstar {α : Type u_1} {β : Type u_2} [] [] (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;
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) :
= 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)
@[reducible, inline]
abbrev Function.Injective.idemSemiring {α : Type u_1} {β : Type u_2} [] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] [Sup β] [Bot β] (f : βα) (hf : ) (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 = ) :

Pullback an IdemSemiring instance along an injective function.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev Function.Injective.idemCommSemiring {α : Type u_1} {β : Type u_2} [] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] [Sup β] [Bot β] (f : βα) (hf : ) (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 = ) :

Pullback an IdemCommSemiring instance along an injective function.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev Function.Injective.kleeneAlgebra {α : Type u_1} {β : Type u_2} [] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] [Sup β] [Bot β] [] (f : βα) (hf : ) (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 (f a)) :

Pullback a KleeneAlgebra instance along an injective function.

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