From b382c18b7257ea6b2728704a7042abef4341131e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 11 Jul 2025 17:02:07 +0100 Subject: [PATCH 1/2] [ DRY ] redefine `Algebra.Definitions.Medial` in terms of `Interchangable`, plus knock-ons --- CHANGELOG.md | 5 ++++ src/Algebra/Definitions.agda | 2 +- .../Properties/CommutativeSemigroup.agda | 23 +++++++++++++++---- .../CommutativeSemigroup/Divisibility.agda | 16 ++++++------- .../IdempotentCommutativeMonoid.agda | 8 +++---- .../Solver/CommutativeMonoid/Normal.agda | 6 ++--- 6 files changed, 40 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4b10f1a54e..5add0e49e0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -80,6 +80,11 @@ Deprecated names uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ ``` +* In `Algebra.Properties.CommutativeSemigroup`: + ```agda + interchange ↦ medial + ``` + * In `Algebra.Properties.Magma.Divisibility`: ```agda ∣∣-sym ↦ ∥-sym 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 ∷ ρ) ∎ ------------------------------------------------------------------------ From cdb9b9005594d532918831b30f0a65284fd62e5a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Jul 2025 20:32:36 +0100 Subject: [PATCH 2/2] reset: `CHANGELOG` for v2.4 --- CHANGELOG.md | 530 +-------------------------------------------------- 1 file changed, 2 insertions(+), 528 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5add0e49e0..0fc6c935f3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.3-dev +Version 2.4-dev =============== -The library has been tested using Agda 2.7.0 and 2.7.0.1. +The library has been tested using Agda 2.8.0. Highlights ---------- @@ -9,551 +9,25 @@ Highlights Bug-fixes --------- -* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` - to `#-sym` in order to avoid overloaded projection. - `irrefl` and `cotrans` are similarly renamed for the sake of consistency. - -* In `Algebra.Definitions.RawMagma` and `Relation.Binary.Construct.Interior.Symmetric`, - the record constructors `_,_` incorrectly had no declared fixity. They have been given - the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`. - -* In `Data.Product.Function.Dependent.Setoid`, `left-inverse` defined a - `RightInverse`. - This has been deprecated in favor or `rightInverse`, and a corrected (and - correctly-named) function `leftInverse` has been added. - -* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` - has been modified to correctly support equational reasoning at the beginning and the end. - The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors - of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps - are changed, this modification is non-backwards compatible. - Non-backwards compatible changes -------------------------------- -* The implementation of `≤-total` in `Data.Nat.Properties` has been altered - to use operations backed by primitives, rather than recursion, making it - significantly faster. However, its reduction behaviour on open terms may have - changed. - Minor improvements ------------------ -* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary` - to its own dedicated module `Relation.Nullary.Irrelevant`. - Deprecated modules ------------------ Deprecated names ---------------- -* In `Algebra.Definitions.RawMagma`: - ```agda - _∣∣_ ↦ _∥_ - _∤∤_ ↦ _∦_ - ``` - -* In `Algebra.Lattice.Properties.BooleanAlgebra` - ```agda - ⊥≉⊤ ↦ ¬⊥≈⊤ - ⊤≉⊥ ↦ ¬⊤≈⊥ - ``` - -* In `Algebra.Module.Consequences` - ```agda - *ₗ-assoc+comm⇒*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ᵣ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - *ᵣ-assoc+comm⇒*ₗ-assoc ↦ *ᵣ-assoc∧comm⇒*ₗ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - ``` - -* In `Algebra.Modules.Structures.IsLeftModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ - ``` - -* In `Algebra.Modules.Structures.IsRightModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ - ``` - * In `Algebra.Properties.CommutativeSemigroup`: ```agda interchange ↦ medial ``` -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣∣-sym ↦ ∥-sym - ∣∣-respˡ-≈ ↦ ∥-respˡ-≈ - ∣∣-respʳ-≈ ↦ ∥-respʳ-≈ - ∣∣-resp-≈ ↦ ∥-resp-≈ - ∤∤-sym -≈ ↦ ∦-sym - ∤∤-respˡ-≈ ↦ ∦-respˡ-≈ - ∤∤-respʳ-≈ ↦ ∦-respʳ-≈ - ∤∤-resp-≈ ↦ ∦-resp-≈ - ∣-respʳ-≈ ↦ ∣ʳ-respʳ-≈ - ∣-respˡ-≈ ↦ ∣ʳ-respˡ-≈ - ∣-resp-≈ ↦ ∣ʳ-resp-≈ - x∣yx ↦ x∣ʳyx - xy≈z⇒y∣z ↦ xy≈z⇒y∣ʳz - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ∣∣-refl ↦ ∥-refl - ∣∣-reflexive ↦ ∥-reflexive - ∣∣-isEquivalence ↦ ∥-isEquivalence - ε∣_ ↦ ε∣ʳ_ - ∣-refl ↦ ∣ʳ-refl - ∣-reflexive ↦ ∣ʳ-reflexive - ∣-isPreorder ↦ ∣ʳ-isPreorder - ∣-preorder ↦ ∣ʳ-preorder - ``` - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣∣-trans ↦ ∥-trans - ∣-trans ↦ ∣ʳ-trans - ``` - -* In `Algebra.Structures.Group`: - ```agda - uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique - uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique - ``` - -* In `Data.List.Base`: - ```agda - and ↦ Data.Bool.ListAction.and - or ↦ Data.Bool.ListAction.or - any ↦ Data.Bool.ListAction.any - all ↦ Data.Bool.ListAction.all - sum ↦ Data.Nat.ListAction.sum - product ↦ Data.Nat.ListAction.product - ``` - -* In `Data.List.Properties`: - ```agda - sum-++ ↦ Data.Nat.ListAction.Properties.sum-++ - ∈⇒∣product ↦ Data.Nat.ListAction.Properties.∈⇒∣product - product≢0 ↦ Data.Nat.ListAction.Properties.product≢0 - ∈⇒≤product ↦ Data.Nat.ListAction.Properties.∈⇒≤product - ∷-ʳ++-eqFree ↦ Data.List.Properties.ʳ++-ʳ++-eqFree - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - sum-↭ ↦ Data.Nat.ListAction.Properties.sum-↭ - product-↭ ↦ Data.Nat.ListAction.Properties.product-↭ - ``` - -* In `Data.Product.Function.Dependent.Setoid`: - ```agda - left-inverse ↦ rightInverse - ``` - -* In `Data.Product.Nary.NonDependent`: - ```agda - Allₙ ↦ Pointwiseₙ - ``` - New modules ----------- -* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`. - -* `Algebra.Morphism.Construct.DirectProduct`. - -* `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. - -* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. - -* `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid. - -* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid. - -* `Data.List.Sort.InsertionSort.{agda|Base|Properties}` defines insertion sort and proves properties of insertion sort such as Sorted and Permutation properties. - -* `Data.List.Sort.MergenSort.{agda|Base|Properties}` is a refactor of the previous `Data.List.Sort.MergenSort`. - -* `Data.Sign.Show` to show a sign. - -* `Relation.Binary.Morphism.Construct.Product` to plumb in the (categorical) product structure on `RawSetoid`. - -* `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER - -* `Relation.Nullary.Recomputable.Core` - Additions to existing modules ----------------------------- - -* In `Algebra.Consequences.Base`: - ```agda - module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) - where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ - ``` - -* In `Algebra.Consequences.Setoid`: - ```agda - module Congruence (cong : Congruent₂ _≈_ _∙_) where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ - ``` - -* In `Algebra.Construct.Pointwise`: - ```agda - isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → - IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# → - IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# → - IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# → - IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#) - isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# → - IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# → - IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#) - commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ) - nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ) - semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ) - idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ) - kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ) - quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ) - commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) - ``` - -* In `Algebra.Modules.Properties`: - ```agda - inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y - inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ - ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_ - ∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_ - x∣ˡxy : ∀ x y → x ∣ˡ x ∙ y - xy≈z⇒x∣ˡz : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ε∣ˡ_ : ∀ x → ε ∣ˡ x - ∣ˡ-refl : Reflexive _∣ˡ_ - ∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_ - ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_ - ∣ˡ-preorder : Preorder a ℓ _ - ``` - -* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups - -``` - uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w - uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x - uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y) - uv≈w⇒x[uv∙y]≈x∙wy : ∀ x y → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y) - uv≈w⇒[x∙yu]v≈x∙yw : ∀ x y → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒[xu∙v]y≈x∙wy : ∀ x y → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y) - uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y) - uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z - uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y)) - [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x) - [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x) - [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x) - uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x - uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y) - uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z) -``` - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣ˡ-trans : Transitive _∣ˡ_ - x∣ʳy⇒x∣ʳzy : x ∣ʳ y → x ∣ʳ z ∙ y - x∣ʳy⇒xz∣ʳyz : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z - x∣ˡy⇒zx∣ˡzy : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y - x∣ˡy⇒x∣ˡyz : x ∣ˡ y → x ∣ˡ y ∙ z - ``` - -* In `Algebra.Properties.CommutativeSemigroup.Divisibility`: - ```agda - ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b - ``` - -* In `Data.Bool.Properties`: - ```agda - if-eta : ∀ b → (if b then x else x) ≡ x - if-idem-then : ∀ b → (if b then (if b then x else y) else y) ≡ (if b then x else y) - if-idem-else : ∀ b → (if b then x else (if b then x else y)) ≡ (if b then x else y) - if-swap-then : ∀ b c → (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y) - if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y)) - if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x) - if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y) - if-∨ : ∀ b → (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y)) - if-xor : ∀ b → (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y)) - if-cong : b ≡ c → (if b then x else y) ≡ (if c then x else y) - if-cong-then : ∀ b → x ≡ z → (if b then x else y) ≡ (if b then z else y) - if-cong-else : ∀ b → y ≡ z → (if b then x else y) ≡ (if b then x else z) - if-cong₂ : ∀ b → x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w) - ``` - -* In `Data.Fin.Base`: - ```agda - _≰_ : Rel (Fin n) 0ℓ - _≮_ : Rel (Fin n) 0ℓ - lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n - ``` - -* In `Data.Fin.Permutation`: - ```agda - cast-id : .(m ≡ n) → Permutation m n - swap : Permutation m n → Permutation (2+ m) (2+ n) - ``` - -* In `Data.Fin.Properties`: - ```agda - cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k - inject!-injective : Injective _≡_ _≡_ inject! - inject!-< : (k : Fin′ i) → inject! k < i - lower-injective : lower i i