From ff6f7770b848d011fb24b2a1ef6d086a06199612 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 11:33:14 +0000 Subject: [PATCH 1/7] refactor: change top-level parameterisation, plus local `variable`s to fix syntax --- src/Algebra/Consequences/Base.agda | 35 +++++++++++++++++++----------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 574ad48a16..780726f3b0 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -1,3 +1,4 @@ + ------------------------------------------------------------------------ -- The Agda standard library -- @@ -7,26 +8,34 @@ {-# OPTIONS --cubical-compatible --safe #-} +open import Relation.Binary.Core using (Rel) + module Algebra.Consequences.Base - {a} {A : Set a} where + {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where -open import Algebra.Core -open import Algebra.Definitions -open import Data.Sum.Base -open import Relation.Binary.Core +open import Algebra.Core using (Op₁; Op₂) +open import Algebra.Definitions _≈_ +open import Data.Sum.Base using (reduce) open import Relation.Binary.Definitions using (Reflexive) -module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where +private + variable + f : Op₁ A + _∙_ : Op₂ A + +------------------------------------------------------------------------ +-- Selective + +sel⇒idem : Selective _∙_ → Idempotent _∙_ +sel⇒idem sel x = reduce (sel x x) - sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_ - sel⇒idem sel x = reduce (sel x x) +------------------------------------------------------------------------ +-- SelfInverse -module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where +reflexive∧selfInverse⇒involutive : Reflexive _≈_ → SelfInverse f → + Involutive f +reflexive∧selfInverse⇒involutive refl inv _ = inv refl - reflexive∧selfInverse⇒involutive : Reflexive _≈_ → - SelfInverse _≈_ f → - Involutive _≈_ f - reflexive∧selfInverse⇒involutive refl inv _ = inv refl ------------------------------------------------------------------------ -- DEPRECATED NAMES From b920bef97c9642477e0ac48d725796242e9c0b31 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 11:34:17 +0000 Subject: [PATCH 2/7] refactor: propagate changes --- src/Algebra/Consequences/Setoid.agda | 125 +++++++++++++-------------- 1 file changed, 62 insertions(+), 63 deletions(-) diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 66e441a9e0..304bd8e004 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -7,10 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.Definitions - using (Substitutive; Symmetric; Total) module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where @@ -21,47 +18,55 @@ open import Data.Sum.Base using (inj₁; inj₂) open import Data.Product.Base using (_,_) open import Function.Base using (_$_; id; _∘_) open import Function.Definitions -import Relation.Binary.Consequences as Bin +import Relation.Binary.Consequences as BinaryConsequences +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions + using (Substitutive; Symmetric; Total) open import Relation.Binary.Reasoning.Setoid S open import Relation.Unary using (Pred) +private + variable + e 0# : A + f _⁻¹ : Op₁ A + _∙_ _◦_ _+_ _*_ : Op₂ A + ------------------------------------------------------------------------ -- Re-exports -- Export base lemmas that don't require the setoid -open import Algebra.Consequences.Base public +open import Algebra.Consequences.Base _≈_ public ------------------------------------------------------------------------ -- MiddleFourExchange -module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where +module _ (cong : Congruent₂ _∙_) where comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_ comm∧assoc⇒middleFour comm assoc w x y z = begin (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩ - w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩ + w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (assoc x y z) ⟨ w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩ w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩ - w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩ + w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨ (w ∙ y) ∙ (x ∙ z) ∎ - identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ → - _∙_ MiddleFourExchange _∙_ → + identity∧middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_ - identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin - (x ∙ y) ∙ z ≈⟨ cong refl (sym (identityˡ z)) ⟩ + identity∧middleFour⇒assoc {e = e} (identityˡ , identityʳ) middleFour x y z + = begin + (x ∙ y) ∙ z ≈⟨ cong refl (identityˡ z) ⟨ (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩ (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩ x ∙ (y ∙ z) ∎ - identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ → - _∙_ MiddleFourExchange _+_ → + identity∧middleFour⇒comm : Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_ - identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y + identity∧middleFour⇒comm {e = e} {_+_ = _+_} (identityˡ , identityʳ) middleFour x y = begin - x ∙ y ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩ + x ∙ y ≈⟨ cong (identityˡ x) (identityʳ y) ⟨ (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩ (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩ y ∙ x ∎ @@ -69,12 +74,12 @@ module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where ------------------------------------------------------------------------ -- SelfInverse -module _ {f : Op₁ A} (self : SelfInverse f) where +module _ (self : SelfInverse f) where selfInverse⇒involutive : Involutive f - selfInverse⇒involutive = reflexive∧selfInverse⇒involutive _≈_ refl self + selfInverse⇒involutive = reflexive∧selfInverse⇒involutive refl self - selfInverse⇒congruent : Congruent _≈_ _≈_ f + selfInverse⇒congruent : Congruent₁ f selfInverse⇒congruent {x} {y} x≈y = sym (self (begin f (f x) ≈⟨ selfInverse⇒involutive x ⟩ x ≈⟨ x≈y ⟩ @@ -98,7 +103,7 @@ module _ {f : Op₁ A} (self : SelfInverse f) where ------------------------------------------------------------------------ -- Magma-like structures -module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where +module _ (comm : Commutative _∙_) where comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_ comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin @@ -117,16 +122,16 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where ------------------------------------------------------------------------ -- Monoid-like structures -module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where +module _ (comm : Commutative _∙_) where comm∧idˡ⇒idʳ : LeftIdentity e _∙_ → RightIdentity e _∙_ - comm∧idˡ⇒idʳ idˡ x = begin + comm∧idˡ⇒idʳ {e = e} 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 + comm∧idʳ⇒idˡ {e = e} idʳ x = begin e ∙ x ≈⟨ comm e x ⟩ x ∙ e ≈⟨ idʳ x ⟩ x ∎ @@ -138,13 +143,13 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where comm∧idʳ⇒id idʳ = comm∧idʳ⇒idˡ idʳ , idʳ comm∧zeˡ⇒zeʳ : LeftZero e _∙_ → RightZero e _∙_ - comm∧zeˡ⇒zeʳ zeˡ x = begin + comm∧zeˡ⇒zeʳ {e = e} 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 + comm∧zeʳ⇒zeˡ {e = e} zeʳ x = begin e ∙ x ≈⟨ comm e x ⟩ x ∙ e ≈⟨ zeʳ x ⟩ e ∎ @@ -157,7 +162,7 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ → AlmostRightCancellative e _∙_ - comm∧almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx = + comm∧almostCancelˡ⇒almostCancelʳ {e = e} cancelˡ-nonZero x y z x≉e yx≈zx = cancelˡ-nonZero x y z x≉e $ begin x ∙ y ≈⟨ comm x y ⟩ y ∙ x ≈⟨ yx≈zx ⟩ @@ -166,7 +171,7 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ → AlmostLeftCancellative e _∙_ - comm∧almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz = + comm∧almostCancelʳ⇒almostCancelˡ {e = e} cancelʳ-nonZero x y z x≉e xy≈xz = cancelʳ-nonZero x y z x≉e $ begin y ∙ x ≈⟨ comm y x ⟩ x ∙ y ≈⟨ xy≈xz ⟩ @@ -176,10 +181,10 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where ------------------------------------------------------------------------ -- Group-like structures -module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) where +module _ (comm : Commutative _∙_) where comm∧invˡ⇒invʳ : LeftInverse e _⁻¹ _∙_ → RightInverse e _⁻¹ _∙_ - comm∧invˡ⇒invʳ invˡ x = begin + comm∧invˡ⇒invʳ {e = e} {_⁻¹ = _⁻¹} invˡ x = begin x ∙ (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩ (x ⁻¹) ∙ x ≈⟨ invˡ x ⟩ e ∎ @@ -188,7 +193,7 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe comm∧invˡ⇒inv invˡ = invˡ , comm∧invˡ⇒invʳ invˡ comm∧invʳ⇒invˡ : RightInverse e _⁻¹ _∙_ → LeftInverse e _⁻¹ _∙_ - comm∧invʳ⇒invˡ invʳ x = begin + comm∧invʳ⇒invˡ {e = e} {_⁻¹ = _⁻¹} invʳ x = begin (x ⁻¹) ∙ x ≈⟨ comm (x ⁻¹) x ⟩ x ∙ (x ⁻¹) ≈⟨ invʳ x ⟩ e ∎ @@ -196,15 +201,15 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe comm∧invʳ⇒inv : RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_ comm∧invʳ⇒inv invʳ = comm∧invʳ⇒invˡ invʳ , invʳ -module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where +module _ (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) ⟩ + assoc∧id∧invʳ⇒invˡ-unique {e = e} {_⁻¹ = _⁻¹} assoc (idˡ , idʳ) invʳ x y eq = begin + x ≈⟨ idʳ x ⟨ x ∙ e ≈⟨ cong refl (sym (invʳ y)) ⟩ - x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩ + x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨ (x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩ e ∙ (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩ y ⁻¹ ∎ @@ -212,9 +217,9 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh 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 ⟩ + assoc∧id∧invˡ⇒invʳ-unique {e = e} {_⁻¹ = _⁻¹} assoc (idˡ , idʳ) invˡ x y eq = begin + y ≈⟨ idˡ y ⟨ + e ∙ y ≈⟨ cong (invˡ x) refl ⟨ ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩ (x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩ (x ⁻¹) ∙ e ≈⟨ idʳ (x ⁻¹) ⟩ @@ -223,10 +228,7 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh ------------------------------------------------------------------------ -- Bisemigroup-like structures -module _ {_∙_ _◦_ : Op₂ A} - (◦-cong : Congruent₂ _◦_) - (∙-comm : Commutative _∙_) - where +module _ (◦-cong : Congruent₂ _◦_) (∙-comm : Commutative _∙_) where comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_ comm∧distrˡ⇒distrʳ distrˡ x y z = begin @@ -256,8 +258,7 @@ module _ {_∙_ _◦_ : Op₂ A} (x ◦ z) ∙ (x ◦ y) ∎ -module _ {_∙_ _◦_ : Op₂ A} - (∙-cong : Congruent₂ _∙_) +module _ (∙-cong : Congruent₂ _∙_) (∙-assoc : Associative _∙_) (◦-comm : Commutative _◦_) where @@ -278,20 +279,17 @@ module _ {_∙_ _◦_ : Op₂ A} ------------------------------------------------------------------------ -- Ring-like structures -module _ {_+_ _*_ : Op₂ A} - {_⁻¹ : Op₁ A} {0# : A} - (+-cong : Congruent₂ _+_) - (*-cong : Congruent₂ _*_) - where +module _ (+-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ʳ _) ⟩ + assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ {0# = 0#} {_⁻¹ = _⁻¹} +-assoc distribʳ idʳ invʳ x + = begin + 0# * x ≈⟨ 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# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨ + ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (distribʳ _ _ _) refl ⟨ ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩ (0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩ 0# ∎ @@ -299,11 +297,12 @@ module _ {_+_ _*_ : Op₂ A} 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ʳ _) ⟩ + assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ {0# = 0#} {_⁻¹ = _⁻¹} +-assoc distribˡ idʳ invʳ x + = begin + x * 0# ≈⟨ 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#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ +-assoc _ _ _ ⟨ + ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (distribˡ _ _ _) refl ⟨ (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩ ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ ⟩ 0# ∎ @@ -311,18 +310,18 @@ module _ {_+_ _*_ : Op₂ A} ------------------------------------------------------------------------ -- Without Loss of Generality -module _ {p} {f : Op₂ A} {P : Pred A p} +module _ {p} {P : Pred A p} (≈-subst : Substitutive _≈_ p) - (comm : Commutative f) + (∙-comm : Commutative _∙_) where - subst∧comm⇒sym : Symmetric (λ a b → P (f a b)) - subst∧comm⇒sym = ≈-subst P (comm _ _) + subst∧comm⇒sym : Symmetric (λ a b → P (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 + (∀ a b → a R b → P (a ∙ b)) → + ∀ a b → P (a ∙ b) + wlog r-total = BinaryConsequences.wlog r-total subst∧comm⇒sym ------------------------------------------------------------------------ From 1e25c10bd5cf98cfb72d0b6c886af7e47201fe02 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 11:37:18 +0000 Subject: [PATCH 3/7] refactor: propagate changes; remove spurious anonymous modules --- src/Algebra/Consequences/Propositional.agda | 104 +++++++++----------- 1 file changed, 47 insertions(+), 57 deletions(-) diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index 29490cbd0c..14451e6e3e 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -20,10 +20,17 @@ open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Relation.Unary using (Pred) -open import Algebra.Core +open import Algebra.Core using (Op₁; Op₂) open import Algebra.Definitions {A = A} _≡_ import Algebra.Consequences.Setoid (setoid A) as Base +private + variable + e ε 0# : A + f _⁻¹ -_ : Op₁ A + _∙_ _◦_ _+_ _*_ : Op₂ A + + ------------------------------------------------------------------------ -- Re-export all proofs that don't require congruence or substitutivity @@ -41,7 +48,6 @@ open Base public ; comm⇒sym[distribˡ] ; subst∧comm⇒sym ; wlog - ; sel⇒idem -- plus all the deprecated versions of the above ; comm+assoc⇒middleFour ; identity+middleFour⇒assoc @@ -58,39 +64,35 @@ open Base public ------------------------------------------------------------------------ -- Group-like structures -module _ {_∙_ _⁻¹ ε} where - - assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ → - RightInverse ε _⁻¹ _∙_ → - ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹) - assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _) +assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ → + RightInverse ε _⁻¹ _∙_ → + ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹) +assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _) - assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ → - LeftInverse ε _⁻¹ _∙_ → - ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹) - assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _) +assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ → + LeftInverse ε _⁻¹ _∙_ → + ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹) +assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _) ------------------------------------------------------------------------ -- Ring-like structures -module _ {_+_ _*_ -_ 0#} where +assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ → + RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → + LeftZero 0# _*_ +assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ {_+_ = _+_} {_*_ = _*_} = + Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_) - assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ → - RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → - LeftZero 0# _*_ - assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ = - Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_) - - assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ → - RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → - RightZero 0# _*_ - assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ = - Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_) +assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ → + RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → + RightZero 0# _*_ +assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ {_+_ = _+_} {_*_ = _*_} = + Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_) ------------------------------------------------------------------------ -- Bisemigroup-like structures -module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where +module _ (∙-comm : Commutative _∙_) where comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_ comm∧distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm @@ -99,49 +101,37 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where comm∧distrʳ⇒distrˡ = Base.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z))) - comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm + comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _) ∙-comm ------------------------------------------------------------------------ --- Selectivity - -module _ {_∙_ : Op₂ A} where - - sel⇒idem : Selective _∙_ → Idempotent _∙_ - sel⇒idem = Base.sel⇒idem _≡_ - ------------------------------------------------------------------------- --- Middle-Four Exchange - -module _ {_∙_ : Op₂ A} where +-- MiddleFourExchange - comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → - _∙_ MiddleFourExchange _∙_ - comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_) +comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → + _∙_ MiddleFourExchange _∙_ +comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _) - identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ → - _∙_ MiddleFourExchange _∙_ → - Associative _∙_ - identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_) +identity∧middleFour⇒assoc : Identity e _∙_ → + _∙_ MiddleFourExchange _∙_ → + Associative _∙_ +identity∧middleFour⇒assoc {_∙_ = _∙_} = Base.identity∧middleFour⇒assoc (cong₂ _∙_) - identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ → - _∙_ MiddleFourExchange _+_ → - Commutative _∙_ - identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _∙_) +identity∧middleFour⇒comm : Identity e _+_ → + _∙_ MiddleFourExchange _+_ → + Commutative _∙_ +identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _) ------------------------------------------------------------------------ -- Without Loss of Generality -module _ {p} {P : Pred A p} where +module _ {p} {P : Pred A p} (∙-comm : Commutative _∙_) where - subst∧comm⇒sym : ∀ {f} (f-comm : Commutative f) → - Symmetric (λ a b → P (f a b)) - subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst + subst∧comm⇒sym : Symmetric (λ a b → P (a ∙ b)) + subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst ∙-comm - wlog : ∀ {f} (f-comm : Commutative f) → - ∀ {r} {_R_ : Rel _ r} → Total _R_ → - (∀ a b → a R b → P (f a b)) → - ∀ a b → P (f a b) - wlog = Base.wlog {P = P} subst + wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ → + (∀ a b → a R b → P (a ∙ b)) → + ∀ a b → P (a ∙ b) + wlog = Base.wlog {P = P} subst ∙-comm ------------------------------------------------------------------------ From 6eab5f223e71e60c599bba3522df7c60287cd5b2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 11:53:17 +0000 Subject: [PATCH 4/7] fix: `CHANGELOG` --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4940047ba8..7556f36d34 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,12 @@ Non-backwards compatible changes Minor improvements ------------------ +* [Issue #2502](https://github.com/agda/agda-stdlib/issues/2502) The top-level + module `Algebra.Consequences.Base` now takes the underlying equality relation + as an additional parameter, with slightly improved ergonomics wrt subsequent + imports; additionally, its internal implicit module parameters capturing the + signature of various algebraic operations, have now been lifted out as `variable`s. + Deprecated modules ------------------ From 2433c3c7ac1154d7644e9cbcd8b1b75f958340e9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 12:04:17 +0000 Subject: [PATCH 5/7] fix: deprecated names from #2206 / #2168 --- src/Data/Rational/Unnormalised/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 181e4a6189..3d7c84554c 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1144,7 +1144,7 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin *-zeroˡ p@record{} = *≡* refl *-zeroʳ : RightZero _≃_ 0ℚᵘ _*_ -*-zeroʳ = Consequences.comm+zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ +*-zeroʳ = Consequences.comm∧zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ *-zero : Zero _≃_ 0ℚᵘ _*_ *-zero = *-zeroˡ , *-zeroʳ @@ -1171,7 +1171,7 @@ invertible⇒≄ {p} {q} (1/p-q , 1/x*x≃1 , x*1/x≃1) p≃q = 0≄1 (begin in *≡* eq where open ℤ-solver *-distribʳ-+ : _DistributesOverʳ_ _≃_ _*_ _+_ -*-distribʳ-+ = Consequences.comm+distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+ +*-distribʳ-+ = Consequences.comm∧distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+ *-distrib-+ : _DistributesOver_ _≃_ _*_ _+_ *-distrib-+ = *-distribˡ-+ , *-distribʳ-+ From d19dac94ae3984c777a1be42598185ea97f313a6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 12:24:10 +0000 Subject: [PATCH 6/7] fix: remove spurious blank line introduced by mistake --- src/Algebra/Consequences/Base.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 780726f3b0..2cedb9a5aa 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -1,4 +1,3 @@ - ------------------------------------------------------------------------ -- The Agda standard library -- From 0f720f873637cf42b0a3f860da6f3604e136b893 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 19 Feb 2025 18:39:06 +0000 Subject: [PATCH 7/7] fix: `CHANGELOG` entry --- CHANGELOG.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fb7b64a703..895cbe789c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,11 +24,10 @@ Non-backwards compatible changes Minor improvements ------------------ -* [Issue #2502](https://github.com/agda/agda-stdlib/issues/2502) The top-level - module `Algebra.Consequences.Base` now takes the underlying equality relation - as an additional parameter, with slightly improved ergonomics wrt subsequent - imports; additionally, its internal implicit module parameters capturing the - signature of various algebraic operations, have now been lifted out as `variable`s. +* [Issue #2502](https://github.com/agda/agda-stdlib/issues/2502) The module + `Algebra.Consequences.Base` now takes the underlying equality relation as + an additional top-level parameter, with slightly improved ergonomics wrt + subsequent imports by clients, as well as streamlined internals. Deprecated modules ------------------