[ fix ] in non-commutative settings distinguish _∣ˡ_ and _∣ʳ_

CHANGELOG.md

@@ -58,18 +58,29 @@ Deprecated names
   ∤∤-respˡ-≈    ↦  ∦-respˡ-≈
   ∤∤-respʳ-≈    ↦  ∦-respʳ-≈
   ∤∤-resp-≈     ↦  ∦-resp-≈
+  ∣-respʳ-≈    ↦ ∣ʳ-respʳ-≈
+  ∣-respˡ-≈    ↦ ∣ʳ-respˡ-≈
+  ∣-resp-≈     ↦ ∣ʳ-resp-≈
+  x∣yx         ↦ x∣ʳyx
+  xy≈z⇒y∣z     ↦ xy≈z⇒y∣ʳz
   ```
 
 * In `Algebra.Properties.Monoid.Divisibility`:
   ```agda
   ∣∣-refl            ↦  ∥-refl
   ∣∣-reflexive       ↦  ∥-reflexive
   ∣∣-isEquivalence   ↦  ∥-isEquivalence
+  ε∣_                ↦ ε∣ʳ_
+  ∣-refl             ↦ ∣ʳ-refl
+  ∣-reflexive        ↦ ∣ʳ-reflexive
+  ∣-isPreorder       ↦ ∣ʳ-isPreorder
+  ∣-preorder         ↦ ∣ʳ-preorder
   ```
 
 * In `Algebra.Properties.Semigroup.Divisibility`:
   ```agda
   ∣∣-trans   ↦  ∥-trans
+  ∣-trans    ↦  ∣ʳ-trans
   ```
 
 * In `Data.List.Base`:
@@ -103,6 +114,10 @@ New modules
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
 
+* `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid.
+
+* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
+
 * `Data.Sign.Show` to show a sign
 
 Additions to existing modules
@@ -137,6 +152,38 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Properties.Magma.Divisibility`:
+  ```agda
+  ∣ˡ-respʳ-≈  : _∣ˡ_ Respectsʳ _≈_
+  ∣ˡ-respˡ-≈  : _∣ˡ_ Respectsˡ _≈_
+  ∣ˡ-resp-≈   : _∣ˡ_ Respects₂ _≈_
+  x∣ˡxy       : ∀ x y → x ∣ˡ x ∙ y
+  xy≈z⇒x∣ˡz   : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
+  ```
+
+* In `Algebra.Properties.Monoid.Divisibility`:
+  ```agda
+  ε∣ˡ_          : ∀ x → ε ∣ˡ x
+  ∣ˡ-refl       : Reflexive _∣ˡ_
+  ∣ˡ-reflexive  : _≈_ ⇒ _∣ˡ_
+  ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_
+  ∣ˡ-preorder   : Preorder a ℓ _
+  ```
+
+* In `Algebra.Properties.Semigroup.Divisibility`:
+  ```agda
+  ∣ˡ-trans     : Transitive _∣ˡ_
+  x∣ʳy⇒x∣ʳzy   : x ∣ʳ y → x ∣ʳ z ∙ y
+  x∣ʳy⇒xz∣ʳyz  : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z
+  x∣ˡy⇒zx∣ˡzy  : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y
+  x∣ˡy⇒x∣ˡyz   : x ∣ˡ y → x ∣ˡ y ∙ z
+  ```
+
+* In `Algebra.Properties.CommutativeSemigroup.Divisibility`:
+  ```agda
+  ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -20,6 +20,13 @@ open CommutativeMagma CM using (magma; _≈_; _∙_; comm)
 -- Re-export the contents of magmas
 
 open import Algebra.Properties.Magma.Divisibility magma public
+  using (_∣_; _,_)
+  renaming ( ∣ʳ-respʳ-≈  to ∣-respʳ-≈
+           ; ∣ʳ-respˡ-≈  to ∣-respˡ-≈
+           ; ∣ʳ-resp-≈   to ∣-resp-≈
+           ; x∣ʳyx       to x∣yx
+           ; xy≈z⇒y∣ʳz   to xy≈z⇒y∣z
+           )
 
 ------------------------------------------------------------------------
 -- Further properties
@@ -36,7 +43,6 @@ x|xy∧y|xy x y = x∣xy x y , x∣yx y x
 xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
 xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
 
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

