From 35ccdba3f9a6086163d0485dc58f25b98544262d Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Wed, 17 Jul 2024 18:57:53 +0800 Subject: [PATCH 1/3] Setup for v2.2 development --- CHANGELOG.md | 810 +----------------------------------- CHANGELOG/v2.1.md | 836 ++++++++++++++++++++++++++++++++++++++ agda-stdlib-utils.cabal | 2 +- standard-library.agda-lib | 2 +- 4 files changed, 839 insertions(+), 811 deletions(-) create mode 100644 CHANGELOG/v2.1.md diff --git a/CHANGELOG.md b/CHANGELOG.md index bb6e91c887..80da9ee48e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,4 @@ -Version 2.1-dev +Version 2.2-dev =============== The library has been tested using Agda 2.6.4.3. @@ -6,831 +6,23 @@ The library has been tested using Agda 2.6.4.3. Highlights ---------- -* The size of the dependency graph for many modules has been - reduced. This may lead to speed ups for first-time loading of some - modules. - -* Added bindings for file handles in `IO.Handle`. - -* Added bindings for random number generation in `System.Random` - -* Added support for 8-bit words and bytestrings in `Data.Word8` and `Data.ByteString`. - Bug-fixes --------- -* Fixed type of `toList-replicate` in `Data.Vec.Properties`, where `replicate` - was mistakenly applied to the level of the type `A` instead of the - variable `x` of type `A`. - -* Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer - incorrectly publicly exports the `Setoid` module under the alias `S`. - -* Removed unbound parameter from `length-alignWith`, - `alignWith-map` and `map-alignWith` in `Data.List.Properties`. - Non-backwards compatible changes -------------------------------- -* The recently added modules and (therefore their contents) in: - ```agda - Algebra.Module.Morphism.Structures - Algebra.Module.Morphism.Construct.Composition - Algebra.Module.Morphism.Construct.Identity - ``` - have been changed so they are now parametrized by _raw_ bundles rather - than lawful bundles. - This is in line with other modules that define morphisms. - As a result many of the `Composition` lemmas now take a proof of - transitivity and the `Identity` lemmas now take a proof of reflexivity. - -* The module `IO.Primitive` was moved to `IO.Primitive.Core`. - Minor improvements ------------------ -* The definition of the `Pointwise` relational combinator in - `Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise` - has been generalised to take heterogeneous arguments in `REL`. - -* The structures `IsSemilattice` and `IsBoundedSemilattice` in - `Algebra.Lattice.Structures` have been redefined as aliases of - `IsCommutativeBand` and `IsIdempotentMonoid` in `Algebra.Structures`. - Deprecated modules ------------------ -* All modules in the `Data.Word` hierarchy have been deprecated in favour - of their newly introduced counterparts in `Data.Word64`. - -* The module `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` - has been deprecated in favour of `Data.List.Relation.Binary.Sublist.Propositional.Slice`. - -* The modules - ``` - Function.Endomorphism.Propositional - Function.Endomorphism.Setoid - ``` - that used the old `Function` hierarchy have been deprecated in favour of: - ``` - Function.Endo.Propositional - Function.Endo.Setoid - ``` - Deprecated names ---------------- -* In `Algebra.Properties.Semiring.Mult`: - ```agda - 1×-identityʳ ↦ ×-homo-1 - ``` - -* In `Algebra.Structures.IsGroup`: - ```agda - _-_ ↦ _//_ - ``` - -* In `Algebra.Structures.Biased`: - ```agda - IsRing* ↦ Algebra.Structures.IsRing - isRing* ↦ Algebra.Structures.isRing - ``` - -* In `Data.Float.Base`: - ```agda - toWord ↦ toWord64 - ``` - -* In `Data.Float.Properties`: - ```agda - toWord-injective ↦ toWord64-injective - ``` - -* In `Data.List.Base`: - ```agda - scanr ↦ Data.List.Scans.Base.scanr - scanl ↦ Data.List.Scans.Base.scanl - ``` - -* In `Data.List.Properties`: - ```agda - scanr-defn ↦ Data.List.Scans.Properties.scanr-defn - scanl-defn ↦ Data.List.Scans.Properties.scanl-defn - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - map-compose ↦ map-∘ - ``` - -* In `Data.Maybe.Base`: - ```agda - decToMaybe ↦ Relation.Nullary.Decidable.Core.dec⇒maybe - ``` - -* In `Data.Nat.Base`: the following pattern synonyms and definitions are all - deprecated in favour of direct pattern matching on `Algebra.Definitions.RawMagma._∣ˡ_._,_` - ```agda - pattern less-than-or-equal {k} eq = k , eq - pattern ≤″-offset k = k , refl - pattern <″-offset k = k , refl - s≤″s⁻¹ - ``` - -* In `Data.Nat.Divisibility.Core`: - ```agda - *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ - ``` - -* In `Data.Sum`: - ```agda - fromDec ↦ Relation.Nullary.Decidable.Core.toSum - toDec ↦ Relation.Nullary.Decidable.Core.fromSum - ``` - -* In `IO.Base`: - ```agda - untilRight ↦ untilInj₂ - ``` - New modules ----------- -* Pointwise lifting of algebraic structures `IsX` and bundles `X` from - carrier set `C` to function space `A → C`: - ``` - Algebra.Construct.Pointwise - ``` - -* Raw bundles for module-like algebraic structures: - ``` - Algebra.Module.Bundles.Raw - ``` - -* Nagata's construction of the "idealization of a module": - ```agda - Algebra.Module.Construct.Idealization - ``` - -* The unique morphism from the initial, resp. terminal, algebra: - ```agda - Algebra.Morphism.Construct.Initial - Algebra.Morphism.Construct.Terminal - ``` - -* Bytestrings and builders: - ```agda - Data.Bytestring.Base - Data.Bytestring.Builder.Base - Data.Bytestring.Builder.Primitive - Data.Bytestring.IO - Data.Bytestring.IO.Primitive - Data.Bytestring.Primitive - ``` - -* Pointwise and equality relations over indexed containers: - ```agda - Data.Container.Indexed.Relation.Binary.Pointwise - Data.Container.Indexed.Relation.Binary.Pointwise.Properties - Data.Container.Indexed.Relation.Binary.Equality.Setoid - ``` - -* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: - ``` - Data.List.Scans.Base - Data.List.Scans.Properties - ``` - -* Various show modules for lists and vector types: - ```agda - Data.List.Show - Data.Vec.Show - Data.Vec.Bounded.Show - ``` - -* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): - ``` - Data.List.Relation.Binary.Equality.Setoid.Properties - ``` - -* Decidability for the subset relation on lists: - ```agda - Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_) - Data.List.Relation.Binary.Subset.DecPropositional - ``` - -* Decidability for the disjoint relation on lists: - ```agda - Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?) - Data.List.Relation.Binary.Disjoint.DecPropositional - ``` - -* Prime factorisation of natural numbers. - ```agda - Data.Nat.Primality.Factorisation - ``` - -* Permutations of vectors as functions: - ```agda - Data.Vec.Functional.Relation.Binary.Permutation - Data.Vec.Functional.Relation.Binary.Permutation.Properties - ``` - -* A type of bytes: - ```agda - Data.Word8.Primitive - Data.Word8.Base - Data.Word8.Literals - Data.Word8.Show - ``` - -* Word64 literals and bit-based functions: - ```agda - Data.Word64.Literals - Data.Word64.Unsafe - Data.Word64.Show - ``` - - -* Pointwise equality over functions - ``` - Function.Relation.Binary.Equality` - ``` - -* Consequences of 'infinite descent' for (accessible elements of) well-founded relations: - ```agda - Induction.InfiniteDescent - ``` - -* New IO primitives to handle buffering - ```agda - IO.Primitive.Handle - IO.Handle - ``` - -* Symmetric interior of a binary relation - ``` - Relation.Binary.Construct.Interior.Symmetric - ``` - -* Properties of `Setoid`s with decidable equality relation: - ``` - Relation.Binary.Properties.DecSetoid - ``` - -* Collection of results about recomputability in - ```agda - Relation.Nullary.Recomputable - ``` - with the main definition `Recomputable` exported publicly from `Relation.Nullary`. - -* New bindings to random numbers: - ```agda - System.Random.Primitive - System.Random - ``` - Additions to existing modules ----------------------------- - -* Added new definitions in `Algebra.Bundles`: - ```agda - record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ)) - record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ)) - ``` - and additional manifest fields for sub-bundles arising from these in: - ```agda - IdempotentCommutativeMonoid - IdempotentSemiring - ``` - -* Added new definition in `Algebra.Bundles.Raw` - ```agda - record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - ``` - -* Added new proofs in `Algebra.Construct.Terminal`: - ```agda - rawNearSemiring : RawNearSemiring c ℓ - nearSemiring : NearSemiring c ℓ - ``` - -* In `Algebra.Module.Bundles`, raw bundles are now re-exported and bundles - consistently expose their raw counterparts. - -* Added proofs in `Algebra.Module.Construct.DirectProduct`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - ``` - -* Added proofs in `Algebra.Module.Construct.TensorUnit`: - ```agda - rawLeftSemimodule : RawLeftSemimodule _ c ℓ - rawLeftModule : RawLeftModule _ c ℓ - rawRightSemimodule : RawRightSemimodule _ c ℓ - rawRightModule : RawRightModule _ c ℓ - rawBisemimodule : RawBisemimodule _ _ c ℓ - rawBimodule : RawBimodule _ _ c ℓ - rawSemimodule : RawSemimodule _ c ℓ - rawModule : RawModule _ c ℓ - ``` - -* Added proofs in `Algebra.Module.Construct.Zero`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R c ℓ - rawLeftModule : RawLeftModule R c ℓ - rawRightSemimodule : RawRightSemimodule R c ℓ - rawRightModule : RawRightModule R c ℓ - rawBisemimodule : RawBisemimodule R c ℓ - rawBimodule : RawBimodule R c ℓ - rawSemimodule : RawSemimodule R c ℓ - rawModule : RawModule R c ℓ - ``` - -* Added definitions in `Algebra.Morphism.Structures`: - ```agda - record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - - IsSemigroupHomomorphism : (A → B) → Set _ - IsSemigroupMonomorphism : (A → B) → Set _ - IsSemigroupIsomorphism : (A → B) → Set _ - ``` - -* Added proof in `Algebra.Properties.AbelianGroup`: - ``` - ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x - ``` - -* Added proofs in `Algebra.Properties.Group`: - ```agda - isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ - quasigroup : Quasigroup _ _ - isLoop : IsLoop _∙_ _\\_ _//_ ε - loop : Loop _ _ - - \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ - \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ - \\-leftDivides : LeftDivides _∙_ _\\_ - //-rightDividesˡ : RightDividesˡ _∙_ _//_ - //-rightDividesʳ : RightDividesʳ _∙_ _//_ - //-rightDivides : RightDivides _∙_ _//_ - - ⁻¹-selfInverse : SelfInverse _⁻¹ - x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y - x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε - \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ - comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x - ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x - ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x - ``` - -* Added new proofs in `Algebra.Properties.Loop`: - ```agda - identityˡ-unique : x ∙ y ≈ y → x ≈ ε - identityʳ-unique : x ∙ y ≈ x → y ≈ ε - identity-unique : Identity x _∙_ → x ≈ ε - ``` - -* Added new proofs in `Algebra.Properties.Monoid.Mult`: - ```agda - ×-homo-0 : 0 × x ≈ 0# - ×-homo-1 : 1 × x ≈ x - ``` - -* Added new proofs in `Algebra.Properties.Semiring.Mult`: - ```agda - ×-homo-0# : 0 × x ≈ 0# * x - ×-homo-1# : 1 × x ≈ 1# * x - idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x - ``` - -* Added new definitions to `Algebra.Structures`: - ```agda - record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ - record IsCommutativeBand (∙ : Op₂ A) : Set _ - record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set _ - ``` - -* Added new definitions in `IsGroup` record in `Algebra.Structures`: - ```agda - x // y = x ∙ (y ⁻¹) - x \\ y = (x ⁻¹) ∙ y - ``` - -* In `Algebra.Structures` added new proof to `IsCancellativeCommutativeSemiring` record: - ```agda - *-cancelʳ-nonZero : AlmostRightCancellative 0# * - ``` - -* In `Data.Bool.Show`: - ```agda - showBit : Bool → Char - ``` - -* In `Data.Container.Indexed.Core`: - ```agda - Subtrees o c = (r : Response c) → X (next c r) - ``` - -* In `Data.Empty`: - ```agda - ⊥-elim-irr : .⊥ → Whatever - ``` - -* In `Data.Fin.Properties`: - ```agda - nonZeroIndex : Fin n → ℕ.NonZero n - ``` - -* In `Data.Float.Base`: - ```agda - _≤_ : Rel Float _ - ``` - -* In `Data.Integer.Divisibility` introduced `divides` as an explicit pattern synonym - ```agda - pattern divides k eq = Data.Nat.Divisibility.divides k eq - ``` - -* In `Data.Integer.Properties`: - ```agda - ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n) - sign-* : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j - i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j) - ``` - -* In `Data.List.Base` added two new functions: - ```agda - Inits.tail : List A → List (List A) - Tails.tail : List A → List (List A) - ``` - and redefined `inits` and `tails` in terms of them. - -* In `Data.List.Membership.Propositional.Properties.Core`: - ```agda - find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p - ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p - ``` - -* In `Data.List.Membership.Setoid.Properties`: - ```agda - reverse⁺ : x ∈ xs → x ∈ reverse xs - reverse⁻ : x ∈ reverse xs → x ∈ xs - ``` - -* In `Data.List.Properties`: - ```agda - length-catMaybes : length (catMaybes xs) ≤ length xs - applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) - applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n) - upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n) - downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n) - reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse - reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n - reverse-upTo : reverse (upTo n) ≡ downFrom n - reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n - reverse-downFrom : reverse (downFrom n) ≡ upTo n - mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g) - map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f) - align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys) - zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys) - unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g) - map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f) - unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip - splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n - uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons - last-map : last ∘ map f ≗ map f ∘ last - tail-map : tail ∘ map f ≗ map (map f) ∘ tail - mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g - zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as - unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g - foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x - alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs - alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs - align-flip : align xs ys ≡ map swap (align ys xs) - zip-flip : zip xs ys ≡ map swap (zip ys xs) - unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f - unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip - take-take : take n (take m xs) ≡ take (n ⊓ m) xs - take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs) - zip-unzip : uncurry′ zip ∘ unzip ≗ id - unzipWith-zipWith : f ∘ uncurry′ g ≗ id → - length xs ≡ length ys → - unzipWith f (zipWith g xs ys) ≡ (xs , ys) - unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys) - mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys - unzipWith-++ : unzipWith f (xs ++ ys) ≡ - zip _++_ _++_ (unzipWith f xs) (unzipWith f ys) - catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe - catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys - map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) - Any-catMaybes⁺ : Any (M.Any P) xs → Any P (catMaybes xs) - mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs - mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ [] - mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs - mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ [] - ``` - -* In `Data.List.Relation.Binary.Pointwise.Base`: - ```agda - unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S) - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid`: - ```agda - ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: - ```agda - ⊆-trans-idˡ : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs - ⊆-trans-idʳ : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs - ⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) → - trans p (trans q r) ≡ trans (trans p q) r) → - (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) → - ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs - ``` - -* In `Data.List.Relation.Unary.All`: - ```agda - universal-U : Universal (All U) - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) - Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) - ``` - -* In `Data.List.Relation.Unary.AllPairs.Properties`: - ```agda - catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs) - tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f) - ``` - -* In `Data.List.Relation.Unary.Any.Properties`: - ```agda - map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) → - (p : Any P xs) → Any.map f p ≡ Any.map g p - ``` - -* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - product-↭ : product Preserves _↭_ ⟶ _≡_ - catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys - mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys - ``` - -* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`: - ```agda - catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys - mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys - ``` - -* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: - ```agda - map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs - - reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs - reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs - reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs - ``` - -* Added new proofs to `Data.List.Relation.Binary.Sublist.Propositional.Slice`: - ```agda - ⊆-upper-bound-is-cospan : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → IsCospan (⊆-upper-bound τ₁ τ₂) - ⊆-upper-bound-cospan : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Cospan τ₁ τ₂ - ``` - -* In `Data.List.Relation.Ternary.Appending.Setoid.Properties`: - ```agda - through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs → - ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs - through← : ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs → - ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs - assoc→ : ∃[ xs ] Appending as bs xs × Appending xs cs ds → - ∃[ ys ] Appending bs cs ys × Appending as ys ds - ``` - -* In `Data.List.Relation.Ternary.Appending.Properties`: - ```agda - through→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → - ∃[ xs ] Pointwise U as xs × Appending V R xs bs cs → - ∃[ ys ] Appending W S as bs ys × Pointwise T ys cs - through← : ((R ; S) ⇒ T) → ((U ; S) ⇒ (V ; W)) → - ∃[ ys ] Appending U R as bs ys × Pointwise S ys cs → - ∃[ xs ] Pointwise V as xs × Appending W T xs bs cs - assoc→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → ((Y ; V) ⇒ X) → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds - assoc← : ((S ; T) ⇒ R) → ((W ; T) ⇒ (U ; V)) → (X ⇒ (Y ; V)) → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds - ``` - -* In `Data.List.NonEmpty.Base`: - ```agda - inits : List A → List⁺ (List A) - tails : List A → List⁺ (List A) - ``` - -* In `Data.List.NonEmpty.Properties`: - ```agda - toList-inits : toList ∘ List⁺.inits ≗ List.inits - toList-tails : toList ∘ List⁺.tails ≗ List.tails - ``` - -* In `Data.Maybe.Relation.Binary.Pointwise`: - ```agda - pointwise⊆any : Pointwise R (just x) ⊆ Any (R x) - ``` - -* In `Data.Nat.Divisibility`: - ```agda - quotient≢0 : m ∣ n → .{{NonZero n}} → NonZero quotient - - m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m - m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient - quotient-∣ : m ∣ n → quotient ∣ n - quotient>1 : m ∣ n → m < n → 1 < quotient - quotient-< : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n - n/m≡quotient : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient - - m/n≡0⇒m⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n - productOfPrimes≢0 : All Prime as → NonZero (product as) - productOfPrimes≥1 : All Prime as → product as ≥ 1 - ``` - -* Added new proofs in `Data.Nat.Properties`: - ```agda - m≤n+o⇒m∸n≤o : m ≤ n + o → m ∸ n ≤ o - m>_ : IO A → IO B → IO B - ``` - -* Added new definition in `Relation.Binary.Construct.Closure.Transitive` - ```agda - transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_ - ``` - -* Added new proofs in `Relation.Binary.Construct.Composition`: - ```agda - transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈ - ``` - -* Added new definitions in `Relation.Binary.Definitions` - ```agda - Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y) - Empty _∼_ = ∀ {x y} → ¬ (x ∼ y) - ``` - -* Added new proofs in `Relation.Binary.Properties.Setoid`: - ```agda - ≉-irrefl : Irreflexive _≈_ _≉_ - ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ - ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ - ``` - -* Added new definitions in `Relation.Nullary` - ```agda - Recomputable : Set _ - WeaklyDecidable : Set _ - ``` - -* Added new proof in `Relation.Nullary.Decidable`: - ```agda - ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋ - ``` - -* Added new definitions and proofs in `Relation.Nullary.Decidable.Core`: - ```agda - dec⇒maybe : Dec A → Maybe A - recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q - toSum : Dec A → A ⊎ ¬ A - fromSum : A ⊎ ¬ A → Dec A - ``` - -* Added new definitions in `Relation.Nullary.Negation.Core`: - ```agda - contradiction-irr : .A → ¬ A → Whatever - ``` - -* Added new definitions in `Relation.Nullary.Reflects`: - ```agda - recompute : Reflects A b → Recomputable A - recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q - ``` - -* Added new definitions in `Relation.Unary`: - ```agda - Stable : Pred A ℓ → Set _ - WeaklyDecidable : Pred A ℓ → Set _ - ``` - -* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details. - - Provide a marker function, `⌞_⌟`, for user-guided anti-unification. - - Improved support for equalities between terms with instance arguments, - such as terms that contain `_/_` or `_%_`. diff --git a/CHANGELOG/v2.1.md b/CHANGELOG/v2.1.md new file mode 100644 index 0000000000..bb6e91c887 --- /dev/null +++ b/CHANGELOG/v2.1.md @@ -0,0 +1,836 @@ +Version 2.1-dev +=============== + +The library has been tested using Agda 2.6.4.3. + +Highlights +---------- + +* The size of the dependency graph for many modules has been + reduced. This may lead to speed ups for first-time loading of some + modules. + +* Added bindings for file handles in `IO.Handle`. + +* Added bindings for random number generation in `System.Random` + +* Added support for 8-bit words and bytestrings in `Data.Word8` and `Data.ByteString`. + +Bug-fixes +--------- + +* Fixed type of `toList-replicate` in `Data.Vec.Properties`, where `replicate` + was mistakenly applied to the level of the type `A` instead of the + variable `x` of type `A`. + +* Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer + incorrectly publicly exports the `Setoid` module under the alias `S`. + +* Removed unbound parameter from `length-alignWith`, + `alignWith-map` and `map-alignWith` in `Data.List.Properties`. + +Non-backwards compatible changes +-------------------------------- + +* The recently added modules and (therefore their contents) in: + ```agda + Algebra.Module.Morphism.Structures + Algebra.Module.Morphism.Construct.Composition + Algebra.Module.Morphism.Construct.Identity + ``` + have been changed so they are now parametrized by _raw_ bundles rather + than lawful bundles. + This is in line with other modules that define morphisms. + As a result many of the `Composition` lemmas now take a proof of + transitivity and the `Identity` lemmas now take a proof of reflexivity. + +* The module `IO.Primitive` was moved to `IO.Primitive.Core`. + +Minor improvements +------------------ + +* The definition of the `Pointwise` relational combinator in + `Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise` + has been generalised to take heterogeneous arguments in `REL`. + +* The structures `IsSemilattice` and `IsBoundedSemilattice` in + `Algebra.Lattice.Structures` have been redefined as aliases of + `IsCommutativeBand` and `IsIdempotentMonoid` in `Algebra.Structures`. + +Deprecated modules +------------------ + +* All modules in the `Data.Word` hierarchy have been deprecated in favour + of their newly introduced counterparts in `Data.Word64`. + +* The module `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` + has been deprecated in favour of `Data.List.Relation.Binary.Sublist.Propositional.Slice`. + +* The modules + ``` + Function.Endomorphism.Propositional + Function.Endomorphism.Setoid + ``` + that used the old `Function` hierarchy have been deprecated in favour of: + ``` + Function.Endo.Propositional + Function.Endo.Setoid + ``` + +Deprecated names +---------------- + +* In `Algebra.Properties.Semiring.Mult`: + ```agda + 1×-identityʳ ↦ ×-homo-1 + ``` + +* In `Algebra.Structures.IsGroup`: + ```agda + _-_ ↦ _//_ + ``` + +* In `Algebra.Structures.Biased`: + ```agda + IsRing* ↦ Algebra.Structures.IsRing + isRing* ↦ Algebra.Structures.isRing + ``` + +* In `Data.Float.Base`: + ```agda + toWord ↦ toWord64 + ``` + +* In `Data.Float.Properties`: + ```agda + toWord-injective ↦ toWord64-injective + ``` + +* In `Data.List.Base`: + ```agda + scanr ↦ Data.List.Scans.Base.scanr + scanl ↦ Data.List.Scans.Base.scanl + ``` + +* In `Data.List.Properties`: + ```agda + scanr-defn ↦ Data.List.Scans.Properties.scanr-defn + scanl-defn ↦ Data.List.Scans.Properties.scanl-defn + ``` + +* In `Data.List.Relation.Unary.All.Properties`: + ```agda + map-compose ↦ map-∘ + ``` + +* In `Data.Maybe.Base`: + ```agda + decToMaybe ↦ Relation.Nullary.Decidable.Core.dec⇒maybe + ``` + +* In `Data.Nat.Base`: the following pattern synonyms and definitions are all + deprecated in favour of direct pattern matching on `Algebra.Definitions.RawMagma._∣ˡ_._,_` + ```agda + pattern less-than-or-equal {k} eq = k , eq + pattern ≤″-offset k = k , refl + pattern <″-offset k = k , refl + s≤″s⁻¹ + ``` + +* In `Data.Nat.Divisibility.Core`: + ```agda + *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ + ``` + +* In `Data.Sum`: + ```agda + fromDec ↦ Relation.Nullary.Decidable.Core.toSum + toDec ↦ Relation.Nullary.Decidable.Core.fromSum + ``` + +* In `IO.Base`: + ```agda + untilRight ↦ untilInj₂ + ``` + +New modules +----------- + +* Pointwise lifting of algebraic structures `IsX` and bundles `X` from + carrier set `C` to function space `A → C`: + ``` + Algebra.Construct.Pointwise + ``` + +* Raw bundles for module-like algebraic structures: + ``` + Algebra.Module.Bundles.Raw + ``` + +* Nagata's construction of the "idealization of a module": + ```agda + Algebra.Module.Construct.Idealization + ``` + +* The unique morphism from the initial, resp. terminal, algebra: + ```agda + Algebra.Morphism.Construct.Initial + Algebra.Morphism.Construct.Terminal + ``` + +* Bytestrings and builders: + ```agda + Data.Bytestring.Base + Data.Bytestring.Builder.Base + Data.Bytestring.Builder.Primitive + Data.Bytestring.IO + Data.Bytestring.IO.Primitive + Data.Bytestring.Primitive + ``` + +* Pointwise and equality relations over indexed containers: + ```agda + Data.Container.Indexed.Relation.Binary.Pointwise + Data.Container.Indexed.Relation.Binary.Pointwise.Properties + Data.Container.Indexed.Relation.Binary.Equality.Setoid + ``` + +* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: + ``` + Data.List.Scans.Base + Data.List.Scans.Properties + ``` + +* Various show modules for lists and vector types: + ```agda + Data.List.Show + Data.Vec.Show + Data.Vec.Bounded.Show + ``` + +* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): + ``` + Data.List.Relation.Binary.Equality.Setoid.Properties + ``` + +* Decidability for the subset relation on lists: + ```agda + Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_) + Data.List.Relation.Binary.Subset.DecPropositional + ``` + +* Decidability for the disjoint relation on lists: + ```agda + Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?) + Data.List.Relation.Binary.Disjoint.DecPropositional + ``` + +* Prime factorisation of natural numbers. + ```agda + Data.Nat.Primality.Factorisation + ``` + +* Permutations of vectors as functions: + ```agda + Data.Vec.Functional.Relation.Binary.Permutation + Data.Vec.Functional.Relation.Binary.Permutation.Properties + ``` + +* A type of bytes: + ```agda + Data.Word8.Primitive + Data.Word8.Base + Data.Word8.Literals + Data.Word8.Show + ``` + +* Word64 literals and bit-based functions: + ```agda + Data.Word64.Literals + Data.Word64.Unsafe + Data.Word64.Show + ``` + + +* Pointwise equality over functions + ``` + Function.Relation.Binary.Equality` + ``` + +* Consequences of 'infinite descent' for (accessible elements of) well-founded relations: + ```agda + Induction.InfiniteDescent + ``` + +* New IO primitives to handle buffering + ```agda + IO.Primitive.Handle + IO.Handle + ``` + +* Symmetric interior of a binary relation + ``` + Relation.Binary.Construct.Interior.Symmetric + ``` + +* Properties of `Setoid`s with decidable equality relation: + ``` + Relation.Binary.Properties.DecSetoid + ``` + +* Collection of results about recomputability in + ```agda + Relation.Nullary.Recomputable + ``` + with the main definition `Recomputable` exported publicly from `Relation.Nullary`. + +* New bindings to random numbers: + ```agda + System.Random.Primitive + System.Random + ``` + +Additions to existing modules +----------------------------- + +* Added new definitions in `Algebra.Bundles`: + ```agda + record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) + record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ)) + record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ)) + ``` + and additional manifest fields for sub-bundles arising from these in: + ```agda + IdempotentCommutativeMonoid + IdempotentSemiring + ``` + +* Added new definition in `Algebra.Bundles.Raw` + ```agda + record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) + ``` + +* Added new proofs in `Algebra.Construct.Terminal`: + ```agda + rawNearSemiring : RawNearSemiring c ℓ + nearSemiring : NearSemiring c ℓ + ``` + +* In `Algebra.Module.Bundles`, raw bundles are now re-exported and bundles + consistently expose their raw counterparts. + +* Added proofs in `Algebra.Module.Construct.DirectProduct`: + ```agda + rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) + rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) + ``` + +* Added proofs in `Algebra.Module.Construct.TensorUnit`: + ```agda + rawLeftSemimodule : RawLeftSemimodule _ c ℓ + rawLeftModule : RawLeftModule _ c ℓ + rawRightSemimodule : RawRightSemimodule _ c ℓ + rawRightModule : RawRightModule _ c ℓ + rawBisemimodule : RawBisemimodule _ _ c ℓ + rawBimodule : RawBimodule _ _ c ℓ + rawSemimodule : RawSemimodule _ c ℓ + rawModule : RawModule _ c ℓ + ``` + +* Added proofs in `Algebra.Module.Construct.Zero`: + ```agda + rawLeftSemimodule : RawLeftSemimodule R c ℓ + rawLeftModule : RawLeftModule R c ℓ + rawRightSemimodule : RawRightSemimodule R c ℓ + rawRightModule : RawRightModule R c ℓ + rawBisemimodule : RawBisemimodule R c ℓ + rawBimodule : RawBimodule R c ℓ + rawSemimodule : RawSemimodule R c ℓ + rawModule : RawModule R c ℓ + ``` + +* Added definitions in `Algebra.Morphism.Structures`: + ```agda + record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + + IsSemigroupHomomorphism : (A → B) → Set _ + IsSemigroupMonomorphism : (A → B) → Set _ + IsSemigroupIsomorphism : (A → B) → Set _ + ``` + +* Added proof in `Algebra.Properties.AbelianGroup`: + ``` + ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x + ``` + +* Added proofs in `Algebra.Properties.Group`: + ```agda + isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ + quasigroup : Quasigroup _ _ + isLoop : IsLoop _∙_ _\\_ _//_ ε + loop : Loop _ _ + + \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ + \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ + \\-leftDivides : LeftDivides _∙_ _\\_ + //-rightDividesˡ : RightDividesˡ _∙_ _//_ + //-rightDividesʳ : RightDividesʳ _∙_ _//_ + //-rightDivides : RightDivides _∙_ _//_ + + ⁻¹-selfInverse : SelfInverse _⁻¹ + x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y + x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε + \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ + comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x + ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x + ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x + ``` + +* Added new proofs in `Algebra.Properties.Loop`: + ```agda + identityˡ-unique : x ∙ y ≈ y → x ≈ ε + identityʳ-unique : x ∙ y ≈ x → y ≈ ε + identity-unique : Identity x _∙_ → x ≈ ε + ``` + +* Added new proofs in `Algebra.Properties.Monoid.Mult`: + ```agda + ×-homo-0 : 0 × x ≈ 0# + ×-homo-1 : 1 × x ≈ x + ``` + +* Added new proofs in `Algebra.Properties.Semiring.Mult`: + ```agda + ×-homo-0# : 0 × x ≈ 0# * x + ×-homo-1# : 1 × x ≈ 1# * x + idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x + ``` + +* Added new definitions to `Algebra.Structures`: + ```agda + record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ + record IsCommutativeBand (∙ : Op₂ A) : Set _ + record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set _ + ``` + +* Added new definitions in `IsGroup` record in `Algebra.Structures`: + ```agda + x // y = x ∙ (y ⁻¹) + x \\ y = (x ⁻¹) ∙ y + ``` + +* In `Algebra.Structures` added new proof to `IsCancellativeCommutativeSemiring` record: + ```agda + *-cancelʳ-nonZero : AlmostRightCancellative 0# * + ``` + +* In `Data.Bool.Show`: + ```agda + showBit : Bool → Char + ``` + +* In `Data.Container.Indexed.Core`: + ```agda + Subtrees o c = (r : Response c) → X (next c r) + ``` + +* In `Data.Empty`: + ```agda + ⊥-elim-irr : .⊥ → Whatever + ``` + +* In `Data.Fin.Properties`: + ```agda + nonZeroIndex : Fin n → ℕ.NonZero n + ``` + +* In `Data.Float.Base`: + ```agda + _≤_ : Rel Float _ + ``` + +* In `Data.Integer.Divisibility` introduced `divides` as an explicit pattern synonym + ```agda + pattern divides k eq = Data.Nat.Divisibility.divides k eq + ``` + +* In `Data.Integer.Properties`: + ```agda + ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n) + sign-* : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j + i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j) + ``` + +* In `Data.List.Base` added two new functions: + ```agda + Inits.tail : List A → List (List A) + Tails.tail : List A → List (List A) + ``` + and redefined `inits` and `tails` in terms of them. + +* In `Data.List.Membership.Propositional.Properties.Core`: + ```agda + find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p + ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p + ``` + +* In `Data.List.Membership.Setoid.Properties`: + ```agda + reverse⁺ : x ∈ xs → x ∈ reverse xs + reverse⁻ : x ∈ reverse xs → x ∈ xs + ``` + +* In `Data.List.Properties`: + ```agda + length-catMaybes : length (catMaybes xs) ≤ length xs + applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) + applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n) + upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n) + downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n) + reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse + reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n + reverse-upTo : reverse (upTo n) ≡ downFrom n + reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n + reverse-downFrom : reverse (downFrom n) ≡ upTo n + mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g) + map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f) + align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys) + zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys) + unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g) + map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f) + unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip + splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n + uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons + last-map : last ∘ map f ≗ map f ∘ last + tail-map : tail ∘ map f ≗ map (map f) ∘ tail + mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g + zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as + unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g + foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x + alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs + alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs + align-flip : align xs ys ≡ map swap (align ys xs) + zip-flip : zip xs ys ≡ map swap (zip ys xs) + unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f + unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip + take-take : take n (take m xs) ≡ take (n ⊓ m) xs + take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs) + zip-unzip : uncurry′ zip ∘ unzip ≗ id + unzipWith-zipWith : f ∘ uncurry′ g ≗ id → + length xs ≡ length ys → + unzipWith f (zipWith g xs ys) ≡ (xs , ys) + unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys) + mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys + unzipWith-++ : unzipWith f (xs ++ ys) ≡ + zip _++_ _++_ (unzipWith f xs) (unzipWith f ys) + catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe + catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys + map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) + Any-catMaybes⁺ : Any (M.Any P) xs → Any P (catMaybes xs) + mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs + mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ [] + mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs + mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ [] + ``` + +* In `Data.List.Relation.Binary.Pointwise.Base`: + ```agda + unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S) + ``` + +* In `Data.List.Relation.Binary.Sublist.Setoid`: + ```agda + ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ + ``` + +* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: + ```agda + ⊆-trans-idˡ : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) → + (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs + ⊆-trans-idʳ : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) → + (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs + ⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) → + trans p (trans q r) ≡ trans (trans p q) r) → + (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) → + ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs + ``` + +* In `Data.List.Relation.Unary.All`: + ```agda + universal-U : Universal (All U) + ``` + +* In `Data.List.Relation.Unary.All.Properties`: + ```agda + All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) + Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) + ``` + +* In `Data.List.Relation.Unary.AllPairs.Properties`: + ```agda + catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs) + tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f) + ``` + +* In `Data.List.Relation.Unary.Any.Properties`: + ```agda + map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) → + (p : Any P xs) → Any.map f p ≡ Any.map g p + ``` + +* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: + ```agda + product-↭ : product Preserves _↭_ ⟶ _≡_ + catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys + mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys + ``` + +* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`: + ```agda + catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys + mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys + ``` + +* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: + ```agda + map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs + + reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs + reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs + reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs + ``` + +* Added new proofs to `Data.List.Relation.Binary.Sublist.Propositional.Slice`: + ```agda + ⊆-upper-bound-is-cospan : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → IsCospan (⊆-upper-bound τ₁ τ₂) + ⊆-upper-bound-cospan : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Cospan τ₁ τ₂ + ``` + +* In `Data.List.Relation.Ternary.Appending.Setoid.Properties`: + ```agda + through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs → + ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs + through← : ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs → + ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs + assoc→ : ∃[ xs ] Appending as bs xs × Appending xs cs ds → + ∃[ ys ] Appending bs cs ys × Appending as ys ds + ``` + +* In `Data.List.Relation.Ternary.Appending.Properties`: + ```agda + through→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → + ∃[ xs ] Pointwise U as xs × Appending V R xs bs cs → + ∃[ ys ] Appending W S as bs ys × Pointwise T ys cs + through← : ((R ; S) ⇒ T) → ((U ; S) ⇒ (V ; W)) → + ∃[ ys ] Appending U R as bs ys × Pointwise S ys cs → + ∃[ xs ] Pointwise V as xs × Appending W T xs bs cs + assoc→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → ((Y ; V) ⇒ X) → + ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds → + ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds + assoc← : ((S ; T) ⇒ R) → ((W ; T) ⇒ (U ; V)) → (X ⇒ (Y ; V)) → + ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds → + ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds + ``` + +* In `Data.List.NonEmpty.Base`: + ```agda + inits : List A → List⁺ (List A) + tails : List A → List⁺ (List A) + ``` + +* In `Data.List.NonEmpty.Properties`: + ```agda + toList-inits : toList ∘ List⁺.inits ≗ List.inits + toList-tails : toList ∘ List⁺.tails ≗ List.tails + ``` + +* In `Data.Maybe.Relation.Binary.Pointwise`: + ```agda + pointwise⊆any : Pointwise R (just x) ⊆ Any (R x) + ``` + +* In `Data.Nat.Divisibility`: + ```agda + quotient≢0 : m ∣ n → .{{NonZero n}} → NonZero quotient + + m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m + m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient + quotient-∣ : m ∣ n → quotient ∣ n + quotient>1 : m ∣ n → m < n → 1 < quotient + quotient-< : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n + n/m≡quotient : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient + + m/n≡0⇒m⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n + productOfPrimes≢0 : All Prime as → NonZero (product as) + productOfPrimes≥1 : All Prime as → product as ≥ 1 + ``` + +* Added new proofs in `Data.Nat.Properties`: + ```agda + m≤n+o⇒m∸n≤o : m ≤ n + o → m ∸ n ≤ o + m>_ : IO A → IO B → IO B + ``` + +* Added new definition in `Relation.Binary.Construct.Closure.Transitive` + ```agda + transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_ + ``` + +* Added new proofs in `Relation.Binary.Construct.Composition`: + ```agda + transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈ + ``` + +* Added new definitions in `Relation.Binary.Definitions` + ```agda + Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y) + Empty _∼_ = ∀ {x y} → ¬ (x ∼ y) + ``` + +* Added new proofs in `Relation.Binary.Properties.Setoid`: + ```agda + ≉-irrefl : Irreflexive _≈_ _≉_ + ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ + ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ + ``` + +* Added new definitions in `Relation.Nullary` + ```agda + Recomputable : Set _ + WeaklyDecidable : Set _ + ``` + +* Added new proof in `Relation.Nullary.Decidable`: + ```agda + ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋ + ``` + +* Added new definitions and proofs in `Relation.Nullary.Decidable.Core`: + ```agda + dec⇒maybe : Dec A → Maybe A + recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q + toSum : Dec A → A ⊎ ¬ A + fromSum : A ⊎ ¬ A → Dec A + ``` + +* Added new definitions in `Relation.Nullary.Negation.Core`: + ```agda + contradiction-irr : .A → ¬ A → Whatever + ``` + +* Added new definitions in `Relation.Nullary.Reflects`: + ```agda + recompute : Reflects A b → Recomputable A + recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q + ``` + +* Added new definitions in `Relation.Unary`: + ```agda + Stable : Pred A ℓ → Set _ + WeaklyDecidable : Pred A ℓ → Set _ + ``` + +* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details. + - Provide a marker function, `⌞_⌟`, for user-guided anti-unification. + - Improved support for equalities between terms with instance arguments, + such as terms that contain `_/_` or `_%_`. diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal index d9fe1dc676..1c37c72fca 100644 --- a/agda-stdlib-utils.cabal +++ b/agda-stdlib-utils.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: agda-stdlib-utils -version: 2.1 +version: 2.2 build-type: Simple description: Helper programs for setting up the Agda standard library. license: MIT diff --git a/standard-library.agda-lib b/standard-library.agda-lib index ba7ae571b9..70de155938 100644 --- a/standard-library.agda-lib +++ b/standard-library.agda-lib @@ -1,4 +1,4 @@ -name: standard-library-2.1 +name: standard-library-2.2 include: src flags: --warning=noUnsupportedIndexedMatch From a88b649c78d8566184f2cc28395ac47991a804aa Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Wed, 17 Jul 2024 19:02:51 +0800 Subject: [PATCH 2/3] Fix missing updates --- CITATION.cff | 4 ++-- doc/installation-guide.md | 12 ++++++------ 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/CITATION.cff b/CITATION.cff index 5e965d00fa..96507925e9 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below." authors: - name: "The Agda Community" title: "Agda Standard Library" -version: 2.0 -date-released: 2023-12-11 +version: 2.1 +date-released: 2024-07-17 url: "https://github.com/agda/agda-stdlib" \ No newline at end of file diff --git a/doc/installation-guide.md b/doc/installation-guide.md index 956fc317db..2abf13aa29 100644 --- a/doc/installation-guide.md +++ b/doc/installation-guide.md @@ -3,19 +3,19 @@ Installation instructions Note: the full story on installing Agda libraries can be found at [readthedocs](http://agda.readthedocs.io/en/latest/tools/package-system.html). -Use version v2.0 of the standard library with Agda 2.6.4 or 2.6.4.1. +Use version v2.1 of the standard library with Agda 2.6.4.X. 1. Navigate to a suitable directory `$HERE` (replace appropriately) where you would like to install the library. -2. Download the tarball of v2.0 of the standard library. This can either be +2. Download the tarball of v2.1 of the standard library. This can either be done manually by visiting the Github repository for the library, or via the command line as follows: ``` - wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.0.tar.gz + wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.1.tar.gz ``` Note that you can replace `wget` with other popular tools such as `curl` and that - you can replace `2.0` with any other version of the library you desire. + you can replace `2.1` with any other version of the library you desire. 3. Extract the standard library from the tarball. Again this can either be done manually or via the command line as follows: @@ -26,7 +26,7 @@ Use version v2.0 of the standard library with Agda 2.6.4 or 2.6.4.1. 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run the commands to install via cabal: ``` - cd agda-stdlib-2.0 + cd agda-stdlib-2.1 cabal install ``` @@ -40,7 +40,7 @@ Use version v2.0 of the standard library with Agda 2.6.4 or 2.6.4.1. 6. Register the standard library with Agda's package system by adding the following line to `$HOME/.agda/libraries`: ``` - $HERE/agda-stdlib-2.0/standard-library.agda-lib + $HERE/agda-stdlib-2.1/standard-library.agda-lib ``` Now, the standard library is ready to be used either: From c70f6b2f6d25d203cd8aa7cc33a3ad12b4ba521b Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sat, 27 Jul 2024 10:54:55 +0800 Subject: [PATCH 3/3] Update CHANGELOG/v2.1.md Co-authored-by: G. Allais --- CHANGELOG/v2.1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG/v2.1.md b/CHANGELOG/v2.1.md index bb6e91c887..1f6d6b0a3a 100644 --- a/CHANGELOG/v2.1.md +++ b/CHANGELOG/v2.1.md @@ -1,4 +1,4 @@ -Version 2.1-dev +Version 2.1 =============== The library has been tested using Agda 2.6.4.3.