Continuing with generic GCD.

CHANGELOG.md

@@ -204,6 +204,8 @@ New modules
   Algebra.Properties.CommutativeSemigroup.Divisibility
   Algebra.Properties.Semiring.Divisibility
   Algebra.Properties.Semiring.GCD
+  Algebra.Properties.CancellativeCommutativeSemiring
+  Algebra.Properties.CancellativeCommutativeSemiring.GCD
   ```
 
 * Generic summation over algebraic structures
@@ -305,6 +307,7 @@ Other minor additions
   RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ))
   RawLattice c ℓ : Set (suc (c ⊔ ℓ))
   CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ))
+  GCDSemiring c ℓ : Set (suc (c ⊔ ℓ))
   ```
 
 * Added new definitions to `Algebra.Definitions`:

src/Algebra/Bundles.agda

@@ -752,6 +752,33 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _≉_
     )
 
+record GCDSemiring 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
+    isGCDSemiring : IsGCDSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsGCDSemiring isGCDSemiring public
+
+  cancellativeCommutativeSemiring : CancellativeCommutativeSemiring c ℓ
+  cancellativeCommutativeSemiring = record
+    { Carrier                           = Carrier
+    ; _≈_                               = _≈_
+    ; _+_                               = _+_
+    ; _*_                               = _*_
+    ; 0#                                = 0#
+    ; 1#                                = 1#
+    ; isCancellativeCommutativeSemiring = isCancellativeCommutativeSemiring
+    }
+
+
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 2 elements
 ------------------------------------------------------------------------

src/Algebra/Divisibility.agda

@@ -1,4 +1,4 @@
-------------------------------------------------------------------------
+-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definition of divisibility
@@ -11,7 +11,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra.Core
-open import Data.Product using (∃; _×_; _,_)
+open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
 open import Level using (_⊔_)
 open import Relation.Binary
 open import Relation.Nullary using (¬_)
@@ -70,12 +70,25 @@ x ∤∤ y =  ¬ x ∣∣ y
 -- Greatest common divisor (GCD)
 
 record IsGCD (x y gcd : A) : Set (a ⊔ ℓ) where
-  constructor gcdᶜ
+  constructor isGCDᶜ
   field
     divides₁ : gcd ∣ x
     divides₂ : gcd ∣ y
     greatest : ∀ {z} → z ∣ x → z ∣ y → z ∣ gcd
 
