Re-organisation of algebra operation definitions (#1387)

Author: MatthewDaggitt

CHANGELOG.md

@@ -193,34 +193,31 @@ New modules
   `Data.Unit.Polymorphic.Instances`, `Data.Vec.Instances`,
   `Data.Word.Instances`, and `Reflection.Instances`.
 
-* Generic divisibility over algebraic structures
+* Generic definitions over algebraic structures (divisibility, multiplication etc.):
   ```
-  Algebra.Divisibility
-  Algebra.GCD
-  Algebra.Primality
-  Algebra.Properties.Magma.Divisibility
-  Algebra.Properties.Semigroup.Divisibility
-  Algebra.Properties.Monoid.Divisibility
-  Algebra.Properties.CommutativeSemigroup.Divisibility
-  Algebra.Properties.Semiring.Divisibility
-  Algebra.Properties.Semiring.GCD
+  Algebra.Definitions.RawMagma
+  Algebra.Definitions.RawMonoid
+  Algebra.Definitions.RawSemiring
   ```
 
-* Generic summation over algebraic structures
+* Properties of generic definitions over algebraic structures (divisibility, multiplication etc.):
   ```
+  Algebra.Properties.Magma.Divisibility
+  
+  Algebra.Properties.Semigroup.Divisibility
+  
+  Algebra.Properties.CommutativeSemigroup.Divisibility
+  
   Algebra.Properties.Monoid.Summation
-  Algebra.Properties.CommutativeMonoid.Summation
-  ```
-
-* Generic multiplication over algebraic structures
-  ```
   Algebra.Properties.Monoid.Multiplication
+  Algebra.Properties.Monoid.Divisibility
+  
+  Algebra.Properties.CommutativeMonoid.Summation
+  
   Algebra.Properties.Semiring.Multiplication
-  ```
-
-* Generic exponentiation over algebraic structures
-  ```
   Algebra.Properties.Semiring.Exponentiation
+  Algebra.Properties.Semiring.GCD
+  Algebra.Properties.Semiring.Divisibility
   ```
 
 * Setoid equality over vectors:

src/Algebra/Bundles.agda

@@ -15,6 +15,7 @@ open import Algebra.Core
 open import Algebra.Structures
 open import Relation.Binary
 open import Function.Base
+import Relation.Nullary as N
 open import Level
 
 ------------------------------------------------------------------------
@@ -29,6 +30,10 @@ record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _≈_     : Rel Carrier ℓ
     _∙_     : Op₂ Carrier
 
+  infix 4 _≉_
+  _≉_ : Rel Carrier _
+  x ≉ y = N.¬ (x ≈ y)
+
 
 record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -44,7 +49,7 @@ record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   rawMagma : RawMagma _ _
   rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }
 
-  open Setoid setoid public
+  open RawMagma rawMagma public
     using (_≉_)
 
 
@@ -178,6 +183,9 @@ record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _∙_ = _∙_
     }
 
+  open RawMagma rawMagma public
+    using (_≉_)
+
 
 record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -281,7 +289,7 @@ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
     }
 
   open RawMonoid rawMonoid public
-    using (rawMagma)
+    using (_≉_; rawMagma)
 
 
 record Group c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -354,6 +362,9 @@ record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   ∧-rawMagma : RawMagma c ℓ
   ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
 
+  open RawMagma ∨-rawMagma public
+    using (_≉_)
+
 
 record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
@@ -428,7 +439,7 @@ record RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     }
 
   open RawMonoid +-rawMonoid public
-    using () renaming (rawMagma to +-rawMagma)
+    using (_≉_) renaming (rawMagma to +-rawMagma)
 
   *-rawMagma : RawMagma c ℓ
   *-rawMagma = record
@@ -568,7 +579,7 @@ record RawSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     }
 
   open RawNearSemiring rawNearSemiring public
-    using (+-rawMonoid; +-rawMagma; *-rawMagma)
+    using (_≉_; +-rawMonoid; +-rawMagma; *-rawMagma)
 
   *-rawMonoid : RawMonoid c ℓ
   *-rawMonoid = record

src/Algebra/Divisibility.agda renamed to src/Algebra/Definitions/RawMagma.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Definition of divisibility
+-- Basic auxiliary definitions for magma-like structures
 ------------------------------------------------------------------------
 
 -- You're unlikely to want to use this module directly. Instead you
@@ -10,16 +10,17 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Algebra.Core
+open import Algebra.Bundles using (RawMagma)
 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)
+module Algebra.Definitions.RawMagma
+  {a ℓ} (M : RawMagma a ℓ)
   where
 
