diff --git a/travis/agda-logo.svg b/.github/tooling/agda-logo.svg similarity index 100% rename from travis/agda-logo.svg rename to .github/tooling/agda-logo.svg diff --git a/travis/index.agda b/.github/tooling/index.agda similarity index 100% rename from travis/index.agda rename to .github/tooling/index.agda diff --git a/travis/index.sh b/.github/tooling/index.sh similarity index 100% rename from travis/index.sh rename to .github/tooling/index.sh diff --git a/travis/landing-bottom.html b/.github/tooling/landing-bottom.html similarity index 100% rename from travis/landing-bottom.html rename to .github/tooling/landing-bottom.html diff --git a/travis/landing-top.html b/.github/tooling/landing-top.html similarity index 100% rename from travis/landing-top.html rename to .github/tooling/landing-top.html diff --git a/travis/landing.sh b/.github/tooling/landing.sh similarity index 100% rename from travis/landing.sh rename to .github/tooling/landing.sh diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 2ecc969589..095f28b1f8 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -8,6 +8,7 @@ on: branches: - master - experimental + merge_group: ######################################################################## ## CONFIGURATION @@ -50,7 +51,7 @@ env: CABAL_VERSION: 3.6.2.0 CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' - AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -i src/ + AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -isrc -idoc jobs: test-stdlib: @@ -71,16 +72,15 @@ jobs: - name: Initialise variables run: | - if [[ '${{ github.ref }}' == 'refs/heads/master' \ - || '${{ github.base_ref }}' == 'master' ]]; then - # Pick Agda version for master - echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV; - echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV - elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \ - || '${{ github.base_ref }}' == 'experimental' ]]; then + if [[ '${{ github.ref }}' == 'refs/heads/experimental' \ + || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> $GITHUB_ENV; echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV + else + # Pick Agda version for master + echo "AGDA_COMMIT=tags/v2.6.4.1" >> $GITHUB_ENV; + echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV fi if [[ '${{ github.ref }}' == 'refs/heads/master' \ @@ -151,10 +151,19 @@ jobs: - name: Test stdlib run: | + # Including deprecated modules purely for testing + cabal run GenerateEverything -- --include-deprecated + ${{ env.AGDA }} -WnoUserWarning --safe EverythingSafe.agda + ${{ env.AGDA }} -WnoUserWarning Everything.agda + + - name: Prepare HTML index + run: | + # Regenerating the Everything files without the deprecated modules cabal run GenerateEverything - cp travis/* . + cp .github/tooling/* . ./index.sh ${{ env.AGDA }} --safe EverythingSafe.agda + ${{ env.AGDA }} Everything.agda ${{ env.AGDA }} index.agda - name: Golden testing @@ -177,8 +186,7 @@ jobs: rm -f '${{ env.AGDA_HTML_DIR }}'/*.html rm -f '${{ env.AGDA_HTML_DIR }}'/*.css ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda - - cp travis/* . + cp .github/tooling/* . ./landing.sh - name: Deploy HTML diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index b8c55c19be..5f9fa86b50 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -8,9 +8,9 @@ # # For more information, see https://github.com/haskell-CI/haskell-ci # -# version: 0.17.20230824 +# version: 0.17.20231010 # -# REGENDATA ("0.17.20230824",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) +# REGENDATA ("0.17.20231010",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) # name: Haskell-CI on: @@ -32,6 +32,7 @@ on: - agda-stdlib-utils.cabal - cabal.haskell-ci - "*.hs" + merge_group: jobs: linux: name: Haskell-CI - Linux - ${{ matrix.compiler }} @@ -44,19 +45,19 @@ jobs: strategy: matrix: include: - - compiler: ghc-9.8.0.20230822 + - compiler: ghc-9.8.1 compilerKind: ghc - compilerVersion: 9.8.0.20230822 + compilerVersion: 9.8.1 setup-method: ghcup - allow-failure: true - - compiler: ghc-9.6.2 + allow-failure: false + - compiler: ghc-9.6.3 compilerKind: ghc - compilerVersion: 9.6.2 + compilerVersion: 9.6.3 setup-method: ghcup allow-failure: false - - compiler: ghc-9.4.6 + - compiler: ghc-9.4.7 compilerKind: ghc - compilerVersion: 9.4.6 + compilerVersion: 9.4.7 setup-method: ghcup allow-failure: false - compiler: ghc-9.2.8 @@ -94,7 +95,6 @@ jobs: mkdir -p "$HOME/.ghcup/bin" curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup" chmod a+x "$HOME/.ghcup/bin/ghcup" - "$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml; "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false) "$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false) else @@ -104,7 +104,6 @@ jobs: mkdir -p "$HOME/.ghcup/bin" curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup" chmod a+x "$HOME/.ghcup/bin/ghcup" - "$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml; "$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false) fi env: @@ -138,7 +137,7 @@ jobs: echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV" echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV" echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV" - if [ $((HCNUMVER >= 90800)) -ne 0 ] ; then echo "HEADHACKAGE=true" >> "$GITHUB_ENV" ; else echo "HEADHACKAGE=false" >> "$GITHUB_ENV" ; fi + echo "HEADHACKAGE=false" >> "$GITHUB_ENV" echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV" echo "GHCJSARITH=0" >> "$GITHUB_ENV" env: @@ -167,18 +166,6 @@ jobs: repository hackage.haskell.org url: http://hackage.haskell.org/ EOF - if $HEADHACKAGE; then - cat >> $CABAL_CONFIG <> $CABAL_CONFIG <> cabal.project cat >> cabal.project <> cabal.project - fi $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(agda-stdlib-utils)$/; }' >> cabal.project.local cat cabal.project cat cabal.project.local diff --git a/CHANGELOG.md b/CHANGELOG.md index 6e03140b75..134309712c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,9 +1,9 @@ -Version 2.0-rc1 -=============== +Version 2.0 +=========== -The library has been tested using Agda 2.6.4. +The library has been tested using Agda 2.6.4 and 2.6.4.1. -NOTE: Version `2.0` contains various breaking changes and is not backwards +NOTE: Version `2.0` contains various breaking changes and is not backwards compatible with code written with version `1.X` of the library. Highlights @@ -33,9 +33,15 @@ Highlights Bug-fixes --------- +* In `Algebra.Structures` the records `IsRing` and `IsRingWithoutOne` contained an unnecessary field + `zero : RightZero 0# *`, which could be derived from the other ring axioms. + Consequently this field has been removed from the record, and the record + `IsRingWithoutAnnihilatingZero` in `Algebra.Structures.Biased` has been + deprecated as it is now identical to is `IsRing`. + * In `Algebra.Definitions.RawSemiring` the record `Prime` did not - enforce that the number was not divisible by `1#`. To fix this - `p∤1 : p ∤ 1#` hsa been added as a field. + enforce that the number was not divisible by `1#`. To fix this + `p∤1 : p ∤ 1#` has been added as a field. * In `Data.Container.FreeMonad`, we give a direct definition of `_⋆_` as an inductive type rather than encoding it as an instance of `μ`. This ensures Agda notices that @@ -45,24 +51,24 @@ Bug-fixes * In `Data.Fin.Properties` the `i` argument to `opposite-suc` was implicit but could not be inferred in general. It has been made explicit. - -* In `Data.List.Membership.Setoid` the operations `_∷=_` and `_─_` + +* In `Data.List.Membership.Setoid` the operations `_∷=_` and `_─_` had an extraneous `{A : Set a}` parameter. This has been removed. -* In `Data.List.Relation.Ternary.Appending.Setoid` the constructors - were re-exported in their full generality which lead to unsolved meta +* In `Data.List.Relation.Ternary.Appending.Setoid` the constructors + were re-exported in their full generality which lead to unsolved meta variables at their use sites. Now versions of the constructors specialised to use the setoid's carrier set are re-exported. - -* In `Data.Nat.DivMod` the parameter `o` in the proof `/-monoˡ-≤` was + +* In `Data.Nat.DivMod` the parameter `o` in the proof `/-monoˡ-≤` was implicit but not inferrable. It has been changed to be explicit. -* In `Data.Nat.DivMod` the parameter `m` in the proof `+-distrib-/-∣ʳ` was +* In `Data.Nat.DivMod` the parameter `m` in the proof `+-distrib-/-∣ʳ` was implicit but not inferrable, while `n` is explicit but inferrable. They have been to explicit and implicit respectively. -* In `Data.Nat.GeneralisedArithmetic` the `s` and `z` arguments to the - following functions were implicit but no inferrable: +* In `Data.Nat.GeneralisedArithmetic` the `s` and `z` arguments to the + following functions were implicit but not inferrable: `fold-+`, `fold-k`, `fold-*`, `fold-pull`. They have been made explicit. * In `Data.Rational(.Unnormalised).Properties` the module `≤-Reasoning` @@ -79,9 +85,9 @@ Bug-fixes _≈⟨_⟨_ ↦ _≃⟨_⟨_ ``` -* In `Function.Construct.Composition` the combinators +* In `Function.Construct.Composition` the combinators `_⟶-∘_`, `_↣-∘_`, `_↠-∘_`, `_⤖-∘_`, `_⇔-∘_`, `_↩-∘_`, `_↪-∘_`, `_↔-∘_` - had their arguments in the wrong order. They have been flipped so they can + had their arguments in the wrong order. They have been flipped so they can actually be used as a composition operator. * In `Function.Definitions` the definitions of `Surjection`, `Inverseˡ`, @@ -98,7 +104,7 @@ Non-backwards compatible changes ### Removed deprecated names -* All modules and names that were deprecated in `v1.2` and before have +* All modules and names that were deprecated in `v1.2` and before have been removed. ### Changes to `LeftCancellative` and `RightCancellative` in `Algebra.Definitions` @@ -112,21 +118,21 @@ Non-backwards compatible changes always true and cannot be assumed in user's code. * Therefore the definitions have been changed as follows to make all their arguments explicit: - - `LeftCancellative _•_` - - From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z` - - To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z` + - `LeftCancellative _∙_` + - From: `∀ x {y z} → (x ∙ y) ≈ (x ∙ z) → y ≈ z` + - To: `∀ x y z → (x ∙ y) ≈ (x ∙ z) → y ≈ z` - - `RightCancellative _•_` - - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z` - - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z` + - `RightCancellative _∙_` + - From: `∀ {x} y z → (y ∙ x) ≈ (z ∙ x) → y ≈ z` + - To: `∀ x y z → (y ∙ x) ≈ (z ∙ x) → y ≈ z` - - `AlmostLeftCancellative e _•_` - - From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` - - To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` + - `AlmostLeftCancellative e _∙_` + - From: `∀ {x} y z → ¬ x ≈ e → (x ∙ y) ≈ (x ∙ z) → y ≈ z` + - To: `∀ x y z → ¬ x ≈ e → (x ∙ y) ≈ (x ∙ z) → y ≈ z` - - `AlmostRightCancellative e _•_` - - From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` - - To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` + - `AlmostRightCancellative e _∙_` + - From: `∀ {x} y z → ¬ x ≈ e → (y ∙ x) ≈ (z ∙ x) → y ≈ z` + - To: `∀ x y z → ¬ x ≈ e → (y ∙ x) ≈ (z ∙ x) → y ≈ z` * Correspondingly some proofs of the above types will need additional arguments passed explicitly. Instances can easily be fixed by adding additional underscores, e.g. @@ -162,8 +168,8 @@ Non-backwards compatible changes `Algebra.Lattice.Properties.Semilattice` or `Algebra.Lattice.Morphism.Lattice`). See the `Deprecated modules` section below for full details. -* The definition of `IsDistributiveLattice` and `IsBooleanAlgebra` have changed so - that they are no longer right-biased which hindered compositionality. +* The definition of `IsDistributiveLattice` and `IsBooleanAlgebra` have changed so + that they are no longer right-biased which hindered compositionality. More concretely, `IsDistributiveLattice` now has fields: ```agda ∨-distrib-∧ : ∨ DistributesOver ∧ @@ -205,7 +211,9 @@ Non-backwards compatible changes * Added new `IsBoundedSemilattice`/`BoundedSemilattice` records. * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice` - which can be used to indicate meet/join-ness of the original structures. + which can be used to indicate meet/join-ness of the original structures, and + the field names in `IsSemilattice` and `Semilattice` have been renamed from + `∧-cong` to `∙-cong`to indicate their undirected nature. * Finally, the following auxiliary files have been moved: ```agda @@ -225,12 +233,12 @@ Non-backwards compatible changes IsSemiringHomomorphism IsRingHomomorphism ``` - all had two separate proofs of `IsRelHomomorphism` within them. - -* To fix this they have all been redefined to build up from `IsMonoidHomomorphism`, - `IsNearSemiringHomomorphism`, and `IsSemiringHomomorphism` respectively, - adding a single property at each step. - + all had two separate proofs of `IsRelHomomorphism` within them. + +* To fix this they have all been redefined to build up from `IsMonoidHomomorphism`, + `IsNearSemiringHomomorphism`, and `IsSemiringHomomorphism` respectively, + adding a single property at each step. + * Similarly, `IsLatticeHomomorphism` is now built as `IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homomorphic. @@ -241,13 +249,13 @@ Non-backwards compatible changes * As observed by Wen Kokke in issue #1636, it no longer really makes sense to group the modules which correspond to the variety of concepts of (effectful) type constructor arising in functional programming (esp. in Haskell) - such as `Monad`, `Applicative`, `Functor`, etc, under `Category.*`, - as this obstructs the importing of the `agda-categories` development into - the Standard Library, and moreover needlessly restricts the applicability of - categorical concepts to this (highly specific) mode of use. - -* Correspondingly, client modules grouped under `*.Categorical.*` which - exploit such structure for effectful programming have been renamed + such as `Monad`, `Applicative`, `Functor`, etc, under `Category.*`, + as this obstructs the importing of the `agda-categories` development into + the Standard Library, and moreover needlessly restricts the applicability of + categorical concepts to this (highly specific) mode of use. + +* Correspondingly, client modules grouped under `*.Categorical.*` which + exploit such structure for effectful programming have been renamed `*.Effectful`, with the originals being deprecated. * Full list of moved modules: @@ -284,7 +292,7 @@ Non-backwards compatible changes IO.Categorical ↦ IO.Effectful Reflection.TCM.Categorical ↦ Reflection.TCM.Effectful ``` - + * Full list of new modules: ``` Algebra.Construct.Initial @@ -374,10 +382,10 @@ Non-backwards compatible changes * Due to the change in Agda 2.6.2 where sized types are no longer compatible with the `--safe` flag, it has become clear that a third variant of codata - will be needed using coinductive records. - -* Therefore all existing modules in `Codata` which used sized types have been - moved inside a new folder named `Codata.Sized`, e.g. `Codata.Stream` + will be needed using coinductive records. + +* Therefore all existing modules in `Codata` which used sized types have been + moved inside a new folder named `Codata.Sized`, e.g. `Codata.Stream` has become `Codata.Sized.Stream`. ### New proof-irrelevant for empty type in `Data.Empty` @@ -398,14 +406,14 @@ Non-backwards compatible changes + In `Relation.Nullary.Decidable.Core`, the type of `dec-no` has changed ```agda dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′ - ↦ + ↦ dec-no : (p? : Dec P) (¬p : ¬ P) → p? ≡ no ¬p ``` + In `Relation.Binary.PropositionalEquality`, the type of `≢-≟-identity` has changed ```agda ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq - ↦ + ↦ ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y ``` @@ -424,7 +432,7 @@ Non-backwards compatible changes ≺-rec ``` these functions are also deprecated. - + * Likewise in `Data.Fin.Properties` the proofs `≺⇒<′` and `<′⇒≺` have been deprecated in favour of their proxy counterparts `<⇒<′` and `<′⇒<`. @@ -473,9 +481,9 @@ Non-backwards compatible changes #### Standardisation of `lookup` in `Data.(List/Vec/...)` -* All the types of `lookup` functions (and variants) in the following modules - have been changed to match the argument convention adopted in the `List` module (i.e. - `lookup` takes its container first and the index, whose type may depend on the +* All the types of `lookup` functions (and variants) in the following modules + have been changed to match the argument convention adopted in the `List` module (i.e. + `lookup` takes its container first and the index, whose type may depend on the container value, second): ``` Codata.Guarded.Stream @@ -500,20 +508,20 @@ Non-backwards compatible changes Data.Vec.Recursive ``` -* To accomodate this in in `Data.Vec.Relation.Unary.Linked.Properties` +* To accommodate this in in `Data.Vec.Relation.Unary.Linked.Properties` and `Codata.Guarded.Stream.Relation.Binary.Pointwise`, the proofs called `lookup` have been renamed `lookup⁺`. -#### Changes to `Data.(Nat/Integer/Rational)` proofs of `NonZero`/`Positive`/`Negative` to instance arguments +#### Changes to `Data.(Nat/Integer/Rational)` proofs of `NonZero`/`Positive`/`Negative` to use instance arguments * Many numeric operations in the library require their arguments to be non-zero, and various proofs require their arguments to be non-zero/positive/negative etc. As discussed on the [mailing list](https://lists.chalmers.se/pipermail/agda/2021/012693.html), - the previous way of constructing and passing round these proofs was extremely + the previous way of constructing and passing round these proofs was extremely clunky and lead to messy and difficult to read code. - -* We have therefore changed every occurrence where we need a proof of - non-zeroness/positivity/etc. to take it as an irrelevant + +* We have therefore changed every occurrence where we need a proof of + non-zeroness/positivity/etc. to take it as an irrelevant [instance argument](https://agda.readthedocs.io/en/latest/language/instance-arguments.html). See the mailing list discussion for a fuller explanation of the motivation and implementation. @@ -538,47 +546,47 @@ Non-backwards compatible changes * At the moment, there are 4 different ways such instance arguments can be provided, listed in order of convenience and clarity: - 1. *Automatic basic instances* - the standard library provides instances based on - the constructors of each numeric type in `Data.X.Base`. For example, - `Data.Nat.Base` constrains an instance of `NonZero (suc n)` for any `n` - and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. - Consequently, if the argument is of the required form, these instances will always - be filled in by instance search automatically, e.g. - ```agda - 0/n≡0 : 0 / suc n ≡ 0 - ``` - - 2. *Add an instance argument parameter* - You can provide the instance argument as - a parameter to your function and Agda's instance search will automatically use it - in the correct place without you having to explicitly pass it, e.g. + 1. *Automatic basic instances* - the standard library provides instances based on + the constructors of each numeric type in `Data.X.Base`. For example, + `Data.Nat.Base` constrains an instance of `NonZero (suc n)` for any `n` + and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. + Consequently, if the argument is of the required form, these instances will always + be filled in by instance search automatically, e.g. + ```agda + 0/n≡0 : 0 / suc n ≡ 0 + ``` + + 2. *Add an instance argument parameter* - You can provide the instance argument as + a parameter to your function and Agda's instance search will automatically use it + in the correct place without you having to explicitly pass it, e.g. ```agda 0/n≡0 : .{{_ : NonZero n}} → 0 / n ≡ 0 ``` - 3. *Define the instance locally* - You can define an instance argument in scope - (e.g. in a `where` clause) and Agda's instance search will again find it automatically, - e.g. - ```agda - instance - n≢0 : NonZero n - n≢0 = ... + 3. *Define the instance locally* - You can define an instance argument in scope + (e.g. in a `where` clause) and Agda's instance search will again find it automatically, + e.g. + ```agda + instance + n≢0 : NonZero n + n≢0 = ... - 0/n≡0 : 0 / n ≡ 0 - ``` + 0/n≡0 : 0 / n ≡ 0 + ``` 4. *Pass the instance argument explicitly* - Finally, if all else fails you can pass the - instance argument explicitly into the function using `{{ }}`, e.g. - ``` - 0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0 - ``` + instance argument explicitly into the function using `{{ }}`, e.g. + ``` + 0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0 + ``` * Suitable constructors for `NonZero`/`Positive` etc. can be found in `Data.X.Base`. -* A full list of proofs that have changed to use instance arguments is available +* A full list of proofs that have changed to use instance arguments is available at the end of this file. Notable changes to proofs are now discussed below. * Previously one of the hacks used in proofs was to explicitly refer to everything - in the correct form, e.g. if the argument `n` had to be non-zero then you would + in the correct form, e.g. if the argument `n` had to be non-zero then you would refer to the argument as `suc n` everywhere instead of `n`, e.g. ``` n/n≡1 : ∀ n → suc n / suc n ≡ 1 @@ -588,13 +596,13 @@ Non-backwards compatible changes ``` n/n≡1 : ∀ n {{_ : NonZero n}} → n / n ≡ 1 ``` - However, note that this means that if you passed in the value `x` to these proofs - before, then you will now have to pass in `suc x`. The proofs for which the - arguments have changed form in this way are highlighted in the list at the bottom + However, note that this means that if you passed in the value `x` to these proofs + before, then you will now have to pass in `suc x`. The proofs for which the + arguments have changed form in this way are highlighted in the list at the bottom of the file. * Finally, in `Data.Rational.Unnormalised.Base` the definition of `_≢0` is now - redundent and so has been removed. Additionally the following proofs about it have + redundant and so has been removed. Additionally the following proofs about it have also been removed from `Data.Rational.Unnormalised.Properties`: ``` p≄0⇒∣↥p∣≢0 : ∀ p → p ≠ 0ℚᵘ → ℤ.∣ (↥ p) ∣ ≢0 @@ -613,9 +621,9 @@ Non-backwards compatible changes ``` which introduced a spurious additional definition, when this is in fact, modulo field names and implicit/explicit qualifiers, equivalent to the definition of left- - divisibility, `_∣ˡ_` for the `RawMagma` structure of `_+_`. - -* Since the addition of raw bundles to `Data.X.Base`, this definition can now be + divisibility, `_∣ˡ_` for the `RawMagma` structure of `_+_`. + +* Since the addition of raw bundles to `Data.X.Base`, this definition can now be made directly. Accordingly, the definition has been changed to: ```agda _≤″_ : (m n : ℕ) → Set @@ -625,8 +633,8 @@ Non-backwards compatible changes ``` * Knock-on consequences include the need to retain the old constructor - name, now introduced as a pattern synonym, and introduction of (a function - equivalent to) the former field name/projection function `proof` as + name, now introduced as a pattern synonym, and introduction of (a function + equivalent to) the former field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`. ### Changes to definition of `Prime` in `Data.Nat.Primality` @@ -645,10 +653,14 @@ Non-backwards compatible changes * To make it easier to use, reason about and read, the definition has been changed to: ```agda - Prime 0 = ⊥ - Prime 1 = ⊥ - Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n + record Prime (p : ℕ) : Set where + constructor prime + field + .{{nontrivial}} : NonTrivial p + notComposite : ¬ Composite p ``` + where `Composite` is now defined as the diagonal of the new relation + `_HasNonTrivialDivisorLessThan_` in `Data.Nat.Divisibility.Core`. ### Changes to operation reduction behaviour in `Data.Rational(.Unnormalised)` @@ -672,24 +684,24 @@ Non-backwards compatible changes ``` * As a consequence of this, some proofs that relied either on this reduction behaviour - or on eta-equality may no longer type-check. - + or on eta-equality may no longer type-check. + * There are several ways to fix this: - + 1. The principled way is to not rely on this reduction behaviour in the first place. The `Properties` files for rational numbers have been greatly expanded in `v1.7` and `v2.0`, and we believe most proofs should be able to be built up from existing proofs contained within these files. - + 2. Alternatively, annotating any rational arguments to a proof with either `@record{}` or `@(mkℚ _ _ _)` should restore the old reduction behaviour for any terms involving those parameters. - + 3. Finally, if the above approaches are not viable then you may be forced to explicitly use `cong` combined with a lemma that proves the old reduction behaviour. * Similarly, in order to prevent reduction, the equality `_≃_` in `Data.Rational.Base` - has been made into a data type with the single constructor `*≡*`. The destructor + has been made into a data type with the single constructor `*≡*`. The destructor `drop-*≡*` has been added to `Data.Rational.Properties`. #### Deprecation of old `Function` hierarchy @@ -697,7 +709,7 @@ Non-backwards compatible changes * The new `Function` hierarchy was introduced in `v1.2` which follows the same `Core`/`Definitions`/`Bundles`/`Structures` as all the other hierarchies in the library. - + * At the time the old function hierarchy in: ``` Function.Equality @@ -711,11 +723,11 @@ Non-backwards compatible changes ``` was unofficially deprecated, but could not be officially deprecated because of it's widespread use in the rest of the library. - -* Now, the old hierarchy modules have all been officially deprecated. All + +* Now, the old hierarchy modules have all been officially deprecated. All uses of them in the rest of the library have been switched to use the - new hierarachy. - + new hierarchy. + * The latter is unfortunately a relatively big breaking change, but was judged to be unavoidable given how widely used the old hierarchy was. @@ -724,9 +736,9 @@ Non-backwards compatible changes * In `Function.Bundles` the names of the fields in the records have been changed from `f`, `g`, `cong₁` and `cong₂` to `to`, `from`, `to-cong`, `from-cong`. -* In `Function.Definitions`, the module no longer has two equalities as - module arguments, as they did not interact as intended with the re-exports - from `Function.Definitions.(Core1/Core2)`. The latter two modules have +* In `Function.Definitions`, the module no longer has two equalities as + module arguments, as they did not interact as intended with the re-exports + from `Function.Definitions.(Core1/Core2)`. The latter two modules have been removed and their definitions folded into `Function.Definitions`. * In `Function.Definitions` the following definitions have been changed from: @@ -741,9 +753,9 @@ Non-backwards compatible changes Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x ``` - This is for several reasons: - i) the new definitions compose much more easily, - ii) Agda can better infer the equalities used. + This is for several reasons: + i) the new definitions compose much more easily, + ii) Agda can better infer the equalities used. * To ease backwards compatibility: - the old definitions have been moved to the new names `StrictlySurjective`, @@ -751,8 +763,10 @@ Non-backwards compatible changes - The records in `Function.Structures` and `Function.Bundles` export proofs of these under the names `strictlySurjective`, `strictlyInverseˡ` and `strictlyInverseʳ`, - - Conversion functions have been added in both directions to - `Function.Consequences(.Propositional)`. + - Conversion functions for the definitions have been added in both directions + to `Function.Consequences(.Propositional/Setoid)`. + - Conversion functions for structures have been added in + `Function.Structures.Biased`. ### New `Function.Strict` @@ -769,9 +783,9 @@ Non-backwards compatible changes WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _ WfRec _<_ P x = ∀ y → y < x → P y ``` - which meant that all arguments involving accessibility and wellfoundedness proofs - were polluted by almost-always-inferrable explicit arguments for the `y` position. - + which meant that all arguments involving accessibility and wellfoundedness proofs + were polluted by almost-always-inferrable explicit arguments for the `y` position. + * The definition has now been changed to make that argument *implicit*, as ```agda WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _ @@ -821,44 +835,47 @@ Non-backwards compatible changes ### Reorganisation of the `Relation.Nullary` hierarchy -* It was very difficult to use the `Relation.Nullary` modules, as - `Relation.Nullary` contained the basic definitions of negation, decidability etc., - and the operations and proofs about these definitions were spread over +* It was very difficult to use the `Relation.Nullary` modules, as + `Relation.Nullary` contained the basic definitions of negation, decidability etc., + and the operations and proofs about these definitions were spread over `Relation.Nullary.(Negation/Product/Sum/Implication etc.)`. * To fix this all the contents of the latter is now exported by `Relation.Nullary`. * In order to achieve this the following backwards compatible changes have been made: - + 1. the definition of `Dec` and `recompute` have been moved to `Relation.Nullary.Decidable.Core` - + 2. the definition of `Reflects` has been moved to `Relation.Nullary.Reflects` - + 3. the definition of `¬_` has been moved to `Relation.Nullary.Negation.Core` - 4. The modules `Relation.Nullary.(Product/Sum/Implication)` have been deprecated - and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)`. + 4. The modules `Relation.Nullary.(Product/Sum/Implication)` have been deprecated + and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)`. + + 5. The proof `T?` has been moved from `Data.Bool.Properties` to `Relation.Nullary.Decidable.Core` + (but is still re-exported by the former). as well as the following breaking changes: - 1. `¬?` has been moved from `Relation.Nullary.Negation.Core` to - `Relation.Nullary.Decidable.Core` - - 2. `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to - `Relation.Nullary.Reflects`. - - 3. `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved - from `Relation.Nullary.Negation` to `Relation.Nullary.Decidable`. - + 1. `¬?` has been moved from `Relation.Nullary.Negation.Core` to + `Relation.Nullary.Decidable.Core` + + 2. `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to + `Relation.Nullary.Reflects`. + + 3. `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved + from `Relation.Nullary.Negation` to `Relation.Nullary.Decidable`. + 4. `fromDec` and `toDec` have been moved from `Data.Sum.Base` to `Data.Sum`. ### (Issue #2096) Introduction of flipped and negated relation symbols to bundles in `Relation.Binary.Bundles` -* Previously, bundles such as `Preorder`, `Poset`, `TotalOrder` etc. did not have the flipped +* Previously, bundles such as `Preorder`, `Poset`, `TotalOrder` etc. did not have the flipped and negated versions of the operators exposed. In some cases they could obtained by opening the relevant `Relation.Binary.Properties.X` file but usually they had to be redefined every time. - + * To fix this, these bundles now all export all 4 versions of the operator: normal, converse, negated, converse-negated. Accordingly they are no longer exported from the corresponding `Properties` file. @@ -867,26 +884,26 @@ Non-backwards compatible changes converse relation could only be discussed *semantically* in terms of `flip _∼_`. * Now, the `Preorder` record field `_∼_` has been renamed to `_≲_`, with `_≳_` - introduced as a definition in `Relation.Binary.Bundles.Preorder`. - Partial backwards compatible has been achieved by redeclaring a deprecated version - of the old symbol in the record. Therefore, only _declarations_ of `PartialOrder` records will + introduced as a definition in `Relation.Binary.Bundles.Preorder`. + Partial backwards compatible has been achieved by redeclaring a deprecated version + of the old symbol in the record. Therefore, only _declarations_ of `PartialOrder` records will need their field names updating. ### Changes to definition of `IsStrictTotalOrder` in `Relation.Binary.Structures` -* The previous definition of the record `IsStrictTotalOrder` did not - build upon `IsStrictPartialOrder` as would be expected. +* The previous definition of the record `IsStrictTotalOrder` did not + build upon `IsStrictPartialOrder` as would be expected. Instead it omitted several fields like irreflexivity as they were derivable from the - proof of trichotomy. However, this led to problems further up the hierarchy where - bundles such as `StrictTotalOrder` which contained multiple distinct proofs of + proof of trichotomy. However, this led to problems further up the hierarchy where + bundles such as `StrictTotalOrder` which contained multiple distinct proofs of `IsStrictPartialOrder`. -* To remedy this the definition of `IsStrictTotalOrder` has been changed to so +* To remedy this the definition of `IsStrictTotalOrder` has been changed to so that it builds upon `IsStrictPartialOrder` as would be expected. -* To aid migration, the old record definition has been moved to - `Relation.Binary.Structures.Biased` which contains the `isStrictTotalOrderᶜ` +* To aid migration, the old record definition has been moved to + `Relation.Binary.Structures.Biased` which contains the `isStrictTotalOrderᶜ` smart constructor (which is re-exported by `Relation.Binary`) . Therefore the old code: ```agda <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_ @@ -917,14 +934,14 @@ Non-backwards compatible changes ### Changes to the interface of `Relation.Binary.Reasoning.Triple` -* The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof +* The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict relation is irreflexive. * This allows the addition of the following new proof combinator: ```agda begin-contradiction : (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → A ``` - that takes a proof that a value is strictly less than itself and then applies the + that takes a proof that a value is strictly less than itself and then applies the principle of explosion to derive anything. * Specialised versions of this combinator are available in the `Reasoning` modules @@ -945,9 +962,9 @@ Non-backwards compatible changes * Previously, every `Reasoning` module in the library tended to roll it's own set of syntax for the combinators. This hindered consistency and maintainability. - -* To improve the situation, a new module `Relation.Binary.Reasoning.Syntax` - has been introduced which exports a wide range of sub-modules containing + +* To improve the situation, a new module `Relation.Binary.Reasoning.Syntax` + has been introduced which exports a wide range of sub-modules containing pre-existing reasoning combinator syntax. * This makes it possible to add new or rename existing reasoning combinators to a @@ -956,39 +973,39 @@ Non-backwards compatible changes * One pre-requisite for that is that `≡-Reasoning` has been moved from `Relation.Binary.PropositionalEquality.Core` (which shouldn't be - imported anyway as it's a `Core` module) to + imported anyway as it's a `Core` module) to `Relation.Binary.PropositionalEquality.Properties`. It is still exported by `Relation.Binary.PropositionalEquality`. ### Renaming of symmetric combinators in `Reasoning` modules -* We've had various complaints about the symmetric version of reasoning combinators +* We've had various complaints about the symmetric version of reasoning combinators that use the syntax `_R˘⟨_⟩_` for some relation `R`, (e.g. `_≡˘⟨_⟩_` and `_≃˘⟨_⟩_`) introduced in `v1.0`. In particular: 1. The symbol `˘` is hard to type. 2. The symbol `˘` doesn't convey the direction of the equality 3. The left brackets aren't vertically aligned with the left brackets of the non-symmetric version. - -* To address these problems we have renamed all the symmetric versions of the + +* To address these problems we have renamed all the symmetric versions of the combinators from `_R˘⟨_⟩_` to `_R⟨_⟨_` (the direction of the last bracket is flipped to indicate the quality goes from right to left). - -* The old combinators still exist but have been deprecated. However due to + +* The old combinators still exist but have been deprecated. However due to [Agda issue #5617](https://github.com/agda/agda/issues/5617), the deprecation warnings don't fire correctly. We will not remove the old combinators before the above issue is addressed. However, we still encourage migrating to the new combinators! * On a Linux-based system, the following command was used to globally migrate all uses of the - old combinators to the new ones in the standard library itself. + old combinators to the new ones in the standard library itself. It *may* be useful when trying to migrate your own code: ```bash find . -type f -name "*.agda" -print0 | xargs -0 sed -i -e 's/˘⟨\(.*\)⟩/⟨\1⟨/g' ``` - USUAL CAVEATS: It has not been widely tested and the standard library developers are not - responsible for the results of this command. It is strongly recommended you back up your + USUAL CAVEATS: It has not been widely tested and the standard library developers are not + responsible for the results of this command. It is strongly recommended you back up your work before you attempt to run it. - -* NOTE: this refactoring may require some extra bracketing around the operator `_⟨_⟩_` from + +* NOTE: this refactoring may require some extra bracketing around the operator `_⟨_⟩_` from `Function.Base` if the `_⟨_⟩_` operator is used within the reasoning proof. The symptom for this is a `Don't know how to parse` error. @@ -1031,14 +1048,18 @@ Non-backwards compatible changes * In `Algebra.Core` the operations `Opₗ` and `Opᵣ` have moved to `Algebra.Module.Core`. +* In `Algebra.Definitions.RawMagma.Divisibility` the definitions for `_∣ˡ_` and `_∣ʳ_` + have been changed from being defined as raw products to being defined as records. However, + the record constructors are called `_,_` so the changes required are minimal. + * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions: * `cycle` * `interleave⁺` * `cantor` - Furthermore, the direction of interleaving of `cantor` has changed. Precisely, - suppose `pair` is the cantor pairing function, then `lookup (pair i j) (cantor xss)` - according to the old definition corresponds to `lookup (pair j i) (cantor xss)` - according to the new definition. + Furthermore, the direction of interleaving of `cantor` has changed. Precisely, + suppose `pair` is the cantor pairing function, then `lookup (pair i j) (cantor xss)` + according to the old definition corresponds to `lookup (pair j i) (cantor xss)` + according to the new definition. For a concrete example see the one included at the end of the module. * In `Data.Fin.Base` the relations `_≤_` `_≥_` `_<_` `_>_` have been @@ -1047,9 +1068,9 @@ Non-backwards compatible changes properties about the orderings themselves the second index must be provided explicitly. -* In `Data.Fin.Properties` the proof `inj⇒≟` that an injection from a type - `A` into `Fin n` induces a decision procedure for `_≡_` on `A` has been - generalized to other equivalences over `A` (i.e. to arbitrary setoids), and +* In `Data.Fin.Properties` the proof `inj⇒≟` that an injection from a type + `A` into `Fin n` induces a decision procedure for `_≡_` on `A` has been + generalised to other equivalences over `A` (i.e. to arbitrary setoids), and renamed from `eq?` to the more descriptive and `inj⇒decSetoid`. * In `Data.Fin.Properties` the proof `pigeonhole` has been strengthened @@ -1058,19 +1079,19 @@ Non-backwards compatible changes * In `Data.Fin.Substitution.TermSubst` the fixity of `_/Var_` has been changed from `infix 8` to `infixl 8`. -* In `Data.Integer.DivMod` the previous implementations of - `_divℕ_`, `_div_`, `_modℕ_`, `_mod_` internally converted to the unary - `Fin` datatype resulting in poor performance. The implementation has been +* In `Data.Integer.DivMod` the previous implementations of + `_divℕ_`, `_div_`, `_modℕ_`, `_mod_` internally converted to the unary + `Fin` datatype resulting in poor performance. The implementation has been updated to use the corresponding operations from `Data.Nat.DivMod` which are efficiently implemented using the Haskell backend. -* In `Data.Integer.Properties` the first two arguments of `m≡n⇒m-n≡0` +* In `Data.Integer.Properties` the first two arguments of `m≡n⇒m-n≡0` (now renamed `i≡j⇒i-j≡0`) have been made implicit. -* In `Data.(List|Vec).Relation.Binary.Lex.Strict` the argument `xs` in +* In `Data.(List|Vec).Relation.Binary.Lex.Strict` the argument `xs` in `xs≮[]` in introduced in PRs #1648 and #1672 has now been made implicit. -* In `Data.List.NonEmpty` the functions `split`, `flatten` and `flatten-split` +* In `Data.List.NonEmpty` the functions `split`, `flatten` and `flatten-split` have been removed from. In their place `groupSeqs` and `ungroupSeqs` have been added to `Data.List.NonEmpty.Base` which morally perform the same operations but without computing the accompanying proofs. The proofs can be @@ -1082,20 +1103,20 @@ Non-backwards compatible changes proofs. * In `Data.Nat.Divisibility` the proof `m/n/o≡m/[n*o]` has been removed. In it's - place a new more general proof `m/n/o≡m/[n*o]` has been added to `Data.Nat.DivMod` + place a new more general proof `m/n/o≡m/[n*o]` has been added to `Data.Nat.DivMod` that doesn't require the `n * o ∣ m` pre-condition. -* In `Data.Product.Relation.Binary.Lex.Strict` the proof of wellfoundedness +* In `Data.Product.Relation.Binary.Lex.Strict` the proof of wellfoundedness of the lexicographic ordering on products, no longer requires the assumption of symmetry for the first equality relation `_≈₁_`. -* In `Data.Rational.Base` the constructors `+0` and `+[1+_]` from `Data.Integer.Base` +* In `Data.Rational.Base` the constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer re-exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)` directly to use them. -* In `Data.Rational(.Unnormalised).Properties` the types of the proofs - `pos⇒1/pos`/`1/pos⇒pos` and `neg⇒1/neg`/`1/neg⇒neg` have been switched, - as the previous naming scheme didn't correctly generalise to e.g. `pos+pos⇒pos`. +* In `Data.Rational(.Unnormalised).Properties` the types of the proofs + `pos⇒1/pos`/`1/pos⇒pos` and `neg⇒1/neg`/`1/neg⇒neg` have been switched, + as the previous naming scheme didn't correctly generalise to e.g. `pos+pos⇒pos`. For example the types of `pos⇒1/pos`/`1/pos⇒pos` were: ```agda pos⇒1/pos : ∀ p .{{_ : NonZero p}} .{{Positive (1/ p)}} → Positive p @@ -1111,7 +1132,7 @@ Non-backwards compatible changes * In `Data.Vec.Base` the definition of `_>>=_` under `Data.Vec.Base` has been moved to the submodule `CartesianBind` in order to avoid clashing with the - new, alternative definition of `_>>=_`, located in the second new submodule + new, alternative definition of `_>>=_`, located in the second new submodule `DiagonalBind`. * In `Data.Vec.Base` the definitions `init` and `last` have been changed from the `initLast` @@ -1119,15 +1140,15 @@ Non-backwards compatible changes * In `Data.Vec.Properties` the type of the proof `zipWith-comm` has been generalised from: ```agda - zipWith-comm : ∀ {f : A → A → B} (comm : ∀ x y → f x y ≡ f y x) (xs ys : Vec A n) → + zipWith-comm : ∀ {f : A → A → B} (comm : ∀ x y → f x y ≡ f y x) (xs ys : Vec A n) → zipWith f xs ys ≡ zipWith f ys xs ``` to ```agda - zipWith-comm : ∀ {f : A → B → C} {g : B → A → C} (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → + zipWith-comm : ∀ {f : A → B → C} {g : B → A → C} (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → zipWith f xs ys ≡ zipWith g ys xs ``` - + * In `Data.Vec.Relation.Unary.All` the functions `lookup` and `tabulate` have been moved to `Data.Vec.Relation.Unary.All.Properties` and renamed `lookup⁺` and `lookup⁻` respectively. @@ -1139,15 +1160,15 @@ Non-backwards compatible changes iterate : (A → A) → A → ∀ n → Vec A n replicate : ∀ n → A → Vec A n ``` - -* In `Relation.Binary.Construct.Closure.Symmetric` the operation + +* In `Relation.Binary.Construct.Closure.Symmetric` the operation `SymClosure` on relations in has been reimplemented as a data type `SymClosure _⟶_ a b` that is parameterized by the input relation `_⟶_` (as well as the elements `a` and `b` of the domain) so that `_⟶_` can be inferred, which it could not from the previous implementation using the sum type `a ⟶ b ⊎ b ⟶ a`. -* In `Relation.Nullary.Decidable.Core` the name `excluded-middle` has been +* In `Relation.Nullary.Decidable.Core` the name `excluded-middle` has been renamed to `¬¬-excluded-middle`. @@ -1185,14 +1206,25 @@ Other major improvements * Raw bundles by design don't contain any proofs so should in theory be able to live in `Data.X.Base` rather than `Data.X.Bundles`. - + * To achieve this while keeping the dependency footprint small, the definitions of - raw bundles (`RawMagma`, `RawMonoid` etc.) have been moved from `Algebra(.Lattice)Bundles` to - a new module `Algebra(.Lattice).Bundles.Raw` which can be imported at much lower cost + raw bundles (`RawMagma`, `RawMonoid` etc.) have been moved from `Algebra(.Lattice)Bundles` to + a new module `Algebra(.Lattice).Bundles.Raw` which can be imported at much lower cost from `Data.X.Base`. * We have then moved raw bundles defined in `Data.X.Properties` to `Data.X.Base` for `X` = `Nat`/`Nat.Binary`/`Integer`/`Rational`/`Rational.Unnormalised`. + +### Upgrades to `README` sub-library + +* The `README` sub-library has been moved to `doc/README` and a new `doc/standard-library-doc.agda-lib` has been added. + +* The first consequence is that `README` files now can be type-checked in Emacs + using an out-of-the-box standard Agda installation without altering the main + `standard-library.agda-lib` file. + +* The second is that the `README` files are now their own first-class library + and can be imported like an other library. Deprecated modules ------------------ @@ -1201,7 +1233,7 @@ Deprecated modules * This fixes the fact we had picked the wrong name originally. The erased modality corresponds to `@0` whereas the irrelevance one corresponds to `.`. - + ### Deprecation of `Data.Fin.Substitution.Example` * The module `Data.Fin.Substitution.Example` has been deprecated, and moved to `README.Data.Fin.Substitution.UntypedLambda` @@ -1212,7 +1244,7 @@ Deprecated modules ### Deprecation of `Data.Product.Function.Dependent.Setoid.WithK` -* This module has been deprecated, as none of its contents actually depended on axiom K. +* This module has been deprecated, as none of its contents actually depended on axiom K. The contents has been moved to `Data.Product.Function.Dependent.Setoid`. ### Moving `Function.Related` @@ -1258,6 +1290,44 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Consequences.Propositional`: + ```agda + comm+assoc⇒middleFour ↦ comm∧assoc⇒middleFour + identity+middleFour⇒assoc ↦ identity∧middleFour⇒assoc + identity+middleFour⇒comm ↦ identity∧middleFour⇒comm + comm+distrˡ⇒distrʳ ↦ comm∧distrˡ⇒distrʳ + comm+distrʳ⇒distrˡ ↦ comm∧distrʳ⇒distrˡ + assoc+distribʳ+idʳ+invʳ⇒zeˡ ↦ assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ + assoc+distribˡ+idʳ+invʳ⇒zeʳ ↦ assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ + assoc+id+invʳ⇒invˡ-unique ↦ assoc∧id∧invʳ⇒invˡ-unique + assoc+id+invˡ⇒invʳ-unique ↦ assoc∧id∧invˡ⇒invʳ-unique + subst+comm⇒sym ↦ subst∧comm⇒sym + ``` + +* In `Algebra.Consequences.Setoid`: + ```agda + comm+assoc⇒middleFour ↦ comm∧assoc⇒middleFour + identity+middleFour⇒assoc ↦ identity∧middleFour⇒assoc + identity+middleFour⇒comm ↦ identity∧middleFour⇒comm + comm+cancelˡ⇒cancelʳ ↦ comm∧cancelˡ⇒cancelʳ + comm+cancelʳ⇒cancelˡ ↦ comm∧cancelʳ⇒cancelˡ + comm+almostCancelˡ⇒almostCancelʳ ↦ comm∧almostCancelˡ⇒almostCancelʳ + comm+almostCancelʳ⇒almostCancelˡ ↦ comm∧almostCancelʳ⇒almostCancelˡ + comm+idˡ⇒idʳ ↦ comm∧idˡ⇒idʳ + comm+idʳ⇒idˡ ↦ comm∧idʳ⇒idˡ + comm+zeˡ⇒zeʳ ↦ comm∧zeˡ⇒zeʳ + comm+zeʳ⇒zeˡ ↦ comm∧zeʳ⇒zeˡ + comm+invˡ⇒invʳ ↦ comm∧invˡ⇒invʳ + comm+invʳ⇒invˡ ↦ comm∧invʳ⇒invˡ + comm+distrˡ⇒distrʳ ↦ comm∧distrˡ⇒distrʳ + comm+distrʳ⇒distrˡ ↦ comm∧distrʳ⇒distrˡ + assoc+distribʳ+idʳ+invʳ⇒zeˡ ↦ assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ + assoc+distribˡ+idʳ+invʳ⇒zeʳ ↦ assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ + assoc+id+invʳ⇒invˡ-unique ↦ assoc∧id∧invʳ⇒invˡ-unique + assoc+id+invˡ⇒invʳ-unique ↦ assoc∧id∧invˡ⇒invʳ-unique + subst+comm⇒sym ↦ subst∧comm⇒sym + ``` + * In `Algebra.Construct.Zero`: ```agda rawMagma ↦ Algebra.Construct.Terminal.rawMagma @@ -1444,7 +1514,7 @@ Deprecated names * In `Data.List.Relation.Unary.All.Properties`: ```agda gmap ↦ gmap⁺ - + updateAt-id-relative ↦ updateAt-id-local updateAt-compose-relative ↦ updateAt-updateAt-local updateAt-compose ↦ updateAt-updateAt @@ -1713,6 +1783,16 @@ Deprecated names invPreorder ↦ converse-preorder ``` +* In `Relation.Binary.PropositionalEquality`: + ```agda + isPropositional ↦ Relation.Nullary.Irrelevant + ``` + +* In `Relation.Unary.Consequences`: + ```agda + dec⟶recomputable ↦ dec⇒recomputable + ``` + ## Missing fixity declarations added * An effort has been made to add sensible fixities for many declarations: @@ -2009,6 +2089,8 @@ New modules * Properties of various types of functions: ``` Function.Consequences + Function.Consequences.Setoid + Function.Consequences.Propositional Function.Properties.Bijection Function.Properties.RightInverse Function.Properties.Surjection @@ -2040,7 +2122,7 @@ New modules Relation.Unary.Algebra ``` -* Both versions of equality on predications are equivalences +* Both versions of equality on predicates are equivalences ``` Relation.Unary.Relation.Binary.Equality ``` @@ -2147,21 +2229,21 @@ Additions to existing modules * Added new proof to `Algebra.Consequences.Base`: ```agda - reflexive+selfInverse⇒involutive : Reflexive _≈_ → SelfInverse _≈_ f → Involutive _≈_ f + reflexive∧selfInverse⇒involutive : Reflexive _≈_ → SelfInverse _≈_ f → Involutive _≈_ f ``` * Added new proofs to `Algebra.Consequences.Propositional`: ```agda - comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ → _•_ MiddleFourExchange _•_ - identity+middleFour⇒assoc : Identity e _•_ → _•_ MiddleFourExchange _•_ → Associative _•_ - identity+middleFour⇒comm : Identity e _+_ → _•_ MiddleFourExchange _+_ → Commutative _•_ + comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_ + identity∧middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_ + identity∧middleFour⇒comm : Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_ ``` * Added new proofs to `Algebra.Consequences.Setoid`: ```agda - comm+assoc⇒middleFour : Congruent₂ _•_ → Commutative _•_ → Associative _•_ → _•_ MiddleFourExchange _•_ - identity+middleFour⇒assoc : Congruent₂ _•_ → Identity e _•_ → _•_ MiddleFourExchange _•_ → Associative _•_ - identity+middleFour⇒comm : Congruent₂ _•_ → Identity e _+_ → _•_ MiddleFourExchange _+_ → Commutative _•_ + comm∧assoc⇒middleFour : Congruent₂ _∙_ → Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_ + identity∧middleFour⇒assoc : Congruent₂ _∙_ → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_ + identity∧middleFour⇒comm : Congruent₂ _∙_ → Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_ involutive⇒surjective : Involutive f → Surjective f selfInverse⇒involutive : SelfInverse f → Involutive f @@ -2171,15 +2253,15 @@ Additions to existing modules selfInverse⇒injective : SelfInverse f → Injective f selfInverse⇒bijective : SelfInverse f → Bijective f - comm+idˡ⇒id : Commutative _•_ → LeftIdentity e _•_ → Identity e _•_ - comm+idʳ⇒id : Commutative _•_ → RightIdentity e _•_ → Identity e _•_ - comm+zeˡ⇒ze : Commutative _•_ → LeftZero e _•_ → Zero e _•_ - comm+zeʳ⇒ze : Commutative _•_ → RightZero e _•_ → Zero e _•_ - comm+invˡ⇒inv : Commutative _•_ → LeftInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_ - comm+invʳ⇒inv : Commutative _•_ → RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_ - comm+distrˡ⇒distr : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_ - comm+distrʳ⇒distr : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_ - distrib+absorbs⇒distribˡ : Associative _•_ → Commutative _◦_ → _•_ Absorbs _◦_ → _◦_ Absorbs _•_ → _◦_ DistributesOver _•_ → _•_ DistributesOverˡ _◦_ + comm∧idˡ⇒id : Commutative _∙_ → LeftIdentity e _∙_ → Identity e _∙_ + comm∧idʳ⇒id : Commutative _∙_ → RightIdentity e _∙_ → Identity e _∙_ + comm∧zeˡ⇒ze : Commutative _∙_ → LeftZero e _∙_ → Zero e _∙_ + comm∧zeʳ⇒ze : Commutative _∙_ → RightZero e _∙_ → Zero e _∙_ + comm∧invˡ⇒inv : Commutative _∙_ → LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_ + comm∧invʳ⇒inv : Commutative _∙_ → RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_ + comm∧distrˡ⇒distr : Commutative _∙_ → _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_ + comm∧distrʳ⇒distr : Commutative _∙_ → _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_ + distrib∧absorbs⇒distribˡ : Associative _∙_ → Commutative _◦_ → _∙_ Absorbs _◦_ → _◦_ Absorbs _∙_ → _◦_ DistributesOver _∙_ → _∙_ DistributesOverˡ _◦_ ``` * Added new functions to `Algebra.Construct.DirectProduct`: @@ -2190,8 +2272,8 @@ Additions to existing modules SemiringWithoutAnnihilatingZero b ℓ₂ → SemiringWithoutAnnihilatingZero (a ⊔ b) (ℓ₁ ⊔ ℓ₂) semiring : Semiring a ℓ₁ → Semiring b ℓ₂ → Semiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) - commutativeSemiring : CommutativeSemiring a ℓ₁ → - CommutativeSemiring b ℓ₂ → + commutativeSemiring : CommutativeSemiring a ℓ₁ → + CommutativeSemiring b ℓ₂ → CommutativeSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ring : Ring a ℓ₁ → Ring b ℓ₂ → Ring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) commutativeRing : CommutativeRing a ℓ₁ → CommutativeRing b ℓ₂ → CommutativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂) @@ -2199,14 +2281,14 @@ Additions to existing modules rawLoop : RawLoop a ℓ₁ → RawLoop b ℓ₂ → RawLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) unitalMagma : UnitalMagma a ℓ₁ → UnitalMagma b ℓ₂ → UnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) invertibleMagma : InvertibleMagma a ℓ₁ → InvertibleMagma b ℓ₂ → InvertibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) - invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → - InvertibleUnitalMagma b ℓ₂ → + invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → + InvertibleUnitalMagma b ℓ₂ → InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂) loop : Loop a ℓ₁ → Loop b ℓ₂ → Loop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) - idempotentSemiring : IdempotentSemiring a ℓ₁ → - IdempotentSemiring b ℓ₂ → - IdempotentSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + idempotentSemiring : IdempotentSemiring a ℓ₁ → + IdempotentSemiring b ℓ₂ → + IdempotentSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) idempotentMagma : IdempotentMagma a ℓ₁ → IdempotentMagma b ℓ₂ → IdempotentMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) alternativeMagma : AlternativeMagma a ℓ₁ → AlternativeMagma b ℓ₂ → AlternativeMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) flexibleMagma : FlexibleMagma a ℓ₁ → FlexibleMagma b ℓ₂ → FlexibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) @@ -2219,9 +2301,9 @@ Additions to existing modules moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) rawRingWithoutOne : RawRingWithoutOne a ℓ₁ → RawRingWithoutOne b ℓ₂ → RawRingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ringWithoutOne : RingWithoutOne a ℓ₁ → RingWithoutOne b ℓ₂ → RingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂) - nonAssociativeRing : NonAssociativeRing a ℓ₁ → - NonAssociativeRing b ℓ₂ → - NonAssociativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + nonAssociativeRing : NonAssociativeRing a ℓ₁ → + NonAssociativeRing b ℓ₂ → + NonAssociativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂) quasiring : Quasiring a ℓ₁ → Quasiring b ℓ₂ → Quasiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) nearring : Nearring a ℓ₁ → Nearring b ℓ₂ → Nearring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ``` @@ -2303,7 +2385,7 @@ Additions to existing modules * Added new proofs to `Algebra.Properties.CommutativeSemigroup`: ```agda xy∙xx≈x∙yxx : (x ∙ y) ∙ (x ∙ x) ≈ x ∙ (y ∙ (x ∙ x)) - + interchange : Interchangable _∙_ _∙_ leftSemimedial : LeftSemimedial _∙_ rightSemimedial : RightSemimedial _∙_ @@ -2401,7 +2483,7 @@ Additions to existing modules xor-annihilates-not : (not x) xor (not y) ≡ x xor y ``` -* Exposed container combinator conversion functions from `Data.Container.Combinator.Properties` +* Exposed container combinator conversion functions from `Data.Container.Combinator.Properties` separately from their correctness proofs in `Data.Container.Combinator`: ``` to-id : F.id A → ⟦ id ⟧ A @@ -2432,7 +2514,7 @@ Additions to existing modules ```agda spo-wellFounded : IsStrictPartialOrder _≈_ _⊏_ → WellFounded _⊏_ spo-noetherian : IsStrictPartialOrder _≈_ _⊏_ → WellFounded (flip _⊏_) - + <-weakInduction-startingFrom : P i → (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j ``` @@ -2503,7 +2585,7 @@ Additions to existing modules sub≡sub : map var (VarSubst.sub x) ≡ T.sub (T.var x) ↑≡↑ : map var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ /Var≡/ : t /Var ρ ≡ t T./ map T.var ρ - + sub-renaming-commutes : t /Var VarSubst.sub x T./ ρ ≡ t T./ ρ T.↑ T./ T.sub (lookup ρ x) sub-commutes-with-renaming : t T./ T.sub t′ /Var ρ ≡ t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) ``` @@ -2597,9 +2679,9 @@ Additions to existing modules * Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties`: ``` ⊆-mergeˡ : xs ⊆ merge _≤?_ xs ys - ⊆-mergeʳ : ys ⊆ merge _≤?_ xs ys + ⊆-mergeʳ : ys ⊆ merge _≤?_ xs ys ``` - + * Added new functions in `Data.List.Relation.Unary.All`: ``` decide : Π[ P ∪ Q ] → Π[ All P ∪ Any Q ] @@ -2626,7 +2708,7 @@ Additions to existing modules mapWith∈-id : mapWith∈ xs (λ {x} _ → x) ≡ xs map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) index-injective : index x₁∈xs ≡ index x₂∈xs → x₁ ≈ x₂ - + ∈-++⁺∘++⁻ : (p : v ∈ xs ++ ys) → [ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ (∈-++⁻ xs p) ≡ p ∈-++⁻∘++⁺ : (p : v ∈ xs ⊎ v ∈ ys) → ∈-++⁻ xs ([ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ p) ≡ p ∈-++↔ : (v ∈ xs ⊎ v ∈ ys) ↔ v ∈ xs ++ ys @@ -2677,12 +2759,12 @@ Additions to existing modules length-removeAt′ : length xs ≡ suc (length (removeAt xs k)) removeAt-insertAt : removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs insertAt-removeAt : insertAt (removeAt xs i) (cast (sym (lengthAt-removeAt xs i)) i) (lookup xs i) ≡ xs - + cartesianProductWith-zeroˡ : cartesianProductWith f [] ys ≡ [] cartesianProductWith-zeroʳ : cartesianProductWith f xs [] ≡ [] cartesianProductWith-distribʳ-++ : cartesianProductWith f (xs ++ ys) zs ≡ cartesianProductWith f xs zs ++ cartesianProductWith f ys zs - + foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs ``` @@ -2728,6 +2810,18 @@ Additions to existing modules s≤″s⁻¹ : suc m ≤″ suc n → m ≤″ n s<″s⁻¹ : suc m <″ suc n → m <″ n + pattern 2+ n = suc (suc n) + pattern 1<2+n {n} = s1⇒nonTrivial : 1 < n → NonTrivial n + nonZero⇒≢1⇒nonTrivial : .{{NonZero n}} → n ≢ 1 → NonTrivial n + recompute-nonTrivial : .{{NonTrivial n}} → NonTrivial n + nonTrivial⇒nonZero : .{{NonTrivial n}} → NonZero n + nonTrivial⇒n>1 : .{{NonTrivial n}} → 1 < n + nonTrivial⇒≢1 : .{{NonTrivial n}} → n ≢ 1 + _⊔′_ : ℕ → ℕ → ℕ _⊓′_ : ℕ → ℕ → ℕ ∣_-_∣′ : ℕ → ℕ → ℕ @@ -2753,20 +2847,42 @@ Additions to existing modules <-asym : Asymmetric _<_ ``` -* Added a new pattern synonym to `Data.Nat.Divisibility.Core`: +* Added a new pattern synonym and a new definition to `Data.Nat.Divisibility.Core`: ```agda pattern divides-refl q = divides q refl + record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where ``` -* Added new definitions and proofs to `Data.Nat.Primality`: +* Added new proofs to `Data.Nat.Divisibility`: ```agda - Composite : ℕ → Set - composite? : Decidable composite - composite⇒¬prime : Composite n → ¬ Prime n - ¬composite⇒prime : 2 ≤ n → ¬ Composite n → Prime n - prime⇒¬composite : Prime n → ¬ Composite n - ¬prime⇒composite : 2 ≤ n → ¬ Prime n → Composite n - euclidsLemma : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n + hasNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → n HasNonTrivialDivisorLessThan n + hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n → m ∣ o → o HasNonTrivialDivisorLessThan n + hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n → n ≤ o → m HasNonTrivialDivisorLessThan o + ``` + +* Added new definitions, smart constructors and proofs to `Data.Nat.Primality`: + ```agda + infix 10 _Rough_ + _Rough_ : ℕ → Pred ℕ _ + 0-rough : 0 Rough n + 1-rough : 1 Rough n + 2-rough : 2 Rough n + rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n + ∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n + rough∧∣⇒rough : m Rough o → n ∣ o → m Rough n + Composite : ℕ → Set + composite-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → Composite n + composite-∣ : .{{NonZero n}} → Composite m → m ∣ n → Composite n + composite? : Decidable Composite + Irreducible : ℕ → Set + irreducible? : Decidable Irreducible + composite⇒¬prime : Composite n → ¬ Prime n + ¬composite⇒prime : .{{NonTrivial n} → ¬ Composite n → Prime n + prime⇒¬composite : Prime n → ¬ Composite n + ¬prime⇒composite : .{{NonTrivial n} → ¬ Prime n → Composite n + prime⇒irreducible : Prime p → Irreducible p + irreducible⇒prime : .{{NonTrivial p}} → Irreducible p → Prime p + euclidsLemma : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n ``` * Added new proofs in `Data.Nat.Properties`: @@ -2776,8 +2892,12 @@ Additions to existing modules n+1+m≢m : n + suc m ≢ m m*n≡0⇒m≡0 : .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0 n>0⇒n≢0 : n > 0 → n ≢ 0 - m^n≢0 : .{{_ : NonZero m}} → NonZero (m ^ n) m*n≢0 : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n) + m*n≢0⇒m≢0 : .{{NonZero (m * n)}} → NonZero m + m*n≢0⇒n≢0 : .{{NonZero (m * n)}} → NonZero n + m≢0∧n>1⇒m*n>1 : .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n) + n≢0∧m>1⇒m*n>1 : .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n) + m^n≢0 : .{{_ : NonZero m}} → NonZero (m ^ n) m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n s-connex : Connex _≥_ _>_ @@ -2852,21 +2972,21 @@ Additions to existing modules m%n≤n : .{{_ : NonZero n}} → m % n ≤ n m*n/m!≡n/[m∸1]! : .{{_ : NonZero m}} → m * n / m ! ≡ n / (pred m) ! - %-congˡ : .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o - %-congʳ : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ≡ n → o % m ≡ o % n - m≤n⇒[n∸m]%m≡n%m : .⦃ _ : NonZero m ⦄ → m ≤ n → (n ∸ m) % m ≡ n % m - m*n≤o⇒[o∸m*n]%n≡o%n : .⦃ _ : NonZero n ⦄ → m * n ≤ o → (o ∸ m * n) % n ≡ o % n - m∣n⇒o%n%m≡o%m : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ∣ n → o % n % m ≡ o % m - m_ : (a : A) → (∀ a → B a) → B a _!|>′_ : A → (A → B) → B ``` - + * Added new proof and record in `Function.Structures`: ```agda record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) @@ -3454,7 +3574,7 @@ Additions to existing modules ⊂-resp-≐ : _⊂_ Respects₂ _≐_ ⊂-irrefl : Irreflexive _≐_ _⊂_ ⊂-antisym : Antisymmetric _≐_ _⊂_ - + ∅-⊆′ : (P : Pred A ℓ) → ∅ ⊆′ P ⊆′-U : (P : Pred A ℓ) → P ⊆′ U ⊆′-refl : Reflexive {A = Pred A ℓ} _⊆′_ @@ -3476,7 +3596,7 @@ Additions to existing modules ⊆′⇒⊆ : _⊆′_ ⇒ _⊆_ ⊂⇒⊂′ : _⊂_ ⇒ _⊂′_ ⊂′⇒⊂ : _⊂′_ ⇒ _⊂_ - + ≐-refl : Reflexive _≐_ ≐-sym : Sym _≐_ _≐_ ≐-trans : Trans _≐_ _≐_ _≐_ @@ -3563,6 +3683,12 @@ Additions to existing modules poset : Set a → Poset _ _ _ ``` +* Added new proof in `Relation.Nullary.Reflects`: + ```agda + T-reflects : Reflects (T b) b + T-reflects-elim : Reflects (T a) b → b ≡ a + ``` + * Added new operations in `System.Exit`: ``` isSuccess : ExitCode → Bool @@ -3597,7 +3723,9 @@ This is a full list of proofs that have changed form to use irrelevant instance * In `Data.Nat.Coprimality`: ``` - Bézout-coprime : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j + ¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2 + n) + Bézout-coprime : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j + prime⇒coprime : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n ``` * In `Data.Nat.Divisibility` diff --git a/CITATION.cff b/CITATION.cff index 416e595b98..5e965d00fa 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: 1.7.2 -date-released: 2023-02-01 +version: 2.0 +date-released: 2023-12-11 url: "https://github.com/agda/agda-stdlib" \ No newline at end of file diff --git a/GNUmakefile b/GNUmakefile index 685d1c990b..e744f066cc 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -9,11 +9,14 @@ AGDA=$(AGDA_EXEC) $(AGDA_OPTIONS) $(AGDA_RTS_OPTIONS) # cabal install fix-whitespace test: Everything.agda check-whitespace - $(AGDA) -i. -isrc README.agda + cd doc && $(AGDA) README.agda testsuite: $(MAKE) -C tests test AGDA="$(AGDA)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only) +fix-whitespace: + cabal exec -- fix-whitespace + check-whitespace: cabal exec -- fix-whitespace --check @@ -21,11 +24,12 @@ setup: Everything.agda .PHONY: Everything.agda Everything.agda: - cabal run GenerateEverything + cabal run GenerateEverything -- --out-dir doc .PHONY: listings listings: Everything.agda - $(AGDA) -i. -isrc --html README.agda -v0 + cd doc && $(AGDA) --html README.agda -v0 clean : find . -type f -name '*.agdai' -delete + rm -f Everything.agda EverythingSafe.agda diff --git a/GenerateEverything.hs b/GenerateEverything.hs index ee49679f3a..f6add73649 100644 --- a/GenerateEverything.hs +++ b/GenerateEverything.hs @@ -1,5 +1,7 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE MultiWayIf #-} import Control.Applicative import Control.Monad @@ -226,10 +228,10 @@ extractHeader mod = extract -- | A crude classifier looking for lines containing options -data Status = Deprecated | Unsafe | Safe - deriving (Eq) +data Safety = Unsafe | Safe deriving (Eq) +data Status = Deprecated | Active deriving (Eq) -classify :: FilePath -> [String] -> [String] -> Exc Status +classify :: FilePath -> [String] -> [String] -> Exc (Safety, Status) classify fp hd ls -- We start with sanity checks | isUnsafe && safe = throwError $ fp ++ contradiction "unsafe" "safe" @@ -238,11 +240,12 @@ classify fp hd ls | isWithK && not withK = throwError $ fp ++ missingWithK | not (isWithK || cubicalC) = throwError $ fp ++ uncategorized "as relying on K" "cubical-compatible" -- And then perform the actual classification - | deprecated = pure $ Deprecated - | isUnsafe = pure $ Unsafe - | safe = pure $ Safe - -- We know that @not (isUnsafe || safe)@, all cases are covered - | otherwise = error "IMPOSSIBLE" + | otherwise = do + let safety = if | safe -> Safe + | isUnsafe -> Unsafe + | otherwise -> error "IMPOSSIBLE" + let status = if deprecated then Deprecated else Active + pure (safety, status) where @@ -279,18 +282,20 @@ classify fp hd ls data LibraryFile = LibraryFile { filepath :: FilePath -- ^ FilePath of the source file , header :: [String] -- ^ All lines in the headers are already prefixed with \"-- \". - , status :: Status -- ^ Safety options used by the module + , safety :: Safety + , status :: Status -- ^ Deprecation status options used by the module } analyse :: FilePath -> IO LibraryFile analyse fp = do ls <- lines <$> readFileUTF8 fp hd <- runExc $ extractHeader fp ls - cl <- runExc $ classify fp hd ls + (sf, st) <- runExc $ classify fp hd ls return $ LibraryFile - { filepath = fp - , header = hd - , status = cl + { filepath = fp + , header = hd + , safety = sf + , status = st } checkFilePaths :: String -> [FilePath] -> IO () @@ -299,18 +304,37 @@ checkFilePaths cat fps = forM_ fps $ \ fp -> do unless b $ die $ fp ++ " is listed as " ++ cat ++ " but does not exist." +data Options = Options + { includeDeprecated :: Bool + , outputDirectory :: FilePath + } + +initOptions :: Options +initOptions = Options + { includeDeprecated = False + , outputDirectory = "." + } + +parseOptions :: [String] -> Options -> Maybe Options +parseOptions [] opts = pure opts +parseOptions ("--include-deprecated" : rest) opts + = parseOptions rest (opts { includeDeprecated = True }) +parseOptions ("--out-dir" : dir : rest) opts + = parseOptions rest (opts { outputDirectory = dir }) +parseOptions _ _ = Nothing + --------------------------------------------------------------------------- -- Collecting all non-Core library files, analysing them and generating --- 4 files: +-- 2 files: -- Everything.agda all the modules -- EverythingSafe.agda all the safe modules +main :: IO () main = do args <- getArgs - includeDeprecated <- case args of - [] -> return False - ["--include-deprecated"] -> return True - _ -> hPutStr stderr usage >> exitFailure + Options{..} <- case parseOptions args initOptions of + Just opts -> pure opts + Nothing -> hPutStr stderr usage >> exitFailure checkFilePaths "unsafe" unsafeModules checkFilePaths "using K" withKModules @@ -325,18 +349,18 @@ main = do let mkModule str = "module " ++ str ++ " where" - writeFileUTF8 (allOutputFile ++ ".agda") $ + writeFileUTF8 (outputDirectory ++ "/" ++ allOutputFile ++ ".agda") $ unlines [ header , "{-# OPTIONS --rewriting --guardedness --sized-types #-}\n" , mkModule allOutputFile , format libraryfiles ] - writeFileUTF8 (safeOutputFile ++ ".agda") $ + writeFileUTF8 (outputDirectory ++ "/" ++ safeOutputFile ++ ".agda") $ unlines [ header , "{-# OPTIONS --safe --guardedness #-}\n" , mkModule safeOutputFile - , format $ filter ((Unsafe /=) . status) libraryfiles + , format $ filter ((Unsafe /=) . safety) libraryfiles ] -- | Usage info. @@ -353,6 +377,9 @@ usage = unlines , "The program generates documentation for the library by extracting" , "headers from library modules. The output is written to " ++ allOutputFile , "with the file " ++ headerFile ++ " inserted verbatim at the beginning." + , "" + , "If the option --out-dir is used then the output is placed in the" + , "subdirectory thus selected." ] diff --git a/HACKING.md b/HACKING.md index b2d619ec32..9b0e7454ac 100644 --- a/HACKING.md +++ b/HACKING.md @@ -4,7 +4,7 @@ Contributing to the library Thank you for your interest in contributing to the Agda standard library. Hopefully this guide should make it easy to do so! Feel free to ask any questions on the Agda mailing list. Before you start please read the -[style-guide](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md). +[style-guide](https://github.com/agda/agda-stdlib/blob/master/doc/style-guide.md). What is an acceptable contribution? =================================== @@ -124,7 +124,7 @@ git push USER -u new_feature You can then proceed to make your changes. Please follow existing conventions in the library, see -[style-guide](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md). +[style-guide](https://github.com/agda/agda-stdlib/blob/master/doc/style-guide.md). for details. Document your changes in `agda-stdlib-fork/CHANGELOG.md`. If you are creating new modules, please make sure you are having a @@ -244,23 +244,14 @@ you are never committing anything with a whitespace violation: Type-checking the README directory ---------------------------------- -* By default the README directory is not exported in the - `standard-library.agda-lib` file in order to avoid clashing with other people's - README files. This means that by default type-checking a file in the README - directory fails. - -* If you wish to type-check a README file, then you will need to change the line: - ``` - include: src - ``` - to - ``` - include: src . - ``` - in the `standard-library.agda-lib` file. - -* Please do not include this change in your pull request. +* By default the README files are not exported in the + `standard-library.agda-lib` file in order to avoid + clashing with other people's README files. +* If you wish to type-check a README file, then you will + need to change the present working directory to `doc/` + where an appropriate `standard-library-doc.agda-lib` + file is present. Continuous Integration (CI) =========================== diff --git a/LICENCE b/LICENCE index df31f24985..3a9d1c3624 100644 --- a/LICENCE +++ b/LICENCE @@ -1,4 +1,4 @@ -Copyright (c) 2007-2021 Nils Anders Danielsson, Ulf Norell, Shin-Cheng +Copyright (c) 2007-2023 Nils Anders Danielsson, Ulf Norell, Shin-Cheng Mu, Bradley Hardy, Samuel Bronson, Dan Doel, Patrik Jansson, Liang-Ting Chen, Jean-Philippe Bernardy, Andrés Sicard-Ramírez, Nicolas Pouillard, Darin Morrison, Peter Berry, Daniel Brown, diff --git a/README.md b/README.md index 16a2f10959..3c66d46ee0 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -![Travis (.org) branch](https://img.shields.io/travis/agda/agda-stdlib/master?label=master) -![Travis (.org) branch](https://img.shields.io/travis/agda/agda-stdlib/experimental?label=experimental) +[![Ubuntu build](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml/badge.svg)](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml) +[![Ubuntu build](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml/badge.svg?branch=experimental)](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml) The Agda standard library ========================= @@ -18,23 +18,19 @@ If you're looking to find your way around the library, there are several different ways to get started: - The library's structure and the associated design choices are described -in the [README.agda](https://github.com/agda/agda-stdlib/tree/master/README.agda). +in the [README.agda](https://github.com/agda/agda-stdlib/tree/master/doc/README.agda). -- The [README folder](https://github.com/agda/agda-stdlib/tree/master/README), +- The [README folder](https://github.com/agda/agda-stdlib/tree/master/doc/README), which mirrors the structure of the main library, contains examples of how to use some of the more common modules. Feel free to [open a new issue](https://github.com/agda/agda-stdlib/issues/new) if there's a particular module you feel could do with some more documentation. -- You can [browse the library's source code](https://agda.github.io/agda-stdlib/README.html) +- You can [browse the library's source code](https://agda.github.io/agda-stdlib/) in glorious clickable HTML. -- Finally, you can get an overview of the entire library by looking at the -[index](https://agda.github.io/agda-stdlib/), which lists all modules -in the library except the deprecated ones. - ## Installation instructions -See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md) for the latest version of the standard library. +See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/doc/installation-guide.md) for the latest version of the standard library. #### Old versions of Agda diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal index a482bee069..3accc6972e 100644 --- a/agda-stdlib-utils.cabal +++ b/agda-stdlib-utils.cabal @@ -6,9 +6,9 @@ description: Helper programs for setting up the Agda standard library. license: MIT tested-with: - GHC == 9.8.0 - GHC == 9.6.2 - GHC == 9.4.6 + GHC == 9.8.1 + GHC == 9.6.3 + GHC == 9.4.7 GHC == 9.2.8 GHC == 9.0.2 GHC == 8.10.7 diff --git a/dev/.gitignore b/dev/.gitignore new file mode 100644 index 0000000000..f59ec20aab --- /dev/null +++ b/dev/.gitignore @@ -0,0 +1 @@ +* \ No newline at end of file diff --git a/dev/README.md b/dev/README.md new file mode 100644 index 0000000000..d97d344209 --- /dev/null +++ b/dev/README.md @@ -0,0 +1,4 @@ +# Development playground + +This directory allows you to develop modules against the current dev +version of the stdlib as it currently sits in `src/`. diff --git a/dev/experimental.agda-lib b/dev/experimental.agda-lib new file mode 100644 index 0000000000..cb094977d8 --- /dev/null +++ b/dev/experimental.agda-lib @@ -0,0 +1,4 @@ +name: standard-library-dev +include: . ../src +flags: + --warning=noUnsupportedIndexedMatch diff --git a/README.agda b/doc/README.agda similarity index 98% rename from README.agda rename to doc/README.agda index ced0f11596..41b536a0d0 100644 --- a/README.agda +++ b/doc/README.agda @@ -7,7 +7,7 @@ module README where -- -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais -- with contributions from Andreas Abel, Stevan Andjelkovic, --- Jean-Philippe Bernardy, Peter Berry, Bradley Hardy Joachim Breitner, +-- Jean-Philippe Bernardy, Peter Berry, Bradley Hardy, Joachim Breitner, -- Samuel Bronson, Daniel Brown, Jacques Carette, James Chapman, -- Liang-Ting Chen, Dominique Devriese, Dan Doel, Érdi Gergő, -- Zack Grannan, Helmut Grohne, Simon Foster, Liyang Hu, Jason Hu, @@ -19,7 +19,7 @@ module README where -- and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.3. +-- This version of the library has been tested using Agda 2.6.4. -- The library comes with a .agda-lib file, for use with the library -- management system. diff --git a/README/Axiom.agda b/doc/README/Axiom.agda similarity index 100% rename from README/Axiom.agda rename to doc/README/Axiom.agda diff --git a/README/Case.agda b/doc/README/Case.agda similarity index 100% rename from README/Case.agda rename to doc/README/Case.agda diff --git a/README/Data.agda b/doc/README/Data.agda similarity index 100% rename from README/Data.agda rename to doc/README/Data.agda diff --git a/README/Data/Container/FreeMonad.agda b/doc/README/Data/Container/FreeMonad.agda similarity index 100% rename from README/Data/Container/FreeMonad.agda rename to doc/README/Data/Container/FreeMonad.agda diff --git a/README/Data/Container/Indexed.agda b/doc/README/Data/Container/Indexed.agda similarity index 100% rename from README/Data/Container/Indexed.agda rename to doc/README/Data/Container/Indexed.agda diff --git a/README/Data/Default.agda b/doc/README/Data/Default.agda similarity index 100% rename from README/Data/Default.agda rename to doc/README/Data/Default.agda diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/doc/README/Data/Fin/Relation/Unary/Top.agda similarity index 100% rename from README/Data/Fin/Relation/Unary/Top.agda rename to doc/README/Data/Fin/Relation/Unary/Top.agda diff --git a/README/Data/Fin/Substitution/UntypedLambda.agda b/doc/README/Data/Fin/Substitution/UntypedLambda.agda similarity index 100% rename from README/Data/Fin/Substitution/UntypedLambda.agda rename to doc/README/Data/Fin/Substitution/UntypedLambda.agda diff --git a/README/Data/Integer.agda b/doc/README/Data/Integer.agda similarity index 100% rename from README/Data/Integer.agda rename to doc/README/Data/Integer.agda diff --git a/README/Data/List.agda b/doc/README/Data/List.agda similarity index 100% rename from README/Data/List.agda rename to doc/README/Data/List.agda diff --git a/README/Data/List/Fresh.agda b/doc/README/Data/List/Fresh.agda similarity index 100% rename from README/Data/List/Fresh.agda rename to doc/README/Data/List/Fresh.agda diff --git a/README/Data/List/Membership.agda b/doc/README/Data/List/Membership.agda similarity index 100% rename from README/Data/List/Membership.agda rename to doc/README/Data/List/Membership.agda diff --git a/README/Data/List/Relation/Binary/Equality.agda b/doc/README/Data/List/Relation/Binary/Equality.agda similarity index 100% rename from README/Data/List/Relation/Binary/Equality.agda rename to doc/README/Data/List/Relation/Binary/Equality.agda diff --git a/README/Data/List/Relation/Binary/Permutation.agda b/doc/README/Data/List/Relation/Binary/Permutation.agda similarity index 100% rename from README/Data/List/Relation/Binary/Permutation.agda rename to doc/README/Data/List/Relation/Binary/Permutation.agda diff --git a/README/Data/List/Relation/Binary/Pointwise.agda b/doc/README/Data/List/Relation/Binary/Pointwise.agda similarity index 100% rename from README/Data/List/Relation/Binary/Pointwise.agda rename to doc/README/Data/List/Relation/Binary/Pointwise.agda diff --git a/README/Data/List/Relation/Binary/Subset.agda b/doc/README/Data/List/Relation/Binary/Subset.agda similarity index 100% rename from README/Data/List/Relation/Binary/Subset.agda rename to doc/README/Data/List/Relation/Binary/Subset.agda diff --git a/README/Data/List/Relation/Ternary/Interleaving.agda b/doc/README/Data/List/Relation/Ternary/Interleaving.agda similarity index 100% rename from README/Data/List/Relation/Ternary/Interleaving.agda rename to doc/README/Data/List/Relation/Ternary/Interleaving.agda diff --git a/README/Data/List/Relation/Unary/All.agda b/doc/README/Data/List/Relation/Unary/All.agda similarity index 100% rename from README/Data/List/Relation/Unary/All.agda rename to doc/README/Data/List/Relation/Unary/All.agda diff --git a/README/Data/List/Relation/Unary/Any.agda b/doc/README/Data/List/Relation/Unary/Any.agda similarity index 100% rename from README/Data/List/Relation/Unary/Any.agda rename to doc/README/Data/List/Relation/Unary/Any.agda diff --git a/README/Data/Nat.agda b/doc/README/Data/Nat.agda similarity index 100% rename from README/Data/Nat.agda rename to doc/README/Data/Nat.agda diff --git a/README/Data/Nat/Induction.agda b/doc/README/Data/Nat/Induction.agda similarity index 100% rename from README/Data/Nat/Induction.agda rename to doc/README/Data/Nat/Induction.agda diff --git a/README/Data/Record.agda b/doc/README/Data/Record.agda similarity index 100% rename from README/Data/Record.agda rename to doc/README/Data/Record.agda diff --git a/README/Data/Tree/AVL.agda b/doc/README/Data/Tree/AVL.agda similarity index 100% rename from README/Data/Tree/AVL.agda rename to doc/README/Data/Tree/AVL.agda diff --git a/README/Data/Tree/Binary.agda b/doc/README/Data/Tree/Binary.agda similarity index 100% rename from README/Data/Tree/Binary.agda rename to doc/README/Data/Tree/Binary.agda diff --git a/README/Data/Tree/Rose.agda b/doc/README/Data/Tree/Rose.agda similarity index 100% rename from README/Data/Tree/Rose.agda rename to doc/README/Data/Tree/Rose.agda diff --git a/README/Data/Trie/NonDependent.agda b/doc/README/Data/Trie/NonDependent.agda similarity index 100% rename from README/Data/Trie/NonDependent.agda rename to doc/README/Data/Trie/NonDependent.agda diff --git a/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda similarity index 100% rename from README/Data/Vec/Relation/Binary/Equality/Cast.agda rename to doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda diff --git a/README/Data/Wrap.agda b/doc/README/Data/Wrap.agda similarity index 100% rename from README/Data/Wrap.agda rename to doc/README/Data/Wrap.agda diff --git a/README/Debug/Trace.agda b/doc/README/Debug/Trace.agda similarity index 100% rename from README/Debug/Trace.agda rename to doc/README/Debug/Trace.agda diff --git a/README/Design/Decidability.agda b/doc/README/Design/Decidability.agda similarity index 100% rename from README/Design/Decidability.agda rename to doc/README/Design/Decidability.agda diff --git a/README/Design/Fixity.agda b/doc/README/Design/Fixity.agda similarity index 100% rename from README/Design/Fixity.agda rename to doc/README/Design/Fixity.agda diff --git a/README/Design/Hierarchies.agda b/doc/README/Design/Hierarchies.agda similarity index 99% rename from README/Design/Hierarchies.agda rename to doc/README/Design/Hierarchies.agda index bc9220ba23..71ca5eed44 100644 --- a/README/Design/Hierarchies.agda +++ b/doc/README/Design/Hierarchies.agda @@ -265,7 +265,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where -- IsA A -- / || \ / || \ -- IsB IsC IsD B C D - + -- The procedure for re-exports in the bundles is as follows: -- 1. `open IsA isA public using (IsC, M)` where `M` is everything @@ -280,7 +280,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where -- 5. `open B b public using (O)` where `O` is everything exported -- by `B` but not exported by `IsA`. - + -- 6. Construct `d : D` via the `isC` obtained in step 1. -- 7. `open D d public using (P)` where `P` is everything exported diff --git a/README/Foreign/Haskell.agda b/doc/README/Foreign/Haskell.agda similarity index 100% rename from README/Foreign/Haskell.agda rename to doc/README/Foreign/Haskell.agda diff --git a/README/Function/Reasoning.agda b/doc/README/Function/Reasoning.agda similarity index 100% rename from README/Function/Reasoning.agda rename to doc/README/Function/Reasoning.agda diff --git a/README/IO.agda b/doc/README/IO.agda similarity index 100% rename from README/IO.agda rename to doc/README/IO.agda diff --git a/README/Inspect.agda b/doc/README/Inspect.agda similarity index 100% rename from README/Inspect.agda rename to doc/README/Inspect.agda diff --git a/README/Nary.agda b/doc/README/Nary.agda similarity index 100% rename from README/Nary.agda rename to doc/README/Nary.agda diff --git a/README/Reflection/External.agda b/doc/README/Reflection/External.agda similarity index 100% rename from README/Reflection/External.agda rename to doc/README/Reflection/External.agda diff --git a/README/Relation/Binary/TypeClasses.agda b/doc/README/Relation/Binary/TypeClasses.agda similarity index 100% rename from README/Relation/Binary/TypeClasses.agda rename to doc/README/Relation/Binary/TypeClasses.agda diff --git a/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda similarity index 100% rename from README/Tactic/Cong.agda rename to doc/README/Tactic/Cong.agda diff --git a/README/Tactic/MonoidSolver.agda b/doc/README/Tactic/MonoidSolver.agda similarity index 100% rename from README/Tactic/MonoidSolver.agda rename to doc/README/Tactic/MonoidSolver.agda diff --git a/README/Tactic/RingSolver.agda b/doc/README/Tactic/RingSolver.agda similarity index 100% rename from README/Tactic/RingSolver.agda rename to doc/README/Tactic/RingSolver.agda diff --git a/README/Text/Pretty.agda b/doc/README/Text/Pretty.agda similarity index 100% rename from README/Text/Pretty.agda rename to doc/README/Text/Pretty.agda diff --git a/README/Text/Printf.agda b/doc/README/Text/Printf.agda similarity index 100% rename from README/Text/Printf.agda rename to doc/README/Text/Printf.agda diff --git a/README/Text/Regex.agda b/doc/README/Text/Regex.agda similarity index 100% rename from README/Text/Regex.agda rename to doc/README/Text/Regex.agda diff --git a/README/Text/Tabular.agda b/doc/README/Text/Tabular.agda similarity index 100% rename from README/Text/Tabular.agda rename to doc/README/Text/Tabular.agda diff --git a/notes/installation-guide.md b/doc/installation-guide.md similarity index 85% rename from notes/installation-guide.md rename to doc/installation-guide.md index f05f21ed90..956fc317db 100644 --- a/notes/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 v1.7.2 of the standard library with Agda 2.6.3. +Use version v2.0 of the standard library with Agda 2.6.4 or 2.6.4.1. 1. Navigate to a suitable directory `$HERE` (replace appropriately) where you would like to install the library. -2. Download the tarball of v1.7.2 of the standard library. This can either be +2. Download the tarball of v2.0 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/v1.7.2.tar.gz + wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.0.tar.gz ``` Note that you can replace `wget` with other popular tools such as `curl` and that - you can replace `1.7.2` with any other version of the library you desire. + you can replace `2.0` 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 v1.7.2 of the standard library with Agda 2.6.3. 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run the commands to install via cabal: ``` - cd agda-stdlib-1.7.2 + cd agda-stdlib-2.0 cabal install ``` @@ -40,7 +40,7 @@ Use version v1.7.2 of the standard library with Agda 2.6.3. 6. Register the standard library with Agda's package system by adding the following line to `$HOME/.agda/libraries`: ``` - $HERE/agda-stdlib-1.7.2/standard-library.agda-lib + $HERE/agda-stdlib-2.0/standard-library.agda-lib ``` Now, the standard library is ready to be used either: diff --git a/notes/release-guide.txt b/doc/release-guide.txt similarity index 80% rename from notes/release-guide.txt rename to doc/release-guide.txt index 2f3f9d862f..0c60b5d4b3 100644 --- a/notes/release-guide.txt +++ b/doc/release-guide.txt @@ -3,7 +3,7 @@ procedure should be followed: #### Pre-release changes -* Update `README.agda` by replacing 'development version' by 'version X.Y' in the title. +* Update `doc/README.agda` by replacing 'development version' by 'version X.Y' in the title. * Update the version to `X.Y` in: - `agda-stdlib-utils.cabal` @@ -11,7 +11,7 @@ procedure should be followed: - `CITATION.cff` - `CHANGELOG.md` - `README.md` - - `notes/installation-guide.txt` + - `doc/installation-guide.md` * Update the copyright year range in the LICENSE file, if necessary. @@ -61,20 +61,12 @@ procedure should be followed: * Announce the release of the new version on the Agda mailing lists (users and developers). -* Add v$VERSION to the list of protected directories in the .travis.yml - file of BOTH master and experimental. They should look something like: - - > git checkout HEAD -- v0.16/ v0.17/ v1.0/ v1.1/ (...) - - Commit & push these changes. This will prevent the next step from being - overwritten by travis. - * Generate and upload documentation for the released version: - cp travis/* . + cp .github/tooling/* . runhaskell GenerateEverything.hs ./index.sh - agda -i. -isrc --html index.agda + agda -i. -idoc -isrc --html index.agda mv html v$VERSION git checkout gh-pages git add v$VERSION/*.html v$VERSION/*.css diff --git a/doc/standard-library-doc.agda-lib b/doc/standard-library-doc.agda-lib new file mode 100644 index 0000000000..02aaaba402 --- /dev/null +++ b/doc/standard-library-doc.agda-lib @@ -0,0 +1,4 @@ +name: standard-library-doc +include: . ../src +flags: + --warning=noUnsupportedIndexedMatch diff --git a/notes/style-guide.md b/doc/style-guide.md similarity index 85% rename from notes/style-guide.md rename to doc/style-guide.md index d6201abe88..5732747cda 100644 --- a/notes/style-guide.md +++ b/doc/style-guide.md @@ -333,6 +333,16 @@ line of code, indented by two spaces. ... | false = filter p xs ``` +* Instance arguments, and their types, should use the vanilla ASCII/UTF-8 `{{_}}` + syntax in preference to the Unicode `⦃_⦄` syntax (written using `\{{`/`\}}`), + which moreover requires additional whitespace to parse correctly. + NB. Even for irrelevant instances, such as typically for `NonZero` arguments, + neverthelesss it is necessary to supply an underscore binding `{{_ : NonZero n}}` + if subsequent terms occurring in the type rely on that argument to be well-formed: + eg in `Data.Nat.DivMod`, in the use of `_/ n` and `_% n` + ```agda + m≡m%n+[m/n]*n : ∀ m n .{{_ : NonZero n}} → m ≡ m % n + (m / n) * n + ``` ## Types @@ -347,12 +357,12 @@ line of code, indented by two spaces. #### Variables -* `Level` and `Set`s can always be generalized using the keyword `variable`. +* `Level` and `Set`s can always be generalised using the keyword `variable`. * A file may only declare variables of other types if those types are used in the definition of the main type that the file concerns itself with. - At the moment the policy is *not* to generalize over any other types to - minimize the amount of information that users have to keep in their head + At the moment the policy is *not* to generalise over any other types to + minimise the amount of information that users have to keep in their head concurrently. * Example 1: the main type in `Data.List.Properties` is `List A` where `A : Set a`. @@ -402,7 +412,7 @@ word within a compound word is capitalized except for the first word. * Rational variables are named `p`, `q`, `r`, ... (default `p`) -* All other variables tend to be named `x`, `y`, `z`. +* All other variables should be named `x`, `y`, `z`. * Collections of elements are usually indicated by appending an `s` (e.g. if you are naming your variables `x` and `y` then lists @@ -443,6 +453,44 @@ word within a compound word is capitalized except for the first word. relations should be used over the `¬` symbol (e.g. `m+n≮n` should be used instead of `¬m+n x <*> y <*> z) , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z) - ; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y) - , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y) } } where module R = RingWithoutOne R; module S = RingWithoutOne S @@ -389,7 +387,6 @@ ring R S = record ; *-assoc = Semiring.*-assoc Semi ; *-identity = Semiring.*-identity Semi ; distrib = Semiring.distrib Semi - ; zero = Semiring.zero Semi } } where diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda index dc96fedc76..f235f5d622 100644 --- a/src/Algebra/Definitions/RawMagma.agda +++ b/src/Algebra/Definitions/RawMagma.agda @@ -27,18 +27,31 @@ open RawMagma M renaming (Carrier to A) infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ --- Divisibility from the left - -_∣ˡ_ : Rel A (a ⊔ ℓ) -x ∣ˡ y = ∃ λ q → (x ∙ q) ≈ y +-- Divisibility from the left. +-- +-- This and, the definition of right divisibility below, are defined as +-- records rather than in terms of the base product type in order to +-- make the use of pattern synonyms more ergonomic (see #2216 for +-- further details). The record field names are not designed to be +-- used explicitly and indeed aren't re-exported publicly by +-- `Algebra.X.Properties.Divisibility` modules. + +record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where + constructor _,_ + field + quotient : A + equality : x ∙ quotient ≈ y _∤ˡ_ : Rel A (a ⊔ ℓ) x ∤ˡ y = ¬ x ∣ˡ y -- Divisibility from the right -_∣ʳ_ : Rel A (a ⊔ ℓ) -x ∣ʳ y = ∃ λ q → (q ∙ x) ≈ y +record _∣ʳ_ (x y : A) : Set (a ⊔ ℓ) where + constructor _,_ + field + quotient : A + equality : quotient ∙ x ≈ y _∤ʳ_ : Rel A (a ⊔ ℓ) x ∤ʳ y = ¬ x ∣ʳ y diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda index 450527ddc0..673434a48f 100644 --- a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda @@ -57,7 +57,7 @@ open DistribLatticeProperties distributiveLattice public x ∎ ∧-identityˡ : LeftIdentity ⊤ _∧_ -∧-identityˡ = comm+idʳ⇒idˡ ∧-comm ∧-identityʳ +∧-identityˡ = comm∧idʳ⇒idˡ ∧-comm ∧-identityʳ ∧-identity : Identity ⊤ _∧_ ∧-identity = ∧-identityˡ , ∧-identityʳ @@ -69,7 +69,7 @@ open DistribLatticeProperties distributiveLattice public x ∎ ∨-identityˡ : LeftIdentity ⊥ _∨_ -∨-identityˡ = comm+idʳ⇒idˡ ∨-comm ∨-identityʳ +∨-identityˡ = comm∧idʳ⇒idˡ ∨-comm ∨-identityʳ ∨-identity : Identity ⊥ _∨_ ∨-identity = ∨-identityˡ , ∨-identityʳ @@ -83,7 +83,7 @@ open DistribLatticeProperties distributiveLattice public ⊥ ∎ ∧-zeroˡ : LeftZero ⊥ _∧_ -∧-zeroˡ = comm+zeʳ⇒zeˡ ∧-comm ∧-zeroʳ +∧-zeroˡ = comm∧zeʳ⇒zeˡ ∧-comm ∧-zeroʳ ∧-zero : Zero ⊥ _∧_ ∧-zero = ∧-zeroˡ , ∧-zeroʳ @@ -97,7 +97,7 @@ open DistribLatticeProperties distributiveLattice public ⊤ ∎ ∨-zeroˡ : LeftZero ⊤ _∨_ -∨-zeroˡ = comm+zeʳ⇒zeˡ ∨-comm ∨-zeroʳ +∨-zeroˡ = comm∧zeʳ⇒zeˡ ∨-comm ∨-zeroʳ ∨-zero : Zero ⊤ _∨_ ∨-zero = ∨-zeroˡ , ∨-zeroʳ @@ -377,7 +377,7 @@ module XorRing (x ∧ (y ∨ z)) ∧ ¬ x ∎ ∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_ - ∧-distribʳ-⊕ = comm+distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕ + ∧-distribʳ-⊕ = comm∧distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕ ∧-distrib-⊕ : _∧_ DistributesOver _⊕_ ∧-distrib-⊕ = ∧-distribˡ-⊕ , ∧-distribʳ-⊕ @@ -516,7 +516,6 @@ module XorRing ; *-assoc = ∧-assoc ; *-identity = ∧-identity ; distrib = ∧-distrib-⊕ - ; zero = ∧-zero } ⊕-∧-isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤ diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda index 88a5cc5518..64ac6d7864 100644 --- a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda @@ -20,8 +20,8 @@ open import Data.Fin.Base using (Fin) open import Data.Nat.Base open import Data.Product.Base using (_,_; proj₁; proj₂) open import Data.Vec.Base as Vec using (Vec) -import Data.Vec.Effectful as VecCat -import Function.Identity.Effectful as IdCat +import Data.Vec.Effectful as Vec +import Function.Identity.Effectful as Identity open import Data.Vec.Properties using (lookup-map) open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW using (Pointwise; ext) @@ -165,18 +165,18 @@ lift n = record } } where - open RawApplicative VecCat.applicative + open RawApplicative Vec.applicative using (pure; zipWith) renaming (_<$>_ to map) ⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier - ⟦_⟧Id = Semantics.⟦_⟧ IdCat.applicative + ⟦_⟧Id = Semantics.⟦_⟧ Identity.applicative ⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m - ⟦_⟧Vec = Semantics.⟦_⟧ VecCat.applicative + ⟦_⟧Vec = Semantics.⟦_⟧ Vec.applicative open module R {n} (i : Fin n) = Reflection setoid var (λ e ρ → Vec.lookup (⟦ e ⟧Vec ρ) i) (λ e ρ → ⟦ e ⟧Id (Vec.map (flip Vec.lookup i) ρ)) (λ e ρ → sym $ reflexive $ - Naturality.natural (VecCat.lookup-morphism i) e ρ) + Naturality.natural (Vec.lookup-morphism i) e ρ) diff --git a/src/Algebra/Lattice/Structures.agda b/src/Algebra/Lattice/Structures.agda index fc40c0c300..116ed85271 100644 --- a/src/Algebra/Lattice/Structures.agda +++ b/src/Algebra/Lattice/Structures.agda @@ -37,20 +37,15 @@ record IsSemilattice (∙ : Op₂ A) : Set (a ⊔ ℓ) where comm : Commutative ∙ open IsBand isBand public - renaming - ( ∙-cong to ∧-cong - ; ∙-congˡ to ∧-congˡ - ; ∙-congʳ to ∧-congʳ - ) -- Used to bring names appropriate for a meet semilattice into scope. IsMeetSemilattice = IsSemilattice module IsMeetSemilattice {∧} (L : IsMeetSemilattice ∧) where open IsSemilattice L public renaming - ( ∧-cong to ∧-cong - ; ∧-congˡ to ∧-congˡ - ; ∧-congʳ to ∧-congʳ + ( ∙-cong to ∧-cong + ; ∙-congˡ to ∧-congˡ + ; ∙-congʳ to ∧-congʳ ) -- Used to bring names appropriate for a join semilattice into scope. @@ -58,9 +53,9 @@ IsJoinSemilattice = IsSemilattice module IsJoinSemilattice {∨} (L : IsJoinSemilattice ∨) where open IsSemilattice L public renaming - ( ∧-cong to ∨-cong - ; ∧-congˡ to ∨-congˡ - ; ∧-congʳ to ∨-congʳ + ( ∙-cong to ∨-cong + ; ∙-congˡ to ∨-congˡ + ; ∙-congʳ to ∨-congʳ ) ------------------------------------------------------------------------ diff --git a/src/Algebra/Lattice/Structures/Biased.agda b/src/Algebra/Lattice/Structures/Biased.agda index b5e1e6c9fd..5da9714354 100644 --- a/src/Algebra/Lattice/Structures/Biased.agda +++ b/src/Algebra/Lattice/Structures/Biased.agda @@ -82,9 +82,9 @@ record IsDistributiveLatticeʳʲᵐ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where setoid : Setoid a ℓ setoid = record { isEquivalence = isEquivalence } - ∨-distrib-∧ = comm+distrʳ⇒distr setoid ∧-cong ∨-comm ∨-distribʳ-∧ - ∧-distribˡ-∨ = distrib+absorbs⇒distribˡ setoid ∧-cong ∧-assoc ∨-comm ∧-absorbs-∨ ∨-absorbs-∧ ∨-distrib-∧ - ∧-distrib-∨ = comm+distrˡ⇒distr setoid ∨-cong ∧-comm ∧-distribˡ-∨ + ∨-distrib-∧ = comm∧distrʳ⇒distr setoid ∧-cong ∨-comm ∨-distribʳ-∧ + ∧-distribˡ-∨ = distrib∧absorbs⇒distribˡ setoid ∧-cong ∧-assoc ∨-comm ∧-absorbs-∨ ∨-absorbs-∧ ∨-distrib-∧ + ∧-distrib-∨ = comm∧distrˡ⇒distr setoid ∨-cong ∧-comm ∧-distribˡ-∨ isDistributiveLatticeʳʲᵐ : IsDistributiveLattice ∨ ∧ isDistributiveLatticeʳʲᵐ = record @@ -115,8 +115,8 @@ record IsBooleanAlgebraʳ isBooleanAlgebraʳ : IsBooleanAlgebra ∨ ∧ ¬ ⊤ ⊥ isBooleanAlgebraʳ = record { isDistributiveLattice = isDistributiveLattice - ; ∨-complement = comm+invʳ⇒inv setoid ∨-comm ∨-complementʳ - ; ∧-complement = comm+invʳ⇒inv setoid ∧-comm ∧-complementʳ + ; ∨-complement = comm∧invʳ⇒inv setoid ∨-comm ∨-complementʳ + ; ∧-complement = comm∧invʳ⇒inv setoid ∧-comm ∧-complementʳ ; ¬-cong = ¬-cong } diff --git a/src/Algebra/Morphism/RingMonomorphism.agda b/src/Algebra/Morphism/RingMonomorphism.agda index 9230c802a9..35a191a0f8 100644 --- a/src/Algebra/Morphism/RingMonomorphism.agda +++ b/src/Algebra/Morphism/RingMonomorphism.agda @@ -150,7 +150,6 @@ isRing isRing = record ; *-assoc = *-assoc R.*-isMagma R.*-assoc ; *-identity = *-identity R.*-isMagma R.*-identity ; distrib = distrib R.+-isGroup R.*-isMagma R.distrib - ; zero = zero R.+-isGroup R.*-isMagma R.zero } where module R = IsRing isRing isCommutativeRing : IsCommutativeRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ → diff --git a/src/Algebra/Operations/Semiring.agda b/src/Algebra/Operations/Semiring.agda index fbc6c254c2..08d55c884d 100644 --- a/src/Algebra/Operations/Semiring.agda +++ b/src/Algebra/Operations/Semiring.agda @@ -26,6 +26,6 @@ open Semiring S -- Re-exports open MonoidOperations +-commutativeMonoid public -open import Algebra.Properties.Semiring.Exponentiation S public -open import Algebra.Properties.Semiring.Multiplication S public - using (×1-homo-*; ×′1-homo-*) +open import Algebra.Properties.Semiring.Exp S public +open import Algebra.Properties.Semiring.Mult S public + using (×1-homo-*) diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda index 2e1f148701..0445f20505 100644 --- a/src/Algebra/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Properties/BooleanAlgebra.agda @@ -28,8 +28,7 @@ import Algebra.Properties.DistributiveLattice as DistribLatticeProperties open import Algebra.Structures _≈_ open import Relation.Binary -open import Function.Equality using (_⟨$⟩_) -open import Function.Equivalence using (_⇔_; module Equivalence) +open import Function.Bundles using (module Equivalence; _⇔_) open import Data.Product.Base using (_,_) ------------------------------------------------------------------------ @@ -47,9 +46,9 @@ replace-equality {_≈′_} ≈⇔≈′ = record { isBooleanAlgebra = record { isDistributiveLattice = DistributiveLattice.isDistributiveLattice (DistribLatticeProperties.replace-equality distributiveLattice ≈⇔≈′) - ; ∨-complement = ((λ x → to ⟨$⟩ ∨-complementˡ x) , λ x → to ⟨$⟩ ∨-complementʳ x) - ; ∧-complement = ((λ x → to ⟨$⟩ ∧-complementˡ x) , λ x → to ⟨$⟩ ∧-complementʳ x) - ; ¬-cong = λ i≈j → to ⟨$⟩ ¬-cong (from ⟨$⟩ i≈j) + ; ∨-complement = ((λ x → to (∨-complementˡ x)) , λ x → to (∨-complementʳ x)) + ; ∧-complement = ((λ x → to (∧-complementˡ x)) , λ x → to (∧-complementʳ x)) + ; ¬-cong = λ i≈j → to (¬-cong (from i≈j)) } } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y}) {-# WARNING_ON_USAGE replace-equality diff --git a/src/Algebra/Properties/DistributiveLattice.agda b/src/Algebra/Properties/DistributiveLattice.agda index adb6266e62..df03dfa38a 100644 --- a/src/Algebra/Properties/DistributiveLattice.agda +++ b/src/Algebra/Properties/DistributiveLattice.agda @@ -12,8 +12,7 @@ open import Algebra.Lattice.Bundles open import Algebra.Lattice.Structures.Biased open import Relation.Binary -open import Function.Equality -open import Function.Equivalence +open import Function.Bundles using (module Equivalence; _⇔_) import Algebra.Construct.Subst.Equality as SubstEq module Algebra.Properties.DistributiveLattice @@ -44,7 +43,7 @@ replace-equality {_≈′_} ≈⇔≈′ = record { isDistributiveLattice = isDistributiveLatticeʳʲᵐ (record { isLattice = Lattice.isLattice (LatticeProperties.replace-equality lattice ≈⇔≈′) - ; ∨-distribʳ-∧ = λ x y z → to ⟨$⟩ ∨-distribʳ-∧ x y z + ; ∨-distribʳ-∧ = λ x y z → to (∨-distribʳ-∧ x y z) }) } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y}) {-# WARNING_ON_USAGE replace-equality diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index d8ffc208f0..629406faa1 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -18,7 +18,7 @@ open Magma M -- Re-export divisibility relations publicly open import Algebra.Definitions.RawMagma rawMagma public - using (_∣_; _∤_; _∣∣_; _∤∤_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_) + using (_∣_; _∤_; _∣∣_; _∤∤_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_) ------------------------------------------------------------------------ -- Properties of divisibility diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index 22dabbac29..461a9a040b 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/src/Algebra/Properties/Ring.agda @@ -12,73 +12,21 @@ module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where open Ring R -import Algebra.Properties.AbelianGroup as AbelianGroupProperties +import Algebra.Properties.RingWithoutOne as RingWithoutOneProperties open import Function.Base using (_$_) open import Relation.Binary.Reasoning.Setoid setoid open import Algebra.Definitions _≈_ ------------------------------------------------------------------------ --- Export properties of abelian groups +-- Export properties of rings without a 1#. -open AbelianGroupProperties +-abelianGroup public - renaming - ( ε⁻¹≈ε to -0#≈0# - ; ∙-cancelˡ to +-cancelˡ - ; ∙-cancelʳ to +-cancelʳ - ; ∙-cancel to +-cancel - ; ⁻¹-involutive to -‿involutive - ; ⁻¹-injective to -‿injective - ; ⁻¹-anti-homo-∙ to -‿anti-homo-+ - ; identityˡ-unique to +-identityˡ-unique - ; identityʳ-unique to +-identityʳ-unique - ; identity-unique to +-identity-unique - ; inverseˡ-unique to +-inverseˡ-unique - ; inverseʳ-unique to +-inverseʳ-unique - ; ⁻¹-∙-comm to -‿+-comm - ) +open RingWithoutOneProperties ringWithoutOne public ------------------------------------------------------------------------ --- Properties of -_ - --‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y --‿distribˡ-* x y = sym $ begin - - x * y ≈⟨ sym $ +-identityʳ _ ⟩ - - x * y + 0# ≈⟨ +-congˡ $ sym (-‿inverseʳ _) ⟩ - - x * y + (x * y + - (x * y)) ≈⟨ sym $ +-assoc _ _ _ ⟩ - - x * y + x * y + - (x * y) ≈⟨ +-congʳ $ sym (distribʳ _ _ _) ⟩ - (- x + x) * y + - (x * y) ≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ _ ⟩ - 0# * y + - (x * y) ≈⟨ +-congʳ $ zeroˡ _ ⟩ - 0# + - (x * y) ≈⟨ +-identityˡ _ ⟩ - - (x * y) ∎ - --‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y --‿distribʳ-* x y = sym $ begin - x * - y ≈⟨ sym $ +-identityˡ _ ⟩ - 0# + x * - y ≈⟨ +-congʳ $ sym (-‿inverseˡ _) ⟩ - - (x * y) + x * y + x * - y ≈⟨ +-assoc _ _ _ ⟩ - - (x * y) + (x * y + x * - y) ≈⟨ +-congˡ $ sym (distribˡ _ _ _) ⟩ - - (x * y) + x * (y + - y) ≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ _ ⟩ - - (x * y) + x * 0# ≈⟨ +-congˡ $ zeroʳ _ ⟩ - - (x * y) + 0# ≈⟨ +-identityʳ _ ⟩ - - (x * y) ∎ +-- Extra properties of 1# -1*x≈-x : ∀ x → - 1# * x ≈ - x -1*x≈-x x = begin - - 1# * x ≈⟨ sym (-‿distribˡ-* 1# x ) ⟩ + - 1# * x ≈⟨ -‿distribˡ-* 1# x ⟨ - (1# * x) ≈⟨ -‿cong ( *-identityˡ x ) ⟩ - x ∎ - -x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0# -x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq - -x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z -x[y-z]≈xy-xz x y z = begin - x * (y - z) ≈⟨ distribˡ x y (- z) ⟩ - x * y + x * - z ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩ - x * y - x * z ∎ - -[y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) -[y-z]x≈yx-zx x y z = begin - (y - z) * x ≈⟨ distribʳ x y (- z) ⟩ - y * x + - z * x ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩ - y * x - z * x ∎ diff --git a/src/Algebra/Properties/RingWithoutOne.agda b/src/Algebra/Properties/RingWithoutOne.agda index cab4d405cb..d81ef58477 100644 --- a/src/Algebra/Properties/RingWithoutOne.agda +++ b/src/Algebra/Properties/RingWithoutOne.agda @@ -38,10 +38,10 @@ open AbelianGroupProperties +-abelianGroup public -‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y -‿distribˡ-* x y = sym $ begin - - x * y ≈⟨ sym $ +-identityʳ (- x * y) ⟩ - - x * y + 0# ≈⟨ +-congˡ $ sym ( -‿inverseʳ (x * y) ) ⟩ - - x * y + (x * y + - (x * y)) ≈⟨ sym $ +-assoc (- x * y) (x * y) (- (x * y)) ⟩ - - x * y + x * y + - (x * y) ≈⟨ +-congʳ $ sym ( distribʳ y (- x) x ) ⟩ + - x * y ≈⟨ +-identityʳ (- x * y) ⟨ + - x * y + 0# ≈⟨ +-congˡ $ -‿inverseʳ (x * y) ⟨ + - x * y + (x * y + - (x * y)) ≈⟨ +-assoc (- x * y) (x * y) (- (x * y)) ⟨ + - x * y + x * y + - (x * y) ≈⟨ +-congʳ $ distribʳ y (- x) x ⟨ (- x + x) * y + - (x * y) ≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ x ⟩ 0# * y + - (x * y) ≈⟨ +-congʳ $ zeroˡ y ⟩ 0# + - (x * y) ≈⟨ +-identityˡ (- (x * y)) ⟩ @@ -49,11 +49,26 @@ open AbelianGroupProperties +-abelianGroup public -‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y -‿distribʳ-* x y = sym $ begin - x * - y ≈⟨ sym $ +-identityˡ (x * (- y)) ⟩ - 0# + x * - y ≈⟨ +-congʳ $ sym ( -‿inverseˡ (x * y) ) ⟩ - - (x * y) + x * y + x * - y ≈⟨ +-assoc (- (x * y)) (x * y) (x * (- y)) ⟩ - - (x * y) + (x * y + x * - y) ≈⟨ +-congˡ $ sym ( distribˡ x y ( - y) ) ⟩ + x * - y ≈⟨ +-identityˡ (x * - y) ⟨ + 0# + x * - y ≈⟨ +-congʳ $ -‿inverseˡ (x * y) ⟨ + - (x * y) + x * y + x * - y ≈⟨ +-assoc (- (x * y)) (x * y) (x * - y) ⟩ + - (x * y) + (x * y + x * - y) ≈⟨ +-congˡ $ distribˡ x y (- y) ⟨ - (x * y) + x * (y + - y) ≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ y ⟩ - (x * y) + x * 0# ≈⟨ +-congˡ $ zeroʳ x ⟩ - (x * y) + 0# ≈⟨ +-identityʳ (- (x * y)) ⟩ - (x * y) ∎ + +x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0# +x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq + +x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z +x[y-z]≈xy-xz x y z = begin + x * (y - z) ≈⟨ distribˡ x y (- z) ⟩ + x * y + x * - z ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩ + x * y - x * z ∎ + +[y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) +[y-z]x≈yx-zx x y z = begin + (y - z) * x ≈⟨ distribʳ x y (- z) ⟩ + y * x + - z * x ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩ + y * x - z * x ∎ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index ed55226d67..44208367ea 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -264,11 +264,11 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w inverseʳ = proj₂ inverse uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹) - uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique + uniqueˡ-⁻¹ = Consequences.assoc∧id∧invʳ⇒invˡ-unique setoid ∙-cong assoc identity inverseʳ uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹) - uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique + uniqueʳ-⁻¹ = Consequences.assoc∧id∧invˡ⇒invʳ-unique setoid ∙-cong assoc identity inverseˡ isInvertibleMagma : IsInvertibleMagma _∙_ ε _⁻¹ @@ -651,7 +651,6 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ *-cong : Congruent₂ * *-assoc : Associative * distrib : * DistributesOver + - zero : Zero 0# * open IsAbelianGroup +-isAbelianGroup public renaming @@ -679,23 +678,28 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ ; isGroup to +-isGroup ) - *-isMagma : IsMagma * - *-isMagma = record - { isEquivalence = isEquivalence - ; ∙-cong = *-cong - } + distribˡ : * DistributesOverˡ + + distribˡ = proj₁ distrib + + distribʳ : * DistributesOverʳ + + distribʳ = proj₂ distrib zeroˡ : LeftZero 0# * - zeroˡ = proj₁ zero + zeroˡ = Consequences.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ setoid + +-cong *-cong +-assoc distribʳ +-identityʳ -‿inverseʳ zeroʳ : RightZero 0# * - zeroʳ = proj₂ zero + zeroʳ = Consequences.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ setoid + +-cong *-cong +-assoc distribˡ +-identityʳ -‿inverseʳ - distribˡ : * DistributesOverˡ + - distribˡ = proj₁ distrib + zero : Zero 0# * + zero = zeroˡ , zeroʳ - distribʳ : * DistributesOverʳ + - distribʳ = proj₂ distrib + *-isMagma : IsMagma * + *-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = *-cong + } *-isSemigroup : IsSemigroup * *-isSemigroup = record @@ -806,45 +810,17 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where *-assoc : Associative * *-identity : Identity 1# * distrib : * DistributesOver + - zero : Zero 0# * - open IsAbelianGroup +-isAbelianGroup public - renaming - ( assoc to +-assoc - ; ∙-cong to +-cong - ; ∙-congˡ to +-congˡ - ; ∙-congʳ to +-congʳ - ; identity to +-identity - ; identityˡ to +-identityˡ - ; identityʳ to +-identityʳ - ; inverse to -‿inverse - ; inverseˡ to -‿inverseˡ - ; inverseʳ to -‿inverseʳ - ; ⁻¹-cong to -‿cong - ; comm to +-comm - ; isMagma to +-isMagma - ; isSemigroup to +-isSemigroup - ; isMonoid to +-isMonoid - ; isUnitalMagma to +-isUnitalMagma - ; isCommutativeMagma to +-isCommutativeMagma - ; isCommutativeMonoid to +-isCommutativeMonoid - ; isCommutativeSemigroup to +-isCommutativeSemigroup - ; isInvertibleMagma to +-isInvertibleMagma - ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma - ; isGroup to +-isGroup - ) - - *-isMagma : IsMagma * - *-isMagma = record - { isEquivalence = isEquivalence - ; ∙-cong = *-cong + isRingWithoutOne : IsRingWithoutOne + * -_ 0# + isRingWithoutOne = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = *-cong + ; *-assoc = *-assoc + ; distrib = distrib } - *-isSemigroup : IsSemigroup * - *-isSemigroup = record - { isMagma = *-isMagma - ; assoc = *-assoc - } + open IsRingWithoutOne isRingWithoutOne public + hiding (+-isAbelianGroup; *-cong; *-assoc; distrib) *-isMonoid : IsMonoid * 1# *-isMonoid = record @@ -855,18 +831,10 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where open IsMonoid *-isMonoid public using () renaming - ( ∙-congˡ to *-congˡ - ; ∙-congʳ to *-congʳ - ; identityˡ to *-identityˡ + ( identityˡ to *-identityˡ ; identityʳ to *-identityʳ ) - zeroˡ : LeftZero 0# * - zeroˡ = proj₁ zero - - zeroʳ : RightZero 0# * - zeroʳ = proj₂ zero - isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# isSemiringWithoutAnnihilatingZero = record @@ -885,7 +853,7 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where } open IsSemiring isSemiring public - using (distribˡ; distribʳ; isNearSemiring; isSemiringWithoutOne) + using (isNearSemiring; isSemiringWithoutOne) record IsCommutativeRing diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index c0c6994e3f..8218a1ee1b 100644 --- a/src/Algebra/Structures/Biased.agda +++ b/src/Algebra/Structures/Biased.agda @@ -2,7 +2,7 @@ -- The Agda standard library -- -- Ways to give instances of certain structures where some fields can --- be given in terms of others +-- be given in terms of others. Re-exported via `Algebra`. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -36,7 +36,7 @@ record IsCommutativeMonoidˡ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where isCommutativeMonoid = record { isMonoid = record { isSemigroup = isSemigroup - ; identity = comm+idˡ⇒id setoid comm identityˡ + ; identity = comm∧idˡ⇒id setoid comm identityˡ } ; comm = comm } where open IsSemigroup isSemigroup @@ -55,7 +55,7 @@ record IsCommutativeMonoidʳ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where isCommutativeMonoid = record { isMonoid = record { isSemigroup = isSemigroup - ; identity = comm+idʳ⇒id setoid comm identityʳ + ; identity = comm∧idʳ⇒id setoid comm identityʳ } ; comm = comm } where open IsSemigroup isSemigroup @@ -146,9 +146,9 @@ record IsCommutativeSemiringˡ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) whe ; *-cong = *.∙-cong ; *-assoc = *.assoc ; *-identity = *.identity - ; distrib = comm+distrʳ⇒distr +.setoid +.∙-cong *.comm distribʳ + ; distrib = comm∧distrʳ⇒distr +.setoid +.∙-cong *.comm distribʳ } - ; zero = comm+zeˡ⇒ze +.setoid *.comm zeroˡ + ; zero = comm∧zeˡ⇒ze +.setoid *.comm zeroˡ } ; *-comm = *.comm } @@ -175,9 +175,9 @@ record IsCommutativeSemiringʳ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) whe ; *-cong = *.∙-cong ; *-assoc = *.assoc ; *-identity = *.identity - ; distrib = comm+distrˡ⇒distr +.setoid +.∙-cong *.comm distribˡ + ; distrib = comm∧distrˡ⇒distr +.setoid +.∙-cong *.comm distribˡ } - ; zero = comm+zeʳ⇒ze +.setoid *.comm zeroʳ + ; zero = comm∧zeʳ⇒ze +.setoid *.comm zeroʳ } ; *-comm = *.comm } @@ -192,6 +192,33 @@ open IsCommutativeSemiringʳ public ------------------------------------------------------------------------ -- IsRing +record IsRing* (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where + field + +-isAbelianGroup : IsAbelianGroup + 0# -_ + *-isMonoid : IsMonoid * 1# + distrib : * DistributesOver + + zero : Zero 0# * + + isRing : IsRing + * -_ 0# 1# + isRing = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = ∙-cong + ; *-assoc = assoc + ; *-identity = identity + ; distrib = distrib + } where open IsMonoid *-isMonoid + +open IsRing* public + using () renaming (isRing to isRing*) + + + +------------------------------------------------------------------------ +-- Deprecated +------------------------------------------------------------------------ + +-- Version 2.0 + -- We can recover a ring without proving that 0# annihilates *. record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where @@ -207,11 +234,11 @@ record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) open * using () renaming (∙-cong to *-cong) zeroˡ : LeftZero 0# * - zeroˡ = assoc+distribʳ+idʳ+invʳ⇒zeˡ setoid + zeroˡ = assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ setoid +-cong *-cong +.assoc (proj₂ distrib) +.identityʳ +.inverseʳ zeroʳ : RightZero 0# * - zeroʳ = assoc+distribˡ+idʳ+invʳ⇒zeʳ setoid + zeroʳ = assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ setoid +-cong *-cong +.assoc (proj₁ distrib) +.identityʳ +.inverseʳ zero : Zero 0# * @@ -224,28 +251,16 @@ record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) ; *-assoc = *.assoc ; *-identity = *.identity ; distrib = distrib - ; zero = zero } open IsRingWithoutAnnihilatingZero public using () renaming (isRing to isRingWithoutAnnihilatingZero) -record IsRing* (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where - field - +-isAbelianGroup : IsAbelianGroup + 0# -_ - *-isMonoid : IsMonoid * 1# - distrib : * DistributesOver + - zero : Zero 0# * - - isRing : IsRing + * -_ 0# 1# - isRing = record - { +-isAbelianGroup = +-isAbelianGroup - ; *-cong = ∙-cong - ; *-assoc = assoc - ; *-identity = identity - ; distrib = distrib - ; zero = zero - } where open IsMonoid *-isMonoid - -open IsRing* public - using () renaming (isRing to isRing*) +{-# WARNING_ON_USAGE IsRingWithoutAnnihilatingZero +"Warning: IsRingWithoutAnnihilatingZero was deprecated in v2.0. +Please use the standard `IsRing` instead." +#-} +{-# WARNING_ON_USAGE isRingWithoutAnnihilatingZero +"Warning: isRingWithoutAnnihilatingZero was deprecated in v2.0. +Please use the standard `IsRing` instead." +#-} diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda index 1270125254..55ed146e2c 100644 --- a/src/Data/Bool.agda +++ b/src/Data/Bool.agda @@ -8,9 +8,6 @@ module Data.Bool where -open import Relation.Nullary -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) - ------------------------------------------------------------------------ -- The boolean type and some operations diff --git a/src/Data/Bool/Base.agda b/src/Data/Bool/Base.agda index bc2e67644b..ea99ee880d 100644 --- a/src/Data/Bool/Base.agda +++ b/src/Data/Bool/Base.agda @@ -57,17 +57,19 @@ true xor b = not b false xor b = b ------------------------------------------------------------------------ --- Other operations - -infix 0 if_then_else_ - -if_then_else_ : Bool → A → A → A -if true then t else f = t -if false then t else f = f +-- Conversion to Set -- A function mapping true to an inhabited type and false to an empty -- type. - T : Bool → Set T true = ⊤ T false = ⊥ + +------------------------------------------------------------------------ +-- Other operations + +infix 0 if_then_else_ + +if_then_else_ : Bool → A → A → A +if true then t else f = t +if false then t else f = f diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index e911390366..bb8cda9a0e 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -28,8 +28,7 @@ open import Relation.Binary.Definitions using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_) open import Relation.Binary.PropositionalEquality.Core open import Relation.Binary.PropositionalEquality.Properties -open import Relation.Nullary.Reflects using (ofʸ; ofⁿ) -open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no) +open import Relation.Nullary.Decidable.Core using (True; yes; no; fromWitness) import Relation.Unary as U open import Algebra.Definitions {A = Bool} _≡_ @@ -726,15 +725,17 @@ xor-∧-commutativeRing = ⊕-∧-commutativeRing open XorRing _xor_ xor-is-ok ------------------------------------------------------------------------ --- Miscellaneous other properties +-- Properties of if_then_else_ -⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y -⇔→≡ {true } {true } hyp = refl -⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp refl) -⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp refl -⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp refl -⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp refl) -⇔→≡ {false} {false} hyp = refl +if-float : ∀ (f : A → B) b {x y} → + f (if b then x else y) ≡ (if b then f x else f y) +if-float _ true = refl +if-float _ false = refl + +------------------------------------------------------------------------ +-- Properties of T + +open Relation.Nullary.Decidable.Core public using (T?) T-≡ : ∀ {x} → T x ⇔ x ≡ true T-≡ {false} = mk⇔ (λ ()) (λ ()) @@ -757,18 +758,20 @@ T-∨ {false} {false} = mk⇔ inj₁ [ id , id ] T-irrelevant : U.Irrelevant T T-irrelevant {true} _ _ = refl -T? : U.Decidable T -does (T? b) = b -proof (T? true ) = ofʸ _ -proof (T? false) = ofⁿ λ() - T?-diag : ∀ b → T b → True (T? b) -T?-diag true _ = _ +T?-diag b = fromWitness + +------------------------------------------------------------------------ +-- Miscellaneous other properties + +⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y +⇔→≡ {true } {true } hyp = refl +⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp refl) +⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp refl +⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp refl +⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp refl) +⇔→≡ {false} {false} hyp = refl -if-float : ∀ (f : A → B) b {x y} → - f (if b then x else y) ≡ (if b then f x else f y) -if-float _ true = refl -if-float _ false = refl ------------------------------------------------------------------------ -- DEPRECATED NAMES diff --git a/src/Data/Fin/Substitution/Example.agda b/src/Data/Fin/Substitution/Example.agda index 02c98c539f..453c47d67f 100644 --- a/src/Data/Fin/Substitution/Example.agda +++ b/src/Data/Fin/Substitution/Example.agda @@ -20,7 +20,7 @@ open import Data.Fin.Substitution.Lemmas open import Data.Nat.Base hiding (_/_) open import Data.Fin.Base using (Fin) open import Data.Vec.Base -open import Relation.Binary.PropositionalEquality.Core as PropEq +open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; sym; cong; cong₂) open PropEq.≡-Reasoning open import Relation.Binary.Construct.Closure.ReflexiveTransitive diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 43152bceee..ca69682633 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -810,7 +810,7 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> +-identityˡ (+ _) = refl +-identityʳ : RightIdentity +0 _+_ -+-identityʳ = comm+idˡ⇒idʳ +-comm +-identityˡ ++-identityʳ = comm∧idˡ⇒idʳ +-comm +-identityˡ +-identity : Identity +0 _+_ +-identity = +-identityˡ , +-identityʳ @@ -904,7 +904,7 @@ distribʳ-⊖-+-neg m n o = begin +-inverseˡ +[1+ n ] = n⊖n≡0 (suc n) +-inverseʳ : RightInverse +0 -_ _+_ -+-inverseʳ = comm+invˡ⇒invʳ +-comm +-inverseˡ ++-inverseʳ = comm∧invˡ⇒invʳ +-comm +-inverseˡ +-inverse : Inverse +0 -_ _+_ +-inverse = +-inverseˡ , +-inverseʳ @@ -1319,7 +1319,7 @@ pred-mono (+≤+ m≤n) = ⊖-monoˡ-≤ 1 m≤n *-identityˡ +[1+ n ] rewrite ℕ.+-identityʳ n = refl *-identityʳ : RightIdentity 1ℤ _*_ -*-identityʳ = comm+idˡ⇒idʳ *-comm *-identityˡ +*-identityʳ = comm∧idˡ⇒idʳ *-comm *-identityˡ *-identity : Identity 1ℤ _*_ *-identity = *-identityˡ , *-identityʳ @@ -1328,7 +1328,7 @@ pred-mono (+≤+ m≤n) = ⊖-monoˡ-≤ 1 m≤n *-zeroˡ _ = refl *-zeroʳ : RightZero 0ℤ _*_ -*-zeroʳ = comm+zeˡ⇒zeʳ *-comm *-zeroˡ +*-zeroʳ = comm∧zeˡ⇒zeʳ *-comm *-zeroˡ *-zero : Zero 0ℤ _*_ *-zero = *-zeroˡ , *-zeroʳ @@ -1469,7 +1469,7 @@ private = refl *-distribˡ-+ : _*_ DistributesOverˡ _+_ -*-distribˡ-+ = comm+distrʳ⇒distrˡ *-comm *-distribʳ-+ +*-distribˡ-+ = comm∧distrʳ⇒distrˡ *-comm *-distribʳ-+ *-distrib-+ : _*_ DistributesOver _+_ *-distrib-+ = *-distribˡ-+ , *-distribʳ-+ @@ -1532,7 +1532,6 @@ private ; *-assoc = *-assoc ; *-identity = *-identity ; distrib = *-distrib-+ - ; zero = *-zero } +-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℤ 1ℤ diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 58b51e4893..16546110b6 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -23,11 +23,11 @@ open import Data.These.Base as These using (These; this; that; these) open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip) open import Level using (Level) -open import Relation.Nullary.Decidable.Core using (does; ¬?) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Core using (Rel) import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality.Core using (_≡_) +open import Relation.Nullary.Decidable.Core using (T?; does; ¬?) private variable @@ -346,141 +346,160 @@ removeAt : (xs : List A) → Fin (length xs) → List A removeAt (x ∷ xs) zero = xs removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i --- The following are functions which split a list up using boolean --- predicates. However, in practice they are difficult to use and --- prove properties about, and are mainly provided for advanced use --- cases where one wants to minimise dependencies. In most cases --- you probably want to use the versions defined below based on --- decidable predicates. e.g. use `takeWhile (_≤? 10) xs` --- instead of `takeWhileᵇ (_≤ᵇ 10) xs` +------------------------------------------------------------------------ +-- Operations for filtering lists + +-- The following are a variety of functions that can be used to +-- construct sublists using a predicate. +-- +-- Each function has two forms. The first main variant uses a +-- proof-relevant decidable predicate, while the second variant uses +-- a irrelevant boolean predicate and are suffixed with a `ᵇ` character, +-- typed as \^b. +-- +-- The decidable versions have several advantages: 1) easier to prove +-- properties, 2) better meta-variable inference and 3) most of the rest +-- of the library is set-up to work with decidable predicates. However, +-- in rare cases the boolean versions can be useful, mainly when one +-- wants to minimise dependencies. +-- +-- In summary, in most cases you probably want to use the decidable +-- versions over the boolean versions, e.g. use `takeWhile (_≤? 10) xs` +-- rather than `takeWhileᵇ (_≤ᵇ 10) xs`. + +takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A +takeWhile P? [] = [] +takeWhile P? (x ∷ xs) with does (P? x) +... | true = x ∷ takeWhile P? xs +... | false = [] takeWhileᵇ : (A → Bool) → List A → List A -takeWhileᵇ p [] = [] -takeWhileᵇ p (x ∷ xs) = if p x then x ∷ takeWhileᵇ p xs else [] +takeWhileᵇ p = takeWhile (T? ∘ p) + +dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A +dropWhile P? [] = [] +dropWhile P? (x ∷ xs) with does (P? x) +... | true = dropWhile P? xs +... | false = x ∷ xs dropWhileᵇ : (A → Bool) → List A → List A -dropWhileᵇ p [] = [] -dropWhileᵇ p (x ∷ xs) = if p x then dropWhileᵇ p xs else x ∷ xs +dropWhileᵇ p = dropWhile (T? ∘ p) + +filter : ∀ {P : Pred A p} → Decidable P → List A → List A +filter P? [] = [] +filter P? (x ∷ xs) with does (P? x) +... | false = filter P? xs +... | true = x ∷ filter P? xs filterᵇ : (A → Bool) → List A → List A -filterᵇ p [] = [] -filterᵇ p (x ∷ xs) = if p x then x ∷ filterᵇ p xs else filterᵇ p xs +filterᵇ p = filter (T? ∘ p) + +partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +partition P? [] = ([] , []) +partition P? (x ∷ xs) with does (P? x) | partition P? xs +... | true | (ys , zs) = (x ∷ ys , zs) +... | false | (ys , zs) = (ys , x ∷ zs) partitionᵇ : (A → Bool) → List A → List A × List A -partitionᵇ p [] = ([] , []) -partitionᵇ p (x ∷ xs) = (if p x then Prod.map₁ else Prod.map₂′) (x ∷_) (partitionᵇ p xs) +partitionᵇ p = partition (T? ∘ p) + +span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +span P? [] = ([] , []) +span P? ys@(x ∷ xs) with does (P? x) +... | true = Prod.map (x ∷_) id (span P? xs) +... | false = ([] , ys) + spanᵇ : (A → Bool) → List A → List A × List A -spanᵇ p [] = ([] , []) -spanᵇ p (x ∷ xs) = if p x - then Prod.map₁ (x ∷_) (spanᵇ p xs) - else ([] , x ∷ xs) +spanᵇ p = span (T? ∘ p) + +break : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) +break P? = span (¬? ∘ P?) breakᵇ : (A → Bool) → List A → List A × List A -breakᵇ p = spanᵇ (not ∘ p) +breakᵇ p = break (T? ∘ p) + +-- The predicate `P` represents the notion of newline character for the +-- type `A`. It is used to split the input list into a list of lines. +-- Some lines may be empty if the input contains at least two +-- consecutive newline characters. +linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) +linesBy {A = A} P? = go nothing where -linesByᵇ : (A → Bool) → List A → List (List A) -linesByᵇ {A = A} p = go nothing - where go : Maybe (List A) → List A → List (List A) go acc [] = maybe′ ([_] ∘′ reverse) [] acc - go acc (c ∷ cs) with p c + go acc (c ∷ cs) with does (P? c) ... | true = reverse (Maybe.fromMaybe [] acc) ∷ go nothing cs ... | false = go (just (c ∷ Maybe.fromMaybe [] acc)) cs -wordsByᵇ : (A → Bool) → List A → List (List A) -wordsByᵇ {A = A} p = go [] - where +linesByᵇ : (A → Bool) → List A → List (List A) +linesByᵇ p = linesBy (T? ∘ p) + +-- The predicate `P` represents the notion of space character for the +-- type `A`. It is used to split the input list into a list of words. +-- All the words are non empty and the output does not contain any space +-- characters. +wordsBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) +wordsBy {A = A} P? = go [] where + cons : List A → List (List A) → List (List A) cons [] ass = ass cons as ass = reverse as ∷ ass go : List A → List A → List (List A) go acc [] = cons acc [] - go acc (c ∷ cs) with p c + go acc (c ∷ cs) with does (P? c) ... | true = cons acc (go [] cs) ... | false = go (c ∷ acc) cs +wordsByᵇ : (A → Bool) → List A → List (List A) +wordsByᵇ p = wordsBy (T? ∘ p) + +derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A +derun R? [] = [] +derun R? (x ∷ []) = x ∷ [] +derun R? (x ∷ xs@(y ∷ _)) with does (R? x y) | derun R? xs +... | true | ys = ys +... | false | ys = x ∷ ys + derunᵇ : (A → A → Bool) → List A → List A -derunᵇ r [] = [] -derunᵇ r (x ∷ []) = x ∷ [] -derunᵇ r (x ∷ y ∷ xs) = if r x y - then derunᵇ r (y ∷ xs) - else x ∷ derunᵇ r (y ∷ xs) +derunᵇ r = derun (T? ∘₂ r) + +deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A +deduplicate R? [] = [] +deduplicate R? (x ∷ xs) = x ∷ filter (¬? ∘ R? x) (deduplicate R? xs) deduplicateᵇ : (A → A → Bool) → List A → List A -deduplicateᵇ r [] = [] -deduplicateᵇ r (x ∷ xs) = x ∷ filterᵇ (not ∘ r x) (deduplicateᵇ r xs) +deduplicateᵇ r = deduplicate (T? ∘₂ r) -- Finds the first element satisfying the boolean predicate +find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A +find P? [] = nothing +find P? (x ∷ xs) = if does (P? x) then just x else find P? xs + findᵇ : (A → Bool) → List A → Maybe A -findᵇ p [] = nothing -findᵇ p (x ∷ xs) = if p x then just x else findᵇ p xs +findᵇ p = find (T? ∘ p) -- Finds the index of the first element satisfying the boolean predicate -findIndexᵇ : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs) -findIndexᵇ p [] = nothing -findIndexᵇ p (x ∷ xs) = if p x +findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs) +findIndex P? [] = nothing +findIndex P? (x ∷ xs) = if does (P? x) then just zero - else Maybe.map suc (findIndexᵇ p xs) + else Maybe.map suc (findIndex P? xs) + +findIndexᵇ : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs) +findIndexᵇ p = findIndex (T? ∘ p) -- Finds indices of all the elements satisfying the boolean predicate -findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs) -findIndicesᵇ p [] = [] -findIndicesᵇ p (x ∷ xs) = if p x +findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs) +findIndices P? [] = [] +findIndices P? (x ∷ xs) = if does (P? x) then zero ∷ indices else indices - where indices = map suc (findIndicesᵇ p xs) - --- Equivalent functions that use a decidable predicate instead of a --- boolean function. - -takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A -takeWhile P? = takeWhileᵇ (does ∘ P?) - -dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A -dropWhile P? = dropWhileᵇ (does ∘ P?) + where indices = map suc (findIndices P? xs) -filter : ∀ {P : Pred A p} → Decidable P → List A → List A -filter P? = filterᵇ (does ∘ P?) - -partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) -partition P? = partitionᵇ (does ∘ P?) - -span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) -span P? = spanᵇ (does ∘ P?) - -break : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A) -break P? = breakᵇ (does ∘ P?) - --- The predicate `P` represents the notion of newline character for the --- type `A`. It is used to split the input list into a list of lines. --- Some lines may be empty if the input contains at least two --- consecutive newline characters. -linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) -linesBy P? = linesByᵇ (does ∘ P?) - --- The predicate `P` represents the notion of space character for the --- type `A`. It is used to split the input list into a list of words. --- All the words are non empty and the output does not contain any space --- characters. -wordsBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A) -wordsBy P? = wordsByᵇ (does ∘ P?) - -derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A -derun R? = derunᵇ (does ∘₂ R?) - -deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A -deduplicate R? = deduplicateᵇ (does ∘₂ R?) - -find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A -find P? = findᵇ (does ∘ P?) - -findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs) -findIndex P? = findIndexᵇ (does ∘ P?) - -findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs) -findIndices P? = findIndicesᵇ (does ∘ P?) +findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs) +findIndicesᵇ p = findIndices (T? ∘ p) ------------------------------------------------------------------------ -- Actions on single elements diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index 31ab6941ac..17af3d8955 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -44,7 +44,7 @@ import Relation.Binary.Reasoning.Preorder as PreorderReasoning open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; _≗_; refl) open import Relation.Binary.Reasoning.Syntax -open import Relation.Nullary +open import Relation.Nullary.Negation using (¬_) open import Data.List.Membership.Propositional.Properties private diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda index 9e97527ff8..73d42b7b8a 100644 --- a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda @@ -12,7 +12,6 @@ open import Data.List.Relation.Unary.All.Properties using (all-filter) open import Data.List.Relation.Unary.Unique.Setoid.Properties open import Level open import Relation.Binary.Bundles using (DecSetoid) -open import Relation.Nullary.Decidable using (¬?) module Data.List.Relation.Unary.Unique.DecSetoid.Properties where @@ -30,5 +29,4 @@ module _ (DS : DecSetoid a ℓ) where deduplicate-! : ∀ xs → Unique (deduplicate _≟_ xs) deduplicate-! [] = [] - deduplicate-! (x ∷ xs) = all-filter (λ y → ¬? (x ≟ y)) (deduplicate _≟_ xs) - ∷ filter⁺ S (λ y → ¬? (x ≟ y)) (deduplicate-! xs) + deduplicate-! (x ∷ xs) = all-filter _ (deduplicate _≟_ xs) ∷ filter⁺ S _ (deduplicate-! xs) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index f2755c55fc..478b71f783 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -12,15 +12,15 @@ module Data.Nat.Base where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring) -open import Algebra.Definitions.RawMagma using (_∣ˡ_) +open import Algebra.Definitions.RawMagma using (_∣ˡ_; _,_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) -open import Data.Product.Base using (_,_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl) open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Unary using (Pred) ------------------------------------------------------------------------ -- Types @@ -28,6 +28,9 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Agda.Builtin.Nat public using (zero; suc) renaming (Nat to ℕ) +--smart constructor +pattern 2+ n = suc (suc n) + ------------------------------------------------------------------------ -- Boolean equality relation @@ -59,8 +62,9 @@ m < n = suc m ≤ n -- Smart constructors of _<_ -pattern z b ------------------------------------------------------------------------ -- Simple predicates --- Defining `NonZero` in terms of `T` and therefore ultimately `⊤` and --- `⊥` allows Agda to automatically infer nonZero-ness for any natural --- of the form `suc n`. Consequently in many circumstances this --- eliminates the need to explicitly pass a proof when the NonZero --- argument is either an implicit or an instance argument. +-- Defining these predicates in terms of `T` and therefore ultimately +-- `⊤` and `⊥` allows Agda to automatically infer them for any natural +-- of the correct form. Consequently in many circumstances this +-- eliminates the need to explicitly pass a proof when the predicate +-- argument is either an implicit or an instance argument. See `_/_` +-- and `_%_` further down this file for examples. -- --- See `Data.Nat.DivMod` for an example. +-- Furthermore, defining these predicates as single-field records +-- (rather defining them directly as the type of their field) is +-- necessary as the current version of Agda is far better at +-- reconstructing meta-variable values for the record parameters. + +-- A predicate saying that a number is not equal to 0. record NonZero (n : ℕ) : Set where field @@ -130,6 +140,34 @@ instance >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0 >-nonZero⁻¹ (suc n) = z1⇒nonTrivial : ∀ {n} → n > 1 → NonTrivial n +n>1⇒nonTrivial sz1 : ∀ n → .{{NonTrivial n}} → n > 1 +nonTrivial⇒n>1 (2+ _) = sz 1 is m-rough, then m ≤ n +rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n +rough⇒≤ rough = ≮⇒≥ n≮m + where n≮m = λ m>n → rough (hasNonTrivialDivisor m>n ∣-refl) + +-- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough +∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n +∤⇒rough-suc m∤n r (hasNonTrivialDivisor d<1+m d∣n) + with m<1+n⇒m1⇒m*n>1 q d + _ = m*n≢0⇒m≢0 q + +-- Basic (counter-)examples of Composite + +¬composite[0] : ¬ Composite 0 +¬composite[0] = 0-rough + +¬composite[1] : ¬ Composite 1 +¬composite[1] = 1-rough + +composite[4] : Composite 4 +composite[4] = composite-≢ 2 (λ()) (divides-refl 2) + +composite[6] : Composite 6 +composite[6] = composite-≢ 3 (λ()) (divides-refl 2) + +composite⇒nonZero : Composite n → NonZero n +composite⇒nonZero {suc _} _ = _ + +composite⇒nonTrivial : Composite n → NonTrivial n +composite⇒nonTrivial {1} composite[1] = + contradiction composite[1] ¬composite[1] +composite⇒nonTrivial {2+ _} _ = _ + +composite? : Decidable Composite +composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n) + where + -- For technical reasons, in order to be able to prove decidability + -- via the `all?` and `any?` combinators for *bounded* predicates on + -- `ℕ`, we further define the bounded counterparts to predicates + -- `P...` as `P...UpTo` and show the equivalence of the two. + + -- Equivalent bounded predicate definition + CompositeUpTo : Pred ℕ _ + CompositeUpTo n = ∃[ d ] d < n × NonTrivial d × d ∣ n + + -- Proof of equivalence + comp-upto⇒comp : CompositeUpTo n → Composite n + comp-upto⇒comp (_ , d 1 divides n, then p must be prime +rough∧∣⇒prime : .{{NonTrivial p}} → p Rough n → p ∣ n → Prime p +rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) + +-- Relationship between compositeness and primality. +composite⇒¬prime : Composite n → ¬ Prime n +composite⇒¬prime composite[d] (prime p) = p composite[d] + +¬composite⇒prime : .{{NonTrivial n}} → ¬ Composite n → Prime n +¬composite⇒prime = prime + +prime⇒¬composite : Prime n → ¬ Composite n +prime⇒¬composite (prime p) = p + +-- Note that this has to recompute the factor! +¬prime⇒composite : .{{NonTrivial n}} → ¬ Prime n → Composite n +¬prime⇒composite {n} ¬prime[n] = + decidable-stable (composite? n) (¬prime[n] ∘′ ¬composite⇒prime) + +------------------------------------------------------------------------ +-- Basic (counter-)examples of Irreducible + +¬irreducible[0] : ¬ Irreducible 0 +¬irreducible[0] irr[0] = contradiction₂ 2≡1⊎2≡0 (λ ()) (λ ()) + where 2≡1⊎2≡0 = irr[0] {2} (divides-refl 0) + +irreducible[1] : Irreducible 1 +irreducible[1] m|1 = inj₁ (∣1⇒≡1 m|1) + +irreducible[2] : Irreducible 2 +irreducible[2] {zero} 0∣2 with () ← 0∣⇒≡0 0∣2 +irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2 +... | z1⇒m*n>1 : ∀ m n .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n) +m≢0∧n>1⇒m*n>1 (suc m) (2+ n) = _ + +n≢0∧m>1⇒m*n>1 : ∀ m n .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n) +n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m + ------------------------------------------------------------------------ -- Other properties of _*_ and _≤_/_<_ @@ -1308,7 +1329,7 @@ m⊔n-nonZero : ∀ {p} → p > 0ℚ → NonZero p >-nonZero {p@(mkℚ _ _ _)} (*<* p-nonZero {toℚᵘ p} (ℚᵘ.*<* p_ diff --git a/src/Function.agda b/src/Function.agda index 1d45b05901..b4155ef8ef 100644 --- a/src/Function.agda +++ b/src/Function.agda @@ -13,4 +13,5 @@ open import Function.Base public open import Function.Strict public open import Function.Definitions public open import Function.Structures public +open import Function.Structures.Biased public open import Function.Bundles public diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 9e18c30fe5..98aac7a48c 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -380,7 +380,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where -- For further background on (split) surjections, one may consult any -- general mathematical references which work without the principle -- of choice. For example: - -- + -- -- https://ncatlab.org/nlab/show/split+epimorphism. -- -- The connection to set-theoretic notions with the same names is diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 60606cc673..2fda92224e 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -28,9 +28,9 @@ private ------------------------------------------------------------------------ -- Injective -contraInjective : Injective ≈₁ ≈₂ f → +contraInjective : ∀ (≈₂ : Rel B ℓ₂) → Injective ≈₁ ≈₂ f → ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y)) -contraInjective inj p = contraposition inj p +contraInjective _ inj p = contraposition inj p ------------------------------------------------------------------------ -- Inverseˡ diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda index d6067a7702..a2558a9c48 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/src/Function/Consequences/Propositional.agda @@ -7,85 +7,47 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Function.Consequences.Propositional where +module Function.Consequences.Propositional + {a b} {A : Set a} {B : Set b} + where +open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (setoid) open import Function.Definitions -open import Level open import Relation.Nullary.Negation.Core using (contraposition) -open import Relation.Binary.PropositionalEquality.Core - using (_≡_; _≢_; refl; sym; trans; cong) -import Function.Consequences as C - -private - variable - a b ℓ₁ ℓ₂ : Level - A B : Set a - f f⁻¹ : A → B - ------------------------------------------------------------------------- --- Injective - -contraInjective : Injective _≡_ _≡_ f → - ∀ {x y} → x ≢ y → f x ≢ f y -contraInjective inj p = contraposition inj p - ------------------------------------------------------------------------- --- Inverseˡ - -inverseˡ⇒surjective : Inverseˡ _≡_ _≡_ f f⁻¹ → Surjective _≡_ _≡_ f -inverseˡ⇒surjective = C.inverseˡ⇒surjective _≡_ - ------------------------------------------------------------------------- --- Inverseʳ - -inverseʳ⇒injective : ∀ f → - Inverseʳ _≡_ _≡_ f f⁻¹ → - Injective _≡_ _≡_ f -inverseʳ⇒injective f = C.inverseʳ⇒injective _≡_ f refl sym trans +import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid ------------------------------------------------------------------------ --- Inverseᵇ +-- Re-export setoid properties -inverseᵇ⇒bijective : Inverseᵇ _≡_ _≡_ f f⁻¹ → Bijective _≡_ _≡_ f -inverseᵇ⇒bijective = C.inverseᵇ⇒bijective _≡_ refl sym trans +open Setoid public + hiding + ( strictlySurjective⇒surjective + ; strictlyInverseˡ⇒inverseˡ + ; strictlyInverseʳ⇒inverseʳ + ) ------------------------------------------------------------------------ --- StrictlySurjective +-- Properties that rely on congruence -surjective⇒strictlySurjective : Surjective _≡_ _≡_ f → - StrictlySurjective _≡_ f -surjective⇒strictlySurjective = - C.surjective⇒strictlySurjective _≡_ refl +private + variable + f : A → B + f⁻¹ : B → A strictlySurjective⇒surjective : StrictlySurjective _≡_ f → Surjective _≡_ _≡_ f strictlySurjective⇒surjective = - C.strictlySurjective⇒surjective trans (cong _) - ------------------------------------------------------------------------- --- StrictlyInverseˡ - -inverseˡ⇒strictlyInverseˡ : Inverseˡ _≡_ _≡_ f f⁻¹ → - StrictlyInverseˡ _≡_ f f⁻¹ -inverseˡ⇒strictlyInverseˡ = - C.inverseˡ⇒strictlyInverseˡ _≡_ _≡_ refl + Setoid.strictlySurjective⇒surjective (cong _) -strictlyInverseˡ⇒inverseˡ : ∀ f → - StrictlyInverseˡ _≡_ f f⁻¹ → +strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → Inverseˡ _≡_ _≡_ f f⁻¹ strictlyInverseˡ⇒inverseˡ f = - C.strictlyInverseˡ⇒inverseˡ trans (cong f) - ------------------------------------------------------------------------- --- StrictlyInverseʳ - -inverseʳ⇒strictlyInverseʳ : Inverseʳ _≡_ _≡_ f f⁻¹ → - StrictlyInverseʳ _≡_ f f⁻¹ -inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ _≡_ _≡_ refl + Setoid.strictlyInverseˡ⇒inverseˡ (cong _) -strictlyInverseʳ⇒inverseʳ : ∀ f → - StrictlyInverseʳ _≡_ f f⁻¹ → +strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → Inverseʳ _≡_ _≡_ f f⁻¹ -strictlyInverseʳ⇒inverseʳ {f⁻¹ = f⁻¹} _ = - C.strictlyInverseʳ⇒inverseʳ trans (cong f⁻¹) +strictlyInverseʳ⇒inverseʳ f = + Setoid.strictlyInverseʳ⇒inverseʳ (cong _) diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda new file mode 100644 index 0000000000..d2c3b948d9 --- /dev/null +++ b/src/Function/Consequences/Setoid.agda @@ -0,0 +1,92 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Relationships between properties of functions where the equality +-- over both the domain and codomain are assumed to be setoids. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Function.Consequences.Setoid + {a b ℓ₁ ℓ₂} + (S : Setoid a ℓ₁) + (T : Setoid b ℓ₂) + where + +open import Function.Definitions +open import Relation.Nullary.Negation.Core + +import Function.Consequences as C + +private + open module S = Setoid S using () renaming (Carrier to A; _≈_ to ≈₁) + open module T = Setoid T using () renaming (Carrier to B; _≈_ to ≈₂) + + variable + f : A → B + f⁻¹ : B → A + +------------------------------------------------------------------------ +-- Injective + +contraInjective : Injective ≈₁ ≈₂ f → + ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y)) +contraInjective = C.contraInjective ≈₂ + +------------------------------------------------------------------------ +-- Inverseˡ + +inverseˡ⇒surjective : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f +inverseˡ⇒surjective = C.inverseˡ⇒surjective ≈₂ + +------------------------------------------------------------------------ +-- Inverseʳ + +inverseʳ⇒injective : ∀ f → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f +inverseʳ⇒injective f = C.inverseʳ⇒injective ≈₂ f T.refl S.sym S.trans + +------------------------------------------------------------------------ +-- Inverseᵇ + +inverseᵇ⇒bijective : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ f +inverseᵇ⇒bijective = C.inverseᵇ⇒bijective ≈₂ T.refl S.sym S.trans + +------------------------------------------------------------------------ +-- StrictlySurjective + +surjective⇒strictlySurjective : Surjective ≈₁ ≈₂ f → + StrictlySurjective ≈₂ f +surjective⇒strictlySurjective = + C.surjective⇒strictlySurjective ≈₂ S.refl + +strictlySurjective⇒surjective : Congruent ≈₁ ≈₂ f → + StrictlySurjective ≈₂ f → + Surjective ≈₁ ≈₂ f +strictlySurjective⇒surjective = + C.strictlySurjective⇒surjective T.trans + +------------------------------------------------------------------------ +-- StrictlyInverseˡ + +inverseˡ⇒strictlyInverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → + StrictlyInverseˡ ≈₂ f f⁻¹ +inverseˡ⇒strictlyInverseˡ = C.inverseˡ⇒strictlyInverseˡ ≈₁ ≈₂ S.refl + +strictlyInverseˡ⇒inverseˡ : Congruent ≈₁ ≈₂ f → + StrictlyInverseˡ ≈₂ f f⁻¹ → + Inverseˡ ≈₁ ≈₂ f f⁻¹ +strictlyInverseˡ⇒inverseˡ = C.strictlyInverseˡ⇒inverseˡ T.trans + +------------------------------------------------------------------------ +-- StrictlyInverseʳ + +inverseʳ⇒strictlyInverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → + StrictlyInverseʳ ≈₁ f f⁻¹ +inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ ≈₁ ≈₂ T.refl + +strictlyInverseʳ⇒inverseʳ : Congruent ≈₂ ≈₁ f⁻¹ → + StrictlyInverseʳ ≈₁ f f⁻¹ → + Inverseʳ ≈₁ ≈₂ f f⁻¹ +strictlyInverseʳ⇒inverseʳ = C.strictlyInverseʳ⇒inverseʳ S.trans diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index 834ee0d4fa..5506f93dd4 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -108,7 +108,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : isLeftInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsLeftInverse ≈₂ ≈₁ f⁻¹ f isLeftInverse inv = record { isCongruent = isCongruent F.isCongruent F.from-cong - ; from-cong = F.cong₁ + ; from-cong = F.to-cong ; inverseˡ = inverseˡ ≈₁ ≈₂ F.inverseʳ } where module F = IsRightInverse inv diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda index 87ce778fec..5ade85d843 100644 --- a/src/Function/Properties/Inverse.agda +++ b/src/Function/Properties/Inverse.agda @@ -19,7 +19,7 @@ open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P import Relation.Binary.Reasoning.Setoid as SetoidReasoning -open import Function.Consequences +import Function.Consequences.Setoid as Consequences import Function.Construct.Identity as Identity import Function.Construct.Symmetry as Symmetry @@ -77,25 +77,25 @@ fromFunction I = record { to = from ; cong = from-cong } where open Inverse I Inverse⇒Injection : Inverse S T → Injection S T -Inverse⇒Injection I = record +Inverse⇒Injection {S = S} {T = T} I = record { to = to ; cong = to-cong - ; injective = inverseʳ⇒injective Eq₂._≈_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ - } where open Inverse I + ; injective = inverseʳ⇒injective to inverseʳ + } where open Inverse I; open Consequences S T Inverse⇒Surjection : Inverse S T → Surjection S T Inverse⇒Surjection {S = S} {T = T} I = record { to = to ; cong = to-cong - ; surjective = inverseˡ⇒surjective (_≈_ T) inverseˡ - } where open Inverse I; open Setoid + ; surjective = inverseˡ⇒surjective inverseˡ + } where open Inverse I; open Consequences S T Inverse⇒Bijection : Inverse S T → Bijection S T -Inverse⇒Bijection I = record +Inverse⇒Bijection {S = S} {T = T} I = record { to = to ; cong = to-cong - ; bijective = inverseᵇ⇒bijective Eq₂._≈_ Eq₂.refl Eq₁.sym Eq₁.trans inverse - } where open Inverse I + ; bijective = inverseᵇ⇒bijective inverse + } where open Inverse I; open Consequences S T Inverse⇒Equivalence : Inverse S T → Equivalence S T Inverse⇒Equivalence I = record diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index baf33dddf0..9533cfb179 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -20,7 +20,6 @@ module Function.Structures {a b ℓ₁ ℓ₂} open import Data.Product.Base as Product using (∃; _×_; _,_) open import Function.Base open import Function.Definitions -open import Function.Consequences open import Level using (_⊔_) ------------------------------------------------------------------------ @@ -121,7 +120,7 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from open IsCongruent isCongruent public - renaming (cong to cong₁) + renaming (cong to to-cong) strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from strictlyInverseʳ x = inverseʳ Eq₂.refl diff --git a/src/Function/Structures/Biased.agda b/src/Function/Structures/Biased.agda new file mode 100644 index 0000000000..e25c4970c9 --- /dev/null +++ b/src/Function/Structures/Biased.agda @@ -0,0 +1,127 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Ways to give instances of certain structures where some fields can +-- be given in terms of others. +-- The contents of this file should usually be accessed from `Function`. +------------------------------------------------------------------------ + + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) + +module Function.Structures.Biased {a b ℓ₁ ℓ₂} + {A : Set a} (_≈₁_ : Rel A ℓ₁) -- Equality over the domain + {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain + where + +open import Data.Product.Base as Product using (∃; _×_; _,_) +open import Function.Base +open import Function.Definitions +open import Function.Structures _≈₁_ _≈₂_ +open import Function.Consequences.Setoid +open import Level using (_⊔_) + +------------------------------------------------------------------------ +-- Surjection +------------------------------------------------------------------------ + +record IsStrictSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isCongruent : IsCongruent f + strictlySurjective : StrictlySurjective _≈₂_ f + + open IsCongruent isCongruent public + + isSurjection : IsSurjection f + isSurjection = record + { isCongruent = isCongruent + ; surjective = strictlySurjective⇒surjective + Eq₁.setoid Eq₂.setoid cong strictlySurjective + } + +open IsStrictSurjection public + using () renaming (isSurjection to isStrictSurjection) + +------------------------------------------------------------------------ +-- Bijection +------------------------------------------------------------------------ + +record IsStrictBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isInjection : IsInjection f + strictlySurjective : StrictlySurjective _≈₂_ f + + isBijection : IsBijection f + isBijection = record + { isInjection = isInjection + ; surjective = strictlySurjective⇒surjective + Eq₁.setoid Eq₂.setoid cong strictlySurjective + } where open IsInjection isInjection + +open IsStrictBijection public + using () renaming (isBijection to isStrictBijection) + +------------------------------------------------------------------------ +-- Left inverse +------------------------------------------------------------------------ + +record IsStrictLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isCongruent : IsCongruent to + from-cong : Congruent _≈₂_ _≈₁_ from + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from + + isLeftInverse : IsLeftInverse to from + isLeftInverse = record + { isCongruent = isCongruent + ; from-cong = from-cong + ; inverseˡ = strictlyInverseˡ⇒inverseˡ + Eq₁.setoid Eq₂.setoid cong strictlyInverseˡ + } where open IsCongruent isCongruent + +open IsStrictLeftInverse public + using () renaming (isLeftInverse to isStrictLeftInverse) + +------------------------------------------------------------------------ +-- Right inverse +------------------------------------------------------------------------ + +record IsStrictRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isCongruent : IsCongruent to + from-cong : Congruent _≈₂_ _≈₁_ from + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from + + isRightInverse : IsRightInverse to from + isRightInverse = record + { isCongruent = isCongruent + ; from-cong = from-cong + ; inverseʳ = strictlyInverseʳ⇒inverseʳ + Eq₁.setoid Eq₂.setoid from-cong strictlyInverseʳ + } where open IsCongruent isCongruent + +open IsStrictRightInverse public + using () renaming (isRightInverse to isStrictRightInverse) + +------------------------------------------------------------------------ +-- Inverse +------------------------------------------------------------------------ + +record IsStrictInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isLeftInverse : IsLeftInverse to from + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from + + isInverse : IsInverse to from + isInverse = record + { isLeftInverse = isLeftInverse + ; inverseʳ = strictlyInverseʳ⇒inverseʳ + Eq₁.setoid Eq₂.setoid from-cong strictlyInverseʳ + } where open IsLeftInverse isLeftInverse + +open IsStrictInverse public + using () renaming (isInverse to isStrictInverse) diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda index 71ab8535d8..43778816c3 100644 --- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda +++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda @@ -130,11 +130,11 @@ _>>=_ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} {j k} → m >>= f = (f ⋆) m -- Note that the monad-like structure above is not an indexed monad --- (as defined in Category.Monad.Indexed). If it were, then _>>=_ +-- (as defined in Effect.Monad.Indexed). If it were, then _>>=_ -- would have a type similar to -- -- ∀ {I} {T U : Rel I t} {i j k} → -- Star T i j → (T i j → Star U j k) → Star U i k. -- ^^^^^ -- Note, however, that there is no scope for applying T to any indices --- in the definition used in Category.Monad.Indexed. +-- in the definition used in Effect.Monad.Indexed. diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda index 22a5031d27..c4846142ec 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda @@ -99,21 +99,21 @@ module _ (semi : IsSemilattice _∙_) where x∙y≤x : ∀ x y → (x ∙ y) ≤ x x∙y≤x x y = begin - x ∙ y ≈⟨ ∧-cong (sym (idem x)) S.refl ⟩ + x ∙ y ≈⟨ ∙-cong (sym (idem x)) S.refl ⟩ (x ∙ x) ∙ y ≈⟨ assoc x x y ⟩ x ∙ (x ∙ y) ≈⟨ comm x (x ∙ y) ⟩ (x ∙ y) ∙ x ∎ x∙y≤y : ∀ x y → (x ∙ y) ≤ y x∙y≤y x y = begin - x ∙ y ≈⟨ ∧-cong S.refl (sym (idem y)) ⟩ + x ∙ y ≈⟨ ∙-cong S.refl (sym (idem y)) ⟩ x ∙ (y ∙ y) ≈⟨ sym (assoc x y y) ⟩ (x ∙ y) ∙ y ∎ ∙-presʳ-≤ : ∀ {x y} z → z ≤ x → z ≤ y → z ≤ (x ∙ y) ∙-presʳ-≤ {x} {y} z z≤x z≤y = begin z ≈⟨ z≤y ⟩ - z ∙ y ≈⟨ ∧-cong z≤x S.refl ⟩ + z ∙ y ≈⟨ ∙-cong z≤x S.refl ⟩ (z ∙ x) ∙ y ≈⟨ assoc z x y ⟩ z ∙ (x ∙ y) ∎ diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index 547d4e7b48..887cb7c4a6 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/src/Relation/Binary/Definitions.agda @@ -99,7 +99,7 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x) Dense : Rel A ℓ → Set _ Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y --- Generalised connex - exactly one of the two relations holds. +-- Generalised connex - at least one of the two relations holds. Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _ Connex P Q = ∀ x y → P x y ⊎ Q y x diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 6ff59d8c28..6c2eb19bed 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -8,14 +8,12 @@ module Relation.Binary.PropositionalEquality where -import Axiom.Extensionality.Propositional as Ext open import Axiom.UniquenessOfIdentityProofs open import Function.Base using (id; _∘_) import Function.Dependent.Bundles as Dependent open import Function.Indexed.Relation.Binary.Equality using (≡-setoid) open import Level using (Level; _⊔_) -open import Data.Product.Base using (∃) - +open import Relation.Nullary using (Irrelevant) open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Definitions using (DecidableEquality) @@ -60,12 +58,6 @@ _≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B) Dependent.Func (setoid A) (Trivial.indexedSetoid B) →-to-⟶ = :→-to-Π ------------------------------------------------------------------------- --- Propositionality - -isPropositional : Set a → Set a -isPropositional A = (a b : A) → a ≡ b - ------------------------------------------------------------------------ -- More complex rearrangement lemmas @@ -113,7 +105,7 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where -- See README.Inspect for an explanation of how/why to use this. -- Normally (but not always) the new `with ... in` syntax described at --- https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality +-- https://agda.readthedocs.io/en/v2.6.4/language/with-abstraction.html#with-abstraction-equality -- can be used instead." record Reveal_·_is_ {A : Set a} {B : A → Set b} @@ -125,3 +117,21 @@ record Reveal_·_is_ {A : Set a} {B : A → Set b} inspect : ∀ {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) → Reveal f · x is f x inspect f x = [ refl ] + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +isPropositional : Set a → Set a +isPropositional = Irrelevant + +{-# WARNING_ON_USAGE isPropositional +"Warning: isPropositional was deprecated in v2.0. +Please use Relation.Nullary.Irrelevant instead. " +#-} + diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda index b8a4c30470..0b0f83f77b 100644 --- a/src/Relation/Nullary.agda +++ b/src/Relation/Nullary.agda @@ -15,20 +15,9 @@ open import Agda.Builtin.Equality ------------------------------------------------------------------------ -- Re-exports -open import Relation.Nullary.Negation.Core public using - ( ¬_; _¬-⊎_ - ; contradiction; contradiction₂; contraposition - ) - -open import Relation.Nullary.Reflects public using - ( Reflects; ofʸ; ofⁿ - ; _×-reflects_; _⊎-reflects_; _→-reflects_ - ) - -open import Relation.Nullary.Decidable.Core public using - ( Dec; does; proof; yes; no; _because_; recompute - ; ¬?; _×-dec_; _⊎-dec_; _→-dec_ - ) +open import Relation.Nullary.Negation.Core public +open import Relation.Nullary.Reflects public +open import Relation.Nullary.Decidable.Core public ------------------------------------------------------------------------ -- Irrelevant types diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 166b1f264e..f77613ea65 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -12,7 +12,7 @@ module Relation.Nullary.Decidable.Core where open import Level using (Level; Lift) -open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_) +open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_) open import Data.Unit.Base using (⊤) open import Data.Empty using (⊥) open import Data.Empty.Irrelevant using (⊥-elim) @@ -35,8 +35,8 @@ private -- reflects the boolean result. This definition allows the boolean -- part of the decision procedure to compute independently from the -- proof. This leads to better computational behaviour when we only care --- about the result and not the proof. See README.Decidability for --- further details. +-- about the result and not the proof. See README.Design.Decidability +-- for further details. infix 2 _because_ @@ -79,6 +79,9 @@ recompute (no ¬a) a = ⊥-elim (¬a a) infixr 1 _⊎-dec_ infixr 2 _×-dec_ _→-dec_ +T? : ∀ x → Dec (T x) +T? x = x because T-reflects x + ¬? : Dec A → Dec (¬ A) does (¬? a?) = not (does a?) proof (¬? a?) = ¬-reflects (proof a?) diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda index 4f97bd8709..3b301fdbce 100644 --- a/src/Relation/Nullary/Reflects.agda +++ b/src/Relation/Nullary/Reflects.agda @@ -11,11 +11,12 @@ module Relation.Nullary.Reflects where open import Agda.Builtin.Equality open import Data.Bool.Base +open import Data.Unit.Base using (⊤) open import Data.Empty open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Level using (Level) -open import Function.Base using (_$_; _∘_; const) +open import Function.Base using (_$_; _∘_; const; id) open import Relation.Nullary.Negation.Core @@ -54,28 +55,31 @@ invert (ofⁿ ¬a) = ¬a ------------------------------------------------------------------------ -- Interaction with negation, product, sums etc. +infixr 1 _⊎-reflects_ +infixr 2 _×-reflects_ _→-reflects_ + +T-reflects : ∀ b → Reflects (T b) b +T-reflects true = of _ +T-reflects false = of id + -- If we can decide A, then we can decide its negation. ¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b) ¬-reflects (ofʸ a) = ofⁿ (_$ a) ¬-reflects (ofⁿ ¬a) = ofʸ ¬a -- If we can decide A and Q then we can decide their product -infixr 2 _×-reflects_ _×-reflects_ : ∀ {a b} → Reflects A a → Reflects B b → Reflects (A × B) (a ∧ b) ofʸ a ×-reflects ofʸ b = ofʸ (a , b) ofʸ a ×-reflects ofⁿ ¬b = ofⁿ (¬b ∘ proj₂) ofⁿ ¬a ×-reflects _ = ofⁿ (¬a ∘ proj₁) - -infixr 1 _⊎-reflects_ _⊎-reflects_ : ∀ {a b} → Reflects A a → Reflects B b → Reflects (A ⊎ B) (a ∨ b) ofʸ a ⊎-reflects _ = ofʸ (inj₁ a) ofⁿ ¬a ⊎-reflects ofʸ b = ofʸ (inj₂ b) ofⁿ ¬a ⊎-reflects ofⁿ ¬b = ofⁿ (¬a ¬-⊎ ¬b) -infixr 2 _→-reflects_ _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b → Reflects (A → B) (not a ∨ b) ofʸ a →-reflects ofʸ b = ofʸ (const b) @@ -95,3 +99,6 @@ det (ofʸ a) (ofʸ _) = refl det (ofʸ a) (ofⁿ ¬a) = contradiction a ¬a det (ofⁿ ¬a) (ofʸ a) = contradiction a ¬a det (ofⁿ ¬a) (ofⁿ _) = refl + +T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a +T-reflects-elim {a} r = det r (T-reflects a) diff --git a/src/Relation/Unary/Consequences.agda b/src/Relation/Unary/Consequences.agda index 1b23578161..75c046c375 100644 --- a/src/Relation/Unary/Consequences.agda +++ b/src/Relation/Unary/Consequences.agda @@ -11,5 +11,19 @@ module Relation.Unary.Consequences where open import Relation.Unary open import Relation.Nullary using (recompute) -dec⟶recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P -dec⟶recomputable P-dec = recompute (P-dec _) +dec⇒recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P +dec⇒recomputable P-dec = recompute (P-dec _) + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +dec⟶recomputable = dec⇒recomputable +{-# WARNING_ON_USAGE dec⟶recomputable +"Warning: dec⟶recomputable was deprecated in v2.0. +Please use dec⇒recomputable instead." +#-} diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda index 0bdfe0cf2f..a4b3c1860d 100644 --- a/src/Text/Pretty.agda +++ b/src/Text/Pretty.agda @@ -23,8 +23,8 @@ open import Data.String.Base using (String; fromList; replicate) open import Function.Base using (_∘_; _∘′_; _$_) open import Effect.Monad using (RawMonad) -import Data.List.Effectful as Cat -open RawMonad (Cat.monad {Level.zero}) +import Data.List.Effectful as List +open RawMonad (List.monad {Level.zero}) import Data.Nat.Properties as ℕₚ open import Data.List.Extrema.Core ℕₚ.≤-totalOrder using (⊓ᴸ)