------------------------------------------------------------------------ -- 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
Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.