Mathlib.Algebra.Order.Kleene

IdemSemiring structure

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

Full source

/-- An idempotent semiring is a semiring with the additional property that addition is idempotent.
-/
class IdemSemiring (α : Type u) extends Semiring α, SemilatticeSup α where
  protected sup := (· + ·)
  protected add_eq_sup : ∀ a b : α, a + b = a ⊔ b := by
    intros
    rfl
  /-- The bottom element of an idempotent semiring: `0` by default -/
  protected bot : α := 0
  protected bot_le : ∀ a, bot ≤ a

Idempotent Semiring

Informal description

An idempotent semiring is a semiring $\alpha$ equipped with a semilattice structure where the addition operation is idempotent (i.e., $a + a = a$ for all $a \in \alpha$) and the partial order is defined by $a \leq b$ if and only if $a + b = b$.

IdemCommSemiring structure

(α : Type u) extends CommSemiring α, IdemSemiring α

Full source

/-- An idempotent commutative semiring is a commutative semiring with the additional property that
addition is idempotent. -/
class IdemCommSemiring (α : Type u) extends CommSemiring α, IdemSemiring α

Idempotent Commutative Semiring

Informal description

An idempotent commutative semiring is a commutative semiring $\alpha$ equipped with a semilattice structure where the addition operation is idempotent (i.e., $a + a = a$ for all $a \in \alpha$) and the partial order is defined by $a \leq b \leftrightarrow a + b = b$.

KStar structure

(α : Type*)

Full source

/-- Notation typeclass for the Kleene star `∗`. -/
class KStar (α : Type*) where
  /-- The Kleene star operator on a Kleene algebra -/
  protected kstar : α → α

Kleene star operator

Informal description

The structure `KStar` represents the typeclass for the Kleene star operator `∗` on a type `α`. This operator is fundamental in the theory of Kleene algebras, where it is used to denote the reflexive-transitive closure operation.

Computability.term_∗ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped[Computability] postfix:1024 "∗" => KStar.kstar

Kleene star notation

Informal description

The notation `a∗` is defined as the Kleene star operation applied to `a`, where `a` is an element of a type equipped with a Kleene algebra structure. This operation is used in the context of computability theory and formal languages.

KleeneAlgebra structure

(α : Type*) extends IdemSemiring α, KStar α

Full source