@@ -15,7 +15,8 @@ module Algebra.Properties.CommutativeSemigroup.Divisibility
   where
 
 open CommutativeSemigroup CS
-open import Algebra.Properties.CommutativeSemigroup CS using (x∙yz≈xz∙y; x∙yz≈y∙xz)
+open import Algebra.Properties.CommutativeSemigroup CS
+  using (interchange; x∙yz≈xz∙y; x∙yz≈y∙xz)
 open ≈-Reasoning setoid
 
 ------------------------------------------------------------------------
@@ -39,6 +40,12 @@ x∣y∧z∣x/y⇒xz∣y {x} {y} {z} (x/y , x/y∙x≈y) (p , pz≈x/y) = p , (b
   x/y ∙ x      ≈⟨ x/y∙x≈y ⟩
   y            ∎)
 
+∙-cong-∣ : ∀ {x y a b} → x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
+∙-cong-∣ {x} {y} {a} {b} (p , px≈y) (q , qa≈b) = p ∙ q , (begin
+  (p ∙ q) ∙ (x ∙ a) ≈⟨ interchange p q x a ⟩
+  (p ∙ x) ∙ (q ∙ a) ≈⟨ ∙-cong px≈y qa≈b ⟩
+  y ∙ b ∎)
+
 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 ⟩

src/Algebra/Properties/Magma/Divisibility.agda

@@ -24,31 +24,49 @@ open import Algebra.Definitions.RawMagma rawMagma public
   using (_∣_; _∤_; _∥_; _∦_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_)
 
 ------------------------------------------------------------------------
--- Properties of divisibility
+-- Properties of right divisibility
 
-∣-respʳ-≈ : _∣_ Respectsʳ _≈_
-∣-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z
+∣ʳ-respʳ-≈ : _∣ʳ_ Respectsʳ _≈_
+∣ʳ-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z
 
-∣-respˡ-≈ : _∣_ Respectsˡ _≈_
-∣-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y
+∣ʳ-respˡ-≈ : _∣ʳ_ Respectsˡ _≈_
+∣ʳ-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y
 
-∣-resp-≈ : _∣_ Respects₂ _≈_
-∣-resp-≈ = ∣-respʳ-≈ , ∣-respˡ-≈
+∣ʳ-resp-≈ : _∣ʳ_ Respects₂ _≈_
+∣ʳ-resp-≈ = ∣ʳ-respʳ-≈ , ∣ʳ-respˡ-≈
 
-x∣yx : ∀ x y → x ∣ y ∙ x
-x∣yx x y = y , refl
+x∣ʳyx : ∀ x y → x ∣ʳ y ∙ x
+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 = x , xy≈z
+xy≈z⇒y∣ʳz : ∀ x y {z} → x ∙ y ≈ z → y ∣ʳ z
+xy≈z⇒y∣ʳz x y xy≈z = x , xy≈z
+
+------------------------------------------------------------------------
+-- Properties of left divisibility
+
+∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_
+∣ˡ-respʳ-≈ y≈z (q , xq≈y) = q , trans xq≈y y≈z
+
+∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_
+∣ˡ-respˡ-≈ x≈z (q , xq≈y) = q , trans (∙-congʳ (sym x≈z)) xq≈y
+
+∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_
+∣ˡ-resp-≈ = ∣ˡ-respʳ-≈ , ∣ˡ-respˡ-≈
+
+x∣ˡxy : ∀ x y → x ∣ˡ x ∙ y
+x∣ˡxy x y = y , refl
+
+xy≈z⇒x∣ˡz : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
+xy≈z⇒x∣ˡz x y xy≈z = y , xy≈z
 
 ------------------------------------------------------------------------
 -- Properties of non-divisibility
 
 ∤-respˡ-≈ : _∤_ Respectsˡ _≈_
-∤-respˡ-≈ x≈y x∤z y∣z = contradiction (∣-respˡ-≈ (sym x≈y) y∣z) x∤z
+∤-respˡ-≈ x≈y x∤z y∣ʳz = contradiction (∣ʳ-respˡ-≈ (sym x≈y) y∣ʳz) x∤z
 
 ∤-respʳ-≈ : _∤_ Respectsʳ _≈_
-∤-respʳ-≈ x≈y z∤x z∣y = contradiction (∣-respʳ-≈ (sym x≈y) z∣y) z∤x
+∤-respʳ-≈ x≈y z∤x z∣ʳy = contradiction (∣ʳ-respʳ-≈ (sym x≈y) z∣ʳy) z∤x
 
 ∤-resp-≈ : _∤_ Respects₂ _≈_
 ∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈
@@ -60,10 +78,10 @@ xy≈z⇒y∣z x y xy≈z = x , xy≈z
 ∥-sym = swap
 
 ∥-respˡ-≈ : _∥_ Respectsˡ _≈_
-∥-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x
+∥-respˡ-≈ x≈z (x∣ʳy , y∣ʳx) = ∣ʳ-respˡ-≈ x≈z x∣ʳy , ∣ʳ-respʳ-≈ x≈z y∣ʳx
 
 ∥-respʳ-≈ : _∥_ Respectsʳ _≈_
-∥-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x
+∥-respʳ-≈ y≈z (x∣ʳy , y∣ʳx) = ∣ʳ-respʳ-≈ y≈z x∣ʳy , ∣ʳ-respˡ-≈ y≈z y∣ʳx
 
 ∥-resp-≈ : _∥_ Respects₂ _≈_
 ∥-resp-≈ = ∥-respʳ-≈ , ∥-respˡ-≈
@@ -92,20 +110,20 @@ xy≈z⇒y∣z x y xy≈z = x , xy≈z
 
 -- Version 2.2
 
-∣-respˡ = ∣-respˡ-≈
+∣-respˡ = ∣ʳ-respˡ-≈
 {-# WARNING_ON_USAGE ∣-respˡ
 "Warning: ∣-respˡ was deprecated in v2.2.
-Please use ∣-respˡ-≈ instead. "
+Please use ∣ʳ-respˡ-≈ instead. "
 #-}
-∣-respʳ = ∣-respʳ-≈
+∣-respʳ = ∣ʳ-respʳ-≈
 {-# WARNING_ON_USAGE ∣-respʳ
 "Warning: ∣-respʳ was deprecated in v2.2.
-Please use ∣-respʳ-≈ instead. "
+Please use ∣ʳ-respʳ-≈ instead. "
 #-}
-∣-resp = ∣-resp-≈
+∣-resp = ∣ʳ-resp-≈
 {-# WARNING_ON_USAGE ∣-resp
 "Warning: ∣-resp was deprecated in v2.2.
-Please use ∣-resp-≈ instead. "
+Please use ∣ʳ-resp-≈ instead. "
 #-}
 
 -- Version 2.3
@@ -150,3 +168,33 @@ Please use ∦-respʳ-≈ instead. "
 "Warning: ∤∤-resp-≈ was deprecated in v2.3.
 Please use ∦-resp-≈ instead. "
 #-}
+
+∣-respʳ-≈ = ∣ʳ-respʳ-≈
+{-# WARNING_ON_USAGE ∣-respʳ-≈
+"Warning: ∣-respʳ-≈ was deprecated in v2.3.
+Please use ∣ʳ-respʳ-≈ instead. "
+#-}
+
+∣-respˡ-≈ = ∣ʳ-respˡ-≈
+{-# WARNING_ON_USAGE ∣-respˡ-≈
+"Warning: ∣-respˡ-≈ was deprecated in v2.3.
+Please use ∣ʳ-respˡ-≈ instead. "
+#-}
+
+∣-resp-≈ = ∣ʳ-resp-≈
+{-# WARNING_ON_USAGE ∣-resp-≈
+"Warning: ∣-resp-≈ was deprecated in v2.3.
+Please use ∣ʳ-resp-≈ instead. "
+#-}
+
+x∣yx = x∣ʳyx
+{-# WARNING_ON_USAGE x∣yx
+"Warning: x∣yx was deprecated in v2.3.
+Please use x∣ʳyx instead. "
+#-}
+
+xy≈z⇒y∣z = xy≈z⇒y∣ʳz
+{-# WARNING_ON_USAGE xy≈z⇒y∣z
+"Warning: xy≈z⇒y∣z was deprecated in v2.3.
+Please use xy≈z⇒y∣ʳz instead. "
+#-}

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -25,39 +25,65 @@ open Monoid M
 open import Algebra.Properties.Semigroup.Divisibility semigroup public
 
 ------------------------------------------------------------------------
--- Additional properties
+-- Additional properties for right divisibility
 
-infix 4 ε∣_
+infix 4 ε∣ʳ_
+
+ε∣ʳ_ : ∀ x → ε ∣ʳ x
+ε∣ʳ x = x , identityʳ x
+
+∣ʳ-refl : Reflexive _∣ʳ_
+∣ʳ-refl {x} = ε , identityˡ x
+
+∣ʳ-reflexive : _≈_ ⇒ _∣ʳ_
+∣ʳ-reflexive x≈y = ε , trans (identityˡ _) x≈y
+
+∣ʳ-isPreorder : IsPreorder _≈_ _∣ʳ_
+∣ʳ-isPreorder = record
+  { isEquivalence = isEquivalence
+  ; reflexive     = ∣ʳ-reflexive
+  ; trans         = ∣ʳ-trans
+  }
+
+∣ʳ-preorder : Preorder a ℓ _
+∣ʳ-preorder = record
+  { isPreorder = ∣ʳ-isPreorder
+  }
+
+------------------------------------------------------------------------
+-- Additional properties for left divisibility
+
+infix 4 ε∣ˡ_
 
-ε∣_ : ∀ x → ε ∣ x
-ε∣ x = x , identityʳ x
+ε∣ˡ_ : ∀ x → ε ∣ˡ x
+ε∣ˡ x = x , identityˡ x
 
-∣-refl : Reflexive _∣_
-∣-refl {x} = ε , identityˡ x
+∣ˡ-refl : Reflexive _∣ˡ_
+∣ˡ-refl {x} = ε , identityʳ x
 
-∣-reflexive : _≈_ ⇒ _∣_
-∣-reflexive x≈y = ε , trans (identityˡ _) x≈y
+∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_
+∣ˡ-reflexive x≈y = ε , trans (identityʳ _) x≈y
 
-∣-isPreorder : IsPreorder _≈_ _∣_
-∣-isPreorder = record
+∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_
+∣ˡ-isPreorder = record
   { isEquivalence = isEquivalence
-  ; reflexive     = ∣-reflexive
-  ; trans         = ∣-trans
+  ; reflexive     = ∣ˡ-reflexive
+  ; trans         = ∣ˡ-trans
   }
 
-∣-preorder : Preorder a ℓ _
-∣-preorder = record
-  { isPreorder = ∣-isPreorder
+∣ˡ-preorder : Preorder a ℓ _
+∣ˡ-preorder = record
+  { isPreorder = ∣ˡ-isPreorder
   }
 
 ------------------------------------------------------------------------
 -- Properties of mutual divisibiity
 
 ∥-refl : Reflexive _∥_
-∥-refl = ∣-refl , ∣-refl
+∥-refl = ∣ʳ-refl , ∣ʳ-refl
 
 ∥-reflexive : _≈_ ⇒ _∥_
-∥-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y)
+∥-reflexive x≈y = ∣ʳ-reflexive x≈y , ∣ʳ-reflexive (sym x≈y)
 
 ∥-isEquivalence : IsEquivalence _∥_
 ∥-isEquivalence = record
@@ -92,3 +118,34 @@ Please use ∥-reflexive instead. "
 "Warning: ∣∣-isEquivalence was deprecated in v2.3.
 Please use ∥-isEquivalence instead. "
 #-}
+
+infix 4 ε∣_
+ε∣_ = ε∣ʳ_
+{-# WARNING_ON_USAGE ε∣_
+"Warning: ε∣_ was deprecated in v2.3.
+Please use ε∣ʳ_ instead. "
+#-}
+
+∣-refl = ∣ʳ-refl
+{-# WARNING_ON_USAGE ∣-refl
+"Warning: ∣-refl was deprecated in v2.3.
+Please use ∣ʳ-refl instead. "
+#-}
+
+∣-reflexive = ∣ʳ-reflexive
+{-# WARNING_ON_USAGE ∣-reflexive
+"Warning: ∣-reflexive was deprecated in v2.3.
+Please use ∣ʳ-reflexive instead. "
+#-}
+
+∣-isPreorder = ∣ʳ-isPreorder
+{-# WARNING_ON_USAGE ∣ʳ-isPreorder
+"Warning: ∣-isPreorder was deprecated in v2.3.
+Please use ∣ʳ-isPreorder instead. "
+#-}
+
+∣-preorder = ∣ʳ-preorder
+{-# WARNING_ON_USAGE ∣-preorder
+"Warning: ∣-preorder was deprecated in v2.3.
+Please use ∣ʳ-preorder instead. "
+#-}