Merge branch 'master' into modular-arithmetic

Author: Taneb

.github/workflows/ci-ubuntu.yml

@@ -76,11 +76,11 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=18cc53941e924b144c0f1f3953280ef726009f7e" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=ef912c68fd329ad3046d156e3c1a70a7fec19ba1" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.7.0.1" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.8.0-rc3" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 

CHANGELOG.md

@@ -1,299 +1,79 @@
-Version 2.3-dev
+Version 2.4-dev
 ===============
 
-The library has been tested using Agda 2.7.0 and 2.7.0.1.
+The library has been tested using Agda 2.8.0.
 
 Highlights
 ----------
 
 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.
+* Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`.
 
 Non-backwards compatible changes
 --------------------------------
 
-* The implementation of `≤-total` in `Data.Nat.Properties` has been altered
-  to use operations backed by primitives, rather than recursion, making it
-  significantly faster. However, its reduction behaviour on open terms may have
-  changed.
-
 Minor improvements
 ------------------
 
-* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
-  to its own dedicated module `Relation.Nullary.Irrelevant`.
+* The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
+  weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
+  safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
+
+* Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
+  ```agda
+  README.Data.Fin.Relation.Unary.Top
+  Algebra.Properties.Semiring.Binomial
+  Data.Fin.Subset.Properties
+  Data.Nat.Binary.Subtraction
+  Data.Nat.Combinatorics
+  ```
 
 Deprecated modules
 ------------------
 
 Deprecated names
 ----------------
 
-* In `Algebra.Definitions.RawMagma`:
+* In `Algebra.Properties.CommutativeSemigroup`:
   ```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
-  ```
-
-* 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
+  interchange  ↦   medial
   ```
 
 New modules
 -----------
 
-* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
-
-* `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
-
-* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
-
-* `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid.
+* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
 
-* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
-
-* `Data.Sign.Show` to show a sign
+* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
 
 Additions to existing modules
 -----------------------------
 
-* 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
-  ```
-
-* In `Algebra.Properties.Magma.Divisibility`:
-  ```agda
-  ∣ˡ-respʳ-≈  : _∣ˡ_ Respectsʳ _≈_
-  ∣ˡ-respˡ-≈  : _∣ˡ_ Respectsˡ _≈_
-  ∣ˡ-resp-≈   : _∣ˡ_ Respects₂ _≈_
-  x∣ˡxy       : ∀ x y → x ∣ˡ x ∙ y
-  xy≈z⇒x∣ˡz   : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
-  ```
-
-* In `Algebra.Properties.Monoid.Divisibility`:
-  ```agda
-  ε∣ˡ_          : ∀ x → ε ∣ˡ x
-  ∣ˡ-refl       : Reflexive _∣ˡ_
-  ∣ˡ-reflexive  : _≈_ ⇒ _∣ˡ_
-  ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_
-  ∣ˡ-preorder   : Preorder a ℓ _
-  ```
-
-* 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.List.Properties`:
-  ```agda
-  map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
-  map-applyDownFrom : ∀ (f : ℕ → A) (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
-  map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
-  map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Propositional`:
-  ```agda
-  ↭⇒↭ₛ′ : IsEquivalence _≈_ → _↭_ ⇒ _↭ₛ′_
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
-  ```agda
-  filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
-  ```
-
-* In `Data.Product.Function.Dependent.Propositional`:
-  ```agda
-  Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B
-  ```
-
-* In `Data.Product.Function.Dependent.Setoid`:
-  ```agda
-  rightInverse :
-     (I↪J : I ↪ J) →
-     (∀ {j} → RightInverse (A atₛ (from I↪J j)) (B atₛ j)) →
-     RightInverse (I ×ₛ A) (J ×ₛ B)
-
-  leftInverse :
-    (I↩J : I ↩ J) →
-    (∀ {i} → LeftInverse (A atₛ i) (B atₛ (to I↩J i))) →
-    LeftInverse (I ×ₛ A) (J ×ₛ B)
-  ```
-
-* In `Data.Vec.Relation.Binary.Pointwise.Inductive`:
+* In `Algebra.Properties.RingWithoutOne`:
   ```agda
-  zipWith-assoc : Associative _∼_ f → Associative (Pointwise _∼_) (zipWith {n = n} f)
-  zipWith-identityˡ: LeftIdentity _∼_ e f → LeftIdentity (Pointwise _∼_) (replicate n e) (zipWith f)
-  zipWith-identityʳ: RightIdentity _∼_ e f → RightIdentity (Pointwise _∼_) (replicate n e) (zipWith f)
-  zipWith-comm : Commutative _∼_ f → Commutative (Pointwise _∼_) (zipWith {n = n} f)
-  zipWith-cong : Congruent₂ _∼_ f → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs → Pointwise _∼_ (zipWith f ws ys) (zipWith f xs zs)
+  [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
   ```
 
-* In `Relation.Binary.Construct.Add.Infimum.Strict`:
+* In `Data.Fin.Permutation.Components`:
   ```agda
-  <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋
-  <₋-accessible[_] : Acc _<_ x → Acc _<₋_ [ x ]
-  <₋-wellFounded   : WellFounded _<_ → WellFounded _<₋_
+  transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j
+  transpose[i,j,j]≡i  : (i j : Fin n) → transpose i j j ≡ i
+  transpose[i,j,i]≡j  : (i j : Fin n) → transpose i j i ≡ j
+  transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k
   ```
 
-* In `Relation.Nullary.Decidable.Core`:
+* In `Data.Fin.Properties`:
   ```agda
-  ⊤-dec : Dec {a} ⊤
-  ⊥-dec : Dec {a} ⊥
+  ≡-irrelevant : Irrelevant {A = Fin n} _≡_
+  ≟-≡          : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
+  ≟-≡-refl     : (i : Fin n) → (i ≟ i) ≡ yes refl
+  ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
   ```
 
-* In `Relation.Nullary.Negation.Core`:
+* In `Data.Nat.Properties`:
   ```agda
-  contra-diagonal : (A → ¬ A) → ¬ A
+  ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
+  ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
   ```

CHANGELOG/v1.3.md

@@ -226,7 +226,7 @@ Deprecated modules
 
 * A warning is now raised whenever you import a deprecated module. This should
   aid the transition to the new modules. These warnings can be disabled locally
-  by adding the pragma `{-# OPTIONS --warn=noUserWarning #-}` to the top of a module.
+  by adding the pragma `{-# OPTIONS --warning=noUserWarning #-}` to the top of a module.
 
 The following modules have been renamed as part of a drive to improve
 consistency across the library. The deprecated modules still exist and