{-# OPTIONS --without-K --safe #-}
open import Algebra 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 Algebra.Properties.Semigroup semigroup public
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) ∎
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) ∎
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))
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)
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))