Kleene algebra (#1730)

Author: Akshobhya1234

CHANGELOG.md

@@ -892,6 +892,7 @@ Other minor changes
   record RawLoop  c ℓ : Set (suc (c ⊔ ℓ))
   record Loop  c ℓ : Set (suc (c ⊔ ℓ))
   record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ))
+  record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) 
   ```
   and the existing record `Lattice` now provides
   ```agda
@@ -937,6 +938,8 @@ Other minor changes
                           InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
   quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
   loop : Loop a ℓ₁ → Loop b ℓ₂ → Loop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
+  kleeneAlgebra : KleeneAlgebra a ℓ₁ → KleeneAlgebra b ℓ₂ → 
+                  KleeneAlgebra (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
  ```
 
 * Added new definition to `Algebra.Definitions`:
@@ -972,6 +975,7 @@ Other minor changes
   record IsQuasigroup (∙ \\ // : Op₂ A) : Set (a ⊔ ℓ)
   record IsLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ)
   record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ)
+  record IsKleeneAlgebra (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ)
   ```
   and the existing record `IsLattice` now provides
   ```

src/Algebra/Bundles.agda

@@ -750,6 +750,36 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _≉_
     )
 
+record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier               : Set c
+    _≈_                   : Rel Carrier ℓ
+    _+_                   : Op₂ Carrier
+    _*_                   : Op₂ Carrier
+    0#                    : Carrier
+    1#                    : Carrier
+    isKleeneAlgebra       : IsKleeneAlgebra _≈_ _+_ _*_ 0# 1#
+
+  open IsKleeneAlgebra isKleeneAlgebra public
+
+  semiring : Semiring _ _
+  semiring = record { isSemiring = isSemiring }
+
+  open Semiring semiring public
+    using
+    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-commutativeMagma
+    ; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    ; rawSemiring
+    )
+
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 1 element
 ------------------------------------------------------------------------

src/Algebra/Construct/DirectProduct.agda

@@ -130,6 +130,16 @@ commutativeSemigroup G H = record
     }
   } where module G = CommutativeSemigroup G; module H = CommutativeSemigroup H
 
+unitalMagma : UnitalMagma a ℓ₁ → UnitalMagma b ℓ₂ → UnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
+unitalMagma M N = record
+  { ε = M.ε , N.ε
+  ; isUnitalMagma = record
+    { isMagma = Magma.isMagma (magma M.magma N.magma)
+    ; identity = (M.identityˡ , N.identityˡ <*>_)
+               , (M.identityʳ , N.identityʳ <*>_)
+    }
+  } where module M = UnitalMagma M; module N = UnitalMagma N
+
 monoid : Monoid a ℓ₁ → Monoid b ℓ₂ → Monoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 monoid M N = record
   { ε = M.ε , N.ε
@@ -163,6 +173,27 @@ idempotentCommutativeMonoid M N = record
   module M = IdempotentCommutativeMonoid M
   module N = IdempotentCommutativeMonoid N
 
+invertibleMagma : InvertibleMagma a ℓ₁ → InvertibleMagma b ℓ₂ → InvertibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
+invertibleMagma M N = record
+  { _⁻¹ = map M._⁻¹ N._⁻¹
+  ; isInvertibleMagma = record
+    { isMagma = Magma.isMagma (magma M.magma N.magma)
+    ; inverse = (λ x → (M.inverseˡ , N.inverseˡ) <*> x)
+                , (λ x → (M.inverseʳ , N.inverseʳ) <*> x)
+    ; ⁻¹-cong = map M.⁻¹-cong N.⁻¹-cong
+    }
+  } where module M = InvertibleMagma M; module N = InvertibleMagma N
+
+invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → InvertibleUnitalMagma b ℓ₂ → InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
+invertibleUnitalMagma M N = record
+  { ε = M.ε , N.ε
+  ; isInvertibleUnitalMagma = record
+    { isInvertibleMagma = InvertibleMagma.isInvertibleMagma (invertibleMagma M.invertibleMagma N.invertibleMagma)
+    ; identity = (M.identityˡ , N.identityˡ <*>_)
+               , (M.identityʳ , N.identityʳ <*>_)
+    }
+  } where module M = InvertibleUnitalMagma M; module N = InvertibleUnitalMagma N
+
 group : Group a ℓ₁ → Group b ℓ₂ → Group (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 group G H = record
   { _⁻¹ = map G._⁻¹ H._⁻¹
@@ -225,6 +256,14 @@ commutativeSemiring R S = record
       }
   } where module R = CommutativeSemiring R;  module S = CommutativeSemiring S
 
+kleeneAlgebra : KleeneAlgebra a ℓ₁ → KleeneAlgebra b ℓ₂ → KleeneAlgebra (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
+kleeneAlgebra K L = record
+  { isKleeneAlgebra = record
+      { isSemiring = Semiring.isSemiring (semiring K.semiring L.semiring)
+      ; +-idem = λ x → (K.+-idem , L.+-idem) <*> x
+      }
+  } where module K = KleeneAlgebra K;  module L = KleeneAlgebra L
+
 ring : Ring a ℓ₁ → Ring b ℓ₂ → Ring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 ring R S = record
   { -_     = uncurry (λ x y → R.-_ x , S.-_ y)
@@ -252,37 +291,6 @@ commutativeRing R S = record
       }
   } where module R = CommutativeRing R; module S = CommutativeRing S
 
-unitalMagma : UnitalMagma a ℓ₁ → UnitalMagma b ℓ₂ → UnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-unitalMagma M N = record
-  { ε = M.ε , N.ε
-  ; isUnitalMagma = record
-    { isMagma = Magma.isMagma (magma M.magma N.magma)
-    ; identity = (M.identityˡ , N.identityˡ <*>_)
-               , (M.identityʳ , N.identityʳ <*>_)
-    }
-  } where module M = UnitalMagma M; module N = UnitalMagma N
-
-invertibleMagma : InvertibleMagma a ℓ₁ → InvertibleMagma b ℓ₂ → InvertibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-invertibleMagma M N = record
-  { _⁻¹ = map M._⁻¹ N._⁻¹
-  ; isInvertibleMagma = record
-    { isMagma = Magma.isMagma (magma M.magma N.magma)
-    ; inverse = (λ x → (M.inverseˡ , N.inverseˡ) <*> x)
-                , (λ x → (M.inverseʳ , N.inverseʳ) <*> x)
-    ; ⁻¹-cong = map M.⁻¹-cong N.⁻¹-cong
-    }
-  } where module M = InvertibleMagma M; module N = InvertibleMagma N
-
-invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → InvertibleUnitalMagma b ℓ₂ → InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-invertibleUnitalMagma M N = record
-  { ε = M.ε , N.ε
-  ; isInvertibleUnitalMagma = record
-    { isInvertibleMagma = InvertibleMagma.isInvertibleMagma (invertibleMagma M.invertibleMagma N.invertibleMagma)
-    ; identity = (M.identityˡ , N.identityˡ <*>_)
-               , (M.identityʳ , N.identityʳ <*>_)
-    }
-  } where module M = InvertibleUnitalMagma M; module N = InvertibleUnitalMagma N
-
 quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 quasigroup M N = record
   { _\\_    = zip M._\\_ N._\\_

src/Algebra/Structures.agda

@@ -496,6 +496,14 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a 
 
   open IsCommutativeSemiring isCommutativeSemiring public
 
+
+record IsKleeneAlgebra (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isSemiring  : IsSemiring + * 0# 1#
+    +-idem      : Idempotent +
+
+  open IsSemiring isSemiring public
+
 ------------------------------------------------------------------------
 -- Structures with 2 binary operations, 1 unary operation & 1 element
 ------------------------------------------------------------------------