Add generic divisibility for magma and monoid-like structures

Author: mechvel

CHANGELOG.md

@@ -81,6 +81,15 @@ New modules
 * Added `Reflection.DeBruijn` with weakening, strengthening and free variable operations
   on reflected terms.
 
+* Generic divisibility over algebraic structures
+  ```
+  Algebra.Divisibility
+  Algebra.Properties.Magma.Divisibility
+  Algebra.Properties.Semigroup.Divisibility
+  Algebra.Properties.Monoid.Divisibility
+  Algebra.Properties.CommutativeSemigroup.Divisibility
+  ```
+
 Other major changes
 -------------------
 
@@ -100,6 +109,7 @@ Other minor additions
 
 * Added new records to `Algebra.Bundles`:
   ```agda
+  CommutativeMagma c ℓ : Set (suc (c ⊔ ℓ))
   RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ))
   RawLattice c ℓ : Set (suc (c ⊔ ℓ))
   CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ))
@@ -134,6 +144,7 @@ Other minor additions
 
 * Added new record to `Algebra.Structures`:
   ```agda
+  IsCommutativeMagma (• : Op₂ A) : Set (a ⊔ ℓ)
   IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ)
   ```
 

src/Algebra/Bundles.agda

@@ -48,6 +48,40 @@ record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
     using (_≉_)
 
 
+record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    _∙_              : Op₂ Carrier
+    isSelectiveMagma : IsSelectiveMagma _≈_ _∙_
+
+  open IsSelectiveMagma isSelectiveMagma public
+
+  magma : Magma c ℓ
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public using (rawMagma)
+
+
+record CommutativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier            : Set c
+    _≈_                : Rel Carrier ℓ
+    _∙_                : Op₂ Carrier
+    isCommutativeMagma : IsCommutativeMagma _≈_ _∙_
+
+  open IsCommutativeMagma isCommutativeMagma public
+
+  magma : Magma c ℓ
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public using (rawMagma)
+
+
 record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infix  4 _≈_
@@ -101,6 +135,9 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   open Semigroup semigroup public
     using (_≉_; magma; rawMagma)
 
+  commutativeMagma : CommutativeMagma c ℓ
+  commutativeMagma = record { isCommutativeMagma = isCommutativeMagma }
+
 
 record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
@@ -120,23 +157,6 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
     using (_≉_; rawMagma; magma; semigroup)
 
 
-record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
-  infixl 7 _∙_
-  infix  4 _≈_
-  field
-    Carrier          : Set c
-    _≈_              : Rel Carrier ℓ
-    _∙_              : Op₂ Carrier
-    isSelectiveMagma : IsSelectiveMagma _≈_ _∙_
-
-  open IsSelectiveMagma isSelectiveMagma public
-
-  magma : Magma c ℓ
-  magma = record { isMagma = isMagma }
-
-  open Magma magma public
-    using (_≉_; rawMagma)
-
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation & 1 element
 ------------------------------------------------------------------------
@@ -202,6 +222,9 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   commutativeSemigroup : CommutativeSemigroup _ _
   commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }
 
+  open CommutativeSemigroup commutativeSemigroup public
+    using (commutativeMagma)
+
 
 record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -219,7 +242,10 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
 
   open CommutativeMonoid commutativeMonoid public
-    using (_≉_; rawMagma; magma; semigroup; rawMonoid; monoid)
+    using
+    ( _≉_; rawMagma; magma; commutativeMagma; semigroup; commutativeSemigroup
+    ; rawMonoid; monoid
+    )
 
 
 -- Idempotent commutative monoids are also known as bounded lattices.
@@ -305,7 +331,7 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
 
   open CommutativeMonoid commutativeMonoid public
-    using (commutativeSemigroup)
+    using (commutativeMagma; commutativeSemigroup)
 
 
 ------------------------------------------------------------------------
@@ -328,6 +354,7 @@ record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   ∧-rawMagma : RawMagma c ℓ
   ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
 
+
 record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
   infixr 6 _∨_
@@ -409,6 +436,7 @@ record RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _∙_ = _*_
     }
 
+
 record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
   infixl 6 _+_
@@ -481,7 +509,10 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
   +-commutativeMonoid = record { isCommutativeMonoid = +-isCommutativeMonoid }
 
   open CommutativeMonoid +-commutativeMonoid public
-    using () renaming (commutativeSemigroup to +-commutativeSemigroup)
+    using () renaming
+    ( commutativeMagma     to +-commutativeMagma
+    ; commutativeSemigroup to +-commutativeSemigroup
+    )
 
 
 record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -584,6 +615,7 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
     using (_≉_) renaming
     ( rawMagma             to +-rawMagma
     ; magma                to +-magma
+    ; commutativeMagma     to +-commutativeMagma
     ; semigroup            to +-semigroup
     ; commutativeSemigroup to +-commutativeSemigroup
     ; rawMonoid            to +-rawMonoid
@@ -626,7 +658,7 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
   open SemiringWithoutAnnihilatingZero
          semiringWithoutAnnihilatingZero public
     using
-    ( _≉_; +-rawMagma;  +-magma;  +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma;  +-magma;  +-commutativeMagma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma;  *-magma;  *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -661,7 +693,7 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -670,16 +702,17 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; rawSemiring
     )
 
-  *-commutativeSemigroup : CommutativeSemigroup _ _
-  *-commutativeSemigroup = record
-    { isCommutativeSemigroup = *-isCommutativeSemigroup
-    }
-
   *-commutativeMonoid : CommutativeMonoid _ _
   *-commutativeMonoid = record
     { isCommutativeMonoid = *-isCommutativeMonoid
     }
 
+  open CommutativeMonoid *-commutativeMonoid public
+    using () renaming
+    ( commutativeMagma     to *-commutativeMagma
+    ; commutativeSemigroup to *-commutativeSemigroup
+    )
+
   commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
   commutativeSemiringWithoutOne = record
     { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
@@ -701,6 +734,21 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open IsCancellativeCommutativeSemiring isCancellativeCommutativeSemiring public
 
+  commutativeSemiring : CommutativeSemiring c ℓ
+  commutativeSemiring = record
+    { isCommutativeSemiring = isCommutativeSemiring
+    }
+
+  open CommutativeSemiring commutativeSemiring public
+    using
+    ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid; *-commutativeMonoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    ; rawSemiring
+    )
 
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 2 elements
@@ -762,7 +810,7 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid ; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -812,8 +860,8 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open CommutativeSemiring commutativeSemiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
-    ; *-rawMagma; *-magma; *-semigroup; *-commutativeSemigroup
+    ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid; *-commutativeMonoid
     ; nearSemiring; semiringWithoutOne

src/Algebra/Divisibility.agda

@@ -0,0 +1,75 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of divisibility
+------------------------------------------------------------------------
+
+-- You're unlikely to want to use this module directly. Instead you
+-- probably want to be importing the appropriate module from
+-- `Algebra.Properties.(Magma/Semigroup/...).Divisibility`
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Core
+open import Data.Product using (∃; _×_; _,_)
+open import Level using (_⊔_)
+open import Relation.Binary
+open import Relation.Nullary using (¬_)
+
+module Algebra.Divisibility
+  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A)
+  where
+
+open import Algebra.Definitions _≈_
+
+------------------------------------------------------------------------
+-- Definitions
+
+-- Divisibility
+
+infix 5 _∣_ _∤_ _∣∣_ _¬∣∣_
+
+_∣_ : Rel A (a ⊔ ℓ)
+x ∣ y = ∃ λ q → (q ∙ x) ≈ y
+
+_∤_ : Rel A (a ⊔ ℓ)
+x ∤ y = ¬ x ∣ y
+
+-- Mutual divisibility.
+
+-- When in a cancellative monoid, elements related by _∣∣_ are called
+-- associated and if x ∣∣ y then x and y differ by an invertible factor.
+
+_∣∣_ : Rel A (a ⊔ ℓ)
+x ∣∣ y = x ∣ y × y ∣ x
+
+_¬∣∣_ : Rel A (a ⊔ ℓ)
+x ¬∣∣ y =  ¬ x ∣∣ y
+
+------------------------------------------------------------------------
+-- Properties
+
+∣-refl : ∀ {ε} → LeftIdentity ε _∙_ → Reflexive _∣_
+∣-refl {ε} idˡ {x} = ε , idˡ x
+
+∣-reflexive : Transitive _≈_ → ∀ {ε} → LeftIdentity ε _∙_ → _≈_ ⇒ _∣_
+∣-reflexive trans {ε} idˡ x≈y = ε , trans (idˡ _) x≈y
+
+∣-trans : Transitive _≈_ → LeftCongruent _∙_ → Associative _∙_ → Transitive _∣_
+∣-trans trans congˡ assoc {x} {y} {z} (p , px≈y) (q , qy≈z) =
+  q ∙ p , trans (assoc q p x) (trans (congˡ px≈y) qy≈z)
+
+∣-respʳ : Transitive _≈_ → _∣_ Respectsʳ _≈_
+∣-respʳ trans y≈z (q , qx≈y) = q , trans qx≈y y≈z
+
+∣-respˡ : Symmetric _≈_ → Transitive _≈_ → LeftCongruent _∙_ → _∣_ Respectsˡ _≈_
+∣-respˡ sym trans congˡ x≈z (q , qx≈y) = q , trans (congˡ (sym x≈z)) qx≈y
+
+∣-resp : Symmetric _≈_ → Transitive _≈_ → LeftCongruent _∙_ → _∣_ Respects₂ _≈_
+∣-resp sym trans cong = ∣-respʳ trans , ∣-respˡ sym trans cong
+
+∣-min : ∀ {ε} → RightIdentity ε _∙_ → Minimum _∣_ ε
+∣-min {ε} idʳ x = x , idʳ x
+
+∣-max : ∀ {ε} → LeftZero ε _∙_ → Maximum _∣_ ε
+∣-max {ε} zeˡ x = ε , zeˡ x

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of divisibility over commutative magmas
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (CommutativeMagma)
+open import Data.Product using (_×_; _,_; map)
+
+module Algebra.Properties.CommutativeMagma.Divisibility
+  {a ℓ} (CM : CommutativeMagma a ℓ)
+  where
+
+open CommutativeMagma CM
+
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------------
+-- Re-export the contents of semigroup
+
+open import Algebra.Properties.Magma.Divisibility magma public
+
+------------------------------------------------------------------------------
+-- Further properties
+
+x∣xy : ∀ x y → x ∣ x ∙ y
+x∣xy x y = y , comm y x
+
+xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z
+xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y)
+
+∣-factors : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
+∣-factors x y = x∣xy x y , x∣yx y x
+
+∣-factors-≈ : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
+∣-factors-≈ x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z

src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

@@ -0,0 +1,26 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of divisibility over commutative semigroups
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (CommutativeSemigroup)
+
+module Algebra.Properties.CommutativeSemigroup.Divisibility
+  {a ℓ} (CM : CommutativeSemigroup a ℓ)
+  where
+
+open CommutativeSemigroup CM
+
+------------------------------------------------------------------------------
+-- Re-export the contents of divisibility over semigroups
+
+open import Algebra.Properties.Semigroup.Divisibility semigroup public
+
+------------------------------------------------------------------------------
+-- Re-export the contents of divisibility over commutative magmas
+
+open import Algebra.Properties.CommutativeMagma.Divisibility commutativeMagma public
+  using (x∣xy; xy≈z⇒x∣z; ∣-factors; ∣-factors-≈)