+open RawMagma M renaming (Carrier to A)
 open import Algebra.Definitions _≈_
 
 ------------------------------------------------------------------------
@@ -65,35 +66,3 @@ x ∣∣ y = x ∣ y × y ∣ x
 
 _∤∤_ : Rel A (a ⊔ ℓ)
 x ∤∤ y =  ¬ x ∣∣ y
-
-------------------------------------------------------------------------------
--- Greatest common divisor (GCD)
-
-record IsGCD (x y gcd : A) : Set (a ⊔ ℓ) where
-  constructor gcdᶜ
-  field
-    divides₁ : gcd ∣ x
-    divides₂ : gcd ∣ y
-    greatest : ∀ {z} → z ∣ x → z ∣ y → z ∣ gcd
-
-------------------------------------------------------------------------
--- 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

src/Algebra/Definitions/RawMonoid.agda

@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Basic auxiliary definitions for monoid-like structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (RawMonoid)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Vec.Functional as Vector using (Vector)
+
+module Algebra.Definitions.RawMonoid {a ℓ} (M : RawMonoid a ℓ) where
+
+open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# )
+
+------------------------------------------------------------------------
+-- Re-export definitions over a magma
+------------------------------------------------------------------------
+
+open import Algebra.Definitions.RawMagma rawMagma public
+
+------------------------------------------------------------------------
+-- Multiplication by natural number
+------------------------------------------------------------------------
+-- Standard definition
+
+-- A simple definition, easy to use and prove properties about.
+
+infixr 8 _×_
+
+_×_ : ℕ → Carrier → Carrier
+0     × x = 0#
+suc n × x = x + (n × x)
+
+------------------------------------------------------------------------
+-- Type-checking optimised definition
+
+-- For use in code where high performance at type-checking time is
+-- important, e.g. solvers and tactics. Firstly it avoids unnecessarily
+-- multiplying by the unit if possible, speeding up type-checking and
+-- makes for much more readable proofs:
+--
+--     Standard definition:  x * 2 = x + x + 0#
+--     Optimised definition: x * 2 = x + x
+--
+-- Secondly, associates to the left which, counterintuitive as it may
+-- seem, also speeds up typechecking.
+--
+--     Standard definition: x * 3 = x + (x + (x + 0#))
+--     Our definition:      x * 3 = (x + x) + x
+
+infixl 8 _×′_
+
+_×′_ : ℕ → Carrier → Carrier
+0     ×′ x = 0#
+1     ×′ x = x
+suc n ×′ x = x + n ×′ x
+
+------------------------------------------------------------------------
+-- Summation
+------------------------------------------------------------------------
+
+sum : ∀ {n} → Vector Carrier n → Carrier
+sum = Vector.foldr _+_ 0#

src/Algebra/Definitions/RawSemiring.agda

@@ -0,0 +1,67 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Basic auxiliary definitions for semiring-like structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (RawSemiring)
+open import Data.Sum.Base using (_⊎_)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+
+module Algebra.Definitions.RawSemiring {a ℓ} (M : RawSemiring a ℓ) where
+
+open RawSemiring M renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definitions over _+_
+
+open import Algebra.Definitions.RawMonoid +-rawMonoid public
+  using
+  ( _×_
+  ; _×′_
+  ; sum
+  )
+
+------------------------------------------------------------------------
+-- Definitions over _*_
+
+open import Algebra.Definitions.RawMonoid *-rawMonoid public
+  using
+  ( _∣_
+  ; _∤_
+  )
+  renaming
+  ( sum to product
+  )
+
+------------------------------------------------------------------------
+-- Coprimality
+
+Coprime : Rel A (a ⊔ ℓ)
+Coprime x y = ∀ {z} → z ∣ x → z ∣ y → z ∣ 1#
+
+record Irreducible (p : A) : Set (a ⊔ ℓ) where
+  constructor mkIrred
+  field
+    p∤1       : p ∤ 1#
+    split-∣1 : ∀ {x y} → p ≈ (x * y) → x ∣ 1# ⊎ y ∣ 1#
+
+record Prime (p : A) : Set (a ⊔ ℓ) where
+  constructor mkPrime
+  field
+    p≉0     : p ≉ 0#
+    split-∣ : ∀ {x y} → p ∣ x * y → p ∣ x ⊎ p ∣ y
+
+------------------------------------------------------------------------
+-- Greatest common divisor
+
+record IsGCD (x y gcd : A) : Set (a ⊔ ℓ) where
+  constructor gcdᶜ
+  field
+    divides₁ : gcd ∣ x
+    divides₂ : gcd ∣ y
+    greatest : ∀ {z} → z ∣ x → z ∣ y → z ∣ gcd
+