From 12d99dbdbf6b002733d21f550a20469cda8f8a8e Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Sat, 2 Aug 2025 01:00:02 -0400 Subject: [PATCH 1/4] Add back accidentally removed lemmas (Issue2788 #2794)) * opposite of a `Ring` [clean version of pr #1900] (#1910) * punchOut preserves ordering (#1913) * Wellfounded proof for sum relations (#1920) * last revert undone by hand * Remove extra line in CHANGELOG * Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update CHANGELOG.md This was indeed anachronistic from 2.0 Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * resolve issues pointed out by James. * Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * remove now obsolete comment * last mistake in CHANGELOG, hopefully fixed now. --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Co-authored-by: Nathan van Doorn Co-authored-by: Alice Laroche <60161310+Seiryn21@users.noreply.github.com> Co-authored-by: matthewdaggitt --- CHANGELOG.md | 1 + src/Algebra/Construct/Flip/Op.agda | 275 +++++++++++++++++--- src/Data/Fin/Properties.agda | 26 ++ src/Data/Sum/Relation/Binary/LeftOrder.agda | 15 ++ src/Data/Sum/Relation/Binary/Pointwise.agda | 14 + 5 files changed, 288 insertions(+), 43 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ef9533efc6..6593dcc7db 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -65,6 +65,7 @@ Additions to existing modules ``` * In `Data.Fin.Properties`: + ```agda ≡-irrelevant : Irrelevant {A = Fin n} _≡_ ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index dd139e4ba1..9f2ca10c6d 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -9,9 +9,13 @@ module Algebra.Construct.Flip.Op where -open import Algebra -import Data.Product.Base as Product -import Data.Sum.Base as Sum +open import Algebra.Core +open import Algebra.Bundles +import Algebra.Definitions as Def +import Algebra.Structures as Str +import Algebra.Consequences.Setoid as Consequences +import Data.Product as Prod +import Data.Sum as Sum open import Function.Base using (flip) open import Level using (Level) open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_) @@ -33,136 +37,270 @@ preserves₂ : (∼ ≈ ≋ : Rel A ℓ) → ∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋ preserves₂ _ _ _ pres = flip pres -module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where +module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where - associative : Symmetric ≈ → Associative ≈ ∙ → Associative ≈ (flip ∙) + open Def ≈ + + associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙) associative sym assoc x y z = sym (assoc z y x) - identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙) - identity id = Product.swap id + identity : Identity ε ∙ → Identity ε (flip ∙) + identity id = Prod.swap id - commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙) + commutative : Commutative ∙ → Commutative (flip ∙) commutative comm = flip comm - selective : Selective ≈ ∙ → Selective ≈ (flip ∙) + selective : Selective ∙ → Selective (flip ∙) selective sel x y = Sum.swap (sel y x) - idempotent : Idempotent ≈ ∙ → Idempotent ≈ (flip ∙) + idempotent : Idempotent ∙ → Idempotent (flip ∙) idempotent idem = idem - inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙) - inverse inv = Product.swap inv + inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙) + inverse inv = Prod.swap inv + + zero : Zero ε ∙ → Zero ε (flip ∙) + zero zer = Prod.swap zer + +module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where + + open Def ≈ + + distributes : * DistributesOver + → (flip *) DistributesOver + + distributes distrib = Prod.swap distrib ------------------------------------------------------------------------ -- Structures module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where - isMagma : IsMagma ≈ ∙ → IsMagma ≈ (flip ∙) + open Def ≈ + open Str ≈ + open ∙-Properties ≈ ∙ + + isMagma : IsMagma ∙ → IsMagma (flip ∙) isMagma m = record { isEquivalence = isEquivalence ; ∙-cong = preserves₂ ≈ ≈ ≈ ∙-cong } where open IsMagma m - isSelectiveMagma : IsSelectiveMagma ≈ ∙ → IsSelectiveMagma ≈ (flip ∙) + isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙) isSelectiveMagma m = record { isMagma = isMagma m.isMagma - ; sel = selective ≈ ∙ m.sel + ; sel = selective m.sel } where module m = IsSelectiveMagma m - isCommutativeMagma : IsCommutativeMagma ≈ ∙ → IsCommutativeMagma ≈ (flip ∙) + isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙) isCommutativeMagma m = record { isMagma = isMagma m.isMagma - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMagma m - isSemigroup : IsSemigroup ≈ ∙ → IsSemigroup ≈ (flip ∙) + isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙) isSemigroup s = record { isMagma = isMagma s.isMagma - ; assoc = associative ≈ ∙ s.sym s.assoc + ; assoc = associative s.sym s.assoc } where module s = IsSemigroup s - isBand : IsBand ≈ ∙ → IsBand ≈ (flip ∙) + isBand : IsBand ∙ → IsBand (flip ∙) isBand b = record { isSemigroup = isSemigroup b.isSemigroup ; idem = b.idem } where module b = IsBand b - isCommutativeSemigroup : IsCommutativeSemigroup ≈ ∙ → - IsCommutativeSemigroup ≈ (flip ∙) + isCommutativeSemigroup : IsCommutativeSemigroup ∙ → + IsCommutativeSemigroup (flip ∙) isCommutativeSemigroup s = record { isSemigroup = isSemigroup s.isSemigroup - ; comm = commutative ≈ ∙ s.comm + ; comm = commutative s.comm } where module s = IsCommutativeSemigroup s - isUnitalMagma : IsUnitalMagma ≈ ∙ ε → IsUnitalMagma ≈ (flip ∙) ε + isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε isUnitalMagma m = record { isMagma = isMagma m.isMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsUnitalMagma m - isMonoid : IsMonoid ≈ ∙ ε → IsMonoid ≈ (flip ∙) ε + isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε isMonoid m = record { isSemigroup = isSemigroup m.isSemigroup - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsMonoid m - isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε → - IsCommutativeMonoid ≈ (flip ∙) ε + isCommutativeMonoid : IsCommutativeMonoid ∙ ε → + IsCommutativeMonoid (flip ∙) ε isCommutativeMonoid m = record { isMonoid = isMonoid m.isMonoid - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMonoid m - isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ≈ ∙ ε → - IsIdempotentCommutativeMonoid ≈ (flip ∙) ε + isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε → + IsIdempotentCommutativeMonoid (flip ∙) ε isIdempotentCommutativeMonoid m = record { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid - ; idem = idempotent ≈ ∙ m.idem + ; idem = idempotent m.idem } where module m = IsIdempotentCommutativeMonoid m - isInvertibleMagma : IsInvertibleMagma ≈ ∙ ε ⁻¹ → - IsInvertibleMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ → + IsInvertibleMagma (flip ∙) ε ⁻¹ isInvertibleMagma m = record { isMagma = isMagma m.isMagma - ; inverse = inverse ≈ ∙ m.inverse + ; inverse = inverse m.inverse ; ⁻¹-cong = m.⁻¹-cong } where module m = IsInvertibleMagma m - isInvertibleUnitalMagma : IsInvertibleUnitalMagma ≈ ∙ ε ⁻¹ → - IsInvertibleUnitalMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ → + IsInvertibleUnitalMagma (flip ∙) ε ⁻¹ isInvertibleUnitalMagma m = record { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsInvertibleUnitalMagma m - isGroup : IsGroup ≈ ∙ ε ⁻¹ → IsGroup ≈ (flip ∙) ε ⁻¹ + isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹ isGroup g = record { isMonoid = isMonoid g.isMonoid - ; inverse = inverse ≈ ∙ g.inverse + ; inverse = inverse g.inverse ; ⁻¹-cong = g.⁻¹-cong } where module g = IsGroup g - isAbelianGroup : IsAbelianGroup ≈ ∙ ε ⁻¹ → IsAbelianGroup ≈ (flip ∙) ε ⁻¹ + isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹ isAbelianGroup g = record { isGroup = isGroup g.isGroup - ; comm = commutative ≈ ∙ g.comm + ; comm = commutative g.comm } where module g = IsAbelianGroup g +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} {0# 1# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# → + IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1# + isSemiringWithoutAnnihilatingZero r = record + { +-isCommutativeMonoid = r.+-isCommutativeMonoid + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + } + where module r = IsSemiringWithoutAnnihilatingZero r + + isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# + isSemiring r = record + { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero + ; zero = zero r.zero + } + where module r = IsSemiring r + + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → + IsCommutativeSemiring + (flip *) 0# 1# + isCommutativeSemiring r = record + { isSemiring = isSemiring r.isSemiring + ; *-comm = commutative r.*-comm + } + where module r = IsCommutativeSemiring r + + isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# → + IsCancellativeCommutativeSemiring + (flip *) 0# 1# + isCancellativeCommutativeSemiring r = record + { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring + ; *-cancelˡ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ r.setoid r.*-comm r.*-cancelˡ-nonZero + } + where module r = IsCancellativeCommutativeSemiring r + + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → + IsIdempotentSemiring + (flip *) 0# 1# + isIdempotentSemiring r = record + { isSemiring = isSemiring r.isSemiring + ; +-idem = r.+-idem + } + where module r = IsIdempotentSemiring r + + isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# + isQuasiring r = record + { +-isMonoid = r.+-isMonoid + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where module r = IsQuasiring r + +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0# + isRingWithoutOne r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; distrib = distributes r.distrib + } + where module r = IsRingWithoutOne r + +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# → + IsNonAssociativeRing + (flip *) - 0# 1# + isNonAssociativeRing r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where module r = IsNonAssociativeRing r + + isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - + isNearring r = record + { isQuasiring = isQuasiring r.isQuasiring + ; +-inverse = r.+-inverse + ; ⁻¹-cong = r.⁻¹-cong + } + where module r = IsNearring r + + isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1# + isRing r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + } + where module r = IsRing r + + isCommutativeRing : IsCommutativeRing + * - 0# 1# → + IsCommutativeRing + (flip *) - 0# 1# + isCommutativeRing r = record + { isRing = isRing r.isRing + ; *-comm = commutative r.*-comm + } + where module r = IsCommutativeRing r + + ------------------------------------------------------------------------ -- Bundles @@ -239,3 +377,54 @@ group g = record { isGroup = isGroup g.isGroup } abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup } where module g = AbelianGroup g + +semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → + SemiringWithoutAnnihilatingZero a ℓ +semiringWithoutAnnihilatingZero r = record + { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero } + where module r = SemiringWithoutAnnihilatingZero r + +semiring : Semiring a ℓ → Semiring a ℓ +semiring r = record { isSemiring = isSemiring r.isSemiring } + where module r = Semiring r + +commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ +commutativeSemiring r = record + { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring } + where module r = CommutativeSemiring r + +cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ → + CancellativeCommutativeSemiring a ℓ +cancellativeCommutativeSemiring r = record + { isCancellativeCommutativeSemiring = isCancellativeCommutativeSemiring r.isCancellativeCommutativeSemiring } + where module r = CancellativeCommutativeSemiring r + +idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ +idempotentSemiring r = record + { isIdempotentSemiring = isIdempotentSemiring r.isIdempotentSemiring } + where module r = IdempotentSemiring r + +quasiring : Quasiring a ℓ → Quasiring a ℓ +quasiring r = record { isQuasiring = isQuasiring r.isQuasiring } + where module r = Quasiring r + +ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ +ringWithoutOne r = record { isRingWithoutOne = isRingWithoutOne r.isRingWithoutOne } + where module r = RingWithoutOne r + +nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ +nonAssociativeRing r = record + { isNonAssociativeRing = isNonAssociativeRing r.isNonAssociativeRing } + where module r = NonAssociativeRing r + +nearring : Nearring a ℓ → Nearring a ℓ +nearring r = record { isNearring = isNearring r.isNearring } + where module r = Nearring r + +ring : Ring a ℓ → Ring a ℓ +ring r = record { isRing = isRing r.isRing } + where module r = Ring r + +commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ +commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing } + where module r = CommutativeRing r diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index f78b652a85..48bcf8a5ee 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -884,6 +884,16 @@ punchIn-injective (suc i) (suc j) (suc k) ↑j+1≡↑k+1 = punchInᵢ≢i : ∀ i (j : Fin n) → punchIn i j ≢ i punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective +punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k +punchIn-mono-≤ zero _ _ j≤k = s≤s j≤k +punchIn-mono-≤ (suc _) zero _ z≤n = z≤n +punchIn-mono-≤ (suc i) (suc j) (suc k) (s≤s j≤k) = s≤s (punchIn-mono-≤ i j k j≤k) + +punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k +punchIn-cancel-≤ zero _ _ (s≤s j≤k) = j≤k +punchIn-cancel-≤ (suc _) zero _ z≤n = z≤n +punchIn-cancel-≤ (suc i) (suc j) (suc k) (s≤s ↑j≤↑k) = s≤s (punchIn-cancel-≤ i j k ↑j≤↑k) + ------------------------------------------------------------------------ -- punchOut ------------------------------------------------------------------------ @@ -918,6 +928,22 @@ punchOut-injective {suc n} {suc i} {zero} {zero} _ _ _ = refl punchOut-injective {suc n} {suc i} {suc j} {suc k} i≢j i≢k pⱼ≡pₖ = cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ)) +punchOut-mono-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → + j ≤ k → punchOut i≢j ≤ punchOut i≢k +punchOut-mono-≤ {_ } {zero } {zero } {_ } 0≢0 _ z≤n = contradiction refl 0≢0 +punchOut-mono-≤ {_ } {zero } {suc _} {suc _} _ _ (s≤s j≤k) = j≤k +punchOut-mono-≤ {suc _} {suc _} {zero } {_ } _ _ z≤n = z≤n +punchOut-mono-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s j≤k) = s≤s (punchOut-mono-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) j≤k) + +punchOut-cancel-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → + punchOut i≢j ≤ punchOut i≢k → j ≤ k +punchOut-cancel-≤ {_ } {zero } {zero } {_ } 0≢0 _ _ = contradiction refl 0≢0 +punchOut-cancel-≤ {_ } {zero } {suc _} {zero } _ 0≢0 _ = contradiction refl 0≢0 +punchOut-cancel-≤ {suc _} {zero } {suc _} {suc _} _ _ pⱼ≤pₖ = s≤s pⱼ≤pₖ +punchOut-cancel-≤ {_ } {suc _} {zero } {_ } _ _ _ = z≤n +punchOut-cancel-≤ {suc _} {suc _} {suc _} {zero } _ _ () +punchOut-cancel-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s pⱼ≤pₖ) = s≤s (punchOut-cancel-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) pⱼ≤pₖ) + punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) → punchIn i (punchOut i≢j) ≡ j punchIn-punchOut {_} {zero} {zero} 0≢0 = contradiction refl 0≢0 diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda index ba80960eb1..f162dd56dc 100644 --- a/src/Data/Sum/Relation/Binary/LeftOrder.agda +++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda @@ -14,6 +14,7 @@ open import Data.Sum.Relation.Binary.Pointwise as PW open import Data.Product.Base using (_,_) open import Data.Empty using (⊥) open import Function.Base using (_$_; _∘_) +open import Induction.WellFounded open import Level using (Level; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Nullary.Decidable.Core using (yes; no) @@ -89,6 +90,20 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ() ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = Dec.map′ ₂∼₂ drop-inj₂ (dec₂ x y) + ⊎-<-wellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (∼₁ ⊎-< ∼₂) + ⊎-<-wellFounded wf₁ wf₂ x = acc (⊎-<-acc x) + where + ⊎-<-acc₁ : ∀ {x} → Acc ∼₁ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₁ x) + ⊎-<-acc₁ (acc rec) (₁∼₁ x∼₁y) = acc (⊎-<-acc₁ (rec x∼₁y)) + + ⊎-<-acc₂ : ∀ {x} → Acc ∼₂ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₂ x) + ⊎-<-acc₂ (acc rec) {inj₁ x} ₁∼₂ = acc (⊎-<-acc₁ (wf₁ x)) + ⊎-<-acc₂ (acc rec) (₂∼₂ x∼₂y) = acc (⊎-<-acc₂ (rec x∼₂y)) + + ⊎-<-acc : ∀ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) x + ⊎-<-acc (inj₁ x) = ⊎-<-acc₁ (wf₁ x) + ⊎-<-acc (inj₂ x) = ⊎-<-acc₂ (wf₂ x) + module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂} {ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄} diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index a52c37f876..6e65ba9691 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -10,6 +10,7 @@ module Data.Sum.Relation.Binary.Pointwise where open import Data.Product.Base using (_,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) +open import Induction.WellFounded open import Level using (Level; _⊔_) open import Function.Base using (const; _∘_; id) open import Function.Bundles using (Inverse; mk↔) @@ -93,6 +94,19 @@ drop-inj₂ (inj₂ x) = x ⊎-irreflexive irrefl₁ irrefl₂ (inj₁ x) (inj₁ y) = irrefl₁ x y ⊎-irreflexive irrefl₁ irrefl₂ (inj₂ x) (inj₂ y) = irrefl₂ x y +⊎-wellFounded : WellFounded ≈₁ → WellFounded ≈₂ → WellFounded (Pointwise ≈₁ ≈₂) +⊎-wellFounded {≈₁ = ≈₁} {≈₂ = ≈₂} wf₁ wf₂ x = acc (⊎-acc x) + where + ⊎-acc₁ : ∀ {x} → Acc ≈₁ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) (inj₁ x) + ⊎-acc₁ (acc rec) (inj₁ x≈₁y) = acc (⊎-acc₁ (rec x≈₁y)) + + ⊎-acc₂ : ∀ {x} → Acc ≈₂ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) (inj₂ x) + ⊎-acc₂ (acc rec) (inj₂ x≈₂y) = acc (⊎-acc₂ (rec x≈₂y)) + + ⊎-acc : ∀ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) x + ⊎-acc (inj₁ x) = ⊎-acc₁ (wf₁ x) + ⊎-acc (inj₂ x) = ⊎-acc₂ (wf₂ x) + ⊎-antisymmetric : Antisymmetric ≈₁ R → Antisymmetric ≈₂ S → Antisymmetric (Pointwise ≈₁ ≈₂) (Pointwise R S) ⊎-antisymmetric antisym₁ antisym₂ (inj₁ x) (inj₁ y) = inj₁ (antisym₁ x y) From e825a086b28393aa98832a3ba9de1c05a2c06133 Mon Sep 17 00:00:00 2001 From: matthewdaggitt Date: Sat, 2 Aug 2025 14:10:29 +0800 Subject: [PATCH 2/4] Bring v2.3 release changes accross --- CHANGELOG/v2.3.md | 615 ++++++++++++++++++++++++++++++++++++++ CITATION.cff | 4 +- README.md | 2 - doc/installation-guide.md | 12 +- 4 files changed, 623 insertions(+), 10 deletions(-) create mode 100644 CHANGELOG/v2.3.md diff --git a/CHANGELOG/v2.3.md b/CHANGELOG/v2.3.md new file mode 100644 index 0000000000..5d03548df1 --- /dev/null +++ b/CHANGELOG/v2.3.md @@ -0,0 +1,615 @@ +Version 2.3 +=========== + +The library has been tested using Agda 2.7.0 and 2.8.0. + +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. + +* The implementation of `≤-total` in `Data.Nat.Properties` used to use recursion + making it infeasibly slow for even relatively small natural numbers. It's definition + has been altered to use operations backed by primitives making it + significantly faster. However, its reduction behaviour on open terms may have + changed in some limited circumstances. + +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.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.Bool.ListAction` - a new location for the lifted specialised list operations `Data.List.Base.{and|or|any|all}`. + +* `Data.Nat.ListAction(.Properties)` - a new location for the definitions and properties of `Data.List.Base.{sum|product}`. + +* `Data.List.Relation.Binary.Prefix.Propositional.Properties`. + +* `Data.List.Relation.Binary.Suffix.Propositional.Properties`. + +* `Data.List.Sort.InsertionSort(.{Base|Properties})` - defines insertion sort and proves properties of insertion sort. + +* `Data.List.Sort.MergeSort(.{Base|Properties})` - a refactor of the previous `Data.List.Sort.MergeSort`. + +* `Data.Sign.Show` - code for converting a sign to a string. + +* `Relation.Binary.Morphism.Construct.Product` - plumbing in the (categorical) product structure on `RawSetoid`. + +* `Relation.Binary.Properties.PartialSetoid` - systematise properties of the partial equivalence relation bundled with a set. + +* `Relation.Nullary.Recomputable.Core` + +* `Relation.Nullary.Irrelevant` - moved the concept `Irrelevant` of irrelevance (h-proposition) + from `Relation.Nullary` to its own dedicated module . + +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.Initial`: + ```agda + assoc : Associative _≈_ _∙_ + idem : Idempotent _≈_ _∙_ + ``` + +* 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 + ``` + +* Added new functions and proofs to `Algebra.Construct.Flip.Op`: + ```agda + zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) + distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# → + IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1# + isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → + IsCommutativeSemiring + (flip *) 0# 1# + isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# → + IsCancellativeCommutativeSemiring + (flip *) 0# 1# + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → + IsIdempotentSemiring + (flip *) 0# 1# + isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# + isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0# + isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# → + IsNonAssociativeRing + (flip *) - 0# 1# + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - + isCommutativeRing : IsCommutativeRing + * - 0# 1# → + IsCommutativeRing + (flip *) - 0# 1# + semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → + SemiringWithoutAnnihilatingZero a ℓ + commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ + cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ → + CancellativeCommutativeSemiring a ℓ + idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ + quasiring : Quasiring a ℓ → Quasiring a ℓ + ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ + nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ + nearring : Nearring a ℓ → Nearring a ℓ + ring : Ring a ℓ → Ring a ℓ + commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ + ``` + +* In `Algebra.Properties.Magma.Divisibility`: + ```agda + ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ + ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_ + ∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_ + x∣ˡxy : x ∣ˡ x ∙ y + xy≈z⇒x∣ˡz : x ∙ y ≈ z → x ∣ˡ z + ``` + +* In `Algebra.Properties.Monoid.Divisibility`: + ```agda + ε∣ˡ_ : ε ∣ˡ x + ∣ˡ-refl : Reflexive _∣ˡ_ + ∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_ + ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_ + ∣ˡ-preorder : Preorder a ℓ _ + ``` + +* In `Algebra.Properties.Monoid`: + ```agda + ε-unique : (∀ b → b ∙ a ≈ b) → a ≈ ε + ε-comm : a ∙ ε ≈ ε ∙ a + elimʳ : a ≈ ε → b ∙ a ≈ b + elimˡ : a ≈ ε → a ∙ b ≈ b + introʳ : a ≈ ε → b ≈ b ∙ a + introˡ : a ≈ ε → b ≈ a ∙ b + introᶜ : a ≈ ε → b ∙ c ≈ b ∙ (a ∙ c) + cancelʳ : a ∙ c ≈ ε → (b ∙ a) ∙ c ≈ b + cancelˡ : a ∙ c ≈ ε → a ∙ (c ∙ b) ≈ b + insertˡ : a ∙ c ≈ ε → b ≈ a ∙ (c ∙ b) + insertʳ : a ∙ c ≈ ε → b ≈ (b ∙ a) ∙ c + cancelᶜ : a ∙ c ≈ ε → (b ∙ a) ∙ (c ∙ d) ≈ b ∙ d + insertᶜ : a ∙ c ≈ ε ∙ d ≈ (b ∙ a) ∙ (c ∙ d) + ``` + +* In `Algebra.Properties.Semigroup`: + ```agda + uv≈w⇒xu∙v≈xw : x → (x ∙ u) ∙ v ≈ x ∙ w + uv≈w⇒u∙vx≈wx : u ∙ (v ∙ x) ≈ w ∙ x + uv≈w⇒u[vx∙y]≈w∙xy : u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y) + uv≈w⇒x[uv∙y]≈x∙wy : x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y) + uv≈w⇒[x∙yu]v≈x∙yw : (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w) + uv≈w⇒[xu∙v]y≈x∙wy : ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y) + uv≈w⇒[xy∙u]v≈x∙yw : ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w) + uv≈w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y) + uv≈w⇒xy≈z⇒u[vx∙y]≈wz : 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 ∙ u) ∙ v ≈ (y ∙ w) ∙ x + uv≈wx⇒u∙vy≈w∙xy : u ∙ (v ∙ y) ≈ w ∙ (x ∙ y) + uv≈wx⇒yu∙vz≈yw∙xz : (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 : if b then x else x ≡ x + if-idem-then : (if b then (if b then x else y) else y) ≡ (if b then x else y) + if-idem-else : (if b then x else (if b then x else y)) ≡ (if b then x else y) + if-swap-then : (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 : (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y)) + if-not : (if not b then x else y) ≡ (if b then y else x) + if-∧ : (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y) + if-∨ : (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y)) + if-xor : (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 : x ≡ z → (if b then x else y) ≡ (if b then z else y) + if-cong-else : y ≡ z → (if b then x else y) ≡ (if b then x else z) + if-cong₂ : 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 + punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k + punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k + punchOut-mono-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → j ≤ k → punchOut i≢j ≤ punchOut i≢k + punchOut-cancel-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≤ punchOut i≢k → j ≤ k + 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 Date: Sat, 2 Aug 2025 14:13:01 +0800 Subject: [PATCH 3/4] Fix typo --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6593dcc7db..ef9533efc6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -65,7 +65,6 @@ Additions to existing modules ``` * In `Data.Fin.Properties`: - ```agda ≡-irrelevant : Irrelevant {A = Fin n} _≡_ ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq From 40c6bab07d2b1035ae34b301a85859f44de4012c Mon Sep 17 00:00:00 2001 From: matthewdaggitt Date: Sat, 2 Aug 2025 14:15:57 +0800 Subject: [PATCH 4/4] Fix whitespace --- src/Data/Sum/Relation/Binary/Pointwise.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 6e65ba9691..f0d0e7c39f 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -102,7 +102,7 @@ drop-inj₂ (inj₂ x) = x ⊎-acc₂ : ∀ {x} → Acc ≈₂ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) (inj₂ x) ⊎-acc₂ (acc rec) (inj₂ x≈₂y) = acc (⊎-acc₂ (rec x≈₂y)) - + ⊎-acc : ∀ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) x ⊎-acc (inj₁ x) = ⊎-acc₁ (wf₁ x) ⊎-acc (inj₂ x) = ⊎-acc₂ (wf₂ x)