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

CHANGELOG.md

@@ -54,18 +54,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`:
@@ -131,6 +142,32 @@ 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⇒xz∣ʳyz  : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z
+  x∣ˡy⇒zx∣ˡzy  : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y
+  ```
+
+
 * In `Data.List.Properties`:
   ```agda
   map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
@@ -143,3 +180,15 @@ Additions to existing modules
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
+
+* In `Data.List.Relation.Binary.Prefix.Homogeneous.Properties`:
+  ```agda
+  Prefix-as-∣ˡ : Prefix _≡_ ⇒ _∣ˡ_
+  ∣ˡ-as-Prefix : _∣ˡ_ ⇒ Prefix _≡_
+  ```
+
+* In `Data.List.Relation.Binary.Suffix.Homogeneous.Properties`:
+  ```agda
+  Suffix-as-∣ʳ : Suffix _≡_ ⇒ _∣ʳ_
+  ∣ʳ-as-Suffix : _∣ʳ_ ⇒ Suffix _≡_
+  ```

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -28,7 +28,7 @@ x∣xy : ∀ x y → x ∣ x ∙ y
 x∣xy x y = y , comm y x
 
 xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z
-xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y)
+xy≈z⇒x∣z x y xy≈z = ∣ʳ-respʳ-≈ xy≈z (x∣xy x y)
 
 x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
 x|xy∧y|xy x y = x∣xy x y , x∣yx y 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 = ∣-respʳ-≈ xy≈z (x∣yx y x)
+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 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 = ∣ˡ-respʳ-≈ xy≈z (x∣ˡxy x y)
 
 ------------------------------------------------------------------------
 -- 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 = ∣-respʳ-≈ xy≈z (x∣yx y x)
 ∥-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 = ∣-respʳ-≈ xy≈z (x∣yx y x)
 
 -- 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. "
+#-}

src/Algebra/Properties/Semigroup/Divisibility.agda

@@ -22,17 +22,30 @@ open Semigroup S
 open import Algebra.Properties.Magma.Divisibility magma public
 
 ------------------------------------------------------------------------
--- Properties of _∣_
+-- Properties of _∣ʳ_
 
-∣-trans : Transitive _∣_
-∣-trans (p , px≈y) (q , qy≈z) =
+x∣ʳy⇒xz∣ʳyz : ∀ {x y} z → x ∣ʳ y → x ∙ z ∣ʳ y ∙ z
+x∣ʳy⇒xz∣ʳyz z (p , px≈y) = p , trans (sym (assoc p _ z)) (∙-congʳ px≈y)
+
+∣ʳ-trans : Transitive _∣ʳ_
+∣ʳ-trans (p , px≈y) (q , qy≈z) =
   q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z)
 
+------------------------------------------------------------------------
+-- Properties of _∣ˡ__
+
+x∣ˡy⇒zx∣ˡzy : ∀ {x y} z → x ∣ˡ y → z ∙ x ∣ˡ z ∙ y
+x∣ˡy⇒zx∣ˡzy z (p , xp≈y) = p , trans (assoc z _ p) (∙-congˡ xp≈y)
+
+∣ˡ-trans : Transitive _∣ˡ_
+∣ˡ-trans (p , xp≈y) (q , yq≈z) =
+  p ∙ q , trans (sym (assoc _ p q)) (trans (∙-congʳ xp≈y) yq≈z)
+
 ------------------------------------------------------------------------
 -- Properties of _∥_
 
 ∥-trans : Transitive _∥_
-∥-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x
+∥-trans (x∣y , y∣x) (y∣z , z∣y) = ∣ʳ-trans x∣y y∣z , ∣ʳ-trans z∣y y∣x
 
 
 ------------------------------------------------------------------------
@@ -48,3 +61,9 @@ open import Algebra.Properties.Magma.Divisibility magma public
 "Warning: ∣∣-trans was deprecated in v2.3.
 Please use ∥-trans instead. "
 #-}
+
+∣-trans = ∣ʳ-trans
+{-# WARNING_ON_USAGE ∣-trans
+"Warning: ∣-trans was deprecated in v2.3.
+Please use ∣ʳ-trans instead. "
+#-}