------------------------------------------------------------------------
-- The Agda standard library
--
-- Some theory for commutative semigroup
------------------------------------------------------------------------

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

open import Algebra.Bundles using (CommutativeSemigroup)

module Algebra.Properties.CommutativeSemigroup
  {a ℓ} (CS : CommutativeSemigroup a ℓ)
  where

open CommutativeSemigroup CS
open import Algebra.Definitions _≈_
open import Relation.Binary.Reasoning.Setoid setoid
open import Data.Product.Base using (_,_)

------------------------------------------------------------------------
-- Re-export the contents of semigroup

open import Algebra.Properties.Semigroup semigroup public

------------------------------------------------------------------------
-- Properties

interchange : Interchangable _∙_ _∙_
interchange a b c d = begin
  (a ∙ b) ∙ (c ∙ d)  ≈⟨  assoc a b (c ∙ d) ⟩
  a ∙ (b ∙ (c ∙ d))  ≈⟨ ∙-congˡ (assoc b c d) ⟨
  a ∙ ((b ∙ c) ∙ d)  ≈⟨  ∙-congˡ (∙-congʳ (comm b c)) ⟩
  a ∙ ((c ∙ b) ∙ d)  ≈⟨  ∙-congˡ (assoc c b d) ⟩
  a ∙ (c ∙ (b ∙ d))  ≈⟨ assoc a c (b ∙ d) ⟨
  (a ∙ c) ∙ (b ∙ d)  ∎

------------------------------------------------------------------------
-- Permutation laws for _∙_ for three factors.

-- There are five nontrivial permutations.

------------------------------------------------------------------------
-- Partitions (1,1).

x∙yz≈y∙xz :  ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (x ∙ z)
x∙yz≈y∙xz x y z = begin
  x ∙ (y ∙ z)    ≈⟨ sym (assoc x y z) ⟩
  (x ∙ y) ∙ z    ≈⟨ ∙-congʳ (comm x y) ⟩
  (y ∙ x) ∙ z    ≈⟨ assoc y x z ⟩
  y ∙ (x ∙ z)    ∎

x∙yz≈z∙yx :  ∀ x y z → x ∙ (y ∙ z) ≈ z ∙ (y ∙ x)
x∙yz≈z∙yx x y z = begin
  x ∙ (y ∙ z)    ≈⟨ ∙-congˡ (comm y z) ⟩
  x ∙ (z ∙ y)    ≈⟨ x∙yz≈y∙xz x z y ⟩
  z ∙ (x ∙ y)    ≈⟨ ∙-congˡ (comm x y) ⟩
  z ∙ (y ∙ x)    ∎

x∙yz≈x∙zy :  ∀ x y z → x ∙ (y ∙ z) ≈ x ∙ (z ∙ y)
x∙yz≈x∙zy _ y z =  ∙-congˡ (comm y z)

x∙yz≈y∙zx :  ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (z ∙ x)
x∙yz≈y∙zx x y z = begin
  x ∙ (y ∙ z)   ≈⟨ comm x _ ⟩
  (y ∙ z) ∙ x   ≈⟨ assoc y z x ⟩
  y ∙ (z ∙ x)   ∎

x∙yz≈z∙xy :  ∀ x y z → x ∙ (y ∙ z) ≈ z ∙ (x ∙ y)
x∙yz≈z∙xy x y z = begin
  x ∙ (y ∙ z)   ≈⟨ sym (assoc x y z) ⟩
  (x ∙ y) ∙ z   ≈⟨ comm _ z ⟩
  z ∙ (x ∙ y)   ∎

------------------------------------------------------------------------
-- Partitions (1,2).

-- These permutation laws are proved by composing the proofs for
-- partitions (1,1) with  \p → trans p (sym (assoc _ _ _)).

x∙yz≈yx∙z :  ∀ x y z → x ∙ (y ∙ z) ≈ (y ∙ x) ∙ z
x∙yz≈yx∙z x y z =  trans (x∙yz≈y∙xz x y z) (sym (assoc y x z))

x∙yz≈zy∙x :  ∀ x y z → x ∙ (y ∙ z) ≈ (z ∙ y) ∙ x
x∙yz≈zy∙x x y z =  trans (x∙yz≈z∙yx x y z) (sym (assoc z y x))

x∙yz≈xz∙y :  ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ z) ∙ y
x∙yz≈xz∙y x y z =  trans (x∙yz≈x∙zy x y z) (sym (assoc x z y))

x∙yz≈yz∙x :  ∀ x y z → x ∙ (y ∙ z) ≈ (y ∙ z) ∙ x
x∙yz≈yz∙x x y z =  trans (x∙yz≈y∙zx _ _ _) (sym (assoc y z x))

x∙yz≈zx∙y :  ∀ x y z → x ∙ (y ∙ z) ≈ (z ∙ x) ∙ y
x∙yz≈zx∙y x y z =  trans (x∙yz≈z∙xy x y z) (sym (assoc z x y))

------------------------------------------------------------------------
-- Partitions (2,1).

