[ fix ] in non-commutative settings distinguish _∣ˡ_ and _∣ʳ_ (agda#2604)

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

* [ new ] Prefix & Suffix as Left & Right division

* [ fix ] my cockup

* [ new ] ∙-cong-∣

* [ cleanup ] in the commutative case we don't care about the direction

* [ refactor ] Moving propositional results in their own module

* [ fix ] forgot the OPTIONS

* [ cleanup ] According to agda#2631

---------

Co-authored-by: jamesmckinna <[email protected]>

Author: gallais

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. "
+#-}

src/Algebra/Properties/Semigroup/Divisibility.agda

@@ -22,17 +22,36 @@ 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⇒x∣ʳzy : ∀ {x y} z → x ∣ʳ y → x ∣ʳ z ∙ y
+x∣ʳy⇒x∣ʳzy z (p , px≈y) = z ∙ p , trans (assoc z p _) (∙-congˡ px≈y)
+
+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⇒x∣ˡyz : ∀ {x y} z → x ∣ˡ y → x ∣ˡ y ∙ z
+x∣ˡy⇒x∣ˡyz z (p , xp≈y) = p ∙ z , trans (sym (assoc _ p z)) (∙-congʳ xp≈y)
+
+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 +67,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. "
+#-}

src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda

@@ -18,6 +18,7 @@ open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
 open import Data.List.Relation.Binary.Prefix.Heterogeneous
 open import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties
 
+
 private
   variable
     a b r s : Level

src/Data/List/Relation/Binary/Prefix/Propositional/Properties.agda

@@ -0,0 +1,34 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the propositional prefix relation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Binary.Prefix.Propositional.Properties {a} {A : Set a} where
+
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Properties using (++-monoid)
+
+open import Data.List.Relation.Binary.Prefix.Heterogeneous
+  using (Prefix; []; _∷_; fromView; _++_)
+open import Data.List.Relation.Binary.Prefix.Homogeneous.Properties
+import Data.List.Relation.Binary.Pointwise as Pointwise
+
+open import Algebra.Properties.Monoid.Divisibility (++-monoid A)
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary using (_⇒_)
+
+------------------------------------------------------------------------
+-- The inductive definition of the propositional Prefix relation is
+-- equivalent to the notion of left divisibility induced by the
+-- (List A, _++_, []) monoid
+
+Prefix-as-∣ˡ : Prefix _≡_ ⇒ _∣ˡ_
+Prefix-as-∣ˡ []          = ε∣ˡ _
+Prefix-as-∣ˡ (refl ∷ tl) = x∣ˡy⇒zx∣ˡzy (_ ∷ []) (Prefix-as-∣ˡ tl)
+
+∣ˡ-as-Prefix : _∣ˡ_ ⇒ Prefix _≡_
+∣ˡ-as-Prefix (rest , refl) = fromView (Pointwise.refl refl ++ rest)