Definitions of GCD and Prime over semirings (#1345)

Author: mechvel

CHANGELOG.md

@@ -196,10 +196,14 @@ New modules
 * Generic divisibility over algebraic structures
   ```
   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
   ```
 
 * Generic summation over algebraic structures
@@ -554,6 +558,11 @@ Other minor additions
   *-distrib-⊓           : _*_ DistributesOver _⊓_
   ```
 
+* Added new operation in `Data.Sum`:
+  ```agda
+  reduce : A ⊎ A → A
+  ```
+
 * Added new proofs in `Data.Sign.Properties`:
   ```agda
   s*opposite[s]≡- : ∀ s → s * opposite s ≡ -

src/Algebra/Bundles.agda

@@ -748,6 +748,8 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; nearSemiring; semiringWithoutOne
     ; semiringWithoutAnnihilatingZero
     ; rawSemiring
+    ; semiring
+    ; _≉_
     )
 
 ------------------------------------------------------------------------

src/Algebra/Divisibility.agda

@@ -23,28 +23,58 @@ module Algebra.Divisibility
 open import Algebra.Definitions _≈_
 
 ------------------------------------------------------------------------
--- Definitions
-
 -- Divisibility
 
-infix 5 _∣_ _∤_ _∣∣_ _¬∣∣_
+infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_
+
+-- Divisibility from the left
+
+_∣ˡ_ : Rel A (a ⊔ ℓ)
+x ∣ˡ y = ∃ λ q → (x ∙ q) ≈ y
+
+_∤ˡ_ : Rel A (a ⊔ ℓ)
+x ∤ˡ y = ¬ x ∣ˡ y
+
+-- Divisibility from the right
+
+_∣ʳ_ : Rel A (a ⊔ ℓ)
+x ∣ʳ y = ∃ λ q → (q ∙ x) ≈ y
+
+_∤ʳ_ : Rel A (a ⊔ ℓ)
+x ∤ʳ y = ¬ x ∣ʳ y
+
+-- _∣ˡ_ and _∣ʳ_ are only equivalent in the commutative case. In this
+-- case we take the right definition to be the primary one.
 
 _∣_ : Rel A (a ⊔ ℓ)
-x ∣ y = ∃ λ q → (q ∙ x) ≈ y
+_∣_ = _∣ʳ_
 
 _∤_ : Rel A (a ⊔ ℓ)
 x ∤ y = ¬ x ∣ y
 
--- Mutual divisibility.
+------------------------------------------------------------------------
+-- 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.
 
+infix 5 _∣∣_ _∤∤_
+
 _∣∣_ : Rel A (a ⊔ ℓ)
 x ∣∣ y = x ∣ y × y ∣ x
 
-_¬∣∣_ : Rel A (a ⊔ ℓ)
-x ¬∣∣ y =  ¬ x ∣∣ y
+_∤∤_ : 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
@@ -67,9 +97,3 @@ x ¬∣∣ y =  ¬ x ∣∣ 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/Primality.agda

