------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of divisibility over semigroups
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles using (Semigroup)

module Algebra.Properties.Semigroup.Divisibility
  {a ℓ} (S : Semigroup a ℓ) where

open import Data.Product.Base using (_,_)
open import Relation.Binary.Definitions using (Transitive)

open Semigroup S

------------------------------------------------------------------------
-- Re-export magma divisibility

open import Algebra.Properties.Magma.Divisibility magma public

------------------------------------------------------------------------
-- Properties of _∣ʳ_

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


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.3

∣∣-trans = ∥-trans
{-# WARNING_ON_USAGE ∣∣-trans
"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. "
#-}