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