From eded6741c35a772e35b23ff78412f5fca1879024 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 18 Jan 2025 04:48:21 +0000 Subject: [PATCH 1/2] Update documentation from v2.2 release version to v2.3-dev (#2557) * Fixes #2556 * missing full stop * updated `doc/README` * archive `v2.2` to `CHANGELOG` subdirectory * `fix-whitespace` --- CHANGELOG.md | 598 +------------------------------------------- CHANGELOG/v2.2.md | 620 ++++++++++++++++++++++++++++++++++++++++++++++ doc/README.agda | 2 +- 3 files changed, 623 insertions(+), 597 deletions(-) create mode 100644 CHANGELOG/v2.2.md diff --git a/CHANGELOG.md b/CHANGELOG.md index 6703f59fb9..edb7c3e57f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,622 +1,28 @@ -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 #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?′ - ``` diff --git a/CHANGELOG/v2.2.md b/CHANGELOG/v2.2.md new file mode 100644 index 0000000000..6f723e58e4 --- /dev/null +++ b/CHANGELOG/v2.2.md @@ -0,0 +1,620 @@ +Version 2.2 +=========== + +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 #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 + ``` + +* 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?′ + ``` diff --git a/doc/README.agda b/doc/README.agda index 844d531899..78ad1cbbee 100644 --- a/doc/README.agda +++ b/doc/README.agda @@ -3,7 +3,7 @@ module README where ------------------------------------------------------------------------ --- The Agda standard library, version 2.1.1 +-- The Agda standard library, version 2.3-dev -- -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais -- with contributions from Andreas Abel, Stevan Andjelkovic, From a78700653de116b1043ce5d80bbe99482a705ecc Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Sat, 18 Jan 2025 05:48:36 +0100 Subject: [PATCH 2/2] Update CI (#2544) * .cabal: allow base-4.21, add GHC 9.12.1 to Haskell-CI * CI: bump GHC to 9.10.1 --- .github/workflows/ci-ubuntu.yml | 8 +++--- .github/workflows/haskell-ci.yml | 48 +++++++++++++++++++------------- agda-stdlib-utils.cabal | 7 +++-- 3 files changed, 37 insertions(+), 26 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 56b4c88637..80c8498d43 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -48,8 +48,8 @@ on: ######################################################################## env: - GHC_VERSION: 9.8.2 - CABAL_VERSION: 3.10.3.0 + GHC_VERSION: 9.10.1 + CABAL_VERSION: 3.12.1.0 CABAL_V1_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc @@ -80,7 +80,7 @@ jobs: echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}" else # Pick Agda version for master - echo "AGDA_COMMIT=tags/v2.7.0" >> "${GITHUB_ENV}"; + echo "AGDA_COMMIT=tags/v2.7.0.1" >> "${GITHUB_ENV}"; echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}" fi @@ -191,7 +191,7 @@ jobs: ./landing.sh - name: Deploy HTML - uses: JamesIves/github-pages-deploy-action@4.1.3 + uses: JamesIves/github-pages-deploy-action@v4 if: success() && env.AGDA_DEPLOY with: diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index 391a975ad6..f48cbcbff4 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -8,9 +8,9 @@ # # For more information, see https://github.com/haskell-CI/haskell-ci # -# version: 0.19.20240514 +# version: 0.19.20241223 # -# REGENDATA ("0.19.20240514",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) +# REGENDATA ("0.19.20241223",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) # name: Haskell-CI on: @@ -45,19 +45,24 @@ jobs: strategy: matrix: include: + - compiler: ghc-9.12.1 + compilerKind: ghc + compilerVersion: 9.12.1 + setup-method: ghcup + allow-failure: false - compiler: ghc-9.10.1 compilerKind: ghc compilerVersion: 9.10.1 setup-method: ghcup allow-failure: false - - compiler: ghc-9.8.2 + - compiler: ghc-9.8.4 compilerKind: ghc - compilerVersion: 9.8.2 + compilerVersion: 9.8.4 setup-method: ghcup allow-failure: false - - compiler: ghc-9.6.5 + - compiler: ghc-9.6.6 compilerKind: ghc - compilerVersion: 9.6.5 + compilerVersion: 9.6.6 setup-method: ghcup allow-failure: false - compiler: ghc-9.4.8 @@ -92,15 +97,29 @@ jobs: allow-failure: false fail-fast: false steps: - - name: apt + - name: apt-get install run: | apt-get update apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5 + - name: Install GHCup + run: | mkdir -p "$HOME/.ghcup/bin" - curl -sL https://downloads.haskell.org/ghcup/0.1.20.0/x86_64-linux-ghcup-0.1.20.0 > "$HOME/.ghcup/bin/ghcup" + curl -sL https://downloads.haskell.org/ghcup/0.1.30.0/x86_64-linux-ghcup-0.1.30.0 > "$HOME/.ghcup/bin/ghcup" chmod a+x "$HOME/.ghcup/bin/ghcup" + - name: Install cabal-install + run: | + "$HOME/.ghcup/bin/ghcup" install cabal 3.14.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false) + echo "CABAL=$HOME/.ghcup/bin/cabal-3.14.1.0 -vnormal+nowrap" >> "$GITHUB_ENV" + - name: Install GHC (GHCup) + if: matrix.setup-method == 'ghcup' + run: | "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false) - "$HOME/.ghcup/bin/ghcup" install cabal 3.10.2.0 || (cat "$HOME"/.ghcup/logs/*.* && false) + HC=$("$HOME/.ghcup/bin/ghcup" whereis ghc "$HCVER") + HCPKG=$(echo "$HC" | sed 's#ghc$#ghc-pkg#') + HADDOCK=$(echo "$HC" | sed 's#ghc$#haddock#') + echo "HC=$HC" >> "$GITHUB_ENV" + echo "HCPKG=$HCPKG" >> "$GITHUB_ENV" + echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV" env: HCKIND: ${{ matrix.compilerKind }} HCNAME: ${{ matrix.compiler }} @@ -111,21 +130,12 @@ jobs: echo "LANG=C.UTF-8" >> "$GITHUB_ENV" echo "CABAL_DIR=$HOME/.cabal" >> "$GITHUB_ENV" echo "CABAL_CONFIG=$HOME/.cabal/config" >> "$GITHUB_ENV" - HCDIR=/opt/$HCKIND/$HCVER - HC=$("$HOME/.ghcup/bin/ghcup" whereis ghc "$HCVER") - HCPKG=$(echo "$HC" | sed 's#ghc$#ghc-pkg#') - HADDOCK=$(echo "$HC" | sed 's#ghc$#haddock#') - echo "HC=$HC" >> "$GITHUB_ENV" - echo "HCPKG=$HCPKG" >> "$GITHUB_ENV" - echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV" - echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.2.0 -vnormal+nowrap" >> "$GITHUB_ENV" HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\d+)\.(\d+)\.(\d+)(\.(\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))') echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV" echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV" echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV" echo "HEADHACKAGE=false" >> "$GITHUB_ENV" echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV" - echo "GHCJSARITH=0" >> "$GITHUB_ENV" env: HCKIND: ${{ matrix.compilerKind }} HCNAME: ${{ matrix.compiler }} @@ -234,8 +244,8 @@ jobs: rm -f cabal.project.local $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks all - name: save cache - uses: actions/cache/save@v4 if: always() + uses: actions/cache/save@v4 with: key: ${{ runner.os }}-${{ matrix.compiler }}-${{ github.sha }} path: ~/.cabal/store diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal index 1c37c72fca..2e5924eda8 100644 --- a/agda-stdlib-utils.cabal +++ b/agda-stdlib-utils.cabal @@ -6,9 +6,10 @@ description: Helper programs for setting up the Agda standard library. license: MIT tested-with: + GHC == 9.12.1 GHC == 9.10.1 - GHC == 9.8.2 - GHC == 9.6.5 + GHC == 9.8.4 + GHC == 9.6.6 GHC == 9.4.8 GHC == 9.2.8 GHC == 9.0.2 @@ -24,7 +25,7 @@ common common-build-parameters PatternSynonyms build-depends: - base >= 4.12.0.0 && < 4.21 + base >= 4.12.0.0 && < 4.22 , filemanip >= 0.3.6.2 && < 0.4 executable GenerateEverything