------------------------------------------------------------------------ -- The Agda standard library -- -- Relations between properties of functions, such as associativity and -- commutativity, when the underlying relation is a setoid ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total) module Algebra.Consequences.Setoid {a } (S : Setoid a ) where open Setoid S renaming (Carrier to A) open import Algebra.Core open import Algebra.Definitions _≈_ open import Data.Sum.Base using (inj₁; inj₂) open import Data.Product using (_,_) open import Function.Base using (_\$_) import Relation.Binary.Consequences as Bin open import Relation.Binary.Reasoning.Setoid S open import Relation.Unary using (Pred) ------------------------------------------------------------------------ -- Re-exports -- Export base lemmas that don't require the setoid open import Algebra.Consequences.Base public ------------------------------------------------------------------------ -- Magma-like structures module _ {_•_ : Op₂ A} (comm : Commutative _•_) where comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ RightCancellative _•_ comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x \$ begin x y ≈⟨ comm x y y x ≈⟨ eq z x ≈⟨ comm z x x z comm+cancelʳ⇒cancelˡ : RightCancellative _•_ LeftCancellative _•_ comm+cancelʳ⇒cancelˡ cancelʳ x {y} {z} eq = cancelʳ y z \$ begin y x ≈⟨ comm y x x y ≈⟨ eq x z ≈⟨ comm x z z x ------------------------------------------------------------------------ -- Monoid-like structures module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where comm+idˡ⇒idʳ : LeftIdentity e _•_ RightIdentity e _•_ comm+idˡ⇒idʳ idˡ x = begin x e ≈⟨ comm x e e x ≈⟨ idˡ x x comm+idʳ⇒idˡ : RightIdentity e _•_ LeftIdentity e _•_ comm+idʳ⇒idˡ idʳ x = begin e x ≈⟨ comm e x x e ≈⟨ idʳ x x comm+zeˡ⇒zeʳ : LeftZero e _•_ RightZero e _•_ comm+zeˡ⇒zeʳ zeˡ x = begin x e ≈⟨ comm x e e x ≈⟨ zeˡ x e comm+zeʳ⇒zeˡ : RightZero e _•_ LeftZero e _•_ comm+zeʳ⇒zeˡ zeʳ x = begin e x ≈⟨ comm e x x e ≈⟨ zeʳ x e comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ AlmostRightCancellative e _•_ comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} y z x≉e yx≈zx = cancelˡ-nonZero y z x≉e \$ begin x y ≈⟨ comm x y y x ≈⟨ yx≈zx z x ≈⟨ comm z x x z comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ AlmostLeftCancellative e _•_ comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} y z x≉e xy≈xz = cancelʳ-nonZero y z x≉e \$ begin y x ≈⟨ comm y x x y ≈⟨ xy≈xz x z ≈⟨ comm x z z x ------------------------------------------------------------------------ -- Group-like structures module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) where comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _•_ RightInverse e _⁻¹ _•_ comm+invˡ⇒invʳ invˡ x = begin x (x ⁻¹) ≈⟨ comm x (x ⁻¹) (x ⁻¹) x ≈⟨ invˡ x e comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ LeftInverse e _⁻¹ _•_ comm+invʳ⇒invˡ invʳ x = begin (x ⁻¹) x ≈⟨ comm (x ⁻¹) x x (x ⁻¹) ≈⟨ invʳ x e module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where assoc+id+invʳ⇒invˡ-unique : Associative _•_ Identity e _•_ RightInverse e _⁻¹ _•_ x y (x y) e x (y ⁻¹) assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin x ≈⟨ sym (idʳ x) x e ≈⟨ cong refl (sym (invʳ y)) x (y (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) (x y) (y ⁻¹) ≈⟨ cong eq refl e (y ⁻¹) ≈⟨ idˡ (y ⁻¹) y ⁻¹ assoc+id+invˡ⇒invʳ-unique : Associative _•_ Identity e _•_ LeftInverse e _⁻¹ _•_ x y (x y) e y (x ⁻¹) assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin y ≈⟨ sym (idˡ y) e y ≈⟨ cong (sym (invˡ x)) refl ((x ⁻¹) x) y ≈⟨ assoc (x ⁻¹) x y (x ⁻¹) (x y) ≈⟨ cong refl eq (x ⁻¹) e ≈⟨ idʳ (x ⁻¹) x ⁻¹ ---------------------------------------------------------------------- -- Bisemigroup-like structures module _ {_•_ _◦_ : Op₂ A} (◦-cong : Congruent₂ _◦_) (•-comm : Commutative _•_) where comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ _•_ DistributesOverʳ _◦_ comm+distrˡ⇒distrʳ distrˡ x y z = begin (y z) x ≈⟨ •-comm (y z) x x (y z) ≈⟨ distrˡ x y z (x y) (x z) ≈⟨ ◦-cong (•-comm x y) (•-comm x z) (y x) (z x) comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ _•_ DistributesOverˡ _◦_ comm+distrʳ⇒distrˡ distrˡ x y z = begin x (y z) ≈⟨ •-comm x (y z) (y z) x ≈⟨ distrˡ x y z (y x) (z x) ≈⟨ ◦-cong (•-comm y x) (•-comm z x) (x y) (x z) comm⇒sym[distribˡ] : x Symmetric y z (x (y z)) ((x y) (x z))) comm⇒sym[distribˡ] x {y} {z} prf = begin x (z y) ≈⟨ ◦-cong refl (•-comm z y) x (y z) ≈⟨ prf (x y) (x z) ≈⟨ •-comm (x y) (x z) (x z) (x y) ---------------------------------------------------------------------- -- Ring-like structures module _ {_+_ _*_ : Op₂ A} {_⁻¹ : Op₁ A} {0# : A} (+-cong : Congruent₂ _+_) (*-cong : Congruent₂ _*_) where assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ _*_ DistributesOverʳ _+_ RightIdentity 0# _+_ RightInverse 0# _⁻¹ _+_ LeftZero 0# _*_ assoc+distribʳ+idʳ+invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x = begin 0# * x ≈⟨ sym (idʳ _) (0# * x) + 0# ≈⟨ +-cong refl (sym (invʳ _)) (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl (0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ 0# assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ _*_ DistributesOverˡ _+_ RightIdentity 0# _+_ RightInverse 0# _⁻¹ _+_ RightZero 0# _*_ assoc+distribˡ+idʳ+invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x = begin x * 0# ≈⟨ sym (idʳ _) (x * 0#) + 0# ≈⟨ +-cong refl (sym (invʳ _)) (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (sym (distribˡ _ _ _)) refl (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ 0# ------------------------------------------------------------------------ -- Without Loss of Generality module _ {p} {f : Op₂ A} {P : Pred A p} (≈-subst : Substitutive _≈_ p) (comm : Commutative f) where subst+comm⇒sym : Symmetric a b P (f a b)) subst+comm⇒sym = ≈-subst P (comm _ _) wlog : {r} {_R_ : Rel _ r} Total _R_ (∀ a b a R b P (f a b)) a b P (f a b) wlog r-total = Bin.wlog r-total subst+comm⇒sym