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.

  • 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 : α), AddMonoid.nsmul 0 x = 0
  • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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.natCast 0 = 0
  • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
  • npow : αα
  • npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
  • npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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
Instances

    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 : α), AddMonoid.nsmul 0 x = 0
    • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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.natCast 0 = 0
    • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
    • npow : αα
    • npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
    • npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 : α
    • bot_le : ∀ (a : α), IdemCommSemiring.bot a
    Instances
      class KStar (α : Type u_5) :
      Type u_5

      Notation typeclass for the Kleene star .

      • kstar : αα
      Instances
        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 IdemSemiring.toOrderBot {α : Type u_1} [IdemSemiring α] :
          Equations
          • IdemSemiring.toOrderBot = let __src := inst; OrderBot.mk
          @[reducible]
          def 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 = 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 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
            Equations
            instance IdemSemiring.toCovariantClass_mul_le {α : Type u_1} [IdemSemiring α] :
            CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
            Equations
            • =
            instance IdemSemiring.toCovariantClass_swap_mul_le {α : Type u_1} [IdemSemiring α] :
            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} [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 : α} :
            theorem kstar_mono {α : Type u_1} [KleeneAlgebra α] :
            Monotone KStar.kstar
            @[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
            Equations
            • Prod.instIdemCommSemiringProd = let __src := Prod.instCommSemiring; let __src_1 := Prod.instIdemSemiring; IdemCommSemiring.mk IdemSemiring.bot
            instance Prod.instKleeneAlgebraProd {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] :
            Equations
            • Prod.instKleeneAlgebraProd = let __src := Prod.instIdemSemiring; KleeneAlgebra.mk
            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
            • Pi.instIdemSemiring = let __src := Pi.semiring; let __src_1 := Pi.instSemilatticeSup; let __src_2 := Pi.instOrderBot; IdemSemiring.mk
            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) :
            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]
            def Function.Injective.idemSemiring {α : Type u_1} {β : Type u_2} [IdemSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [SMul β] [NatCast β] [Sup β] [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 IdemSemiring instance along an injective function.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[reducible]
              def Function.Injective.idemCommSemiring {α : Type u_1} {β : Type u_2} [IdemCommSemiring α] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [SMul β] [NatCast β] [Sup β] [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 IdemCommSemiring instance along an injective function.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible]
                def Function.Injective.kleeneAlgebra {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [SMul β] [NatCast β] [Sup β] [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 : ∀ (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 (KStar.kstar a) = 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