scilib documentation

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 #

Notation #

a∗ is notation for kstar a in locale computability.

References #

TODO #

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

Tags #

kleene algebra, idempotent semiring

source
@[instance]
def idem_semiring.to_semiring (α : Type u) [self : idem_semiring α] :
semiring α
source
@[class]
structure idem_semiring (α : Type u) :
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 : α), idem_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), idem_semiring.nsmul n.succ x = x + idem_semiring.nsmul 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 : idem_semiring.nat_cast 0 = 0 . "control_laws_tac"
  • nat_cast_succ : (∀ (n : ℕ), idem_semiring.nat_cast (n + 1) = idem_semiring.nat_cast n + 1) . "control_laws_tac"
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), idem_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), idem_semiring.npow n.succ x = x * idem_semiring.npow n 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 : α), idem_semiring.bot ≤ 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
source
@[instance]
def idem_semiring.to_semilattice_sup (α : Type u) [self : idem_semiring α] :
semilattice_sup α
source
@[instance]
def idem_comm_semiring.to_comm_semiring (α : Type u) [self : idem_comm_semiring α] :
comm_semiring α
source
@[instance]
def idem_comm_semiring.to_idem_semiring (α : Type u) [self : idem_comm_semiring α] :
idem_semiring α
source
@[class]
structure idem_comm_semiring (α : Type u) :
Type u

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

Construct an idempotent semiring from an idempotent addition.

Equations
source
@[simp]
theorem add_eq_sup {α : Type u_1} [idem_semiring α] (a b : α) :
a + b = a ⊔ b
source
theorem add_idem {α : Type u_1} [idem_semiring α] (a : α) :
a + a = a
source
theorem nsmul_eq_self {α : Type u_1} [idem_semiring α] {n : ℕ} (hn : n ≠ 0) (a : α) :
n • a = a
source
theorem add_eq_left_iff_le {α : Type u_1} [idem_semiring α] {a b : α} :
a + b = a ↔ b ≤ a
source
theorem add_eq_right_iff_le {α : Type u_1} [idem_semiring α] {a b : α} :
a + b = b ↔ a ≤ b
source
theorem has_le.le.add_eq_left {α : Type u_1} [idem_semiring α] {a b : α} :
b ≤ a → a + b = a

Alias of the reverse direction of add_eq_left_iff_le.

source
theorem has_le.le.add_eq_right {α : Type u_1} [idem_semiring α] {a b : α} :
a ≤ b → a + b = b

Alias of the reverse direction of add_eq_right_iff_le.

