diff --git a/CHANGELOG/v2.3.md b/CHANGELOG/v2.3.md new file mode 100644 index 0000000000..5d03548df1 --- /dev/null +++ b/CHANGELOG/v2.3.md @@ -0,0 +1,615 @@ +Version 2.3 +=========== + +The library has been tested using Agda 2.7.0 and 2.8.0. + +Bug-fixes +--------- + +* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` + to `#-sym` in order to avoid overloaded projection. + `irrefl` and `cotrans` are similarly renamed for the sake of consistency. + +* In `Algebra.Definitions.RawMagma` and `Relation.Binary.Construct.Interior.Symmetric`, + the record constructors `_,_` incorrectly had no declared fixity. They have been given + the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`. + +* In `Data.Product.Function.Dependent.Setoid`, `left-inverse` defined a + `RightInverse`. + This has been deprecated in favor or `rightInverse`, and a corrected (and + correctly-named) function `leftInverse` has been added. + +* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` + has been modified to correctly support equational reasoning at the beginning and the end. + The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors + of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps + are changed, this modification is non-backwards compatible. + +* The implementation of `≤-total` in `Data.Nat.Properties` used to use recursion + making it infeasibly slow for even relatively small natural numbers. It's definition + has been altered to use operations backed by primitives making it + significantly faster. However, its reduction behaviour on open terms may have + changed in some limited circumstances. + +Deprecated names +---------------- + +* In `Algebra.Definitions.RawMagma`: + ```agda + _∣∣_ ↦ _∥_ + _∤∤_ ↦ _∦_ + ``` + +* In `Algebra.Lattice.Properties.BooleanAlgebra` + ```agda + ⊥≉⊤ ↦ ¬⊥≈⊤ + ⊤≉⊥ ↦ ¬⊤≈⊥ + ``` + +* In `Algebra.Module.Consequences` + ```agda + *ₗ-assoc+comm⇒*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ᵣ-assoc + *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc + *ᵣ-assoc+comm⇒*ₗ-assoc ↦ *ᵣ-assoc∧comm⇒*ₗ-assoc + *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc + ``` + +* In `Algebra.Modules.Structures.IsLeftModule`: + ```agda + uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ + uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ + ``` + +* In `Algebra.Modules.Structures.IsRightModule`: + ```agda + uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ + uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ + ``` + +* In `Algebra.Properties.Magma.Divisibility`: + ```agda + ∣∣-sym ↦ ∥-sym + ∣∣-respˡ-≈ ↦ ∥-respˡ-≈ + ∣∣-respʳ-≈ ↦ ∥-respʳ-≈ + ∣∣-resp-≈ ↦ ∥-resp-≈ + ∤∤-sym -≈ ↦ ∦-sym + ∤∤-respˡ-≈ ↦ ∦-respˡ-≈ + ∤∤-respʳ-≈ ↦ ∦-respʳ-≈ + ∤∤-resp-≈ ↦ ∦-resp-≈ + ∣-respʳ-≈ ↦ ∣ʳ-respʳ-≈ + ∣-respˡ-≈ ↦ ∣ʳ-respˡ-≈ + ∣-resp-≈ ↦ ∣ʳ-resp-≈ + x∣yx ↦ x∣ʳyx + xy≈z⇒y∣z ↦ xy≈z⇒y∣ʳz + ``` + +* In `Algebra.Properties.Monoid.Divisibility`: + ```agda + ∣∣-refl ↦ ∥-refl + ∣∣-reflexive ↦ ∥-reflexive + ∣∣-isEquivalence ↦ ∥-isEquivalence + ε∣_ ↦ ε∣ʳ_ + ∣-refl ↦ ∣ʳ-refl + ∣-reflexive ↦ ∣ʳ-reflexive + ∣-isPreorder ↦ ∣ʳ-isPreorder + ∣-preorder ↦ ∣ʳ-preorder + ``` + +* In `Algebra.Properties.Semigroup.Divisibility`: + ```agda + ∣∣-trans ↦ ∥-trans + ∣-trans ↦ ∣ʳ-trans + ``` + +* In `Algebra.Structures.Group`: + ```agda + uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique + uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique + ``` + +* In `Data.List.Base`: + ```agda + and ↦ Data.Bool.ListAction.and + or ↦ Data.Bool.ListAction.or + any ↦ Data.Bool.ListAction.any + all ↦ Data.Bool.ListAction.all + sum ↦ Data.Nat.ListAction.sum + product ↦ Data.Nat.ListAction.product + ``` + +* In `Data.List.Properties`: + ```agda + sum-++ ↦ Data.Nat.ListAction.Properties.sum-++ + ∈⇒∣product ↦ Data.Nat.ListAction.Properties.∈⇒∣product + product≢0 ↦ Data.Nat.ListAction.Properties.product≢0 + ∈⇒≤product ↦ Data.Nat.ListAction.Properties.∈⇒≤product + ∷-ʳ++-eqFree ↦ Data.List.Properties.ʳ++-ʳ++-eqFree + ``` + +* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: + ```agda + sum-↭ ↦ Data.Nat.ListAction.Properties.sum-↭ + product-↭ ↦ Data.Nat.ListAction.Properties.product-↭ + ``` + +* In `Data.Product.Function.Dependent.Setoid`: + ```agda + left-inverse ↦ rightInverse + ``` + +* In `Data.Product.Nary.NonDependent`: + ```agda + Allₙ ↦ Pointwiseₙ + ``` + +New modules +----------- + +* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`. + +* `Algebra.Morphism.Construct.DirectProduct`. + +* `Data.Bool.ListAction` - a new location for the lifted specialised list operations `Data.List.Base.{and|or|any|all}`. + +* `Data.Nat.ListAction(.Properties)` - a new location for the definitions and properties of `Data.List.Base.{sum|product}`. + +* `Data.List.Relation.Binary.Prefix.Propositional.Properties`. + +* `Data.List.Relation.Binary.Suffix.Propositional.Properties`. + +* `Data.List.Sort.InsertionSort(.{Base|Properties})` - defines insertion sort and proves properties of insertion sort. + +* `Data.List.Sort.MergeSort(.{Base|Properties})` - a refactor of the previous `Data.List.Sort.MergeSort`. + +* `Data.Sign.Show` - code for converting a sign to a string. + +* `Relation.Binary.Morphism.Construct.Product` - plumbing in the (categorical) product structure on `RawSetoid`. + +* `Relation.Binary.Properties.PartialSetoid` - systematise properties of the partial equivalence relation bundled with a set. + +* `Relation.Nullary.Recomputable.Core` + +* `Relation.Nullary.Irrelevant` - moved the concept `Irrelevant` of irrelevance (h-proposition) + from `Relation.Nullary` to its own dedicated module . + +Additions to existing modules +----------------------------- + +* In `Algebra.Consequences.Base`: + ```agda + module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) + where + ∙-congˡ : LeftCongruent _≈_ _∙_ + ∙-congʳ : RightCongruent _≈_ _∙_ + ``` + +* In `Algebra.Consequences.Setoid`: + ```agda + module Congruence (cong : Congruent₂ _≈_ _∙_) where + ∙-congˡ : LeftCongruent _≈_ _∙_ + ∙-congʳ : RightCongruent _≈_ _∙_ + ``` + +* In `Algebra.Construct.Initial`: + ```agda + assoc : Associative _≈_ _∙_ + idem : Idempotent _≈_ _∙_ + ``` + +* In `Algebra.Construct.Pointwise`: + ```agda + isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → + IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) + isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# → + IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) + isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# → + IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) + isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# → + IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) + isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# → + IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) + isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# → + IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#) + isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# → + IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) + isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# → + IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#) + commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ) + nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ) + semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) + commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) + commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ) + idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ) + kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ) + quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ) + commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) + ``` + +* In `Algebra.Modules.Properties`: + ```agda + inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y + inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x + ``` + +* Added new functions and proofs to `Algebra.Construct.Flip.Op`: + ```agda + zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) + distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# → + IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1# + isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → + IsCommutativeSemiring + (flip *) 0# 1# + isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# → + IsCancellativeCommutativeSemiring + (flip *) 0# 1# + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → + IsIdempotentSemiring + (flip *) 0# 1# + isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# + isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0# + isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# → + IsNonAssociativeRing + (flip *) - 0# 1# + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - + isCommutativeRing : IsCommutativeRing + * - 0# 1# → + IsCommutativeRing + (flip *) - 0# 1# + semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → + SemiringWithoutAnnihilatingZero a ℓ + commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ + cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ → + CancellativeCommutativeSemiring a ℓ + idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ + quasiring : Quasiring a ℓ → Quasiring a ℓ + ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ + nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ + nearring : Nearring a ℓ → Nearring a ℓ + ring : Ring a ℓ → Ring a ℓ + commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ + ``` + +* In `Algebra.Properties.Magma.Divisibility`: + ```agda + ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ + ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_ + ∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_ + x∣ˡxy : x ∣ˡ x ∙ y + xy≈z⇒x∣ˡz : x ∙ y ≈ z → x ∣ˡ z + ``` + +* In `Algebra.Properties.Monoid.Divisibility`: + ```agda + ε∣ˡ_ : ε ∣ˡ x + ∣ˡ-refl : Reflexive _∣ˡ_ + ∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_ + ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_ + ∣ˡ-preorder : Preorder a ℓ _ + ``` + +* In `Algebra.Properties.Monoid`: + ```agda + ε-unique : (∀ b → b ∙ a ≈ b) → a ≈ ε + ε-comm : a ∙ ε ≈ ε ∙ a + elimʳ : a ≈ ε → b ∙ a ≈ b + elimˡ : a ≈ ε → a ∙ b ≈ b + introʳ : a ≈ ε → b ≈ b ∙ a + introˡ : a ≈ ε → b ≈ a ∙ b + introᶜ : a ≈ ε → b ∙ c ≈ b ∙ (a ∙ c) + cancelʳ : a ∙ c ≈ ε → (b ∙ a) ∙ c ≈ b + cancelˡ : a ∙ c ≈ ε → a ∙ (c ∙ b) ≈ b + insertˡ : a ∙ c ≈ ε → b ≈ a ∙ (c ∙ b) + insertʳ : a ∙ c ≈ ε → b ≈ (b ∙ a) ∙ c + cancelᶜ : a ∙ c ≈ ε → (b ∙ a) ∙ (c ∙ d) ≈ b ∙ d + insertᶜ : a ∙ c ≈ ε ∙ d ≈ (b ∙ a) ∙ (c ∙ d) + ``` + +* In `Algebra.Properties.Semigroup`: + ```agda + uv≈w⇒xu∙v≈xw : x → (x ∙ u) ∙ v ≈ x ∙ w + uv≈w⇒u∙vx≈wx : u ∙ (v ∙ x) ≈ w ∙ x + uv≈w⇒u[vx∙y]≈w∙xy : u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y) + uv≈w⇒x[uv∙y]≈x∙wy : x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y) + uv≈w⇒[x∙yu]v≈x∙yw : (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w) + uv≈w⇒[xu∙v]y≈x∙wy : ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y) + uv≈w⇒[xy∙u]v≈x∙yw : ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w) + uv≈w⇒xu∙vy≈x∙wy : (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y) + uv≈w⇒xy≈z⇒u[vx∙y]≈wz : x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z + uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y)) + [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x) + [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) + [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x) + [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) + uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x) + uv≈wx⇒yu∙v≈yw∙x : (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x + uv≈wx⇒u∙vy≈w∙xy : u ∙ (v ∙ y) ≈ w ∙ (x ∙ y) + uv≈wx⇒yu∙vz≈yw∙xz : (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z) + ``` + +* In `Algebra.Properties.Semigroup.Divisibility`: + ```agda + ∣ˡ-trans : Transitive _∣ˡ_ + x∣ʳy⇒x∣ʳzy : x ∣ʳ y → x ∣ʳ z ∙ y + x∣ʳy⇒xz∣ʳyz : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z + x∣ˡy⇒zx∣ˡzy : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y + x∣ˡy⇒x∣ˡyz : x ∣ˡ y → x ∣ˡ y ∙ z + ``` + +* In `Algebra.Properties.CommutativeSemigroup.Divisibility`: + ```agda + ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b + ``` + +* In `Data.Bool.Properties`: + ```agda + if-eta : if b then x else x ≡ x + if-idem-then : (if b then (if b then x else y) else y) ≡ (if b then x else y) + if-idem-else : (if b then x else (if b then x else y)) ≡ (if b then x else y) + if-swap-then : (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y) + if-swap-else : (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y)) + if-not : (if not b then x else y) ≡ (if b then y else x) + if-∧ : (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y) + if-∨ : (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y)) + if-xor : (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y)) + if-cong : b ≡ c → (if b then x else y) ≡ (if c then x else y) + if-cong-then : x ≡ z → (if b then x else y) ≡ (if b then z else y) + if-cong-else : y ≡ z → (if b then x else y) ≡ (if b then x else z) + if-cong₂ : x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w) + ``` + +* In `Data.Fin.Base`: + ```agda + _≰_ : Rel (Fin n) 0ℓ + _≮_ : Rel (Fin n) 0ℓ + lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n + ``` + +* In `Data.Fin.Permutation`: + ```agda + cast-id : .(m ≡ n) → Permutation m n + swap : Permutation m n → Permutation (2+ m) (2+ n) + ``` + +* In `Data.Fin.Properties`: + + ```agda + punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k + punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k + punchOut-mono-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → j ≤ k → punchOut i≢j ≤ punchOut i≢k + punchOut-cancel-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≤ punchOut i≢k → j ≤ k + cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k + inject!-injective : Injective _≡_ _≡_ inject! + inject!-< : (k : Fin′ i) → inject! k < i + lower-injective : lower i i