Some more properties of algebraic bundles

Author: mechvel

CHANGELOG.md

@@ -140,8 +140,10 @@ Deprecated names
 New modules
 -----------
 
-* Added `Data.Maybe.Relation.Binary.Connected`, a variant of the `Pointwise` 
-  relation where `nothing` is also related to `just`.
+* Properties of cancellative commutative semirings
+  ```
+  Algebra.Properties.CancellativeCommutativeSemiring
+  ```
 
 * Specifications for min and max operators
   ```
@@ -169,6 +171,9 @@ New modules
   Data.List.Sort.MergeSort
   ```
 
+* Added `Data.Maybe.Relation.Binary.Connected`, a variant of the `Pointwise` 
+  relation where `nothing` is also related to `just`.
+
 * Linear congruential pseudo random generators for ℕ.
   /!\ NB: LCGs must not be used for cryptographic applications
   /!\ NB: the example parameters provided are not claimed to be good
@@ -224,6 +229,45 @@ New modules
 Other minor additions
 ---------------------
 
+* Added new proofs to `Algebra.Consequences.Setoid`:
+  ```agda
+  comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative  e _•_ → AlmostRightCancellative e _•_
+  comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ → AlmostLeftCancellative  e _•_
+  ```
+
+* Added new proofs in `Algebra.Properties.Magma.Divisibility`:
+  ```agda
+  ∣∣-sym     : Symmetric _∣∣_
+  ∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_
+  ∣∣-respˡ-≈ : _∣∣_ Respectsˡ _≈_
+  ∣∣-resp-≈  : _∣∣_ Respects₂ _≈_
+  ```
+
+* Added new proofs in `Algebra.Properties.Semigroup.Divisibility`:
+  ```agda
+  ∣∣-trans : Transitive _∣∣_
+  ```
+
+* Added new proofs in `Algebra.Properties.CommutativeSemigroup.Divisibility`:
+  ```agda
+  x∣y∧z∣x/y⇒xz∣y : ((x/y , _) : x ∣ y) → z ∣ x/y → x ∙ z ∣ y
+  x∣y⇒zx∣zy      : x ∣ y → z ∙ x ∣ z ∙ y
+  ```
+
+* Added new proofs in `Algebra.Properties.Monoid.Divisibility`:
+  ```agda
+  ∣∣-refl          : Reflexive _∣∣_
+  ∣∣-reflexive     : _≈_ ⇒ _∣∣_
+  ∣∣-isEquivalence : IsEquivalence _∣∣_
+  ```
+
+* Added new proofs in `Algebra.Properties.CancellativeCommutativeSemiring`:
+  ```agda
+  xy≈0⇒x≈0∨y≈0 : Decidable _≈_ →  x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
+  x≉0∧y≉0⇒xy≉0 : Decidable _≈_ →  x ≉ 0# → y ≉ 0# → x * y ≉ 0#
+  xy∣x⇒y∣1     : x ≉ 0# → x * y ∣ x → y ∣ 1#
+  ```
+
 * Added new function in `Data.Char.Base`:
   ```agda
   _≈ᵇ_ : (c d : Char) → Bool

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

@@ -9,23 +9,22 @@
 
 open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)
 
-module Algebra.Consequences.Setoid
-  {a ℓ} (S : Setoid a ℓ) where
+module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 
 open Setoid S renaming (Carrier to A)
-
 open import Algebra.Core
 open import Algebra.Definitions _≈_
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product using (_,_)
+open import Function.Base using (_$_)
 import Relation.Binary.Consequences as Bin
 open import Relation.Binary.Reasoning.Setoid S
 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,19 +33,19 @@ open import Algebra.Consequences.Base public
 
 module _ {_•_ : Op₂ A} (comm : Commutative _•_) where
 
-  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ →  RightCancellative _•_
-  comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x (begin
+  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
+  comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x $ begin
     x • y ≈⟨ comm x y ⟩
     y • x ≈⟨ eq ⟩
     z • x ≈⟨ comm z x ⟩
-    x • z ∎)
+    x • z ∎
 
   comm+cancelʳ⇒cancelˡ : RightCancellative _•_ → LeftCancellative _•_
-  comm+cancelʳ⇒cancelˡ cancelʳ x {y} {z} eq = cancelʳ y z (begin
+  comm+cancelʳ⇒cancelˡ cancelʳ x {y} {z} eq = cancelʳ y z $ begin
     y • x ≈⟨ comm y x ⟩
     x • y ≈⟨ eq ⟩
     x • z ≈⟨ comm x z ⟩
-    z • x ∎)
+    z • x ∎
 
 ------------------------------------------------------------------------
 -- Monoid-like structures
@@ -77,6 +76,24 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where
     x • e ≈⟨ zeʳ x ⟩
     e     ∎
 
+  comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ →
+                                     AlmostRightCancellative e _•_
+  comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} y z x≉e yx≈zx =
+    cancelˡ-nonZero y z x≉e $ begin
+      x • y ≈⟨ comm x y ⟩
+      y • x ≈⟨ yx≈zx ⟩
+      z • x ≈⟨ comm z x ⟩
+      x • z ∎
+
+  comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ →
+                                     AlmostLeftCancellative e _•_
+  comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} y z x≉e xy≈xz =
+    cancelʳ-nonZero y z x≉e $ begin
+      y • x ≈⟨ comm y x ⟩
+      x • y ≈⟨ xy≈xz ⟩
+      x • z ≈⟨ comm x z ⟩
+      z • x ∎
+
 ------------------------------------------------------------------------
 -- Group-like structures
 

src/Algebra/Definitions/RawMagma.agda

@@ -11,17 +11,16 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra.Bundles using (RawMagma)
-open import Data.Product using (∃; _×_; _,_)
+open import Data.Product using (_×_; ∃)
 open import Level using (_⊔_)
-open import Relation.Binary
+open import Relation.Binary.Core
 open import Relation.Nullary using (¬_)
 
 module Algebra.Definitions.RawMagma
   {a ℓ} (M : RawMagma a ℓ)
   where
 
 open RawMagma M renaming (Carrier to A)
-open import Algebra.Definitions _≈_
 
 ------------------------------------------------------------------------
 -- Divisibility
@@ -44,8 +43,11 @@ 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.
+-- General divisibility
+
+-- The relations _∣ˡ_ and _∣ʳ_ are only equivalent when _∙_ is
+-- commutative. When that is not the case we take `_∣ʳ_` to be the
+-- primary one.
 
 _∣_ : Rel A (a ⊔ ℓ)
 _∣_ = _∣ʳ_
@@ -54,15 +56,18 @@ _∤_ : 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.
+-- In a  monoid, this is an equivalence relation extending _≈_.
+-- When in a cancellative monoid,  elements related by _∣∣_ are called
+-- associated, and `x ∣∣ y` means that `x` and `y` differ by some
+-- invertible factor.
 
-infix 5 _∣∣_ _∤∤_
+-- 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

src/Algebra/Definitions/RawSemiring.agda

@@ -71,4 +71,3 @@ record Prime (p : A) : Set (a ⊔ ℓ) where
   field
     p≉0     : p ≉ 0#
     split-∣ : ∀ {x y} → p ∣ x * y → p ∣ x ⊎ p ∣ y
-

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- 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 Relation.Binary using (Decidable)
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
+
+module Algebra.Properties.CancellativeCommutativeSemiring
+  {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
+  where
+
+open CancellativeCommutativeSemiring R
+open import Algebra.Consequences.Setoid setoid
+open import Relation.Binary.Reasoning.Setoid setoid
+
+*-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_
+*-almostCancelʳ = comm+almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
+
+xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
+xy≈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 xy≈0⇒x≈0∨y≈0 _≟_ xy≈0
+... | inj₁ x≈0 = x≉0 x≈0
+... | inj₂ y≈0 = y≉0 y≈0

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,19 @@ 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-≈)
+
+------------------------------------------------------------------------------
+-- New properties
+
+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        ∎)

src/Algebra/Properties/Magma/Divisibility.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra using (Magma)
-open import Data.Product using (_×_; _,_; ∃; map)
+open import Data.Product using (_×_; _,_; ∃; map; swap)
 open import Relation.Binary.Definitions
 
 module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where
@@ -37,3 +37,18 @@ x∣yx x y = y , refl
 
 xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z
 xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x)
+
+------------------------------------------------------------------------
+-- Properties of mutual divisibility _∣∣_
+
+∣∣-sym : Symmetric _∣∣_
+∣∣-sym = swap
+
+∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_
+∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ y≈z x∣y , ∣-respˡ y≈z y∣x
+
+∣∣-respˡ-≈ : _∣∣_ Respectsˡ _≈_
+∣∣-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ x≈z x∣y , ∣-respʳ x≈z y∣x
+
+∣∣-resp-≈ : _∣∣_ Respects₂ _≈_
+∣∣-resp-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -43,3 +43,19 @@ open import Algebra.Properties.Semigroup.Divisibility semigroup public
 ∣-preorder = record
   { isPreorder = ∣-isPreorder
   }
+
+------------------------------------------------------------------------
+-- Properties of mutual divisibiity
+
+∣∣-refl : Reflexive _∣∣_
+∣∣-refl = ∣-refl , ∣-refl
+
+∣∣-reflexive : _≈_ ⇒ _∣∣_
+∣∣-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y)
+
+∣∣-isEquivalence : IsEquivalence _∣∣_
+∣∣-isEquivalence = record
+  { refl  = λ {x} → ∣∣-refl {x}
+  ; sym   = λ {x} {y} → ∣∣-sym {x} {y}
+  ; trans = λ {x} {y} {z} → ∣∣-trans {x} {y} {z}
+  }

src/Algebra/Properties/Semigroup/Divisibility.agda

@@ -21,8 +21,14 @@ open Semigroup S
 open import Algebra.Properties.Magma.Divisibility magma public
 
 ------------------------------------------------------------------------
--- Additional properties
+-- Properties of _∣_
 
 ∣-trans : Transitive _∣_
 ∣-trans (p , px≈y) (q , qy≈z) =
   q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z)
+
+------------------------------------------------------------------------
+-- Properties of _∣∣_
+
+∣∣-trans : Transitive _∣∣_
+∣∣-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x