@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions of irreducibility, primality, coprimality.
+------------------------------------------------------------------------
+
+-- You're unlikely to want to use this module directly. Instead you
+-- probably want to be importing the appropriate module from e.g.
+-- `Algebra.Properties.Semiring.Primality`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Core using (Op₂)
+open import Data.Sum using (_⊎_)
+open import Function using (flip)
+open import Level using (_⊔_)
+open import Relation.Binary using (Rel; Symmetric)
+open import Relation.Nullary using (¬_)
+
+module Algebra.Primality
+  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_*_ : Op₂ A) (0# 1# : A)
+  where
+
+open import Algebra.Divisibility _≈_ _*_
+
+------------------------------------------------------------------------------
+-- Definitions
+
+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

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -18,7 +18,7 @@ open CommutativeMagma CM
 open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------------
--- Re-export the contents of semigroup
+-- Re-export the contents of magmas
 
 open import Algebra.Properties.Magma.Divisibility magma public
 

src/Algebra/Properties/Magma/Divisibility.agda

@@ -14,13 +14,13 @@ module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where
 
 open Magma M
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Re-export divisibility relations publicly
 
 open import Algebra.Divisibility _≈_ _∙_ as Div public
-  using (_∣_; _∤_; _∣∣_; _¬∣∣_)
+  using (_∣_; _∤_; _∣∣_; _∤∤_)
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Properties of divisibility
 
 ∣-respʳ : _∣_ Respectsʳ _≈_

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -18,15 +18,15 @@ open Monoid M
 import Algebra.Divisibility _≈_ _∙_ as Div
 
 ------------------------------------------------------------------------
--- Re-export magma divisibility
+-- Re-export semigroup divisibility
 
 open import Algebra.Properties.Semigroup.Divisibility semigroup public
 
 ------------------------------------------------------------------------
 -- Additional properties
 
 ε∣_ : ∀ x → ε ∣ x
-ε∣_ = Div.∣-min identityʳ
+ε∣ x = x , identityʳ x
 
 ∣-refl : Reflexive _∣_
 ∣-refl = Div.∣-refl identityˡ

src/Algebra/Properties/Semiring/Divisibility.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of divisibility over semirings
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Semiring)
+import Algebra.Properties.Monoid.Divisibility as MonoidDivisibility
+open import Data.Product using (_,_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+
+module Algebra.Properties.Semiring.Divisibility
+  {a ℓ} (R : Semiring a ℓ) where
+
+open Semiring R
+
+------------------------------------------------------------------------
+-- Re-exporting divisibility over monoids
+
+open MonoidDivisibility *-monoid public
+  renaming (ε∣_ to 1∣_)
+
+------------------------------------------------------------------------
+-- Divisibility properties specific to semirings.
+
+_∣0 : ∀ x → x ∣ 0#
+x ∣0 = 0# , zeroˡ x
+
+0∣x⇒x≈0 : ∀ {x} → 0# ∣ x → x ≈ 0#
+0∣x⇒x≈0 (q , q*0≈x) = trans (sym q*0≈x) (zeroʳ q)
+
+x∣y∧y≉0⇒x≉0 : ∀ {x y} → x ∣ y → y ≉ 0# → x ≉ 0#
+x∣y∧y≉0⇒x≉0 x∣y y≉0 x≈0 = y≉0 (0∣x⇒x≈0 (∣-respˡ x≈0 x∣y))
+
+0∤1 : 0# ≉ 1# → 0# ∤ 1#
+0∤1 0≉1 (q , q*0≈1) = 0≉1 (trans (sym (zeroʳ q)) q*0≈1)

src/Algebra/Properties/Semiring/GCD.agda

@@ -0,0 +1,30 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the Greatest Common Divisor over semirings.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Semiring)
+import Algebra.Properties.Monoid.Divisibility as MonoidDiv
+open import Data.Product using (_,_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+
+module Algebra.Properties.Semiring.GCD {a ℓ} (R : Semiring a ℓ) where
+
+open Semiring R
+open import Algebra.Properties.Semiring.Divisibility R
+
+------------------------------------------------------------------------
+-- Re-exporting definition of GCD
+
+open import Algebra.Divisibility _≈_ _*_ public
+  using (IsGCD; gcdᶜ)
+
+------------------------------------------------------------------------
+-- Properties of GCD
+
+x≉0⊎y≉0⇒gcd≉0 : ∀ {x y d} → IsGCD x y d → x ≉ 0# ⊎ y ≉ 0# → d ≉ 0#
+x≉0⊎y≉0⇒gcd≉0 (gcdᶜ d∣x _ _) (inj₁ x≉0) = x∣y∧y≉0⇒x≉0 d∣x x≉0
+x≉0⊎y≉0⇒gcd≉0 (gcdᶜ _ d∣y _) (inj₂ y≉0) = x∣y∧y≉0⇒x≉0 d∣y y≉0

src/Algebra/Properties/Semiring/Primality.agda

@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some theory for CancellativeCommutativeSemiring.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Semiring)
+import Algebra.Primality
+import Algebra.Properties.Semigroup.Divisibility as SemigroupDiv
+import Algebra.Properties.Semiring.Divisibility as SemiringDiv
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂; reduce)
+open import Function using (case_of_; flip)
+open import Level using (_⊔_)
+open import Relation.Binary using (Rel; Symmetric; Setoid)
+open import Relation.Unary using (Pred)
+
+module Algebra.Properties.Semiring.Primality
+  {a ℓ} (R : Semiring a ℓ)
+  where
+
+open Semiring R renaming (Carrier to A)
+open SemiringDiv R
+
+------------------------------------------------------------------------------
+-- Re-export primality definitions
+
+open Algebra.Primality _≈_ _*_ 0# 1# public
+
+------------------------------------------------------------------------------
+-- Properties of Irreducible
+
+Irreducible⇒≉0 : 0# ≉ 1# → ∀ {p} → Irreducible p → p ≉ 0#
+Irreducible⇒≉0 0≉1 (mkIrred _ chooseInvertible) p≈0 =
+  0∤1 0≉1 (reduce (chooseInvertible (trans p≈0 (sym (zeroˡ 0#)))))
+
+------------------------------------------------------------------------------
+-- Properties of Coprime
+
+Coprime-sym : Symmetric Coprime
+Coprime-sym coprime = flip coprime
+
+∣1⇒Coprime : ∀ {x} y → x ∣ 1# → Coprime x y
+∣1⇒Coprime {x} y x∣1 z∣x _ = ∣-trans z∣x x∣1