/-- 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`
-/
class KleeneAlgebra (α : Type*) extends IdemSemiring α, KStar α where
  protected one_le_kstar : ∀ a : α, 1 ≤ a∗
  protected mul_kstar_le_kstar : ∀ a : α, a * a∗ ≤ a∗
  protected kstar_mul_le_kstar : ∀ a : α, a∗ * a ≤ a∗
  protected mul_kstar_le_self : ∀ a b : α, b * a ≤ b → b * a∗ ≤ b
  protected kstar_mul_le_self : ∀ a b : α, a * b ≤ b → a∗ * b ≤ b

Kleene Algebra

Informal description

A Kleene algebra is an idempotent semiring $\alpha$ equipped with an additional unary operation $*$ (called the Kleene star) satisfying the following properties for all $a, b, c \in \alpha$: 1. $1 + a \cdot a^* \leq a^*$ 2. $1 + a^* \cdot a \leq a^*$ 3. If $a \cdot c + b \leq c$, then $a^* \cdot b \leq c$ 4. If $c \cdot a + b \leq c$, then $b \cdot a^* \leq c$

IdemSemiring.toOrderBot instance

[IdemSemiring α] : OrderBot α

Full source

instance (priority := 100) IdemSemiring.toOrderBot [IdemSemiring α] : OrderBot α :=
  { ‹IdemSemiring α› with }

Bottom Element in Idempotent Semirings

Informal description

Every idempotent semiring $\alpha$ has a bottom element $\bot$ with respect to its canonical order.

IdemSemiring.ofSemiring abbrev

[Semiring α] (h : ∀ a : α, a + a = a) : IdemSemiring α

Full source

/-- Construct an idempotent semiring from an idempotent addition. -/
abbrev IdemSemiring.ofSemiring [Semiring α] (h : ∀ a : α, a + a = a) : IdemSemiring α :=
  { ‹Semiring α› with
    le := fun a b ↦ a + b = b
    le_refl := h
    le_trans := fun a b c hab hbc ↦ by
      rw [← hbc, ← add_assoc, hab]
    le_antisymm := fun a b hab hba ↦ by rwa [← hba, add_comm]
    sup := (· + ·)
    le_sup_left := fun a b ↦ by
      rw [← add_assoc, h]
    le_sup_right := fun a b ↦ by
      rw [add_comm, add_assoc, h]
    sup_le := fun a b c hab hbc ↦ by
      rwa [add_assoc, hbc]
    bot := 0
    bot_le := zero_add }

Construction of Idempotent Semiring from Semiring with Idempotent Addition

Informal description

Given a semiring $\alpha$ where addition is idempotent (i.e., $a + a = a$ for all $a \in \alpha$), the structure `IdemSemiring α` can be constructed, equipping $\alpha$ with the properties of an idempotent semiring.

add_eq_sup theorem

(a b : α) : a + b = a ⊔ b

Full source

theorem add_eq_sup (a b : α) : a + b = a ⊔ b :=
  IdemSemiring.add_eq_sup _ _

Addition as Supremum in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, the addition operation coincides with the supremum operation, i.e., for any elements $a, b \in \alpha$, we have $a + b = a \sqcup b$.

add_idem theorem

(a : α) : a + a = a

Full source

theorem add_idem (a : α) : a + a = a := by simp

Idempotence of Addition in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, addition is idempotent, meaning that for any element $a \in \alpha$, we have $a + a = a$.

natCast_eq_one theorem

{n : ℕ} (nezero : n ≠ 0) : (n : α) = 1

Full source

lemma natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1 := by
  rw [← Nat.one_le_iff_ne_zero] at nezero
  induction n, nezero using Nat.le_induction with
  | base => exact Nat.cast_one
  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

Embedding of Nonzero Natural Numbers Yields One in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, for any nonzero natural number $n$, the canonical embedding of $n$ into $\alpha$ equals the multiplicative identity $1$, i.e., $n = 1$.

ofNat_eq_one theorem

{n : ℕ} [n.AtLeastTwo] : (ofNat(n) : α) = 1

Full source

lemma ofNat_eq_one {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : α) = 1 :=
  natCast_eq_one <| Nat.ne_zero_of_lt Nat.AtLeastTwo.prop

Embedding of Numerals $\geq 2$ Yields One in Idempotent Semirings

Informal description

For any natural number $n \geq 2$ in an idempotent semiring $\alpha$, the canonical embedding of $n$ into $\alpha$ equals the multiplicative identity $1$, i.e., $n = 1$.

nsmul_eq_self theorem

: ∀ {n : ℕ} (_ : n ≠ 0) (a : α), n • a = a

Full source

theorem nsmul_eq_self : ∀ {n : ℕ} (_ : n ≠ 0) (a : α), n • a = a
  | 0, h => (h rfl).elim
  | 1, _ => one_nsmul
  | n + 2, _ => fun a ↦ by rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]

$n$-fold Sum Equals Original Element in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, for any nonzero natural number $n$ and any element $a \in \alpha$, the $n$-fold sum of $a$ with itself equals $a$, i.e., $n \cdot a = a$.

add_eq_left_iff_le theorem

: a + b = a ↔ b ≤ a

Full source

theorem add_eq_left_iff_le : a + b = a ↔ b ≤ a := by simp

Equivalence of Addition Equality and Order Relation in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, for any elements $a, b \in \alpha$, the equality $a + b = a$ holds if and only if $b \leq a$ in the associated partial order.

add_eq_right_iff_le theorem

: a + b = b ↔ a ≤ b

Full source

theorem add_eq_right_iff_le : a + b = b ↔ a ≤ b := by simp

Addition Equals Right Operand iff Left Operand is Less Than or Equal in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, for any elements $a, b \in \alpha$, the equality $a + b = b$ holds if and only if $a$ is less than or equal to $b$ with respect to the canonical order of the semiring.

add_le_iff theorem

: a + b ≤ c ↔ a ≤ c ∧ b ≤ c

Full source

theorem add_le_iff : a + b ≤ c ↔ a ≤ c ∧ b ≤ c := by simp

Sum Inequality in Idempotent Semirings: $a + b \leq c \leftrightarrow a \leq c \land b \leq c$

Informal description

In an idempotent semiring $\alpha$, for any elements $a, b, c \in \alpha$, the sum $a + b$ is less than or equal to $c$ if and only if both $a \leq c$ and $b \leq c$ hold.

add_le theorem

(ha : a ≤ c) (hb : b ≤ c) : a + b ≤ c

Full source

theorem add_le (ha : a ≤ c) (hb : b ≤ c) : a + b ≤ c :=
  add_le_iff.2 ⟨ha, hb⟩

Addition Preserves Order in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, for any elements $a, b, c \in \alpha$, if $a \leq c$ and $b \leq c$, then $a + b \leq c$.

IdemSemiring.toIsOrderedAddMonoid instance

: IsOrderedAddMonoid α

Full source

instance (priority := 100) IdemSemiring.toIsOrderedAddMonoid :
    IsOrderedAddMonoid α :=
  { add_le_add_left := fun a b hbc c ↦ by
      simp_rw [add_eq_sup]
      exact sup_le_sup_left hbc _ }

Idempotent Semirings as Ordered Additive Monoids

Informal description

Every idempotent semiring $\alpha$ is an ordered additive monoid, where the addition operation is monotone with respect to the partial order defined by $a \leq b$ if and only if $a + b = b$.

IdemSemiring.toCanonicallyOrderedAdd instance

: CanonicallyOrderedAdd α

Full source

instance (priority := 100) IdemSemiring.toCanonicallyOrderedAdd :
    CanonicallyOrderedAdd α :=
  { exists_add_of_le := fun h ↦ ⟨_, h.add_eq_right.symm⟩
    le_self_add := fun a b ↦ add_eq_right_iff_le.1 <| by rw [← add_assoc, add_idem] }

Idempotent Semirings are Canonically Ordered Additive Monoids

Informal description

Every idempotent semiring $\alpha$ is canonically ordered as an additive monoid, meaning that the order relation $\leq$ coincides with the subtractibility relation: $a \leq b$ if and only if there exists $c$ such that $b = a + c$.

IdemSemiring.toMulLeftMono instance

: MulLeftMono α

Full source

instance (priority := 100) IdemSemiring.toMulLeftMono : MulLeftMono α :=
  ⟨fun a b c hbc ↦ add_eq_left_iff_le.1 <| by rw [← mul_add, hbc.add_eq_left]⟩

Monotonicity of Left Multiplication in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, left multiplication is monotone with respect to the associated partial order. That is, for any elements $a, b_1, b_2 \in \alpha$, if $b_1 \leq b_2$, then $a * b_1 \leq a * b_2$.

IdemSemiring.toMulRightMono instance

: MulRightMono α

Full source

instance (priority := 100) IdemSemiring.toMulRightMono : MulRightMono α :=
  ⟨fun a b c hbc ↦ add_eq_left_iff_le.1 <| by rw [← add_mul, hbc.add_eq_left]⟩

Right Multiplication Monotonicity in Idempotent Semirings

Informal description

In an idempotent semiring $\alpha$, multiplication on the right is monotone with respect to the associated partial order. That is, for any elements $a, b, c \in \alpha$, if $a \leq b$, then $a * c \leq b * c$.

one_le_kstar theorem

: 1 ≤ a∗

Full source

@[simp]
theorem one_le_kstar : 1 ≤ a∗ :=
  KleeneAlgebra.one_le_kstar _

Kleene Star Bounds Identity: $1 \leq a^*$

Informal description

In any Kleene algebra $\alpha$, the Kleene star of any element $a \in \alpha$ satisfies $1 \leq a^*$, where $1$ is the multiplicative identity and $a^*$ is the Kleene star of $a$.

mul_kstar_le_kstar theorem

: a * a∗ ≤ a∗

Full source

theorem mul_kstar_le_kstar : a * a∗ ≤ a∗ :=
  KleeneAlgebra.mul_kstar_le_kstar _

Kleene Star Right Absorption: $a \cdot a^* \leq a^*$

Informal description

In any Kleene algebra $\alpha$, for any element $a \in \alpha$, the product of $a$ and its Kleene star $a^*$ is less than or equal to $a^*$, i.e., $a \cdot a^* \leq a^*$.

kstar_mul_le_kstar theorem

: a∗ * a ≤ a∗

Full source

theorem kstar_mul_le_kstar : a∗ * a ≤ a∗ :=
  KleeneAlgebra.kstar_mul_le_kstar _

Kleene Star Absorption: $a^* \cdot a \leq a^*$

Informal description

In any Kleene algebra $\alpha$, for any element $a \in \alpha$, the product of the Kleene star of $a$ and $a$ itself is less than or equal to the Kleene star of $a$, i.e., $a^* \cdot a \leq a^*$.

mul_kstar_le_self theorem

: b * a ≤ b → b * a∗ ≤ b

Full source

theorem mul_kstar_le_self : b * a ≤ b → b * a∗ ≤ b :=
  KleeneAlgebra.mul_kstar_le_self _ _

Kleene Star Absorption: $b \cdot a \leq b$ implies $b \cdot a^* \leq b$

Informal description

In a Kleene algebra $\alpha$, for any elements $a, b \in \alpha$, if $b \cdot a \leq b$, then $b \cdot a^* \leq b$.

kstar_mul_le_self theorem

: a * b ≤ b → a∗ * b ≤ b

Full source

theorem kstar_mul_le_self : a * b ≤ b → a∗ * b ≤ b :=
  KleeneAlgebra.kstar_mul_le_self _ _

Kleene Star Absorption: $a \cdot b \leq b$ implies $a^* \cdot b \leq b$

Informal description

In a Kleene algebra $\alpha$, for any elements $a, b \in \alpha$, if $a \cdot b \leq b$, then $a^* \cdot b \leq b$.

mul_kstar_le theorem

(hb : b ≤ c) (ha : c * a ≤ c) : b * a∗ ≤ c

Full source

theorem mul_kstar_le (hb : b ≤ c) (ha : c * a ≤ c) : b * a∗ ≤ c :=
  (mul_le_mul_right' hb _).trans <| mul_kstar_le_self ha

Kleene Star Absorption: $b \leq c$ and $c \cdot a \leq c$ implies $b \cdot a^* \leq c$

Informal description

In a Kleene algebra $\alpha$, for any elements $a, b, c \in \alpha$, if $b \leq c$ and $c \cdot a \leq c$, then $b \cdot a^* \leq c$.

kstar_mul_le theorem

(hb : b ≤ c) (ha : a * c ≤ c) : a∗ * b ≤ c

Full source

theorem kstar_mul_le (hb : b ≤ c) (ha : a * c ≤ c) : a∗ * b ≤ c :=
  (mul_le_mul_left' hb _).trans <| kstar_mul_le_self ha

Kleene Star Absorption: $a^* \cdot b \leq c$ under $b \leq c$ and $a \cdot c \leq c$

Informal description

In a Kleene algebra $\alpha$, for any elements $a, b, c \in \alpha$, if $b \leq c$ and $a \cdot c \leq c$, then $a^* \cdot b \leq c$.

kstar_le_of_mul_le_left theorem

(hb : 1 ≤ b) : b * a ≤ b → a∗ ≤ b

Full source

theorem kstar_le_of_mul_le_left (hb : 1 ≤ b) : b * a ≤ b → a∗ ≤ b := by
  simpa using mul_kstar_le hb

Kleene Star Upper Bound from Left Multiplication: $1 \leq b$ and $b \cdot a \leq b$ implies $a^* \leq b$

Informal description

In a Kleene algebra $\alpha$, for any elements $a, b \in \alpha$, if $1 \leq b$ and $b \cdot a \leq b$, then the Kleene star of $a$ satisfies $a^* \leq b$.

kstar_le_of_mul_le_right theorem

(hb : 1 ≤ b) : a * b ≤ b → a∗ ≤ b

Full source

theorem kstar_le_of_mul_le_right (hb : 1 ≤ b) : a * b ≤ b → a∗ ≤ b := by
  simpa using kstar_mul_le hb

Kleene Star Upper Bound under Right Multiplication: $a^* \leq b$ given $1 \leq b$ and $a \cdot b \leq b$

Informal description

In a Kleene algebra $\alpha$, for any elements $a, b \in \alpha$, if $1 \leq b$ and $a \cdot b \leq b$, then the Kleene star of $a$ satisfies $a^* \leq b$.

le_kstar theorem

: a ≤ a∗

Full source

@[simp]
theorem le_kstar : a ≤ a∗ :=
  le_trans (le_mul_of_one_le_left' one_le_kstar) kstar_mul_le_kstar

Element is Bounded by its Kleene Star: $a \leq a^*$

Informal description

In any Kleene algebra $\alpha$, for any element $a \in \alpha$, the element $a$ is less than or equal to its Kleene star $a^*$.

kstar_mono theorem

: Monotone (KStar.kstar : α → α)

Full source

@[mono]
theorem kstar_mono : Monotone (KStar.kstar : α → α) :=
  fun _ _ h ↦
    kstar_le_of_mul_le_left one_le_kstar <| kstar_mul_le (h.trans le_kstar) <| mul_kstar_le_kstar

Monotonicity of the Kleene Star Operation

Informal description

The Kleene star operation $* : \alpha \to \alpha$ is monotone, meaning that for any elements $a, b \in \alpha$ in a Kleene algebra, if $a \leq b$, then $a^* \leq b^*$.

kstar_eq_one theorem

: a∗ = 1 ↔ a ≤ 1

Full source

@[simp]
theorem kstar_eq_one : a∗a∗ = 1 ↔ a ≤ 1 :=
  ⟨le_kstar.trans_eq,
    fun h ↦ one_le_kstar.antisymm' <| kstar_le_of_mul_le_left le_rfl <| by rwa [one_mul]⟩

Kleene Star Equals One if and only if Element Bounded by One

Informal description

In a Kleene algebra $\alpha$, for any element $a \in \alpha$, the Kleene star of $a$ equals the multiplicative identity $1$ if and only if $a \leq 1$.

kstar_zero theorem

: (0 : α)∗ = 1

Full source

@[simp] lemma kstar_zero : (0 : α)∗ = 1 := kstar_eq_one.2 (zero_le _)

Kleene Star of Zero: $0^* = 1$

Informal description

In any Kleene algebra $\alpha$, the Kleene star of the additive identity $0$ equals the multiplicative identity $1$, i.e., $0^* = 1$.

kstar_one theorem

: (1 : α)∗ = 1

Full source

@[simp]
theorem kstar_one : (1 : α)∗ = 1 :=
  kstar_eq_one.2 le_rfl

Kleene Star of One Equals One

Informal description

In a Kleene algebra $\alpha$, the Kleene star of the multiplicative identity $1$ is equal to $1$, i.e., $1^* = 1$.

kstar_mul_kstar theorem

(a : α) : a∗ * a∗ = a∗

Full source

@[simp]
theorem kstar_mul_kstar (a : α) : a∗ * a∗ = a∗ :=
  (mul_kstar_le le_rfl <| kstar_mul_le_kstar).antisymm <| le_mul_of_one_le_left' one_le_kstar

Idempotence of Kleene Star: $a^* \cdot a^* = a^*$

Informal description

In any Kleene algebra $\alpha$, for any element $a \in \alpha$, the product of the Kleene star of $a$ with itself is equal to the Kleene star of $a$, i.e., $a^* \cdot a^* = a^*$.

kstar_eq_self theorem

: a∗ = a ↔ a * a = a ∧ 1 ≤ a

Full source

@[simp]
theorem kstar_eq_self : a∗a∗ = a ↔ a * a = a ∧ 1 ≤ a :=
  ⟨fun h ↦ ⟨by rw [← h, kstar_mul_kstar], one_le_kstar.trans_eq h⟩,
    fun h ↦ (kstar_le_of_mul_le_left h.2 h.1.le).antisymm le_kstar⟩

Characterization of Kleene Star Fixed Points: $a^* = a \Leftrightarrow (a^2 = a \land 1 \leq a)$

Informal description

In a Kleene algebra $\alpha$, for any element $a \in \alpha$, the Kleene star of $a$ equals $a$ if and only if $a$ is idempotent (i.e., $a \cdot a = a$) and the multiplicative identity $1$ is less than or equal to $a$. In other words: $$ a^* = a \Leftrightarrow (a \cdot a = a) \land (1 \leq a) $$

kstar_idem theorem

(a : α) : a∗∗ = a∗

Full source

@[simp]
theorem kstar_idem (a : α) : a∗a∗∗ = a∗ :=
  kstar_eq_self.2 ⟨kstar_mul_kstar _, one_le_kstar⟩

Idempotence of Kleene Star Operation: $(a^*)^* = a^*$

Informal description

In any Kleene algebra $\alpha$, for any element $a \in \alpha$, the Kleene star of the Kleene star of $a$ equals the Kleene star of $a$, i.e., $(a^*)^* = a^*$.

pow_le_kstar theorem

: ∀ {n : ℕ}, a ^ n ≤ a∗

Full source

@[simp]
theorem pow_le_kstar : ∀ {n : ℕ}, a ^ n ≤ a∗
  | 0 => (pow_zero _).trans_le one_le_kstar
  | n + 1 => by
    rw [pow_succ']
    exact (mul_le_mul_left' pow_le_kstar _).trans mul_kstar_le_kstar

Powers Bounded by Kleene Star: $a^n \leq a^*$

Informal description

In any Kleene algebra $\alpha$, for any element $a \in \alpha$ and any natural number $n$, the $n$-th power of $a$ is less than or equal to the Kleene star of $a$, i.e., $a^n \leq a^*$.

Prod.instIdemSemiring instance

[IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β)

Full source

instance instIdemSemiring [IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β) :=
  { Prod.instSemiring, Prod.instSemilatticeSup _ _, Prod.instOrderBot _ _ with
    add_eq_sup := fun _ _ ↦ Prod.ext (add_eq_sup _ _) (add_eq_sup _ _) }

Idempotent Semiring Structure on Product Types

Informal description

For any idempotent semirings $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also an idempotent semiring, where the addition and multiplication operations are defined componentwise, and the order is given by $(x_1, x_2) \leq (y_1, y_2)$ if and only if $x_1 \leq y_1$ in $\alpha$ and $x_2 \leq y_2$ in $\beta$.

Prod.instIdemCommSemiring instance

[IdemCommSemiring α] [IdemCommSemiring β] : IdemCommSemiring (α × β)

Full source

instance [IdemCommSemiring α] [IdemCommSemiring β] : IdemCommSemiring (α × β) :=
  { Prod.instCommSemiring, Prod.instIdemSemiring with }

Idempotent Commutative Semiring Structure on Product Types

Informal description

For any idempotent commutative semirings $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also an idempotent commutative semiring, where the addition and multiplication operations are defined componentwise, and the order is given by $(x_1, x_2) \leq (y_1, y_2)$ if and only if $x_1 \leq y_1$ in $\alpha$ and $x_2 \leq y_2$ in $\beta$.

Prod.instKleeneAlgebra instance

: KleeneAlgebra (α × β)

Full source

instance : KleeneAlgebra (α × β) :=
  { Prod.instIdemSemiring with
    kstar := fun a ↦ (a.1∗, a.2∗)
    one_le_kstar := fun _ ↦ ⟨one_le_kstar, one_le_kstar⟩
    mul_kstar_le_kstar := fun _ ↦ ⟨mul_kstar_le_kstar, mul_kstar_le_kstar⟩
    kstar_mul_le_kstar := fun _ ↦ ⟨kstar_mul_le_kstar, kstar_mul_le_kstar⟩
    mul_kstar_le_self := fun _ _ ↦ And.imp mul_kstar_le_self mul_kstar_le_self
    kstar_mul_le_self := fun _ _ ↦ And.imp kstar_mul_le_self kstar_mul_le_self }

Kleene Algebra Structure on Product Types

Informal description

For any Kleene algebras $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also a Kleene algebra, where the addition, multiplication, and Kleene star operations are defined componentwise.

Prod.kstar_def theorem

(a : α × β) : a∗ = (a.1∗, a.2∗)

Full source

theorem kstar_def (a : α × β) : a∗ = (a.1∗, a.2∗) :=
  rfl

Componentwise Definition of Kleene Star in Product Algebra

Informal description

For any element $a = (a_1, a_2)$ in the product Kleene algebra $\alpha \times \beta$, the Kleene star operation is defined componentwise as $a^* = (a_1^*, a_2^*)$.

Prod.fst_kstar theorem

(a : α × β) : a∗.1 = a.1∗

Full source

@[simp]
theorem fst_kstar (a : α × β) : a∗.1 = a.1∗ :=
  rfl

First Component of Kleene Star in Product Algebra

Informal description

For any element $a = (a_1, a_2)$ in the product Kleene algebra $\alpha \times \beta$, the first component of the Kleene star of $a$ equals the Kleene star of its first component, i.e., $(a^*)_1 = a_1^*$.

Prod.snd_kstar theorem

(a : α × β) : a∗.2 = a.2∗

Full source

@[simp]
theorem snd_kstar (a : α × β) : a∗.2 = a.2∗ :=
  rfl

Second Component of Kleene Star in Product Algebra: $(a_1, a_2)^*.2 = a_2^*$

Informal description

For any pair $(a_1, a_2)$ in the product Kleene algebra $\alpha \times \beta$, the second component of the Kleene star $(a_1, a_2)^*$ is equal to the Kleene star of the second component $a_2^*$. In other words, $(a_1, a_2)^* = (a_1^*, a_2^*)$ implies $(a_1, a_2)^*.2 = a_2^*$.

Pi.instIdemSemiring instance

[∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i)

Full source

instance instIdemSemiring [∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i) :=
  { Pi.semiring, Pi.instSemilatticeSup, Pi.instOrderBot with
    add_eq_sup := fun _ _ ↦ funext fun _ ↦ add_eq_sup _ _ }

Pointwise Idempotent Semiring Structure on Product Types

Informal description

For any family of types $\pi_i$ where each $\pi_i$ is an idempotent semiring, the product type $\forall i, \pi_i$ is also an idempotent semiring with pointwise operations and order.

Pi.instIdemCommSemiringForall instance

[∀ i, IdemCommSemiring (π i)] : IdemCommSemiring (∀ i, π i)

Full source

instance [∀ i, IdemCommSemiring (π i)] : IdemCommSemiring (∀ i, π i) :=
  { Pi.commSemiring, Pi.instIdemSemiring with }

Pointwise Idempotent Commutative Semiring Structure on Product Types

Informal description

For any family of types $\pi_i$ where each $\pi_i$ is an idempotent commutative semiring, the product type $\forall i, \pi_i$ is also an idempotent commutative semiring with pointwise operations and order.

Pi.instKleeneAlgebraForall instance

: KleeneAlgebra (∀ i, π i)

Full source

instance : KleeneAlgebra (∀ i, π i) :=
  { Pi.instIdemSemiring with
    kstar := fun a i ↦ (a i)∗
    one_le_kstar := fun _ _ ↦ one_le_kstar
    mul_kstar_le_kstar := fun _ _ ↦ mul_kstar_le_kstar
    kstar_mul_le_kstar := fun _ _ ↦ kstar_mul_le_kstar
    mul_kstar_le_self := fun _ _ h _ ↦ mul_kstar_le_self <| h _
    kstar_mul_le_self := fun _ _ h _ ↦ kstar_mul_le_self <| h _ }

Pointwise Kleene Algebra Structure on Product Types

Informal description

For any family of types $\pi_i$ where each $\pi_i$ is a Kleene algebra, the product type $\forall i, \pi_i$ is also a Kleene algebra with pointwise operations, including the Kleene star operation defined componentwise.

Pi.kstar_def theorem

(a : ∀ i, π i) : a∗ = fun i ↦ (a i)∗

Full source

theorem kstar_def (a : ∀ i, π i) : a∗ = fun i ↦ (a i)∗ :=
  rfl

Componentwise Definition of Kleene Star in Product Algebra

Informal description

For any family of elements $a = (a_i)_{i \in \iota}$ in a product of Kleene algebras $\prod_{i \in \iota} \pi_i$, the Kleene star operation is defined componentwise as $(a^*)_i = (a_i)^*$ for each index $i \in \iota$.

Pi.kstar_apply theorem

(a : ∀ i, π i) (i : ι) : a∗ i = (a i)∗

Full source

@[simp]
theorem kstar_apply (a : ∀ i, π i) (i : ι) : a∗ i = (a i)∗ :=
  rfl

Componentwise Kleene Star in Product Algebra: $(a^*)_i = (a_i)^*$

Informal description

For any family of Kleene algebras $\pi_i$ indexed by $i \in \iota$, and for any element $a$ in the product Kleene algebra $\forall i, \pi_i$, the Kleene star operation applied to $a$ at index $i$ equals the Kleene star of $a_i$, i.e., $(a^*)_i = (a_i)^*$.

Function.Injective.idemSemiring abbrev

 [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 (a ⊔ b) = f a ⊔ f b)
  (bot : f ⊥ = ⊥) : IdemSemiring β

Full source

/-- Pullback an `IdemSemiring` instance along an injective function. -/
protected abbrev idemSemiring [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 (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) :
    IdemSemiring β :=
  { hf.semiring f zero one add mul nsmul npow natCast, hf.semilatticeSup _ sup,
    ‹Bot β› with
    add_eq_sup := fun a b ↦ hf <| by rw [sup, add, add_eq_sup]
    bot := ⊥
    bot_le := fun a ↦ bot.trans_le <| @bot_le _ _ _ <| f a }

Injective Function Induces Idempotent Semiring Structure

Informal description

Let $\alpha$ be an idempotent semiring and $\beta$ be a type equipped with operations for zero, one, addition, multiplication, natural number power, natural number scalar multiplication, natural number casting, maximum, and bottom element. Given an injective function $f : \beta \to \alpha$ that preserves all these operations (i.e., $f(0) = 0$, $f(1) = 1$, $f(x + y) = f(x) + f(y)$, $f(x * y) = f(x) * f(y)$, $f(n \cdot x) = n \cdot f(x)$, $f(x^n) = f(x)^n$, $f(n) = n$ for all $n \in \mathbb{N}$, $f(a \sqcup b) = f(a) \sqcup f(b)$, and $f(\bot) = \bot$), then $\beta$ inherits an idempotent semiring structure from $\alpha$ via $f$.

Function.Injective.idemCommSemiring abbrev

 [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 (a ⊔ b) = f a ⊔ f b)
  (bot : f ⊥ = ⊥) : IdemCommSemiring β

Full source

/-- Pullback an `IdemCommSemiring` instance along an injective function. -/
protected abbrev idemCommSemiring [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 (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥) :
    IdemCommSemiring β :=
  { hf.commSemiring f zero one add mul nsmul npow natCast,
    hf.idemSemiring f zero one add mul nsmul npow natCast sup bot with }

Injective Homomorphism Induces Idempotent Commutative Semiring Structure

Informal description

Let $\alpha$ be an idempotent commutative semiring and $\beta$ be a type equipped with operations for zero, one, addition, multiplication, natural number power, natural number scalar multiplication, natural number casting, maximum, and bottom element. Given an injective function $f : \beta \to \alpha$ that preserves all these operations (i.e., $f(0) = 0$, $f(1) = 1$, $f(x + y) = f(x) + f(y)$, $f(x \cdot y) = f(x) \cdot f(y)$, $f(n \cdot x) = n \cdot f(x)$, $f(x^n) = f(x)^n$, $f(n) = n$ for all $n \in \mathbb{N}$, $f(\max(a, b)) = \max(f(a), f(b))$, and $f(\bot) = \bot$), then $\beta$ inherits an idempotent commutative semiring structure from $\alpha$ via $f$.

Function.Injective.kleeneAlgebra abbrev

 [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 (a ⊔ b) = f a ⊔ f b)
  (bot : f ⊥ = ⊥) (kstar : ∀ a, f a∗ = (f a)∗) : KleeneAlgebra β

Full source

/-- Pullback a `KleeneAlgebra` instance along an injective function. -/
protected abbrev kleeneAlgebra [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 (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥)
    (kstar : ∀ a, f a∗ = (f a)∗) : KleeneAlgebra β :=
  { hf.idemSemiring f zero one add mul nsmul npow natCast sup bot,
    ‹KStar β› with
    one_le_kstar := fun a ↦ one.trans_le <| by
      rw [kstar]
      exact one_le_kstar
    mul_kstar_le_kstar := fun a ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      exact mul_kstar_le_kstar
    kstar_mul_le_kstar := fun a ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      exact kstar_mul_le_kstar
    mul_kstar_le_self := fun a b (h : f _ ≤ _) ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      rw [mul] at h
      exact mul_kstar_le_self h
    kstar_mul_le_self := fun a b (h : f _ ≤ _) ↦ by
      change f _ ≤ _
      rw [mul, kstar]
      rw [mul] at h
      exact kstar_mul_le_self h }

Injective Function Induces Kleene Algebra Structure

Informal description

Let $\alpha$ be a Kleene algebra and $\beta$ be a type equipped with operations for zero, one, addition, multiplication, natural number power, natural number scalar multiplication, natural number casting, maximum, bottom element, and Kleene star. Given an injective function $f : \beta \to \alpha$ that preserves all these operations (i.e., $f(0) = 0$, $f(1) = 1$, $f(x + y) = f(x) + f(y)$, $f(x \cdot y) = f(x) \cdot f(y)$, $f(n \cdot x) = n \cdot f(x)$, $f(x^n) = f(x)^n$, $f(n) = n$ for all $n \in \mathbb{N}$, $f(\max(a, b)) = \max(f(a), f(b))$, $f(\bot) = \bot$, and $f(a^*) = (f(a))^*$), then $\beta$ inherits a Kleene algebra structure from $\alpha$ via $f$.

Mathlib.Algebra.Order.Kleene

Main declarations

Notation

References

TODO

Tags