------------------------------------------------------------------------ -- The Agda standard library -- -- Some theory for commutative semigroup ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Algebra using (CommutativeSemigroup) module Algebra.Properties.CommutativeSemigroup {a } (CS : CommutativeSemigroup a ) where open CommutativeSemigroup CS open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------------ -- Re-export the contents of semigroup open import Algebra.Properties.Semigroup semigroup public ------------------------------------------------------------------------------ -- Permutation laws for _∙_ for three factors. ------------------------------------------------------------------------------ -- Partitions (1,1). -- There are five nontrivial permutations. ------------------------------------------------------------------------------ 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))