Merge branch 'master' into add-type-relations

.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=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=18cc53941e924b144c0f1f3953280ef726009f7e" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.6.4.3" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.7.0" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 

CHANGELOG.md

@@ -1,7 +1,7 @@
 Version 2.2-dev
 ===============
 
-The library has been tested using Agda 2.6.4.3.
+The library has been tested using Agda 2.7.0.
 
 Highlights
 ----------
@@ -24,6 +24,41 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Properties.CommutativeMagma.Divisibility`:
+  ```agda
+  ∣-factors    ↦  x|xy∧y|xy
+  ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
+  ```
+
+* In `Algebra.Properties.Magma.Divisibility`:
+  ```agda
+  ∣-respˡ   ↦  ∣-respˡ-≈
+  ∣-respʳ   ↦  ∣-respʳ-≈
+  ∣-resp    ↦  ∣-resp-≈
+ ```
+
+* In `Algebra.Solver.CommutativeMonoid`:
+  ```agda
+  normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
+  sg                 ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton
+  sg-correct         ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton-correct
+  ```
+
+* In `Algebra.Solver.IdempotentCommutativeMonoid`:
+  ```agda
+  flip12             ↦  Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz
+  distr              ↦  Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙
+  normalise-correct  ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct
+  sg                 ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton
+  sg-correct         ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct
+  ```
+
+* In `Algebra.Solver.Monoid`:
+  ```agda
+  homomorphic        ↦  Algebra.Solver.Monoid.Normal.comp-correct
+  normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   ++-assoc _      ↦  ++-assoc-eqFree
@@ -45,12 +80,48 @@ New modules
   Algebra.Properties.IdempotentCommutativeMonoid
   ```
 
+* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
+  a single `Solver` module API based on the existing `Expr`, and
+  a common `Normal`-form API:
+  ```agda
+  Algebra.Solver.CommutativeMonoid.Normal
+  Algebra.Solver.IdempotentCommutativeMonoid.Normal
+  Algebra.Solver.Monoid.Expression
+  Algebra.Solver.Monoid.Normal
+  Algebra.Solver.Monoid.Solver
+  ```
+
+  NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
+
+* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  Data.List.Relation.Unary.All.Properties.Core
+  ```
+
 Additions to existing modules
 -----------------------------
 
-* In `Data.Product.Function.Dependent.Propositional`:
+* Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`:
   ```agda
-  cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
+  ∤-respˡ-≈ : _∤_ Respectsˡ _≈_
+  ∤-respʳ-≈ : _∤_ Respectsʳ _≈_
+  ∤-resp-≈  : _∤_ Respects₂ _≈_
+  ∤∤-sym    : Symmetric _∤∤_
+  ∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_
+  ∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_
+  ∤∤-resp-≈  : _∤∤_ Respects₂ _≈_
+  ```
+
+* In `Algebra.Solver.Ring`
+  ```agda
+  Env : ℕ → Set _
+  Env = Vec Carrier
+ ```
+
+* In `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  Any-∈-swap :  Any (_∈ ys) xs → Any (_∈ xs) ys
+  All-∉-swap :  All (_∉ ys) xs → All (_∉ xs) ys
   ```
 
 * In `Data.List.Properties`:
@@ -76,6 +147,11 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* In `Data.Maybe.Properties`:
+  ```agda
+  maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
+  ```
+
 * New lemmas in `Data.Nat.Properties`:
   ```agda
   m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o
@@ -88,6 +164,11 @@ Additions to existing modules
   m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
   ```
 
+* In `Data.Product.Function.Dependent.Propositional`:
+  ```agda
+  cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
+  ```
+
 * New lemma in `Data.Vec.Properties`:
   ```agda
   map-concat : map f (concat xss) ≡ concat (map (map f) xss)
@@ -113,7 +194,7 @@ Additions to existing modules
   does-≡  : (a? b? : Dec A) → does a? ≡ does b?
   ```
 
-* In `Relation.Nullary.Properties`:
+* In `Relation.Unary.Properties`:
   ```agda
   map    : P ≐ Q → Decidable P → Decidable Q
   does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?