source
theorem add_le_iff {α : Type u_1} [idem_semiring α] {a b c : α} :
a + b ≤ c ↔ a ≤ c ∧ b ≤ c
source
theorem add_le {α : Type u_1} [idem_semiring α] {a b c : α} (ha : a ≤ c) (hb : b ≤ c) :
a + b ≤ c
source
@[protected, instance]
def idem_semiring.to_canonically_ordered_add_monoid {α : Type u_1} [idem_semiring α] :
canonically_ordered_add_monoid α
Equations
source
@[protected, instance]
def idem_semiring.to_covariant_class_mul_le {α : Type u_1} [idem_semiring α] :
covariant_class α α has_mul.mul has_le.le
source
@[protected, instance]
def idem_semiring.to_covariant_class_swap_mul_le {α : Type u_1} [idem_semiring α] :
covariant_class α α (function.swap has_mul.mul) has_le.le
source
@[simp]
theorem one_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :
1 ≤ has_kstar.kstar a
source
theorem mul_kstar_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :
a * has_kstar.kstar a ≤ has_kstar.kstar a
source
theorem kstar_mul_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :
has_kstar.kstar a * a ≤ has_kstar.kstar a
source
theorem mul_kstar_le_self {α : Type u_1} [kleene_algebra α] {a b : α} :
b * a ≤ b → b * has_kstar.kstar a ≤ b
source
theorem kstar_mul_le_self {α : Type u_1} [kleene_algebra α] {a b : α} :
a * b ≤ b → has_kstar.kstar a * b ≤ b
source
theorem mul_kstar_le {α : Type u_1} [kleene_algebra α] {a b c : α} (hb : b ≤ c) (ha : c * a ≤ c) :
b * has_kstar.kstar a ≤ c
source
theorem kstar_mul_le {α : Type u_1} [kleene_algebra α] {a b c : α} (hb : b ≤ c) (ha : a * c ≤ c) :
has_kstar.kstar a * b ≤ c
source
theorem kstar_le_of_mul_le_left {α : Type u_1} [kleene_algebra α] {a b : α} (hb : 1 ≤ b) :
b * a ≤ b → has_kstar.kstar a ≤ b
source
theorem kstar_le_of_mul_le_right {α : Type u_1} [kleene_algebra α] {a b : α} (hb : 1 ≤ b) :
a * b ≤ b → has_kstar.kstar a ≤ b
source
@[simp]
theorem le_kstar {α : Type u_1} [kleene_algebra α] {a : α} :
a ≤ has_kstar.kstar a
source
theorem kstar_mono {α : Type u_1} [kleene_algebra α] :
monotone has_kstar.kstar
source
@[simp]
theorem kstar_eq_one {α : Type u_1} [kleene_algebra α] {a : α} :
has_kstar.kstar a = 1 ↔ a ≤ 1
source
@[simp]
theorem kstar_zero {α : Type u_1} [kleene_algebra α] :
has_kstar.kstar 0 = 1
source
@[simp]
theorem kstar_one {α : Type u_1} [kleene_algebra α] :
has_kstar.kstar 1 = 1
source
@[simp]
theorem kstar_mul_kstar {α : Type u_1} [kleene_algebra α] (a : α) :
has_kstar.kstar a * has_kstar.kstar a = has_kstar.kstar a
source
@[simp]
theorem kstar_eq_self {α : Type u_1} [kleene_algebra α] {a : α} :
has_kstar.kstar a = a ↔ a * a = a ∧ 1 ≤ a
source
@[simp]
theorem kstar_idem {α : Type u_1} [kleene_algebra α] (a : α) :
has_kstar.kstar (has_kstar.kstar a) = has_kstar.kstar a
source
@[simp]
theorem pow_le_kstar {α : Type u_1} [kleene_algebra α] {a : α} {n : ℕ} :
a ^ n ≤ has_kstar.kstar a
source
@[protected, instance]
def prod.idem_semiring {α : Type u_1} {β : Type u_2} [idem_semiring α] [idem_semiring β] :
idem_semiring (α × β)
Equations
source
@[protected, instance]
def prod.idem_comm_semiring {α : Type u_1} {β : Type u_2} [idem_comm_semiring α] [idem_comm_semiring β] :
idem_comm_semiring (α × β)
Equations
source
@[protected, instance]
def prod.kleene_algebra {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] :
kleene_algebra (α × β)
Equations
source
theorem prod.kstar_def {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] (a : α × β) :
has_kstar.kstar a = (has_kstar.kstar a.fst, has_kstar.kstar a.snd)
source
@[simp]
theorem prod.fst_kstar {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] (a : α × β) :
(has_kstar.kstar a).fst = has_kstar.kstar a.fst
source
@[simp]
theorem prod.snd_kstar {α : Type u_1} {β : Type u_2} [kleene_algebra α] [kleene_algebra β] (a : α × β) :
(has_kstar.kstar a).snd = has_kstar.kstar a.snd
source
@[protected, instance]
def pi.idem_semiring {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), idem_semiring (π i)] :
idem_semiring (Π (i : ι), π i)
Equations
source
@[protected, instance]
def pi.idem_comm_semiring {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), idem_comm_semiring (π i)] :
idem_comm_semiring (Π (i : ι), π i)
Equations
source
@[protected, instance]
def pi.kleene_algebra {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), kleene_algebra (π i)] :
kleene_algebra (Π (i : ι), π i)
Equations
source
theorem pi.kstar_def {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), kleene_algebra (π i)] (a : Π (i : ι), π i) :
has_kstar.kstar a = λ (i : ι), has_kstar.kstar (a i)
source
@[simp]
theorem pi.kstar_apply {ι : Type u_3} {π : ι → Type u_4} [Π (i : ι), kleene_algebra (π i)] (a : Π (i : ι), π i) (i : ι) :
has_kstar.kstar a i = has_kstar.kstar (a i)
source
@[protected, reducible]
def function.injective.idem_semiring {α : Type u_1} {β : Type u_2} [idem_semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_pow β ℕ] [has_smul ℕ β] [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 ⊥ = ⊥) :
idem_semiring β

Pullback an idem_semiring instance along an injective function.

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

Pullback an idem_comm_semiring instance along an injective function.

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

Pullback an idem_comm_semiring instance along an injective function.

Equations