+  quot₁ : A               -- a complementory quotient  x/gcd
+  quot₁ = proj₁ divides₁
+
+  quot₂ : A               -- y/gcd
+  quot₂ = proj₁ divides₂
+
+  quot₁∙gcd≈x : (quot₁ ∙ gcd) ≈ x
+  quot₁∙gcd≈x = proj₂ divides₁
+
+  quot₂∙gcd≈y : (quot₂ ∙ gcd) ≈ y
+  quot₂∙gcd≈y = proj₂ divides₂
+
+
 ------------------------------------------------------------------------
 -- Properties
 

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some properties of operations in CancellativeCommutativeSemiring.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (CancellativeCommutativeSemiring)
+open import Algebra.Definitions using (AlmostRightCancellative)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Function using (_$_)
+open import Relation.Binary using (Decidable)
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
+
+module Algebra.Properties.CancellativeCommutativeSemiring
+  {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
+  (open CancellativeCommutativeSemiring R) (_≟_ : Decidable _≈_) where
+
+open EqReasoning setoid
+
+*-cancelʳ-nonZero : AlmostRightCancellative _≈_ 0# _*_
+                   -- ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+                   -- as * is commutative, left and right cancellation
+                   -- are equivalent
+*-cancelʳ-nonZero {x} y z x≉0 yx≈zx = *-cancelˡ-nonZero y z x≉0 $ begin
+  x * y   ≈⟨ *-comm x y ⟩
+  y * x   ≈⟨ yx≈zx ⟩
+  z * x   ≈⟨ *-comm z x ⟩
+  x * z   ∎
+
+x*y≈0⇒x≈0⊎y≈0 : ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
+x*y≈0⇒x≈0⊎y≈0 {x} {y} xy≈0 with x ≟ 0# | y ≟ 0#
+... | yes x≈0 | _       = inj₁ x≈0
+... | no _    | yes y≈0 = inj₂ y≈0
+... | no x≉0  | no y≉0  = contradiction y≈0 y≉0
+  where
+  xy≈x*0 = trans xy≈0 (sym (zeroʳ x));   y≈0 = *-cancelˡ-nonZero y 0# x≉0 xy≈x*0
+
+x≉0∧y≉0⇒xy≉0 : ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
+x≉0∧y≉0⇒xy≉0 x≉0 y≉0 xy≈0 with x*y≈0⇒x≈0⊎y≈0 xy≈0
+... | inj₁ x≈0 = x≉0 x≈0
+... | inj₂ y≈0 = y≉0 y≈0

src/Algebra/Properties/CancellativeCommutativeSemiring/GCD.agda

@@ -0,0 +1,183 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the Greatest Common Divisor in CancellativeCommutativeSemiring.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (CancellativeCommutativeSemiring)
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_)
+open import Relation.Binary using (Decidable)
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+open import Relation.Nullary using (Dec; yes; no)
+
+module Algebra.Properties.CancellativeCommutativeSemiring.GCD
+  {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
+  (open CancellativeCommutativeSemiring R)
+  (_≟_ : Decidable _≈_)
+  where
+
+open import Algebra.Properties.Semiring.Divisibility semiring using (_∣0; 0∣x⇒x≈0)
+open EqReasoning setoid
+open import Algebra.Properties.Monoid.Divisibility *-monoid using
+  (∣-refl; ∣-trans; ∣-respˡ; ∣-respʳ; ∣∣-reflexive)
+import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as Of*CSemig
+open import Algebra.Properties.CommutativeSemigroup.Divisibility
+  *-commutativeSemigroup using (x∣xy)
+
+------------------------------------------------------------------------
+-- Re-exporting definition of GCD, primality, properties of GCD in semiring
+
+open import Algebra.Divisibility _≈_ _*_ public
+  using (_∣_; _∣∣_)
+open import Algebra.Primality _≈_ _*_ 0# 1# public
+  using (Coprime)
+open import Algebra.Properties.Semiring.GCD semiring public
+
+------------------------------------------------------------------------
+-- Properties of GCD
+
+x≈0⊎y≉0⇒Coprime[x/gcd,y/gcd] :
+  ∀ {x y d} (isGCD : IsGCD x y d) → (x ≉ 0#) ⊎ (y ≉ 0#) →
+  let open IsGCD isGCD
+  in  Coprime quot₁ quot₂     -- x/gcd(x,y) is coprime with y/gcd(x,y)
+                              -- if any of x, y is nonzero
+
+x≈0⊎y≉0⇒Coprime[x/gcd,y/gcd] {x} {y} {d} isGCD nz⊎nz {c}
+                             (q₁ , q₁c≈quot₁) (q₂ , q₂c≈quot₂) = c∣1
+  where
+  open IsGCD isGCD using (greatest; quot₁; quot₂; quot₁∙gcd≈x; quot₂∙gcd≈y)
+  d≉0     = x≉0⊎y≉0⇒gcd≉0 isGCD nz⊎nz
+  q₁*dc≈x = begin
+    q₁ * (d * c)    ≈⟨ Of*CSemig.x∙yz≈xz∙y q₁ d c ⟩
+    (q₁ * c) * d    ≈⟨ *-congʳ q₁c≈quot₁ ⟩
+    quot₁ * d       ≈⟨ quot₁∙gcd≈x ⟩
+    x               ∎
+
+  q₂*dc≈y = begin
+    q₂ * (d * c)    ≈⟨ Of*CSemig.x∙yz≈xz∙y q₂ d c ⟩
+    (q₂ * c) * d    ≈⟨ *-congʳ q₂c≈quot₂ ⟩
+    quot₂ * d       ≈⟨ quot₂∙gcd≈y ⟩
+    y               ∎
+
+  dc∣x = q₁ , q₁*dc≈x
+  dc∣y = q₂ , q₂*dc≈y
+  c∣1  = let
+           (q , q*dc≈d) = greatest dc∣x dc∣y
+           d*qc≈d*1     = begin
+             d * (q * c)   ≈⟨ Of*CSemig.x∙yz≈y∙xz d q c ⟩
+             q * (d * c)   ≈⟨ q*dc≈d ⟩
+             d             ≈⟨ sym (*-identityʳ d) ⟩
+             d * 1#        ∎
+
+           qc≈1 = *-cancelˡ-nonZero {d} (q * c) 1# d≉0 d*qc≈d*1
+        in
+        q , qc≈1
+
+------------------------------------------------------------------------------
+-- Recall that  x ∣∣ y  means that x and y are equal as association classes by
+-- division. For example, for ℕ  this means  x ≡ y,
+-- for ℤ  this means (x ≡ y  or  x ≡ -y).
+
+GCD-unique : ∀ {x x' y y' d d'} → x ∣∣ x' → y ∣∣ y' →
+             IsGCD x y d → IsGCD x' y' d' → d ∣∣ d'
+                                            -- gcd-s for assoc-equal pairs are assoc-equal.
+GCD-unique {x} {x'} {y} {y'} {d} {d'} (x∣x' , x'∣x) (y∣y' , y'∣y) isGCD isGCD' =
+  d∣d' , d'∣d
+  where
+  open IsGCD isGCD  using () renaming (divides₁ to d∣x; divides₂ to d∣y)
+  open IsGCD isGCD' using () renaming (divides₁ to d'∣x'; divides₂ to d'∣y')
+  d∣x' = ∣-trans d∣x x∣x'
+  d∣y' = ∣-trans d∣y y∣y'
+  d∣d' = IsGCD.greatest isGCD' d∣x' d∣y'
+  d'∣x = ∣-trans d'∣x' x'∣x
+  d'∣y = ∣-trans d'∣y' y'∣y
+  d'∣d = IsGCD.greatest isGCD d'∣x d'∣y
+
+------------------------------------------------------------------------------
+-- gcd-distr  is an important lemma of the gcd distributivity:
+-- gcd (c*a) (c*b)  assoc-equal  c * (gcd a b).
+
+gcd-distr : ∀ {a b c d d'} → IsGCD a b d → IsGCD (c * a) (c * b) d' → d' ∣∣ (c * d)
+gcd-distr {a} {b} {c} {d} {d'} isGCD-a-b-d isGCD-ca-cb-d' =  aux (c ≟ 0#)
+  where
+  aux : Dec (c ≈ 0#) → d' ∣∣ (c * d)
+  aux (yes c≈0) = d'∣cd , cd∣d'   -- A trivial case. The goal is reduced to 0 ∣∣ 0.
+    where
+    cd≈0  = trans (*-congʳ c≈0) (zeroˡ d)
+    d'∣cd = ∣-respʳ (sym cd≈0) (_∣0 d')     -- the first part of the goal
+
+    ca≈0  = trans (*-congʳ c≈0) (zeroˡ a)
+    ca∣∣0 = ∣∣-reflexive ca≈0
+    cb≈0  = trans (*-congʳ c≈0) (zeroˡ b)
+    cb∣∣0 = ∣∣-reflexive cb≈0
+    d'∣∣0 = GCD-unique ca∣∣0 cb∣∣0 isGCD-ca-cb-d' (isGCD-0-x-x 0#)
+    d'≈0  = 0∣x⇒x≈0 (proj₂ d'∣∣0)
+    cd∣0  = _∣0 (c * d)
+    cd∣d' = ∣-respʳ (sym d'≈0) cd∣0    -- the second part of the goal
+
+  aux (no c≉0) = d'∣cd , cd∣d'    -- general case
+    where
+    -- First derive  cd ∣ d'  from that  cd  divides both  ca and cb.
+
+    open IsGCD isGCD-a-b-d using ()
+                           renaming (quot₁ to a'; quot₂ to b';
+                                     quot₁∙gcd≈x to a'd≈a; quot₂∙gcd≈y to b'd≈b
+                                    )
+    open IsGCD isGCD-ca-cb-d' using () renaming (divides₁ to d'∣ca;  divides₂ to d'∣cb)
+    ca = c * a;  cb = c * b;  cd = c * d
+
+    cd∣ca = a' , a'*cd≈ca
+      where
+      a'*cd≈ca = begin
+        a' * (c * d)   ≈⟨ Of*CSemig.x∙yz≈y∙xz a' c d ⟩
+        c * (a' * d)   ≈⟨ *-congˡ a'd≈a ⟩
+        c * a          ∎
+
+    cd∣cb = b' , b'*cd≈cb
+      where
+      b'*cd≈cb = begin
+        b' * (c * d)   ≈⟨ Of*CSemig.x∙yz≈y∙xz b' c d ⟩
+        c * (b' * d)   ≈⟨ *-congˡ b'd≈b ⟩
+        c * b          ∎
+
+    cd∣d' = IsGCD.greatest isGCD-ca-cb-d' cd∣ca cd∣cb
+
+    -- Now, prove  d' ∣ cd  ----------------
+
+    c∣ca = x∣xy c a;  c∣cb = x∣xy c b   -- hence  xc ≈ gcd ca cb = d'  for some x
+
+    c∣d'    = IsGCD.greatest isGCD-ca-cb-d' c∣ca c∣cb
+    x       = proj₁ c∣d'
+    xc≈d'   = proj₂ c∣d'
+    xc∣ca   = ∣-respˡ (sym xc≈d') d'∣ca
+    xc∣cb   = ∣-respˡ (sym xc≈d') d'∣cb
+    y       = proj₁ xc∣ca   -- y*xc ≈ ca
+    z       = proj₁ xc∣cb   -- z*xc ≈ cb
+    ca≈c*yx = begin
+      c * a         ≈⟨ sym (proj₂ xc∣ca) ⟩
+      y * (x * c)   ≈⟨ Of*CSemig.x∙yz≈z∙xy y x c ⟩
+      c * (y * x)   ∎
+
+    cb≈c*zx = begin
+      c * b         ≈⟨ sym (proj₂ xc∣cb) ⟩
+      z * (x * c)   ≈⟨ Of*CSemig.x∙yz≈z∙xy z x c ⟩
+      c * (z * x)   ∎
+
+    yx≈a     = *-cancelˡ-nonZero {c} (y * x) a c≉0 (sym ca≈c*yx)
+    zx≈b     = *-cancelˡ-nonZero {c} (z * x) b c≉0 (sym cb≈c*zx)
+    x∣a      = y , yx≈a
+    x∣b      = z , zx≈b
+    x∣d      = IsGCD.greatest isGCD-a-b-d x∣a x∣b
+    x'       = proj₁ x∣d
+    x'x≈d    = proj₂ x∣d
+    x'*cx≈cd = begin
+      x' * (c * x)   ≈⟨ Of*CSemig.x∙yz≈y∙xz x' c x ⟩
+      c * (x' * x)   ≈⟨ *-congˡ x'x≈d ⟩
+      c * d          ∎
+
+    cx∣cd = x' , x'*cx≈cd
+    cx≈d' = trans (*-comm c x) xc≈d'
+    d'∣cd = ∣-respˡ cx≈d' cx∣cd

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -34,6 +34,9 @@ open import Algebra.Properties.Semigroup.Divisibility semigroup public
 ∣-reflexive : _≈_ ⇒ _∣_
 ∣-reflexive = Div.∣-reflexive trans identityˡ
 
+∣∣-reflexive : _≈_ ⇒ _∣∣_
+∣∣-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y)
+
 ∣-isPreorder : IsPreorder _≈_ _∣_
 ∣-isPreorder = record
   { isEquivalence = isEquivalence

src/Algebra/Properties/Semiring/GCD.agda

@@ -7,24 +7,45 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra using (Semiring)
-import Algebra.Properties.Monoid.Divisibility as MonoidDiv
-open import Data.Product using (_,_)
+import Algebra.Primality as Primality
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
 module Algebra.Properties.Semiring.GCD {a ℓ} (R : Semiring a ℓ) where
 
 open Semiring R
+open Primality _≈_ _*_ 0# 1# using (Coprime)
+-- open import Algebra.Properties.Monoid.Divisibility *-monoid using (∣-refl)
+
 open import Algebra.Properties.Semiring.Divisibility R
 
 ------------------------------------------------------------------------
 -- Re-exporting definition of GCD
 
 open import Algebra.Divisibility _≈_ _*_ public
-  using (IsGCD; gcdᶜ)
+  using (IsGCD; isGCDᶜ)
 
 ------------------------------------------------------------------------
 -- Properties of GCD
 
+isGCD-0-x-x : ∀ x → IsGCD 0# x x
+isGCD-0-x-x x =  isGCDᶜ (_∣0 x) ∣-refl (λ _ y∣x → y∣x)
+
+isGCD-x-0-x : ∀ x → IsGCD x 0# x
+isGCD-x-0-x x =  isGCDᶜ ∣-refl (_∣0 x) (λ y∣x _ → y∣x)
+
 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
+x≉0⊎y≉0⇒gcd≉0 (isGCDᶜ d∣x _ _) (inj₁ x≉0) = x∣y∧y≉0⇒x≉0 d∣x x≉0
+x≉0⊎y≉0⇒gcd≉0 (isGCDᶜ _ d∣y _) (inj₂ y≉0) = x∣y∧y≉0⇒x≉0 d∣y y≉0
+
+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 (isGCDᶜ _ _ greatest) x≈0 y≈0 =  0∣x⇒x≈0 0∣d
+  where
+  0∣x = ∣-respʳ (sym x≈0) (0# ∣0)
+  0∣y = ∣-respʳ (sym y≈0) (0# ∣0)
+  0∣d = greatest {0#} 0∣x 0∣y
+
+coprime⇒gcd∣1 : ∀ {x y d} → IsGCD x y d → Coprime x y →  d ∣ 1#
+                                   -- (gcd x y) is invertible for (coprime x y)
+coprime⇒gcd∣1 isGCD coprime-x-y =  coprime-x-y divides₁ divides₂
+  where
+  open IsGCD isGCD