From 16c1fba69261dab462ed1f5f2d936048e4945712 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Mon, 20 Feb 2023 09:57:36 +0000 Subject: [PATCH 01/14] opposite of a `Ring` [clean version of pr #1900] (#1910) --- CHANGELOG.md | 36 ++++ src/Algebra/Construct/Flip/Op.agda | 275 ++++++++++++++++++++++++----- 2 files changed, 268 insertions(+), 43 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b9dce3e816..7d2cff097f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -231,7 +231,43 @@ Additions to existing modules 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ˡ _≈_ 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 From 35b39c462c9711b332af1b528839fa948d1b4256 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 20 Feb 2023 10:55:41 +0100 Subject: [PATCH 02/14] punchOut preserves ordering (#1913) --- CHANGELOG.md | 62 ++++++++++++++++++++++++++++++++++++ src/Data/Fin/Properties.agda | 26 +++++++++++++++ 2 files changed, 88 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7d2cff097f..1f757d9a9c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -391,6 +391,68 @@ Additions to existing modules ``` * In `Data.Fin.Properties`: + the proof that an injection from a type `A` into `Fin n` induces a + decision procedure for `_≡_` on `A` has been generalized to other + equivalences over `A` (i.e. to arbitrary setoids), and renamed from + `eq?` to the more descriptive `inj⇒≟` and `inj⇒decSetoid`. + +* Added new proofs in `Data.Fin.Properties`: + ``` + 1↔⊤ : Fin 1 ↔ ⊤ + + 0≢1+n : zero ≢ suc i + + ↑ˡ-injective : i ↑ˡ n ≡ j ↑ˡ n → i ≡ j + ↑ʳ-injective : n ↑ʳ i ≡ n ↑ʳ j → i ≡ j + finTofun-funToFin : funToFin ∘ finToFun ≗ id + funTofin-funToFun : finToFun (funToFin f) ≗ f + ^↔→ : Extensionality _ _ → Fin (m ^ n) ↔ (Fin n → Fin m) + + toℕ-mono-< : i < j → toℕ i ℕ.< toℕ j + toℕ-mono-≤ : i ≤ j → toℕ i ℕ.≤ toℕ j + toℕ-cancel-≤ : toℕ i ℕ.≤ toℕ j → i ≤ j + toℕ-cancel-< : toℕ i ℕ.< toℕ j → i < j + + toℕ-combine : toℕ (combine i j) ≡ k ℕ.* toℕ i ℕ.+ toℕ j + combine-injectiveˡ : combine i j ≡ combine k l → i ≡ k + combine-injectiveʳ : combine i j ≡ combine k l → j ≡ l + combine-injective : combine i j ≡ combine k l → i ≡ k × j ≡ l + combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i + combine-monoˡ-< : i < j → combine i k < combine j l + + ℕ-ℕ≡toℕ‿ℕ- : n ℕ-ℕ i ≡ toℕ (n ℕ- i) + + 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 + + lower₁-injective : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j + pinch-injective : suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k + + i<1+i : i < suc i + + injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective f → m ℕ.≤ n + <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective f) + ℕ→Fin-notInjective : ∀ (f : ℕ → Fin n) → ¬ (Injective f) + cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} → Injective f → Injective g → m ≡ n + + cast-is-id : cast eq k ≡ k + subst-is-cast : subst Fin eq k ≡ cast eq k + cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k + ``` + +* Added new functions in `Data.Integer.Base`: + ``` + _^_ : ℤ → ℕ → ℤ + + +-0-rawGroup : Rawgroup 0ℓ 0ℓ + + *-rawMagma : RawMagma 0ℓ 0ℓ + *-1-rawMonoid : RawMonoid 0ℓ 0ℓ + ``` + +* Added new proofs in `Data.Integer.Properties`: ```agda cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k inject!-injective : Injective _≡_ _≡_ inject! diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0f87eef534..f8c476139d 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -869,6 +869,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 ------------------------------------------------------------------------ @@ -903,6 +913,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 From d9c7ba62fe4f988425b989641313702b40c6e20c Mon Sep 17 00:00:00 2001 From: Alice Laroche <60161310+Seiryn21@users.noreply.github.com> Date: Mon, 20 Feb 2023 10:58:14 +0100 Subject: [PATCH 03/14] Wellfounded proof for sum relations (#1920) --- CHANGELOG.md | 11 +++++++++++ src/Data/Sum/Relation/Binary/LeftOrder.agda | 15 +++++++++++++++ src/Data/Sum/Relation/Binary/Pointwise.agda | 19 +++++++++++++++++++ 3 files changed, 45 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1f757d9a9c..114f44ea2b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -600,6 +600,16 @@ Additions to existing modules HomoProduct n A = HomoProduct′ n (const A) ``` +* In `Data.Sum.Relation.Binary.LeftOrder` : + ```agda + ⊎-<-wellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (∼₁ ⊎-< ∼₂) + ``` + +* in `Data.Sum.Relation.Binary.Pointwise` : + ```agda + ⊎-wellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (Pointwise ∼₁ ∼₂) + ``` + * In `Data.Vec.Properties`: ```agda toList-injective : .(m=n : m ≡ n) → (xs : Vec A m) (ys : Vec A n) → toList xs ≡ toList ys → xs ≈[ m=n ] ys @@ -652,6 +662,7 @@ Additions to existing modules ``` * In `Relation.Nullary.Decidable.Core`: +>>>>>>> da073f171 (Wellfounded proof for sum relations (#1920)) ```agda ⊤-dec : Dec ⊤ ⊥-dec : Dec ⊥ 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..a8b30b9261 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,24 @@ 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 +-- need to be more explicit here otherwise Agda does something odd with the variables +⊎-wellFounded : {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂} → 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) + +module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} + {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂} + {ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄} where + ⊎-antisymmetric : Antisymmetric ≈₁ R → Antisymmetric ≈₂ S → Antisymmetric (Pointwise ≈₁ ≈₂) (Pointwise R S) ⊎-antisymmetric antisym₁ antisym₂ (inj₁ x) (inj₁ y) = inj₁ (antisym₁ x y) From 4547ae1a51d2b15af28f2c1141d967d255176e94 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 30 Jul 2025 14:13:22 -0400 Subject: [PATCH 04/14] last revert undone by hand --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 114f44ea2b..25f27cabc8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -576,6 +576,11 @@ Additions to existing modules map-id : map id ≗ id ``` +* In `Data.Nat.Combinatorics.Specification`: + ```agda + k![n∸k]!∣n! : k ≤ n → k ! * (n ∸ k) ! ∣ n ! + ``` + * In `Data.Product.Function.Dependent.Propositional`: ```agda Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B From a596e55c1d2ae1bcd95f81d9d8371bca53d53de7 Mon Sep 17 00:00:00 2001 From: matthewdaggitt Date: Thu, 31 Jul 2025 07:57:33 +0800 Subject: [PATCH 05/14] Remove extra line in CHANGELOG --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 25f27cabc8..2437065d11 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -667,7 +667,6 @@ Additions to existing modules ``` * In `Relation.Nullary.Decidable.Core`: ->>>>>>> da073f171 (Wellfounded proof for sum relations (#1920)) ```agda ⊤-dec : Dec ⊤ ⊥-dec : Dec ⊥ From baa4a2aeb5cdca846819ad9a88d464d43cc528e6 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 31 Jul 2025 14:08:22 -0400 Subject: [PATCH 06/14] Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2437065d11..6179dedf5d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -442,16 +442,6 @@ Additions to existing modules cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k ``` -* Added new functions in `Data.Integer.Base`: - ``` - _^_ : ℤ → ℕ → ℤ - - +-0-rawGroup : Rawgroup 0ℓ 0ℓ - - *-rawMagma : RawMagma 0ℓ 0ℓ - *-1-rawMonoid : RawMonoid 0ℓ 0ℓ - ``` - * Added new proofs in `Data.Integer.Properties`: ```agda cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k From 517183d8c7233d7032cd4b9fb0d553afd3365fa2 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 31 Jul 2025 14:11:30 -0400 Subject: [PATCH 07/14] Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6179dedf5d..d330fcc571 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -566,11 +566,6 @@ Additions to existing modules map-id : map id ≗ id ``` -* In `Data.Nat.Combinatorics.Specification`: - ```agda - k![n∸k]!∣n! : k ≤ n → k ! * (n ∸ k) ! ∣ n ! - ``` - * In `Data.Product.Function.Dependent.Propositional`: ```agda Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B From 67d68fc337bb0a890e09c370fd03e96a8129304b Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 31 Jul 2025 14:53:16 -0400 Subject: [PATCH 08/14] Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d330fcc571..b0d4c4c416 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -267,7 +267,6 @@ Additions to existing modules ``` * In `Algebra.Properties.Magma.Divisibility`: - ```agda ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_ From 4381f54f000cce05f210bb5280fff597d6ab180c Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 31 Jul 2025 14:56:10 -0400 Subject: [PATCH 09/14] Update CHANGELOG.md This was indeed anachronistic from 2.0 Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 30 ------------------------------ 1 file changed, 30 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b0d4c4c416..4f9cfdc2c7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -390,36 +390,6 @@ Additions to existing modules ``` * In `Data.Fin.Properties`: - the proof that an injection from a type `A` into `Fin n` induces a - decision procedure for `_≡_` on `A` has been generalized to other - equivalences over `A` (i.e. to arbitrary setoids), and renamed from - `eq?` to the more descriptive `inj⇒≟` and `inj⇒decSetoid`. - -* Added new proofs in `Data.Fin.Properties`: - ``` - 1↔⊤ : Fin 1 ↔ ⊤ - - 0≢1+n : zero ≢ suc i - - ↑ˡ-injective : i ↑ˡ n ≡ j ↑ˡ n → i ≡ j - ↑ʳ-injective : n ↑ʳ i ≡ n ↑ʳ j → i ≡ j - finTofun-funToFin : funToFin ∘ finToFun ≗ id - funTofin-funToFun : finToFun (funToFin f) ≗ f - ^↔→ : Extensionality _ _ → Fin (m ^ n) ↔ (Fin n → Fin m) - - toℕ-mono-< : i < j → toℕ i ℕ.< toℕ j - toℕ-mono-≤ : i ≤ j → toℕ i ℕ.≤ toℕ j - toℕ-cancel-≤ : toℕ i ℕ.≤ toℕ j → i ≤ j - toℕ-cancel-< : toℕ i ℕ.< toℕ j → i < j - - toℕ-combine : toℕ (combine i j) ≡ k ℕ.* toℕ i ℕ.+ toℕ j - combine-injectiveˡ : combine i j ≡ combine k l → i ≡ k - combine-injectiveʳ : combine i j ≡ combine k l → j ≡ l - combine-injective : combine i j ≡ combine k l → i ≡ k × j ≡ l - combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i - combine-monoˡ-< : i < j → combine i k < combine j l - - ℕ-ℕ≡toℕ‿ℕ- : n ℕ-ℕ i ≡ toℕ (n ℕ- i) 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 From ba88e5784c007e4965fb06c892122fdade95b8a2 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 31 Jul 2025 14:56:59 -0400 Subject: [PATCH 10/14] Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4f9cfdc2c7..2f66bb2165 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -395,20 +395,6 @@ Additions to existing modules 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 - - lower₁-injective : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j - pinch-injective : suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k - - i<1+i : i < suc i - - injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective f → m ℕ.≤ n - <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective f) - ℕ→Fin-notInjective : ∀ (f : ℕ → Fin n) → ¬ (Injective f) - cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} → Injective f → Injective g → m ≡ n - - cast-is-id : cast eq k ≡ k - subst-is-cast : subst Fin eq k ≡ cast eq k - cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k ``` * Added new proofs in `Data.Integer.Properties`: From ca8f6e8dd23d627f42803021b030ae139d9e82d5 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 31 Jul 2025 15:06:00 -0400 Subject: [PATCH 11/14] resolve issues pointed out by James. --- src/Data/Sum/Relation/Binary/Pointwise.agda | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index a8b30b9261..6ef498ea0c 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -95,8 +95,8 @@ drop-inj₂ (inj₂ x) = x ⊎-irreflexive irrefl₁ irrefl₂ (inj₂ x) (inj₂ y) = irrefl₂ x y -- need to be more explicit here otherwise Agda does something odd with the variables -⊎-wellFounded : {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂} → WellFounded ≈₁ → WellFounded ≈₂ → WellFounded (Pointwise ≈₁ ≈₂) -⊎-wellFounded {≈₁ = ≈₁} {≈₂} wf₁ wf₂ x = acc (⊎-acc x) +⊎-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)) @@ -108,10 +108,6 @@ drop-inj₂ (inj₂ x) = 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₂ ℓ₄} where - ⊎-antisymmetric : Antisymmetric ≈₁ R → Antisymmetric ≈₂ S → Antisymmetric (Pointwise ≈₁ ≈₂) (Pointwise R S) ⊎-antisymmetric antisym₁ antisym₂ (inj₁ x) (inj₁ y) = inj₁ (antisym₁ x y) From bf9715f3ae14eec1492987dcf80166b3fd2e752b Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Fri, 1 Aug 2025 11:10:04 -0400 Subject: [PATCH 12/14] Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2f66bb2165..9f68f9ca2b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -552,7 +552,7 @@ Additions to existing modules * in `Data.Sum.Relation.Binary.Pointwise` : ```agda - ⊎-wellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (Pointwise ∼₁ ∼₂) + ⊎-wellFounded : WellFounded ≈₁ → WellFounded ≈₂ → WellFounded (Pointwise ≈₁ ≈₂) ``` * In `Data.Vec.Properties`: From 7f84017a81cebb1af4f98b03b91080896400ac9d Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Fri, 1 Aug 2025 11:11:46 -0400 Subject: [PATCH 13/14] remove now obsolete comment --- src/Data/Sum/Relation/Binary/Pointwise.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 6ef498ea0c..6e65ba9691 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -94,7 +94,6 @@ 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 --- need to be more explicit here otherwise Agda does something odd with the variables ⊎-wellFounded : WellFounded ≈₁ → WellFounded ≈₂ → WellFounded (Pointwise ≈₁ ≈₂) ⊎-wellFounded {≈₁ = ≈₁} {≈₂ = ≈₂} wf₁ wf₂ x = acc (⊎-acc x) where From 812067fa55494c1394434c6b3545f35570a5a60c Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Fri, 1 Aug 2025 11:15:49 -0400 Subject: [PATCH 14/14] last mistake in CHANGELOG, hopefully fixed now. --- CHANGELOG.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f68f9ca2b..3a4c39e948 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -391,14 +391,11 @@ Additions to existing modules * 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 - ``` - -* Added new proofs in `Data.Integer.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