Continuing with generic GCD.

CHANGELOG.md

@@ -52,15 +52,29 @@ Deprecated names
 New modules
 -----------
 
-* Specifications for min and max operators
+* Specifications and properties for greater common divisor
   ```
-  Algebra.Construct.NaturalChoice.MinOp
-  Algebra.Construct.NaturalChoice.MaxOp 
+  Algebra.Properties.Semiring.GCD
+  Algebra.Properties.CancellativeCommutativeSemiring
+  Algebra.Properties.CancellativeCommutativeSemiring.GCD
   ```
 
 Other minor additions
 ---------------------
 
+* Added new proofs to `Algebra.Consequences.Setoid`:
+  ```agda
+  comm+cancelˡ-nonZero⇒cancelʳ-nonZero :
+    (0# : A) → AlmostLeftCancellative 0# _•_ → AlmostRightCancellative 0# _•_
+  comm+cancelʳ-nonZero⇒cancelˡ-nonZero :
+    (0# : A) → AlmostRightCancellative 0# _•_ → AlmostLeftCancellative 0# _•_
+  ```
+
+* Added new definitions to `Algebra.Structures`:
+  ```agda
+  IsGCDSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ)
+  ```
+
 * Added new proofs to `Data.Nat.Properties`:
   ```agda
   ⊔-⊓-absorptive            : Absorptive _⊓_ _
@@ -138,3 +152,16 @@ Other minor additions
   *-inverseˡ : ∀ p → 1/ p * p ≡ 1ℚ
   *-inverseʳ : ∀ p → p * 1/ p ≡ 1ℚ
   ```
+
+* Added new proofs in `Algebra.Properties.CommutativeSemigroup.Divisibility`:
+  ```agda
+  x∣y∧z∣x/y⇒xz∣y : ∀ {x y z} → ((x/y , _) : x ∣ y) → z ∣ x/y → x ∙ z ∣ y
+  x∣y⇒zx∣zy      : ∀ {x y} z → x ∣ y → z ∙ x ∣ z ∙ y
+  ```
+
+* Added new proofs in `Algebra.Properties.CancellativeCommutativeSemiring`:
+  ```agda
+  x*y≈0⇒x≈0⊎y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
+  x≉0∧y≉0⇒xy≉0  : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
+  xy∣x⇒y∣1      : ∀ {x y} → x ≉ 0# → x * y ∣ x → y ∣ 1#
+  ```

src/Algebra/Bundles.agda

@@ -763,6 +763,7 @@ record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _≉_
     )
 
+
 ------------------------------------------------------------------------
 -- Bundles with 2 binary operations, 1 unary operation & 2 elements
 ------------------------------------------------------------------------

src/Algebra/Consequences/Setoid.agda

@@ -25,7 +25,7 @@ open import Relation.Unary using (Pred)
 ------------------------------------------------------------------------
 -- Re-exports
 
--- Export base lemmas that don't require the setoidd
+-- Export base lemmas that don't require the setoid
 
 open import Algebra.Consequences.Base public
 
@@ -34,7 +34,7 @@ open import Algebra.Consequences.Base public
 
 module _ {_•_ : Op₂ A} (comm : Commutative _•_) where
 
-  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ →  RightCancellative _•_
+  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
   comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x (begin
     x • y ≈⟨ comm x y ⟩
     y • x ≈⟨ eq ⟩
@@ -48,6 +48,24 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) where
     x • z ≈⟨ comm x z ⟩
     z • x ∎)
 
+  comm+cancelˡ-nonZero⇒cancelʳ-nonZero :
+    (0# : A) → AlmostLeftCancellative 0# _•_ → AlmostRightCancellative 0# _•_
+  comm+cancelˡ-nonZero⇒cancelʳ-nonZero 0# 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   ∎)
+
+  comm+cancelʳ-nonZero⇒cancelˡ-nonZero :
+    (0# : A) → AlmostRightCancellative 0# _•_ → AlmostLeftCancellative 0# _•_
+  comm+cancelʳ-nonZero⇒cancelˡ-nonZero 0# cancelʳ-nonZero {x} y z x≉0 xy≈xz =
+    cancelʳ-nonZero y z x≉0 (begin
+      y • x   ≈⟨ comm y x ⟩
+      x • y   ≈⟨ xy≈xz ⟩
+      x • z   ≈⟨ comm x z ⟩
+      z • x   ∎)
+
 ------------------------------------------------------------------------
 -- Monoid-like structures
 

src/Algebra/Definitions/RawMagma.agda

@@ -10,6 +10,8 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+open import Algebra.Core
+open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃; swap)
 open import Algebra.Bundles using (RawMagma)
 open import Data.Product using (∃; _×_; _,_)
 open import Level using (_⊔_)
@@ -54,15 +56,38 @@ _∤_ : 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.
-
-infix 5 _∣∣_ _∤∤_
+-- Mutual divisibility _∣∣_.
+-- In a  monoid,  this is an equivalence relation extending _≈_.
+-- When in a  cancellative monoid,  elements related by _∣∣_ are called
+-- associated,  and there x ∣∣ y is equivalent to that x and y differ by
+-- some invertible factor.
+-- Example: for ℕ  this is equivalent to  x ≡ y,
+--          for ℤ  this is equivalent to  (x ≡ y  or  x ≡ -y).
 
 _∣∣_ : Rel A (a ⊔ ℓ)
 x ∣∣ y = x ∣ y × y ∣ x
 
 _∤∤_ : Rel A (a ⊔ ℓ)
-x ∤∤ y =  ¬ x ∣∣ y
+x ∤∤ y = ¬ x ∣∣ y
+
+------------------------------------------------------------------------
+-- Greatest common divisor (GCD)
+
+record IsGCD (x y gcd : A) : Set (a ⊔ ℓ) where
+  constructor mkIsGCD
+  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₂

src/Algebra/Definitions/RawSemiring.agda

@@ -9,6 +9,7 @@
 open import Algebra.Bundles using (RawSemiring)
 open import Data.Sum.Base using (_⊎_)
 open import Data.Nat using (ℕ)
+open import Data.Product using (proj₁; proj₂)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)
 