CHANGELOG/v2.1.1.md

@@ -0,0 +1,8 @@
+Version 2.1.1
+=============
+
+The library has been tested using Agda 2.7.0.
+
+* Fixed `Reflection.AST.Definition` to take into account Agda now exposes a `Quantity` argument on the reflection `constructor` constructor.
+
+* In `Reflection.AST.Show` added new function `showQuantity`

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.1
-date-released: 2024-07-17
+version: 2.1.1
+date-released: 2024-09-07
 url: "https://github.com/agda/agda-stdlib"

doc/README.agda

@@ -3,7 +3,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 2.0
+-- The Agda standard library, version 2.1.1
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,
@@ -19,7 +19,7 @@ module README where
 -- and other anonymous contributors.
 ------------------------------------------------------------------------
 
--- This version of the library has been tested using Agda 2.6.4.
+-- This version of the library has been tested using Agda 2.7.0
 
 -- The library comes with a .agda-lib file, for use with the library
 -- management system.

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.1 of the standard library with Agda 2.6.4.X. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
+Use version v2.1.1 of the standard library with Agda 2.7.0. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary).
 
 1. Navigate to a suitable directory `$HERE` (replace appropriately) where
    you would like to install the library.
 
-2. Download the tarball of v2.1 of the standard library. This can either be
+2. Download the tarball of v2.1.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.1.tar.gz
+   wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.1.1.tar.gz
    ```
    Note that you can replace `wget` with other popular tools such as `curl` and that
-   you can replace `2.1` with any other version of the library you desire.
+   you can replace `2.1.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.1 of the standard library with Agda 2.6.4.X. You can find the cor
 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run
    the commands to install via cabal:
    ```
-   cd agda-stdlib-2.1
+   cd agda-stdlib-2.1.1
    cabal install
    ```
 
@@ -40,7 +40,7 @@ Use version v2.1 of the standard library with Agda 2.6.4.X. You can find the cor
 6. Register the standard library with Agda's package system by adding
    the following line to `$HOME/.agda/libraries`:
    ```
-   $HERE/agda-stdlib-2.1/standard-library.agda-lib
+   $HERE/agda-stdlib-2.1.1/standard-library.agda-lib
    ```
 
 Now, the standard library is ready to be used either:

doc/release-guide.txt

@@ -13,7 +13,7 @@ procedure should be followed:
   - `README.md`
   - `doc/installation-guide.md`
 
-* Update the copyright year range in the LICENSE file, if necessary.
+* Update the copyright year range in the LICENCE file, if necessary.
 
 #### Pre-release tests
 

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -7,15 +7,14 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeMagma)
-open import Data.Product.Base using (_×_; _,_; map)
 
 module Algebra.Properties.CommutativeMagma.Divisibility
   {a ℓ} (CM : CommutativeMagma a ℓ)
   where
 
-open CommutativeMagma CM
+open import Data.Product.Base using (_×_; _,_)
 
-open import Relation.Binary.Reasoning.Setoid setoid
+open CommutativeMagma CM using (magma; _≈_; _∙_; comm)
 
 ------------------------------------------------------------------------
 -- Re-export the contents of magmas
@@ -31,8 +30,28 @@ x∣xy x y = y , comm y x
 xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z
 xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y)
 
-∣-factors : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
-∣-factors x y = x∣xy x y , x∣yx y x
+x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
+x|xy∧y|xy x y = x∣xy x y , x∣yx y x
 
-∣-factors-≈ : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
-∣-factors-≈ x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
+xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
+xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.2
+
+∣-factors = x|xy∧y|xy
+{-# WARNING_ON_USAGE ∣-factors
+"Warning: ∣-factors was deprecated in v2.2.
+Please use x|xy∧y|xy instead. "
+#-}
+∣-factors-≈ = xy≈z⇒x|z∧y|z
+{-# WARNING_ON_USAGE ∣-factors-≈
+"Warning: ∣-factors-≈ was deprecated in v2.2.
+Please use xy≈z⇒x|z∧y|z instead. "
+#-}