-- Their laws are proved by composing proofs for partitions (1,1) with
-- trans (assoc x y z).

xy∙z≈y∙xz :  ∀ x y z → (x ∙ y) ∙ z ≈ y ∙ (x ∙ z)
xy∙z≈y∙xz x y z =  trans (assoc x y z) (x∙yz≈y∙xz x y z)

xy∙z≈z∙yx :  ∀ x y z → (x ∙ y) ∙ z ≈ z ∙ (y ∙ x)
xy∙z≈z∙yx x y z =  trans (assoc x y z) (x∙yz≈z∙yx x y z)

xy∙z≈x∙zy :  ∀ x y z → (x ∙ y) ∙ z ≈ x ∙ (z ∙ y)
xy∙z≈x∙zy x y z =  trans (assoc x y z) (x∙yz≈x∙zy x y z)

xy∙z≈y∙zx :  ∀ x y z → (x ∙ y) ∙ z ≈ y ∙ (z ∙ x)
xy∙z≈y∙zx x y z =  trans (assoc x y z) (x∙yz≈y∙zx x y z)

xy∙z≈z∙xy :  ∀ x y z → (x ∙ y) ∙ z ≈ z ∙ (x ∙ y)
xy∙z≈z∙xy x y z =  trans (assoc x y z) (x∙yz≈z∙xy x y z)

------------------------------------------------------------------------
-- Partitions (2,2).

-- These proofs are by composing with the proofs for (2,1).

xy∙z≈yx∙z :  ∀ x y z → (x ∙ y) ∙ z ≈ (y ∙ x) ∙ z
xy∙z≈yx∙z x y z =  trans (xy∙z≈y∙xz _ _ _) (sym (assoc y x z))

xy∙z≈zy∙x :  ∀ x y z → (x ∙ y) ∙ z ≈ (z ∙ y) ∙ x
xy∙z≈zy∙x x y z =  trans (xy∙z≈z∙yx x y z) (sym (assoc z y x))

xy∙z≈xz∙y :  ∀ x y z → (x ∙ y) ∙ z ≈ (x ∙ z) ∙ y
xy∙z≈xz∙y x y z =  trans (xy∙z≈x∙zy x y z) (sym (assoc x z y))

xy∙z≈yz∙x :  ∀ x y z → (x ∙ y) ∙ z ≈ (y ∙ z) ∙ x
xy∙z≈yz∙x x y z =  trans (xy∙z≈y∙zx x y z) (sym (assoc y z x))

xy∙z≈zx∙y :  ∀ x y z → (x ∙ y) ∙ z ≈ (z ∙ x) ∙ y
xy∙z≈zx∙y x y z =  trans (xy∙z≈z∙xy x y z) (sym (assoc z x y))

------------------------------------------------------------------------
-- commutative semigroup has Jordan identity

xy∙xx≈x∙yxx : ∀ x y → (x ∙ y) ∙ (x ∙ x) ≈ x ∙ (y ∙ (x ∙ x))
xy∙xx≈x∙yxx x y = assoc x y ((x ∙ x))

------------------------------------------------------------------------
-- commutative semigroup is left/right/middle semiMedial

semimedialˡ : LeftSemimedial _∙_
semimedialˡ x y z = begin
  (x ∙ x) ∙ (y ∙ z) ≈⟨ assoc x x (y ∙ z) ⟩
  x ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (sym (assoc x y z)) ⟩
  x ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
  x ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
  x ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc x y ((x ∙ z))) ⟩
  (x ∙ y) ∙ (x ∙ z) ∎

semimedialʳ : RightSemimedial _∙_
semimedialʳ x y z = begin
  (y ∙ z) ∙ (x ∙ x) ≈⟨ assoc y z (x ∙ x) ⟩
  y ∙ (z ∙ (x ∙ x)) ≈⟨ ∙-congˡ (sym (assoc z x x)) ⟩
  y ∙ ((z ∙ x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (comm z x)) ⟩
  y ∙ ((x ∙ z) ∙ x) ≈⟨ ∙-congˡ (assoc x z x) ⟩
  y ∙ (x ∙ (z ∙ x)) ≈⟨ sym (assoc y x ((z ∙ x))) ⟩
  (y ∙ x) ∙ (z ∙ x) ∎

middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x)
middleSemimedial x y z = begin
  (x ∙ y) ∙ (z ∙ x) ≈⟨ assoc x y ((z ∙ x)) ⟩
  x ∙ (y ∙ (z ∙ x)) ≈⟨ ∙-congˡ (sym (assoc y z x)) ⟩
  x ∙ ((y ∙ z) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (comm y z)) ⟩
  x ∙ ((z ∙ y) ∙ x) ≈⟨ ∙-congˡ ( assoc z y x) ⟩
  x ∙ (z ∙ (y ∙ x)) ≈⟨ sym (assoc x z ((y ∙ x))) ⟩
  (x ∙ z) ∙ (y ∙ x) ∎

semimedial : Semimedial _∙_
semimedial = semimedialˡ , semimedialʳ