From c0bedbc7d776441cb3902b742221a162da1891e0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 15 Jan 2025 22:53:15 +0000 Subject: [PATCH 1/4] fix names in `Transitive`, `Antisym`, and `Antisymmetric` --- src/Relation/Binary/Definitions.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index 167b63a8cb..2762305568 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/src/Relation/Binary/Definitions.agda @@ -54,7 +54,7 @@ Symmetric _∼_ = Sym _∼_ _∼_ -- Generalised transitivity. Trans : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _ -Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k +Trans P Q R = ∀ {x y z} → P x y → Q y z → R x z RightTrans : REL A B ℓ₁ → REL B B ℓ₂ → Set _ RightTrans R S = Trans R S R @@ -65,7 +65,7 @@ LeftTrans S R = Trans S R R -- A flipped variant of generalised transitivity. TransFlip : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _ -TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k +TransFlip P Q R = ∀ {x y z} → Q y z → P x y → R x z -- Transitivity. @@ -75,7 +75,7 @@ Transitive _∼_ = Trans _∼_ _∼_ _∼_ -- Generalised antisymmetry Antisym : REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _ -Antisym R S E = ∀ {i j} → R i j → S j i → E i j +Antisym R S E = ∀ {x y} → R x y → S y x → E x y -- Antisymmetry. From 15aac2e2582e59509c5043418356d55ccb09b009 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 15 Jan 2025 22:53:47 +0000 Subject: [PATCH 2/4] knock-on consequences: fix named bindings --- .../Data/Container/Indexed/MultiSortedAlgebraExample.agda | 2 +- src/Algebra/Construct/Initial.agda | 2 +- src/Data/Container/Indexed/WithK.agda | 2 +- src/Data/Fin/Subset/Properties.agda | 4 ++-- src/Data/Fin/Substitution.agda | 2 +- .../Relation/Binary/Infix/Heterogeneous/Properties.agda | 6 +++--- .../Tree/AVL/Map/Membership/Propositional/Properties.agda | 2 +- .../Functional/Relation/Binary/Permutation/Properties.agda | 2 +- src/Relation/Binary/Consequences.agda | 2 +- 9 files changed, 12 insertions(+), 12 deletions(-) diff --git a/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda b/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda index 0c466c932c..a8bad10f32 100644 --- a/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda +++ b/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda @@ -335,7 +335,7 @@ module _ (Sort : Set ℓˢ) (Ops : Container Sort Sort ℓᵒ ℓᵃ) where {x = t} {y = t'} (sound e) sound (trans {t₁ = t₁} {t₂ = t₂} {t₃ = t₃} e e') = isEquiv {M = M} .IsEquivalence.trans - {i = t₁} {j = t₂} {k = t₃} (sound e) (sound e') + {x = t₁} {y = t₂} {z = t₃} (sound e) (sound e') ------------------------------------------------------------------------ diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda index 57648d6735..212280005d 100644 --- a/src/Algebra/Construct/Initial.agda +++ b/src/Algebra/Construct/Initial.agda @@ -58,7 +58,7 @@ module ℤero where sym {x = ()} trans : Transitive _≈_ - trans {i = ()} + trans {x = ()} ∙-cong : Congruent₂ _≈_ _∙_ ∙-cong {x = ()} diff --git a/src/Data/Container/Indexed/WithK.agda b/src/Data/Container/Indexed/WithK.agda index bda5a15e34..cbb132d2ac 100644 --- a/src/Data/Container/Indexed/WithK.agda +++ b/src/Data/Container/Indexed/WithK.agda @@ -53,7 +53,7 @@ setoid C X = record ; isEquivalence = record { refl = refl , refl , λ { r .r refl → X.refl } ; sym = sym - ; trans = λ { {_} {i = xs} {ys} {zs} → trans {_} {i = xs} {ys} {zs} } + ; trans = λ { {_} {x = xs} {ys} {zs} → trans {_} {x = xs} {ys} {zs} } } } where diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index 03467dcee7..e7c99edea2 100644 --- a/src/Data/Fin/Subset/Properties.agda +++ b/src/Data/Fin/Subset/Properties.agda @@ -214,8 +214,8 @@ x∉⁅y⁆⇒x≢y x∉⁅x⁆ refl = x∉⁅x⁆ (x∈⁅x⁆ _) ⊆-trans p⊆q q⊆r x∈p = q⊆r (p⊆q x∈p) ⊆-antisym : Antisymmetric {A = Subset n} _≡_ _⊆_ -⊆-antisym {i = []} {[]} p⊆q q⊆p = refl -⊆-antisym {i = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y +⊆-antisym {x = []} {[]} p⊆q q⊆p = refl +⊆-antisym {x = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y ... | inside | inside = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p)) ... | inside | outside = contradiction (p⊆q here) λ() ... | outside | inside = contradiction (q⊆p here) λ() diff --git a/src/Data/Fin/Substitution.agda b/src/Data/Fin/Substitution.agda index 84a4484715..18e5773b7b 100644 --- a/src/Data/Fin/Substitution.agda +++ b/src/Data/Fin/Substitution.agda @@ -104,7 +104,7 @@ record Application (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ -- Application of multiple substitutions. _/✶_ : T₁ m → Subs T₂ m n → T₁ n - _/✶_ = Star.gfold Fun.id _ (flip _/_) {k = zero} + _/✶_ = Star.gfold Fun.id _ (flip _/_) {z = zero} -- A combination of the two records above. diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda index 7e85ae8661..27a88cc04b 100644 --- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda @@ -97,17 +97,17 @@ module _ {c t} {C : Set c} {T : REL A C t} where antisym : Antisym R S T → Antisym (Infix R) (Infix S) (Pointwise T) antisym asym (here p) (here q) = Prefix.antisym asym p q - antisym asym {i = a ∷ as} {j = bs} p@(here _) (there q) + antisym asym {x = a ∷ as} {y = bs} p@(here _) (there q) = ⊥-elim $′ ℕ.<-irrefl refl $′ begin-strict length as <⟨ length-mono p ⟩ length bs ≤⟨ length-mono q ⟩ length as ∎ where open ℕ.≤-Reasoning - antisym asym {i = as} {j = b ∷ bs} (there p) q@(here _) + antisym asym {x = as} {y = b ∷ bs} (there p) q@(here _) = ⊥-elim $′ ℕ.<-irrefl refl $′ begin-strict length bs <⟨ length-mono q ⟩ length as ≤⟨ length-mono p ⟩ length bs ∎ where open ℕ.≤-Reasoning - antisym asym {i = a ∷ as} {j = b ∷ bs} (there p) (there q) + antisym asym {x = a ∷ as} {y = b ∷ bs} (there p) (there q) = ⊥-elim $′ ℕ.<-irrefl refl $′ begin-strict length as <⟨ length-mono p ⟩ length bs <⟨ length-mono q ⟩ diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda index 2368c44bcd..4739286d52 100644 --- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda +++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda @@ -51,7 +51,7 @@ private kx : Key × V ≈ₖᵥ-trans : Transitive (_≈ₖᵥ_ {V = V}) -≈ₖᵥ-trans {i = i} {k = k} = ×-transitive Eq.trans ≡-trans {i = i} {k = k} +≈ₖᵥ-trans {x = x} {z = z} = ×-transitive Eq.trans ≡-trans {x = x} {z = z} ≈ₖᵥ-sym : Symmetric (_≈ₖᵥ_ {V = V}) ≈ₖᵥ-sym {x = x} {y = y} = ×-symmetric sym ≡-sym {x} {y} diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda index 83d65ab5bb..22c54abb40 100644 --- a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda +++ b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda @@ -58,7 +58,7 @@ isIndexedEquivalence {A = A} = record { refl = ↭-refl ; sym = ↭-sym ; trans = λ {n₁ n₂ n₃} {xs : Vector A n₁} {ys : Vector A n₂} {zs : Vector A n₃} - xs↭ys ys↭zs → ↭-trans {i = n₁} {i = xs} xs↭ys ys↭zs + xs↭ys ys↭zs → ↭-trans {i = n₁} {x = xs} xs↭ys ys↭zs } ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda index 3cdb4db356..6fac011714 100644 --- a/src/Relation/Binary/Consequences.agda +++ b/src/Relation/Binary/Consequences.agda @@ -55,7 +55,7 @@ module _ {_∼_ : Rel A ℓ} where -- N.B. the implicit arguments to Cotransitive are permuted w.r.t. -- those of Transitive cotrans⇒¬-trans : Cotransitive _∼_ → Transitive (¬_ ∘₂ _∼_) - cotrans⇒¬-trans cotrans {j = z} x≁z z≁y x∼y = + cotrans⇒¬-trans cotrans {y = z} x≁z z≁y x∼y = [ x≁z , z≁y ]′ (cotrans x∼y z) ------------------------------------------------------------------------ From 8dc9ae70f9dd18f9e515c736741307d6a4794a1b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 16 Jan 2025 08:20:43 +0000 Subject: [PATCH 3/4] a more robust proof? --- src/Relation/Binary/Consequences.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda index 6fac011714..2d7fdc10c2 100644 --- a/src/Relation/Binary/Consequences.agda +++ b/src/Relation/Binary/Consequences.agda @@ -55,8 +55,7 @@ module _ {_∼_ : Rel A ℓ} where -- N.B. the implicit arguments to Cotransitive are permuted w.r.t. -- those of Transitive cotrans⇒¬-trans : Cotransitive _∼_ → Transitive (¬_ ∘₂ _∼_) - cotrans⇒¬-trans cotrans {y = z} x≁z z≁y x∼y = - [ x≁z , z≁y ]′ (cotrans x∼y z) + cotrans⇒¬-trans cotrans x≁z z≁y x∼y = [ x≁z , z≁y ]′ (cotrans x∼y _) ------------------------------------------------------------------------ -- Proofs for Irreflexive relations From dc6f537e2791015ae59f8d7690a002b52a86f474 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 18 Jan 2025 08:59:34 +0000 Subject: [PATCH 4/4] `CHANGELOG`: added new entry --- CHANGELOG.md | 598 +-------------------------------------------------- 1 file changed, 4 insertions(+), 594 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6703f59fb9..91f9cb5dd3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,622 +1,32 @@ -Version 2.2 -=========== +Version 2.3-dev +=============== The library has been tested using Agda 2.7.0 and 2.7.0.1. Highlights ---------- -* Added missing morphisms between the more advanced algebraic structures. - -* Added many missing lemmas about positive and negative rational numbers. - Bug-fixes --------- -* Made the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality` more general. - These operators are used for equational reasoning of heterogeneous equality - `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily required - `x` and `y` to have the same type, making them unusable in many situations. - -* Removed unnecessary parameter `#-trans : Transitive _#_` from - `Relation.Binary.Reasoning.Base.Apartness`. - -* The `IsSemiringWithoutOne` record no longer incorrectly exposes the `Carrier` field - inherited from `Setoid` when opening the record publicly. - Non-backwards compatible changes -------------------------------- -* In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the majority of uses, and would only be non-backwards compatible if for some reason you were explicitly supplying these implicit parameters when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected. +* [issue #2547](https://github.com/agda/agda-stdlib/issues/2547) The names of the *implicit* binders in the following definitions have been rectified to be consistent with those in the rest of `Relation.Binary.Definitions`: `Transitive`, `Antisym`, and `Antisymmetric`. + -* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) and [issue #2519](https://github.com/agda/agda-stdlib/issues/2510) In `Data.Nat.Base` the definitions of `_≤′_` and `_≤‴_` have been modified to make the witness to equality explicit in new constructors `≤′-reflexive` and `≤‴-reflexive`; pattern synonyms `≤′-refl` and `≤‴-refl` have been added for backwards compatibility. This should be a backwards compatible change for the majority of uses, but the change in parametrisation means that these patterns are *not* necessarily well-formed if the old implicit arguments `m`,`n` are supplied explicitly. Minor improvements ------------------ -* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold. - Deprecated modules ------------------ Deprecated names ---------------- -* In `Algebra.Properties.CommutativeMagma.Divisibility`: - ```agda - ∣-factors ↦ x|xy∧y|xy - ∣-factors-≈ ↦ xy≈z⇒x|z∧y|z - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣-respˡ ↦ ∣-respˡ-≈ - ∣-respʳ ↦ ∣-respʳ-≈ - ∣-resp ↦ ∣-resp-≈ - ``` - -* In `Algebra.Solver.CommutativeMonoid`: - ```agda - normalise-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.correct - sg ↦ Algebra.Solver.CommutativeMonoid.Normal.singleton - sg-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.singleton-correct - ``` - -* In `Algebra.Solver.IdempotentCommutativeMonoid`: - ```agda - flip12 ↦ Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz - distr ↦ Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙ - normalise-correct ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct - sg ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton - sg-correct ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct - ``` - -* In `Algebra.Solver.Monoid`: - ```agda - homomorphic ↦ Algebra.Solver.Monoid.Normal.comp-correct - normalise-correct ↦ Algebra.Solver.Monoid.Normal.correct - ``` - -* In `Data.List.Properties`: - ```agda - concat-[-] ↦ concat-map-[_] - ``` - -* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: - ```agda - split ↦ ↭-split - ``` - with a more informative type (see below). - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - takeWhile⁻ ↦ all-takeWhile - ``` - -* In `Data.Vec.Properties`: - ```agda - ++-assoc _ ↦ ++-assoc-eqFree - ++-identityʳ _ ↦ ++-identityʳ-eqFree - unfold-∷ʳ _ ↦ unfold-∷ʳ-eqFree - ++-∷ʳ _ ↦ ++-∷ʳ-eqFree - ∷ʳ-++ _ ↦ ∷ʳ-++-eqFree - reverse-++ _ ↦ reverse-++-eqFree - ∷-ʳ++ _ ↦ ∷-ʳ++-eqFree - ++-ʳ++ _ ↦ ++-ʳ++-eqFree - ʳ++-ʳ++ _ ↦ ʳ++-ʳ++-eqFree - ``` - New modules ----------- -* Consequences of module monomorphisms - ``` - Algebra.Module.Morphism.BimoduleMonomorphism - Algebra.Module.Morphism.BisemimoduleMonomorphism - Algebra.Module.Morphism.LeftModuleMonomorphism - Algebra.Module.Morphism.LeftSemimoduleMonomorphism - Algebra.Module.Morphism.ModuleMonomorphism - Algebra.Module.Morphism.RightModuleMonomorphism - Algebra.Module.Morphism.RightSemimoduleMonomorphism - Algebra.Module.Morphism.SemimoduleMonomorphism - ``` - -* Bundled morphisms between (raw) algebraic structures: - ``` - Algebra.Morphism.Bundles - ``` - -* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`: - ``` - Algebra.Properties.IdempotentCommutativeMonoid - ``` - -* Refactoring of the `Algebra.Solver.*Monoid` implementations, via - a single `Solver` module API based on the existing `Expr`, and - a common `Normal`-form API: - ``` - Algebra.Solver.CommutativeMonoid.Normal - Algebra.Solver.IdempotentCommutativeMonoid.Normal - Algebra.Solver.Monoid.Expression - Algebra.Solver.Monoid.Normal - Algebra.Solver.Monoid.Solver - ``` - NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`. - -* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`: - Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties` - -* Properties of list permutations that require the `--with-K` flag: - ``` - Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK - ``` - -* Refactored `Data.Refinement` into: - ```agda - Data.Refinement.Base - Data.Refinement.Properties - ``` - -* Added implementation of Haskell-like `Foldable`: - ```agda - Effect.Foldable - Data.List.Effectful.Foldable - Data.Vec.Effectful.Foldable - ``` - -* Raw bundles for the `Relation.Binary.Bundles` hierarchy: - ```agda - Relation.Binary.Bundles.Raw - ``` - Additions to existing modules ----------------------------- - -* In `Algebra.Bundles.KleeneAlgebra`: - ```agda - rawKleeneAlgebra : RawKleeneAlgebra _ _ - ``` - -* In `Algebra.Bundles.Raw.*` - ```agda - rawSetoid : RawSetoid c ℓ - ``` - -* In `Algebra.Bundles.Raw.RawRingWithoutOne` - ```agda - rawNearSemiring : RawNearSemiring c ℓ - ``` - -* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: - ```agda - rawNearSemiring : RawNearSemiring _ _ - rawRingWithoutOne : RawRingWithoutOne _ _ - +-rawGroup : RawGroup _ _ - ``` - -* Exporting `RawRingWithoutOne` and `(Raw)NearSemiring` subbundles from - `Algebra.Bundles.RingWithoutOne`: - ```agda - nearSemiring : NearSemiring _ _ - rawNearSemiring : RawNearSemiring _ _ - rawRingWithoutOne : RawRingWithoutOne _ _ - ``` - -* In `Algebra.Morphism.Construct.Composition`: - ```agda - magmaHomomorphism : MagmaHomomorphism M₁.rawMagma M₂.rawMagma → - MagmaHomomorphism M₂.rawMagma M₃.rawMagma → - MagmaHomomorphism M₁.rawMagma M₃.rawMagma - monoidHomomorphism : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid → - MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid → - MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid - groupHomomorphism : GroupHomomorphism M₁.rawGroup M₂.rawGroup → - GroupHomomorphism M₂.rawGroup M₃.rawGroup → - GroupHomomorphism M₁.rawGroup M₃.rawGroup - nearSemiringHomomorphism : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring → - NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring → - NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring - semiringHomomorphism : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring → - SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring → - SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring - kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₂.rawKleeneAlgebra → - KleeneAlgebraHomomorphism M₂.rawKleeneAlgebra M₃.rawKleeneAlgebra → - KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₃.rawKleeneAlgebra - nearSemiringHomomorphism : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring → - NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring → - NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne → - RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne → - RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne - ringHomomorphism : RingHomomorphism M₁.rawRing M₂.rawRing → - RingHomomorphism M₂.rawRing M₃.rawRing → - RingHomomorphism M₁.rawRing M₃.rawRing - quasigroupHomomorphism : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup → - QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup → - QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup - loopHomomorphism : LoopHomomorphism M₁.rawLoop M₂.rawLoop → - LoopHomomorphism M₂.rawLoop M₃.rawLoop → - LoopHomomorphism M₁.rawLoop M₃.rawLoop - ``` - -* In `Algebra.Morphism.Construct.Identity`: - ```agda - magmaHomomorphism : MagmaHomomorphism M.rawMagma M.rawMagma - monoidHomomorphism : MonoidHomomorphism M.rawMonoid M.rawMonoid - groupHomomorphism : GroupHomomorphism M.rawGroup M.rawGroup - nearSemiringHomomorphism : NearSemiringHomomorphism M.raw M.raw - semiringHomomorphism : SemiringHomomorphism M.rawNearSemiring M.rawNearSemiring - kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism M.rawKleeneAlgebra M.rawKleeneAlgebra - nearSemiringHomomorphism : NearSemiringHomomorphism M.rawNearSemiring M.rawNearSemiring - ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M.rawRingWithoutOne M.rawRingWithoutOne - ringHomomorphism : RingHomomorphism M.rawRing M.rawRing - quasigroupHomomorphism : QuasigroupHomomorphism M.rawQuasigroup M.rawQuasigroup - loopHomomorphism : LoopHomomorphism M.rawLoop M.rawLoop - ``` - -* In `Algebra.Morphism.Structures.RingMorphisms` - ```agda - isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧ - ``` - -* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms` - ```agda - isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ - ``` - -* In `Algebra.Structures.IsSemiringWithoutOne`: - ```agda - distribˡ : * DistributesOverˡ + - distribʳ : * DistributesOverʳ + - +-cong : Congruent + - +-congˡ : LeftCongruent + - +-congʳ : RightCongruent + - +-assoc : Associative + - +-identity : Identity 0# + - +-identityˡ : LeftIdentity 0# + - +-identityʳ : RightIdentity 0# + - ``` - -* Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`: - ```agda - ∤-respˡ-≈ : _∤_ Respectsˡ _≈_ - ∤-respʳ-≈ : _∤_ Respectsʳ _≈_ - ∤-resp-≈ : _∤_ Respects₂ _≈_ - ∤∤-sym : Symmetric _∤∤_ - ∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_ - ∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_ - ∤∤-resp-≈ : _∤∤_ Respects₂ _≈_ - ``` - -* In `Algebra.Solver.Ring` - ```agda - Env : ℕ → Set _ - Env = Vec Carrier - ``` - -* In `Algebra.Structures.RingWithoutOne`: - ```agda - isNearSemiring : IsNearSemiring _ _ - ``` - -* In `Data.List.Membership.Propositional.Properties`: - ```agda - ∈-AllPairs₂ : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x - ∈-map∘filter⁻ : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x) - ∈-map∘filter⁺ : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs) - ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs - ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs - ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys) - []∉map∷ : [] ∉ map (x ∷_) xss - map∷⁻ : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys - map∷-decomp∈ : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss - ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs - ∉[] : x ∉ [] - deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs - ``` - -* In `Data.List.Membership.Propositional.Properties.WithK`: - ```agda - unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys - ``` - -* In `Data.List.Membership.Setoid.Properties`: - ```agda - ∉⇒All[≉] : x ∉ xs → All (x ≉_) xs - All[≉]⇒∉ : All (x ≉_) xs → x ∉ xs - Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys - All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys - ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x - ∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ → - ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x → - y ∈₂ map f (filter P? xs) - ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs - ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs - ∉[] : x ∉ [] - deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs - ``` - -* In `Data.List.Properties`: - ```agda - product≢0 : All NonZero ns → NonZero (product ns) - ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns - concat-[_] : concat ∘ [_] ≗ id - concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys - filter-≐ : P ≐ Q → filter P? ≗ filter Q? - - partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then map₁ (x ∷_) else map₂ (x ∷_)) ([] , []) - ``` - -* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`: - ```agda - deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys) - ``` - -* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`: - ```agda - deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys) - ``` - -* In `Data.List.Relation.Binary.Equality.Setoid`: - ```agda - ++⁺ˡ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs - ++⁺ʳ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs - ``` - -* In `Data.List.Relation.Binary.Permutation.Homogeneous`: - ```agda - steps : Permutation R xs ys → ℕ - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional`: - constructor aliases - ```agda - ↭-refl : Reflexive _↭_ - ↭-prep : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys - ↭-swap : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys - ``` - and properties - ```agda - ↭-reflexive-≋ : _≋_ ⇒ _↭_ - ↭⇒↭ₛ : _↭_ ⇒ _↭ₛ_ - ↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_ - ``` - where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) → - Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy - ∈-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : y ∈ ys) → - ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy - product-↭ : product Preserves _↭_ ⟶ _≡_ - sum-↭ : sum Preserves _↭_ ⟶ _≡_ - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`: - ```agda - dedup-++-↭ : Disjoint xs ys → - deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys - ``` - -* In `Data.List.Relation.Binary.Permutation.Setoid`: - ```agda - ↭-reflexive-≋ : _≋_ ⇒ _↭_ - ↭-transˡ-≋ : LeftTrans _≋_ _↭_ - ↭-transʳ-≋ : RightTrans _↭_ _≋_ - ↭-trans′ : Transitive _↭_ - ``` - -* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: - ```agda - ↭-split : xs ↭ (as ++ [ v ] ++ bs) → - ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs) × (ps ++ qs) ↭ (as ++ bs) - drop-∷ : x ∷ xs ↭ x ∷ ys → xs ↭ ys - ``` - -* In `Data.List.Relation.Binary.Pointwise`: - ```agda - ++⁺ˡ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) - ++⁺ʳ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) - ``` - -* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`: - ```agda - Sublist-[]-universal : Universal (Sublist R []) - - module ⊆-Reasoning (≲ : Preorder a e r) - ``` - -* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`: - ```agda - ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: - ```agda - []⊆-universal : Universal ([] ⊆_) - - module ⊆-Reasoning - - concat⁺ : Sublist _⊆_ ass bss → concat ass ⊆ concat bss - xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss - all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss - ``` - -* In `Data.List.Relation.Binary.Subset.Propositional.Properties`: - ```agda - ∷⊈[] : x ∷ xs ⊈ [] - ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys - ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys - - concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys - ``` - -* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: - ```agda - ∷⊈[] : x ∷ xs ⊈ [] - ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys - ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys - ``` - -* In `Data.List.Relation.Unary.First.Properties`: - ```agda - ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P - ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q - ``` - -* In `Data.List.Relation.Unary.All`: - ```agda - search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ [] - all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs - ``` - -* In `Data.List.Relation.Unary.Any.Properties`: - ```agda - concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs) - concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs - ``` - -* In `Data.List.Relation.Unary.Unique.Propositional.Properties`: - ```agda - Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs - ``` - -* In `Data.List.Relation.Unary.Unique.Setoid.Properties`: - ```agda - Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs - ``` - -* In `Data.Maybe.Properties`: - ```agda - maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b) - ``` - -* New lemmas in `Data.Nat.Properties`: - ```agda - m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o - m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n - <‴-irrefl : Irreflexive _≡_ _<‴_ - ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_ - <‴-irrelevant : Irrelevant {A = ℕ} _<‴_ - >‴-irrelevant : Irrelevant {A = ℕ} _>‴_ - ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_ - ``` - - Added adjunction between `suc` and `pred` - ```agda - suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n - m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n - ``` - -* In `Data.Product.Function.Dependent.Propositional`: - ```agda - congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B - ``` - -* New lemmas in `Data.Rational.Properties`: - ```agda - nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q) - nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q) - pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q) - nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q) - pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q) - neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q) - nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q) - neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q) - nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q) - nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q) - nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q) - nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q) - pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q) - neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q) - pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q) - neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q) - ``` - -* New properties re-exported from `Data.Refinement`: - ```agda - value-injective : value v ≡ value w → v ≡ w - _≟_ : DecidableEquality A → DecidableEquality [ x ∈ A ∣ P x ] - ``` - -* New lemma in `Data.Vec.Properties`: - ```agda - map-concat : map f (concat xss) ≡ concat (map (map f) xss) - ``` - -* New lemma in `Data.Vec.Relation.Binary.Equality.Cast`: - ```agda - ≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n)) - {m n} {xs : Vec A m} {ys : Vec A n} .{eq} → - xs ≈[ eq ] ys → f xs ≈[ _ ] f ys - ``` - -* In `Data.Vec.Relation.Binary.Equality.DecPropositional`: - ```agda - _≡?_ : DecidableEquality (Vec A n) - ``` - -* In `Function.Related.TypeIsomorphisms`: - ```agda - Σ-distribˡ-⊎ : (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q) - Σ-distribʳ-⊎ : (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂)) - ×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C) - ×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C) - ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) - ``` - -* In `Relation.Binary.Bundles`: - ```agda - record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) - ``` - plus associated sub-bundles. - -* In `Relation.Binary.Construct.Interior.Symmetric`: - ```agda - decidable : Decidable R → Decidable (SymInterior R) - ``` - and for `Reflexive` and `Transitive` relations `R`: - ```agda - isDecEquivalence : Decidable R → IsDecEquivalence (SymInterior R) - isDecPreorder : Decidable R → IsDecPreorder (SymInterior R) R - isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R - decPreorder : Decidable R → DecPreorder _ _ _ - decPoset : Decidable R → DecPoset _ _ _ - ``` - -* In `Relation.Binary.Structures`: - ```agda - record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where - field - isPreorder : IsPreorder _≲_ - _≟_ : Decidable _≈_ - _≲?_ : Decidable _≲_ - ``` - plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure. - -* In `Relation.Binary.Bundles` added `rawX` (e.g. `RawSetoid`) fields to each bundle. - -* In `Relation.Nullary.Decidable`: - ```agda - does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b? - does-≡ : (a? b? : Dec A) → does a? ≡ does b? - ``` - -* In `Relation.Nullary.Recomputable`: - ```agda - irrelevant-recompute : Recomputable (Irrelevant A) - ``` - -* In `Relation.Unary.Properties`: - ```agda - map : P ≐ Q → Decidable P → Decidable Q - does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q? - does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′ - ```