# mathlib3documentation

algebra.order.kleene

# Kleene Algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• idem_semiring: Idempotent semiring
• idem_comm_semiring: Idempotent commutative semiring
• kleene_algebra: Kleene algebra

## Notation #

a∗ is notation for kstar a in locale computability.

## TODO #

Instances for add_opposite, mul_opposite, ulift, subsemiring, subring, subalgebra.

## Tags #

kleene algebra, idempotent semiring

@[instance]
def idem_semiring.to_semiring (α : Type u) [self : idem_semiring α] :
@[class]
structure idem_semiring (α : Type u) :
• 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) . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : α), = x + . "try_refl_tac"
• 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
• nat_cast : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), idem_semiring.nat_cast (n + 1) = . "control_laws_tac"
• npow : α α
• npow_zero' : ( (x : α), = 1) . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), = x * . "try_refl_tac"
• 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) . "order_laws_tac"
• 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) . "try_refl_tac"
• bot : α
• bot_le : (a : α),

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

Instances of this typeclass
Instances of other typeclasses for idem_semiring
• idem_semiring.has_sizeof_inst
@[instance]
@[instance]
@[instance]
@[class]
structure idem_comm_semiring (α : Type u) :
• 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 : α), . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : α), . "try_refl_tac"
• 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
• nat_cast : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), . "control_laws_tac"
• npow : α α
• npow_zero' : ( (x : α), = 1) . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), = x * . "try_refl_tac"
• 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) . "order_laws_tac"
• 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) . "try_refl_tac"
• bot : α
• bot_le : (a : α),

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

Instances of this typeclass
Instances of other typeclasses for idem_comm_semiring
• idem_comm_semiring.has_sizeof_inst
@[class]
structure has_kstar (α : Type u_5) :
Type u_5
• kstar : α α

Notation typeclass for the Kleene star ∗.

Instances of this typeclass
Instances of other typeclasses for has_kstar
• has_kstar.has_sizeof_inst
@[instance]
def kleene_algebra.to_idem_semiring (α : Type u_5) [self : kleene_algebra α] :
@[class]
structure kleene_algebra (α : Type u_5) :
Type u_5
• 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) . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : α), = x + . "try_refl_tac"
• 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
• nat_cast : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), kleene_algebra.nat_cast (n + 1) = . "control_laws_tac"
• npow : α α
• npow_zero' : ( (x : α), = 1) . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), = x * . "try_refl_tac"
• 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) . "order_laws_tac"
• 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) . "try_refl_tac"
• bot : α
• bot_le : (a : α),
• kstar : α α
• one_le_kstar : (a : α),
• mul_kstar_le_kstar : (a : α),
• kstar_mul_le_kstar : (a : α),
• mul_kstar_le_self : (a b : α), b * a b b
• kstar_mul_le_self : (a b : α), a * b b b

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
Instances of this typeclass
Instances of other typeclasses for kleene_algebra
• kleene_algebra.has_sizeof_inst
@[instance]
def kleene_algebra.to_has_kstar (α : Type u_5) [self : kleene_algebra α] :
@[protected, instance]
def idem_semiring.to_order_bot {α : Type u_1}  :
Equations
@[reducible]
def idem_semiring.of_semiring {α : Type u_1} [semiring α] (h : (a : α), a + a = a) :

Construct an idempotent semiring from an idempotent addition.

Equations
@[simp]
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 : } (hn : 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 has_le.le.add_eq_left {α : Type u_1} {a b : α} :
b a a + b = a

Alias of the reverse direction of add_eq_left_iff_le.

theorem has_le.le.add_eq_right {α : Type u_1} {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} {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
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[simp]
theorem one_le_kstar {α : Type u_1} {a : α} :
theorem mul_kstar_le_kstar {α : Type u_1} {a : α} :
theorem kstar_mul_le_kstar {α : Type u_1} {a : α} :
theorem mul_kstar_le_self {α : Type u_1} {a b : α} :
b * a b b
theorem kstar_mul_le_self {α : Type u_1} {a b : α} :
a * b b b
theorem mul_kstar_le {α : Type u_1} {a b c : α} (hb : b c) (ha : c * a c) :
c
theorem kstar_mul_le {α : Type u_1} {a b c : α} (hb : b c) (ha : a * c c) :
c
theorem kstar_le_of_mul_le_left {α : Type u_1} {a b : α} (hb : 1 b) :
b * a b
theorem kstar_le_of_mul_le_right {α : Type u_1} {a b : α} (hb : 1 b) :
a * b b
@[simp]
theorem le_kstar {α : Type u_1} {a : α} :
theorem kstar_mono {α : Type u_1}  :
@[simp]
theorem kstar_eq_one {α : Type u_1} {a : α} :
a 1
@[simp]
theorem kstar_zero {α : Type u_1}  :
@[simp]
theorem kstar_one {α : Type u_1}  :
@[simp]
theorem kstar_mul_kstar {α : Type u_1} (a : α) :
@[simp]
theorem kstar_eq_self {α : Type u_1} {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
@[protected, instance]
def prod.idem_semiring {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def prod.idem_comm_semiring {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def prod.kleene_algebra {α : Type u_1} {β : Type u_2}  :
Equations
theorem prod.kstar_def {α : Type u_1} {β : Type u_2} (a : α × β) :
@[simp]
theorem prod.fst_kstar {α : Type u_1} {β : Type u_2} (a : α × β) :
@[simp]
theorem prod.snd_kstar {α : Type u_1} {β : Type u_2} (a : α × β) :
@[protected, instance]
def pi.idem_semiring {ι : Type u_3} {π : ι Type u_4} [Π (i : ι), idem_semiring (π i)] :
idem_semiring (Π (i : ι), π i)
Equations
@[protected, instance]
def pi.idem_comm_semiring {ι : Type u_3} {π : ι Type u_4} [Π (i : ι), idem_comm_semiring (π i)] :
idem_comm_semiring (Π (i : ι), π i)
Equations
@[protected, instance]
def pi.kleene_algebra {ι : Type u_3} {π : ι Type u_4} [Π (i : ι), kleene_algebra (π i)] :
kleene_algebra (Π (i : ι), π i)
Equations
theorem pi.kstar_def {ι : Type u_3} {π : ι Type u_4} [Π (i : ι), kleene_algebra (π i)] (a : Π (i : ι), π i) :
= λ (i : ι), has_kstar.kstar (a i)
@[simp]
theorem pi.kstar_apply {ι : Type u_3} {π : ι Type u_4} [Π (i : ι), kleene_algebra (π i)] (a : Π (i : ι), π i) (i : ι) :
@[protected, reducible]
def function.injective.idem_semiring {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] [has_sup β] [has_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 = ) :

Pullback an idem_semiring instance along an injective function.

Equations
@[protected, reducible]
def function.injective.idem_comm_semiring {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] [has_sup β] [has_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 = ) :

Pullback an idem_comm_semiring instance along an injective function.

Equations
@[protected, reducible]
def function.injective.kleene_algebra {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] [has_sup β] [has_bot β] [has_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 = has_kstar.kstar (f a)) :

Pullback an idem_comm_semiring instance along an injective function.

Equations