Documentation

Mathlib.Algebra.Order.Kleene

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 #

Notation #

a∗ is notation for kstar a in locale Computability.

References #

TODO #

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

Tags #

kleene algebra, idempotent semiring

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

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

Instances
    class IdemCommSemiring (α : Type u) extends CommSemiring α, IdemSemiring α :

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

    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 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
            Instances
              @[instance 100]
              instance IdemSemiring.toOrderBot {α : Type u_1} [IdemSemiring α] :
              Equations
                @[reducible, inline]
                abbrev IdemSemiring.ofSemiring {α : Type u_1} [Semiring α] (h : ∀ (a : α), a + a = a) :

                Construct an idempotent semiring from an idempotent addition.

                Equations
                  Instances For
                    theorem add_eq_sup {α : Type u_1} [IdemSemiring α] (a b : α) :
                    a + b = ab
                    theorem add_idem {α : Type u_1} [IdemSemiring α] (a : α) :
                    a + a = a
                    theorem natCast_eq_one {α : Type u_1} [IdemSemiring α] {n : } (nezero : n 0) :
                    n = 1
                    theorem ofNat_eq_one {α : Type u_1} [IdemSemiring α] {n : } [n.AtLeastTwo] :
                    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 aa + 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 ba + 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 100]
                    @[simp]
                    theorem one_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} :
                    theorem mul_kstar_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} :
                    theorem kstar_mul_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} :
                    theorem mul_kstar_le_self {α : Type u_1} [KleeneAlgebra α] {a b : α} :
                    b * a bb * KStar.kstar a b
                    theorem kstar_mul_le_self {α : Type u_1} [KleeneAlgebra α] {a b : α} :
                    a * b bKStar.kstar a * b b
                    theorem mul_kstar_le {α : Type u_1} [KleeneAlgebra α] {a b c : α} (hb : b c) (ha : c * a c) :
                    theorem kstar_mul_le {α : Type u_1} [KleeneAlgebra α] {a b c : α} (hb : b c) (ha : a * c c) :
                    theorem kstar_le_of_mul_le_left {α : Type u_1} [KleeneAlgebra α] {a b : α} (hb : 1 b) :
                    b * a bKStar.kstar a b
                    theorem kstar_le_of_mul_le_right {α : Type u_1} [KleeneAlgebra α] {a b : α} (hb : 1 b) :
                    a * b bKStar.kstar a b
                    @[simp]
                    theorem le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} :
                    @[simp]
                    theorem kstar_eq_one {α : Type u_1} [KleeneAlgebra α] {a : α} :
                    @[simp]
                    theorem kstar_zero {α : Type u_1} [KleeneAlgebra α] :
                    @[simp]
                    theorem kstar_one {α : Type u_1} [KleeneAlgebra α] :
                    @[simp]
                    theorem kstar_mul_kstar {α : Type u_1} [KleeneAlgebra α] (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 : α) :
                    @[simp]
                    theorem pow_le_kstar {α : Type u_1} [KleeneAlgebra α] {a : α} {n : } :
                    instance Prod.instIdemSemiring {α : Type u_1} {β : Type u_2} [IdemSemiring α] [IdemSemiring β] :
                    Equations
                      instance Prod.instIdemCommSemiring {α : Type u_1} {β : Type u_2} [IdemCommSemiring α] [IdemCommSemiring β] :
                      Equations
                        instance Prod.instKleeneAlgebra {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] :
                        Equations
                          theorem Prod.kstar_def {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) :
                          @[simp]
                          theorem Prod.fst_kstar {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) :
                          @[simp]
                          theorem Prod.snd_kstar {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) :
                          instance Pi.instIdemSemiring {ι : Type u_3} {π : ιType u_4} [(i : ι) → IdemSemiring (π i)] :
                          IdemSemiring ((i : ι) → π i)
                          Equations
                            instance Pi.instIdemCommSemiringForall {ι : Type u_3} {π : ιType u_4} [(i : ι) → IdemCommSemiring (π i)] :
                            IdemCommSemiring ((i : ι) → π i)
                            Equations
                              instance Pi.instKleeneAlgebraForall {ι : Type u_3} {π : ιType u_4} [(i : ι) → KleeneAlgebra (π i)] :
                              KleeneAlgebra ((i : ι) → π i)
                              Equations
                                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 : ι) :
                                @[reducible, inline]
                                abbrev Function.Injective.idemSemiring {α : Type u_1} {β : Type u_2} [IdemSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [SMul β] [NatCast β] [Max β] [Bot β] (f : βα) (hf : 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 (ab) = f af b) (bot : f = ) :

                                Pullback an IdemSemiring instance along an injective function.

                                Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev Function.Injective.idemCommSemiring {α : Type u_1} {β : Type u_2} [IdemCommSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [SMul β] [NatCast β] [Max β] [Bot β] (f : βα) (hf : 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 (ab) = f af b) (bot : f = ) :

                                    Pullback an IdemCommSemiring instance along an injective function.

                                    Equations
                                      Instances For
                                        @[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 : 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 (ab) = f af b) (bot : f = ) (kstar : ∀ (a : β), f (KStar.kstar a) = KStar.kstar (f a)) :

                                        Pullback a KleeneAlgebra instance along an injective function.

                                        Equations
                                          Instances For