diff --git a/CHANGELOG.md b/CHANGELOG.md index 3cf9a9ac90..0fc6c935f3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,11 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Properties.CommutativeSemigroup`: + ```agda + interchange ↦ medial + ``` + New modules ----------- diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index eb64aa8e76..e42958da4d 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -212,7 +212,7 @@ Flexible : Op₂ A → Set _ Flexible _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ (x ∙ (y ∙ x)) Medial : Op₂ A → Set _ -Medial _∙_ = ∀ x y u z → ((x ∙ y) ∙ (u ∙ z)) ≈ ((x ∙ u) ∙ (y ∙ z)) +Medial _∙_ = Interchangable _∙_ _∙_ LeftSemimedial : Op₂ A → Set _ LeftSemimedial _∙_ = ∀ x y z → ((x ∙ x) ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ (x ∙ z)) diff --git a/src/Algebra/Properties/CommutativeSemigroup.agda b/src/Algebra/Properties/CommutativeSemigroup.agda index 3f5f7721e1..966e993343 100644 --- a/src/Algebra/Properties/CommutativeSemigroup.agda +++ b/src/Algebra/Properties/CommutativeSemigroup.agda @@ -9,10 +9,10 @@ open import Algebra.Bundles using (CommutativeSemigroup) module Algebra.Properties.CommutativeSemigroup - {a ℓ} (CS : CommutativeSemigroup a ℓ) + {a ℓ} (commutativeSemigroup : CommutativeSemigroup a ℓ) where -open CommutativeSemigroup CS +open CommutativeSemigroup commutativeSemigroup open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid open import Data.Product.Base using (_,_) @@ -25,8 +25,8 @@ open import Algebra.Properties.Semigroup semigroup public ------------------------------------------------------------------------ -- Properties -interchange : Interchangable _∙_ _∙_ -interchange a b c d = begin +medial : Medial _∙_ +medial a b c d = begin (a ∙ b) ∙ (c ∙ d) ≈⟨ assoc a b (c ∙ d) ⟩ a ∙ (b ∙ (c ∙ d)) ≈⟨ ∙-congˡ (assoc b c d) ⟨ a ∙ ((b ∙ c) ∙ d) ≈⟨ ∙-congˡ (∙-congʳ (comm b c)) ⟩ @@ -171,3 +171,18 @@ middleSemimedial x y z = begin semimedial : Semimedial _∙_ semimedial = semimedialˡ , semimedialʳ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +interchange = medial +{-# WARNING_ON_USAGE interchange +"Warning: interchange was deprecated in v2.3. +Please use medial instead." +#-} diff --git a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda b/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda index 26ff00f8d2..4d049d495b 100644 --- a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda +++ b/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda @@ -7,17 +7,17 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra using (CommutativeSemigroup) -open import Data.Product.Base using (_,_) -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning module Algebra.Properties.CommutativeSemigroup.Divisibility - {a ℓ} (CS : CommutativeSemigroup a ℓ) + {a ℓ} (commutativeSemigroup : CommutativeSemigroup a ℓ) where -open CommutativeSemigroup CS -open import Algebra.Properties.CommutativeSemigroup CS - using (interchange; x∙yz≈xz∙y; x∙yz≈y∙xz) -open ≈-Reasoning setoid +open import Data.Product.Base using (_,_) + +open CommutativeSemigroup commutativeSemigroup +open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup + using (medial; x∙yz≈xz∙y; x∙yz≈y∙xz) +open import Relation.Binary.Reasoning.Setoid setoid ------------------------------------------------------------------------ -- Re-export the contents of divisibility over semigroups @@ -42,7 +42,7 @@ x∣y∧z∣x/y⇒xz∣y {x} {y} {z} (x/y , x/y∙x≈y) (p , pz≈x/y) = p , (b ∙-cong-∣ : ∀ {x y a b} → x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b ∙-cong-∣ {x} {y} {a} {b} (p , px≈y) (q , qa≈b) = p ∙ q , (begin - (p ∙ q) ∙ (x ∙ a) ≈⟨ interchange p q x a ⟩ + (p ∙ q) ∙ (x ∙ a) ≈⟨ medial p q x a ⟩ (p ∙ x) ∙ (q ∙ a) ≈⟨ ∙-cong px≈y qa≈b ⟩ y ∙ b ∎) diff --git a/src/Algebra/Properties/IdempotentCommutativeMonoid.agda b/src/Algebra/Properties/IdempotentCommutativeMonoid.agda index c5fde763fe..4306e7818c 100644 --- a/src/Algebra/Properties/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Properties/IdempotentCommutativeMonoid.agda @@ -9,16 +9,16 @@ open import Algebra.Bundles using (IdempotentCommutativeMonoid) module Algebra.Properties.IdempotentCommutativeMonoid - {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where + {c ℓ} (idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ) where -open IdempotentCommutativeMonoid M +open IdempotentCommutativeMonoid idempotentCommutativeMonoid open import Algebra.Consequences.Setoid setoid using (comm∧distrˡ⇒distrʳ; comm∧distrˡ⇒distr) open import Algebra.Definitions _≈_ using (_DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_) open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup - using (interchange) + using (medial) open import Relation.Binary.Reasoning.Setoid setoid @@ -28,7 +28,7 @@ open import Relation.Binary.Reasoning.Setoid setoid ∙-distrˡ-∙ : _∙_ DistributesOverˡ _∙_ ∙-distrˡ-∙ a b c = begin a ∙ (b ∙ c) ≈⟨ ∙-congʳ (idem a) ⟨ - (a ∙ a) ∙ (b ∙ c) ≈⟨ interchange _ _ _ _ ⟩ + (a ∙ a) ∙ (b ∙ c) ≈⟨ medial _ _ _ _ ⟩ (a ∙ b) ∙ (a ∙ c) ∎ ∙-distrʳ-∙ : _∙_ DistributesOverʳ _∙_ diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index ff12a6080f..7713e497e1 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -13,7 +13,7 @@ open import Algebra.Bundles using (CommutativeMonoid) module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where import Algebra.Properties.CommutativeSemigroup as CSProperties - using (interchange) + using (medial) import Algebra.Properties.Monoid.Mult as MultProperties using (_×_; ×-homo-1; ×-homo-+) open import Data.Fin.Base using (Fin; zero; suc) @@ -27,7 +27,7 @@ import Relation.Nullary.Decidable as Dec using (map) open CommutativeMonoid M open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+) -open CSProperties commutativeSemigroup using (interchange) +open CSProperties commutativeSemigroup using (medial) open ≈-Reasoning setoid private @@ -117,7 +117,7 @@ comp-correct [] [] _ = sym (identityˡ _) comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = begin ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ ≈⟨ ∙-congʳ (×-homo-+ a l m) ⟩ (l × a) ∙ (m × a) ∙ ⟦ v • w ⟧⇓ ρ ≈⟨ ∙-congˡ (comp-correct v w ρ) ⟩ - (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ interchange _ _ _ _ ⟩ + (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ medial _ _ _ _ ⟩ ⟦ l ∷ v ⟧⇓ (a ∷ ρ) ∙ ⟦ m ∷ w ⟧⇓ (a ∷ ρ) ∎ ------------------------------------------------------------------------