From 8693ddcc9283ac4f7d4e4abc11424bd77e050421 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 17:33:01 +0000 Subject: [PATCH 1/4] refactor: put lemma in the right place --- CHANGELOG.md | 5 +++++ src/Algebra/Consequences/Propositional.agda | 11 +---------- src/Algebra/Consequences/Setoid.agda | 10 +++++++++- 3 files changed, 15 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3eb803ac39..b68d6df09c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,10 @@ Bug-fixes * Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`. +* Remove spurious definition of `Algebra.Consequences.Propositional.sel⇒idem`, + which duplicated lemma from `Algebra.Consequences.Base`, instead of importing + from `Algebra.Consequences.Setoid`. + * Fix a typo in `Algebra.Morphism.Construct.DirectProduct`. * Fix a typo in `Function.Construct.Constant`. @@ -122,6 +126,7 @@ Additions to existing modules * In `Algebra.Consequences.Setoid`: ```agda + sel⇒idem : Selective _∙_ → Idempotent _∙_ binomial-expansion : Congruent₂ _∙_ → Associative _∙_ → _◦_ DistributesOver _∙_ → ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) ``` diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index f975cdef5e..36aa343b25 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -41,7 +41,6 @@ open Base public ; comm⇒sym[distribˡ] ; subst∧comm⇒sym ; wlog - ; sel⇒idem ; binomial-expansion -- plus all the deprecated versions of the above ; comm+assoc⇒middleFour @@ -55,7 +54,7 @@ open Base public ; comm+distrʳ⇒distrˡ ; subst+comm⇒sym ) - +test = {!sel⇒idem!} ------------------------------------------------------------------------ -- Group-like structures @@ -111,14 +110,6 @@ module _ {_∙_ _◦_ : Op₂ A} ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) binomial-expansion = Base.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib ------------------------------------------------------------------------- --- Selectivity - -module _ {_∙_ : Op₂ A} where - - sel⇒idem : Selective _∙_ → Idempotent _∙_ - sel⇒idem = Base.sel⇒idem _≡_ - ------------------------------------------------------------------------ -- Middle-Four Exchange diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 4d6bb4dbba..f2fdd9bba2 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -33,7 +33,7 @@ open import Relation.Binary.Reasoning.Setoid S -- Export base lemmas that don't require the setoid open Base public - hiding (module Congruence) + hiding (module Congruence; sel⇒idem) -- Export congruence lemmas using reflexivity @@ -41,6 +41,14 @@ module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where open Base.Congruence _≈_ cong refl public +------------------------------------------------------------------------ +-- Selectivity + +module _ {_∙_ : Op₂ A} where + + sel⇒idem : Selective _∙_ → Idempotent _∙_ + sel⇒idem = Base.sel⇒idem _≈_ + ------------------------------------------------------------------------ -- MiddleFourExchange From 177e788af08c6fc854876008b31ed17b735d8662 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 17:36:32 +0000 Subject: [PATCH 2/4] fix: uncommitted edits --- src/Algebra/Consequences/Propositional.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index 36aa343b25..9236791395 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -54,7 +54,7 @@ open Base public ; comm+distrʳ⇒distrˡ ; subst+comm⇒sym ) -test = {!sel⇒idem!} + ------------------------------------------------------------------------ -- Group-like structures From 91d4151de17757438c12fada057d4827058918b9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 20 Nov 2025 04:18:01 +0000 Subject: [PATCH 3/4] fix: `CHANGELOG` --- CHANGELOG.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b68d6df09c..15c7997247 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,10 +11,6 @@ Bug-fixes * Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`. -* Remove spurious definition of `Algebra.Consequences.Propositional.sel⇒idem`, - which duplicated lemma from `Algebra.Consequences.Base`, instead of importing - from `Algebra.Consequences.Setoid`. - * Fix a typo in `Algebra.Morphism.Construct.DirectProduct`. * Fix a typo in `Function.Construct.Constant`. From a54e0bce84852e82625fc9524e87b792b45712fc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 20 Nov 2025 04:20:39 +0000 Subject: [PATCH 4/4] fix: qualified module name --- src/Algebra/Consequences/Propositional.agda | 30 ++++++++++----------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index 9236791395..6664889796 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -22,12 +22,12 @@ open import Relation.Binary.PropositionalEquality.Properties open import Relation.Unary using (Pred) open import Algebra.Definitions {A = A} _≡_ -import Algebra.Consequences.Setoid (setoid A) as Base +import Algebra.Consequences.Setoid (setoid A) as SetoidConsequences ------------------------------------------------------------------------ -- Re-export all proofs that don't require congruence or substitutivity -open Base public +open SetoidConsequences public hiding ( comm∧assoc⇒middleFour ; identity∧middleFour⇒assoc @@ -63,12 +63,12 @@ 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 = SetoidConsequences.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 = SetoidConsequences.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _) ------------------------------------------------------------------------ -- Ring-like structures @@ -79,13 +79,13 @@ module _ {_+_ _*_ -_ 0#} where RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → LeftZero 0# _*_ assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ = - Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_) + SetoidConsequences.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₂ _*_) + SetoidConsequences.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_) ------------------------------------------------------------------------ -- Bisemigroup-like structures @@ -93,13 +93,13 @@ module _ {_+_ _*_ -_ 0#} where module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_ - comm∧distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm + comm∧distrˡ⇒distrʳ = SetoidConsequences.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm comm∧distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_ - comm∧distrʳ⇒distrˡ = Base.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm + comm∧distrʳ⇒distrˡ = SetoidConsequences.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ˡ] = SetoidConsequences.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm module _ {_∙_ _◦_ : Op₂ A} (∙-assoc : Associative _∙_) @@ -108,7 +108,7 @@ module _ {_∙_ _◦_ : Op₂ A} binomial-expansion : ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) - binomial-expansion = Base.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib + binomial-expansion = SetoidConsequences.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib ------------------------------------------------------------------------ -- Middle-Four Exchange @@ -117,17 +117,17 @@ module _ {_∙_ : Op₂ A} where comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_ - comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_) + comm∧assoc⇒middleFour = SetoidConsequences.comm∧assoc⇒middleFour (cong₂ _∙_) identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_ - identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_) + identity∧middleFour⇒assoc = SetoidConsequences.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 = SetoidConsequences.identity∧middleFour⇒comm (cong₂ _∙_) ------------------------------------------------------------------------ -- Without Loss of Generality @@ -136,13 +136,13 @@ module _ {p} {P : Pred A p} 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 = SetoidConsequences.subst∧comm⇒sym {P = P} subst 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 = SetoidConsequences.wlog {P = P} subst ------------------------------------------------------------------------