@@ -63,7 +64,7 @@ Coprime x y = ∀ {z} → z ∣ x → z ∣ y → z ∣ 1#
 record Irreducible (p : A) : Set (a ⊔ ℓ) where
   constructor mkIrred
   field
-    p∤1       : p ∤ 1#
+    p∤1      : p ∤ 1#
     split-∣1 : ∀ {x y} → p ≈ (x * y) → x ∣ 1# ⊎ y ∣ 1#
 
 record Prime (p : A) : Set (a ⊔ ℓ) where
@@ -72,3 +73,13 @@ record Prime (p : A) : Set (a ⊔ ℓ) where
     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 mkIsGCD
+  field
+    divides₁ : gcd ∣ x
+    divides₂ : gcd ∣ y
+    greatest : ∀ {z} → z ∣ x → z ∣ y → z ∣ gcd

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -0,0 +1,51 @@
+------------------------------------------------------------------------
+-- 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.Product using (_,_)
+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) where
+
+open EqReasoning setoid
+open import Algebra.Consequences.Setoid setoid
+  using (comm+cancelˡ-nonZero⇒cancelʳ-nonZero)
+open import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup
+  using (x∙yz≈y∙xz)
+open import Algebra.Properties.Semiring.Divisibility semiring
+
+*-cancelʳ-nonZero : AlmostRightCancellative _≈_ 0# _*_
+*-cancelʳ-nonZero = comm+cancelˡ-nonZero⇒cancelʳ-nonZero *-comm 0# *-cancelˡ-nonZero
+
+x*y≈0⇒x≈0⊎y≈0 : Decidable _≈_ → ∀ {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 : Decidable _≈_ → ∀ {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
+
+xy∣x⇒y∣1 : ∀ {x y} → x ≉ 0# → x * y ∣ x → y ∣ 1#
+xy∣x⇒y∣1 {x} {y} x≉0 (q , q*xy≈x) = q , *-cancelˡ-nonZero (q * y) 1# x≉0 (begin
+  x * (q * y)  ≈⟨ x∙yz≈y∙xz x q y ⟩
+  q * (x * y)  ≈⟨ q*xy≈x ⟩
+  x            ≈˘⟨ *-identityʳ x ⟩
+  x * 1#       ∎)

src/Algebra/Properties/CancellativeCommutativeSemiring/GCD.agda

@@ -0,0 +1,115 @@
+------------------------------------------------------------------------
+-- 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)
+  where
+
+open import Algebra.Properties.Semiring.Primality semiring using (Coprime)
+open import Algebra.Properties.Semiring.Divisibility semiring
+open EqReasoning setoid
+import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as Of*CSemig
+open import Algebra.Properties.CommutativeSemigroup.Divisibility
+  *-commutativeSemigroup using (x∣xy; x∣y∧z∣x/y⇒xz∣y; x∣y⇒zx∣zy)
+open import Algebra.Properties.CancellativeCommutativeSemiring R using (xy∣x⇒y∣1)
+
+---------------------------------------------------------------------------
+-- Re-exporting definition of GCD and its properties in semiring
+
+open import Algebra.Properties.Semiring.GCD semiring public
+
+---------------------------------------------------------------------------
+-- Properties of GCD
+
+x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd] : ∀ {x y d} → x ≉ 0# ⊎ y ≉ 0# →
+                                ((mkIsGCD (q₁ , _) (q₂ , _) _) : IsGCD x y d) →
+                                Coprime q₁ q₂
+x≉0⊎y≉0⇒Coprime[x/gcd,y/gcd] x≉0∨y≉0 gcd@(mkIsGCD d∣x d∣y greatest) x/d∣z y/d∣z =
+  xy∣x⇒y∣1 (x≉0∨y≉0⇒gcd≉0 gcd x≉0∨y≉0) (greatest
+    (x∣y∧z∣x/y⇒xz∣y d∣x x/d∣z)
+    (x∣y∧z∣x/y⇒xz∣y d∣y y/d∣z))
+
+------------------------------------------------------------------------------
+-- gcd-s for two division-equivalent pairs
+-- are division-equivalent
+
+GCD-unique : ∀ {x x' y y' d d'} → x ∣∣ x' → y ∣∣ y' →
+             IsGCD x y d → IsGCD x' y' d' → d ∣∣ d'
+GCD-unique (x∣x' , x'∣x) (y∣y' , y'∣y)
+           (mkIsGCD d∣x d∣y greatest) (mkIsGCD d'∣x' d'∣y' greatest') = d∣d' , d'∣d
+  where
+  d∣x' = ∣-trans d∣x x∣x';    d∣y' = ∣-trans d∣y y∣y';    d∣d' = greatest' d∣x' d∣y'
+  d'∣x = ∣-trans d'∣x' x'∣x;  d'∣y = ∣-trans d'∣y' y'∣y;  d'∣d = greatest d'∣x d'∣y
+
+------------------------------------------------------------------------------
+-- gcd-distr  is an important lemma of the gcd distributivity:
+-- gcd (c*a) (c*b)  is division-equivalent to  c * (gcd a b).
+
+gcd-distr : Decidable _≈_ → ∀ {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]@(mkIsGCD (a' , a'd≈a) (b' , b'd≈b) _)
+  isGCD[ca,cb,d']@(mkIsGCD d'∣ca d'∣cb _) = aux (c ≟ 0#)
+  where
+  d∣a = (a' , a'd≈a);  d∣b = (b' , b'd≈b)
+
+  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) =   -- General case. First prove  cd ∣ d'
+    let
+      cd∣ca = x∣y⇒zx∣zy c d∣a
+      cd∣cb = x∣y⇒zx∣zy c d∣b
+      cd∣d' = IsGCD.greatest isGCD[ca,cb,d'] cd∣ca cd∣cb
+
+      -- It remains to 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'@(x , xc≈d') = IsGCD.greatest isGCD[ca,cb,d'] c∣ca c∣cb
+      xc∣ca@(y , _) = ∣-respˡ (sym xc≈d') d'∣ca
+      xc∣cb@(z , _) = ∣-respˡ (sym xc≈d') d'∣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
+      cx∣cd = x∣y⇒zx∣zy c x∣d
+      cx≈d' = trans (*-comm c x) xc≈d'
+      d'∣cd = ∣-respˡ cx≈d' cx∣cd
+    in
+    d'∣cd , cd∣d'

src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

@@ -7,12 +7,16 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra using (CommutativeSemigroup)
+open import Data.Product using (_,_)
+import Relation.Binary.Reasoning.Setoid as EqReasoning
 
 module Algebra.Properties.CommutativeSemigroup.Divisibility
-  {a ℓ} (CM : CommutativeSemigroup a ℓ)
+  {a ℓ} (CS : CommutativeSemigroup a ℓ)
   where
 
-open CommutativeSemigroup CM
+open CommutativeSemigroup CS
+open import Algebra.Properties.CommutativeSemigroup CS using (x∙yz≈xz∙y; x∙yz≈y∙xz)
+open EqReasoning setoid
 
 ------------------------------------------------------------------------------
 -- Re-export the contents of divisibility over semigroups
@@ -24,3 +28,16 @@ open import Algebra.Properties.Semigroup.Divisibility semigroup public
 
 open import Algebra.Properties.CommutativeMagma.Divisibility commutativeMagma public
   using (x∣xy; xy≈z⇒x∣z; ∣-factors; ∣-factors-≈)
+
+x∣y∧z∣x/y⇒xz∣y : ∀ {x y z} → ((x/y , _) : x ∣ y) → z ∣ x/y → x ∙ z ∣ y
+x∣y∧z∣x/y⇒xz∣y {x} {y} {z} (x/y , x/y∙x≈y) (p , pz≈x/y) = p , (begin
+  p ∙ (x ∙ z)  ≈⟨ x∙yz≈xz∙y p x z ⟩
+  (p ∙ z) ∙ x  ≈⟨ ∙-congʳ pz≈x/y ⟩
+  x/y ∙ x      ≈⟨ x/y∙x≈y ⟩
+  y            ∎)
+
+x∣y⇒zx∣zy : ∀ {x y} z → x ∣ y → z ∙ x ∣ z ∙ y
+x∣y⇒zx∣zy {x} {y} z (q , qx≈y) = q , (begin
+ q ∙ (z ∙ x)  ≈⟨ x∙yz≈y∙xz q z x ⟩
+ z ∙ (q ∙ x)  ≈⟨ ∙-congˡ qx≈y ⟩
+ z ∙ y        ∎)