diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 054a8c493e..93c23f6fe7 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -76,11 +76,11 @@ jobs: if [[ '${{ github.ref }}' == 'refs/heads/experimental' \ || '${{ github.base_ref }}' == 'experimental' ]]; then # Pick Agda version for experimental - echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> "${GITHUB_ENV}"; + echo "AGDA_COMMIT=18cc53941e924b144c0f1f3953280ef726009f7e" >> "${GITHUB_ENV}"; echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}" else # Pick Agda version for master - echo "AGDA_COMMIT=tags/v2.6.4.3" >> "${GITHUB_ENV}"; + echo "AGDA_COMMIT=tags/v2.7.0" >> "${GITHUB_ENV}"; echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}" fi diff --git a/CHANGELOG.md b/CHANGELOG.md index 8852110e2b..af16162afa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ Version 2.2-dev =============== -The library has been tested using Agda 2.6.4.3. +The library has been tested using Agda 2.7.0. Highlights ---------- @@ -24,6 +24,41 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Properties.CommutativeMagma.Divisibility`: + ```agda + ∣-factors ↦ x|xy∧y|xy + ∣-factors-≈ ↦ xy≈z⇒x|z∧y|z + ``` + +* In `Algebra.Properties.Magma.Divisibility`: + ```agda + ∣-respˡ ↦ ∣-respˡ-≈ + ∣-respʳ ↦ ∣-respʳ-≈ + ∣-resp ↦ ∣-resp-≈ + ``` + +* In `Algebra.Solver.CommutativeMonoid`: + ```agda + normalise-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.correct + sg ↦ Algebra.Solver.CommutativeMonoid.Normal.singleton + sg-correct ↦ Algebra.Solver.CommutativeMonoid.Normal.singleton-correct + ``` + +* In `Algebra.Solver.IdempotentCommutativeMonoid`: + ```agda + flip12 ↦ Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz + distr ↦ Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙ + normalise-correct ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct + sg ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton + sg-correct ↦ Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct + ``` + +* In `Algebra.Solver.Monoid`: + ```agda + homomorphic ↦ Algebra.Solver.Monoid.Normal.comp-correct + normalise-correct ↦ Algebra.Solver.Monoid.Normal.correct + ``` + * In `Data.Vec.Properties`: ```agda ++-assoc _ ↦ ++-assoc-eqFree @@ -45,12 +80,48 @@ New modules Algebra.Properties.IdempotentCommutativeMonoid ``` +* Refactoring of the `Algebra.Solver.*Monoid` implementations, via + a single `Solver` module API based on the existing `Expr`, and + a common `Normal`-form API: + ```agda + Algebra.Solver.CommutativeMonoid.Normal + Algebra.Solver.IdempotentCommutativeMonoid.Normal + Algebra.Solver.Monoid.Expression + Algebra.Solver.Monoid.Normal + Algebra.Solver.Monoid.Solver + ``` + + NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`. + +* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`: + ```agda + Data.List.Relation.Unary.All.Properties.Core + ``` + Additions to existing modules ----------------------------- -* In `Data.Product.Function.Dependent.Propositional`: +* Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`: ```agda - cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B + ∤-respˡ-≈ : _∤_ Respectsˡ _≈_ + ∤-respʳ-≈ : _∤_ Respectsʳ _≈_ + ∤-resp-≈ : _∤_ Respects₂ _≈_ + ∤∤-sym : Symmetric _∤∤_ + ∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_ + ∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_ + ∤∤-resp-≈ : _∤∤_ Respects₂ _≈_ + ``` + +* In `Algebra.Solver.Ring` + ```agda + Env : ℕ → Set _ + Env = Vec Carrier + ``` + +* In `Data.List.Membership.Setoid.Properties`: + ```agda + Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys + All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys ``` * In `Data.List.Properties`: @@ -76,6 +147,11 @@ Additions to existing modules ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) ``` +* In `Data.Maybe.Properties`: + ```agda + maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b) + ``` + * New lemmas in `Data.Nat.Properties`: ```agda m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o @@ -88,6 +164,11 @@ Additions to existing modules m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n ``` +* In `Data.Product.Function.Dependent.Propositional`: + ```agda + cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B + ``` + * New lemma in `Data.Vec.Properties`: ```agda map-concat : map f (concat xss) ≡ concat (map (map f) xss) @@ -113,7 +194,7 @@ Additions to existing modules does-≡ : (a? b? : Dec A) → does a? ≡ does b? ``` -* In `Relation.Nullary.Properties`: +* In `Relation.Unary.Properties`: ```agda map : P ≐ Q → Decidable P → Decidable Q does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q? diff --git a/CHANGELOG/v2.1.1.md b/CHANGELOG/v2.1.1.md new file mode 100644 index 0000000000..a6e081a55b --- /dev/null +++ b/CHANGELOG/v2.1.1.md @@ -0,0 +1,8 @@ +Version 2.1.1 +============= + +The library has been tested using Agda 2.7.0. + +* Fixed `Reflection.AST.Definition` to take into account Agda now exposes a `Quantity` argument on the reflection `constructor` constructor. + +* In `Reflection.AST.Show` added new function `showQuantity` diff --git a/CITATION.cff b/CITATION.cff index 96507925e9..d24084c327 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: 2.1 -date-released: 2024-07-17 +version: 2.1.1 +date-released: 2024-09-07 url: "https://github.com/agda/agda-stdlib" \ No newline at end of file diff --git a/doc/README.agda b/doc/README.agda index 6a9a3e398c..844d531899 100644 --- a/doc/README.agda +++ b/doc/README.agda @@ -3,7 +3,7 @@ module README where ------------------------------------------------------------------------ --- The Agda standard library, version 2.0 +-- The Agda standard library, version 2.1.1 -- -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais -- with contributions from Andreas Abel, Stevan Andjelkovic, @@ -19,7 +19,7 @@ module README where -- and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.4. +-- This version of the library has been tested using Agda 2.7.0 -- The library comes with a .agda-lib file, for use with the library -- management system. diff --git a/doc/installation-guide.md b/doc/installation-guide.md index 893753932d..d06cec93e1 100644 --- a/doc/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 v2.1 of the standard library with Agda 2.6.4.X. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary). +Use version v2.1.1 of the standard library with Agda 2.7.0. You can find the correct version of the library to use for different Agda versions on the [Agda Wiki](https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary). 1. Navigate to a suitable directory `$HERE` (replace appropriately) where you would like to install the library. -2. Download the tarball of v2.1 of the standard library. This can either be +2. Download the tarball of v2.1.1 of the standard library. This can either be done manually by visiting the Github repository for the library, or via the command line as follows: ``` - wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.1.tar.gz + wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.1.1.tar.gz ``` Note that you can replace `wget` with other popular tools such as `curl` and that - you can replace `2.1` with any other version of the library you desire. + you can replace `2.1.1` with any other version of the library you desire. 3. Extract the standard library from the tarball. Again this can either be done manually or via the command line as follows: @@ -26,7 +26,7 @@ Use version v2.1 of the standard library with Agda 2.6.4.X. You can find the cor 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run the commands to install via cabal: ``` - cd agda-stdlib-2.1 + cd agda-stdlib-2.1.1 cabal install ``` @@ -40,7 +40,7 @@ Use version v2.1 of the standard library with Agda 2.6.4.X. You can find the cor 6. Register the standard library with Agda's package system by adding the following line to `$HOME/.agda/libraries`: ``` - $HERE/agda-stdlib-2.1/standard-library.agda-lib + $HERE/agda-stdlib-2.1.1/standard-library.agda-lib ``` Now, the standard library is ready to be used either: diff --git a/doc/release-guide.txt b/doc/release-guide.txt index 77a5e77ba5..a1ff2f1f69 100644 --- a/doc/release-guide.txt +++ b/doc/release-guide.txt @@ -13,7 +13,7 @@ procedure should be followed: - `README.md` - `doc/installation-guide.md` -* Update the copyright year range in the LICENSE file, if necessary. +* Update the copyright year range in the LICENCE file, if necessary. #### Pre-release tests diff --git a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda index 3f6cae0f0c..9261d80e82 100644 --- a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda +++ b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda @@ -7,15 +7,14 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra using (CommutativeMagma) -open import Data.Product.Base using (_×_; _,_; map) module Algebra.Properties.CommutativeMagma.Divisibility {a ℓ} (CM : CommutativeMagma a ℓ) where -open CommutativeMagma CM +open import Data.Product.Base using (_×_; _,_) -open import Relation.Binary.Reasoning.Setoid setoid +open CommutativeMagma CM using (magma; _≈_; _∙_; comm) ------------------------------------------------------------------------ -- Re-export the contents of magmas @@ -31,8 +30,28 @@ x∣xy x y = y , comm y x xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y) -∣-factors : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y) -∣-factors x y = x∣xy x y , x∣yx y x +x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y) +x|xy∧y|xy x y = x∣xy x y , x∣yx y x -∣-factors-≈ : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z -∣-factors-≈ x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z +xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z +xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +∣-factors = x|xy∧y|xy +{-# WARNING_ON_USAGE ∣-factors +"Warning: ∣-factors was deprecated in v2.2. +Please use x|xy∧y|xy instead. " +#-} +∣-factors-≈ = xy≈z⇒x|z∧y|z +{-# WARNING_ON_USAGE ∣-factors-≈ +"Warning: ∣-factors-≈ was deprecated in v2.2. +Please use xy≈z⇒x|z∧y|z instead. " +#-} diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index 629406faa1..aa9f4e53c5 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -7,11 +7,14 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra using (Magma) -open import Data.Product.Base using (_×_; _,_; ∃; map; swap) -open import Relation.Binary.Definitions module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where +open import Data.Product.Base using (_,_; swap) +open import Relation.Binary.Definitions + using (_Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Symmetric) +open import Relation.Nullary.Negation.Core using (contradiction) + open Magma M ------------------------------------------------------------------------ @@ -23,20 +26,32 @@ open import Algebra.Definitions.RawMagma rawMagma public ------------------------------------------------------------------------ -- Properties of divisibility -∣-respʳ : _∣_ Respectsʳ _≈_ -∣-respʳ y≈z (q , qx≈y) = q , trans qx≈y y≈z +∣-respʳ-≈ : _∣_ Respectsʳ _≈_ +∣-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z -∣-respˡ : _∣_ Respectsˡ _≈_ -∣-respˡ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y +∣-respˡ-≈ : _∣_ Respectsˡ _≈_ +∣-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y -∣-resp : _∣_ Respects₂ _≈_ -∣-resp = ∣-respʳ , ∣-respˡ +∣-resp-≈ : _∣_ Respects₂ _≈_ +∣-resp-≈ = ∣-respʳ-≈ , ∣-respˡ-≈ x∣yx : ∀ x y → x ∣ y ∙ x x∣yx x y = y , refl xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z -xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) +xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x) + +------------------------------------------------------------------------ +-- Properties of non-divisibility + +∤-respˡ-≈ : _∤_ Respectsˡ _≈_ +∤-respˡ-≈ x≈y x∤z y∣z = contradiction (∣-respˡ-≈ (sym x≈y) y∣z) x∤z + +∤-respʳ-≈ : _∤_ Respectsʳ _≈_ +∤-respʳ-≈ x≈y z∤x z∣y = contradiction (∣-respʳ-≈ (sym x≈y) z∣y) z∤x + +∤-resp-≈ : _∤_ Respects₂ _≈_ +∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈ ------------------------------------------------------------------------ -- Properties of mutual divisibility _∣∣_ @@ -44,11 +59,51 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ xy≈z (x∣yx y x) ∣∣-sym : Symmetric _∣∣_ ∣∣-sym = swap -∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_ -∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ y≈z x∣y , ∣-respˡ y≈z y∣x - ∣∣-respˡ-≈ : _∣∣_ Respectsˡ _≈_ -∣∣-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ x≈z x∣y , ∣-respʳ x≈z y∣x +∣∣-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x + +∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_ +∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x ∣∣-resp-≈ : _∣∣_ Respects₂ _≈_ ∣∣-resp-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈ + +------------------------------------------------------------------------ +-- Properties of mutual non-divisibility _∤∤_ + +∤∤-sym : Symmetric _∤∤_ +∤∤-sym x∤∤y y∣∣x = contradiction (∣∣-sym y∣∣x) x∤∤y + +∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_ +∤∤-respˡ-≈ x≈y x∤∤z y∣∣z = contradiction (∣∣-respˡ-≈ (sym x≈y) y∣∣z) x∤∤z + +∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_ +∤∤-respʳ-≈ x≈y z∤∤x z∣∣y = contradiction (∣∣-respʳ-≈ (sym x≈y) z∣∣y) z∤∤x + +∤∤-resp-≈ : _∤∤_ Respects₂ _≈_ +∤∤-resp-≈ = ∤∤-respʳ-≈ , ∤∤-respˡ-≈ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +∣-respˡ = ∣-respˡ-≈ +{-# WARNING_ON_USAGE ∣-respˡ +"Warning: ∣-respˡ was deprecated in v2.2. +Please use ∣-respˡ-≈ instead. " +#-} +∣-respʳ = ∣-respʳ-≈ +{-# WARNING_ON_USAGE ∣-respʳ +"Warning: ∣-respʳ was deprecated in v2.2. +Please use ∣-respʳ-≈ instead. " +#-} +∣-resp = ∣-resp-≈ +{-# WARNING_ON_USAGE ∣-resp +"Warning: ∣-resp was deprecated in v2.2. +Please use ∣-resp-≈ instead. " +#-} diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 04d4d372e6..9316418660 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -8,196 +8,40 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra +open import Algebra.Bundles using (CommutativeMonoid) -module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁ m₂) where +module Algebra.Solver.CommutativeMonoid {c ℓ} (M : CommutativeMonoid c ℓ) where -open import Data.Fin.Base using (Fin; zero; suc) -open import Data.Maybe.Base as Maybe - using (Maybe; From-just; from-just) -open import Data.Nat as ℕ using (ℕ; zero; suc; _+_) -open import Data.Nat.GeneralisedArithmetic using (fold) -open import Data.Product.Base using (_×_; uncurry) -open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate) +import Algebra.Solver.CommutativeMonoid.Normal as Normal +import Algebra.Solver.Monoid.Solver as Solver -open import Function.Base using (_∘_) - -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Relation.Binary.Reflection as Reflection -import Relation.Nullary.Decidable as Dec -import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise - -open import Relation.Binary.Consequences using (dec⇒weaklyDec) -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) -open import Relation.Nullary.Decidable as Dec using (Dec) - -open CommutativeMonoid M -open ≈-Reasoning setoid +open CommutativeMonoid M using (monoid) private - variable - n : ℕ - ------------------------------------------------------------------------- --- Monoid expressions - --- There is one constructor for every operation, plus one for --- variables; there may be at most n variables. - -infixr 5 _⊕_ -infixr 10 _•_ - -data Expr (n : ℕ) : Set where - var : Fin n → Expr n - id : Expr n - _⊕_ : Expr n → Expr n → Expr n - --- An environment contains one value for every variable. - -Env : ℕ → Set _ -Env n = Vec Carrier n - --- The semantics of an expression is a function from an environment to --- a value. + module N = Normal M -⟦_⟧ : Expr n → Env n → Carrier -⟦ var x ⟧ ρ = lookup ρ x -⟦ id ⟧ ρ = ε -⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ------------------------------------------------------------------------ -- Normal forms --- A normal form is a vector of multiplicities (a bag). - -Normal : ℕ → Set -Normal n = Vec ℕ n - --- The semantics of a normal form. - -⟦_⟧⇓ : Normal n → Env n → Carrier -⟦ [] ⟧⇓ _ = ε -⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (a ∙_) n +open N public + renaming (correct to normalise-correct) ------------------------------------------------------------------------ --- Constructions on normal forms - --- The empty bag. - -empty : Normal n -empty = replicate _ 0 - --- A singleton bag. +-- Proof procedures -sg : (i : Fin n) → Normal n -sg zero = 1 ∷ empty -sg (suc i) = 0 ∷ sg i +open Solver monoid (record { N }) public --- The composition of normal forms. - -_•_ : (v w : Normal n) → Normal n -[] • [] = [] -(l ∷ v) • (m ∷ w) = l + m ∷ v • w ------------------------------------------------------------------------ --- Correctness of the constructions on normal forms - --- The empty bag stands for the unit ε. - -empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε -empty-correct [] = refl -empty-correct (a ∷ ρ) = empty-correct ρ - --- The singleton bag stands for a single variable. - -sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x -sg-correct zero (x ∷ ρ) = begin - x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ - x ∙ ε ≈⟨ identityʳ _ ⟩ - x ∎ -sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ - --- Normal form composition corresponds to the composition of the monoid. - -comp-correct : (v w : Normal n) (ρ : Env n) → - ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) -comp-correct [] [] ρ = sym (identityˡ _) -comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ) - where - flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c) - flip12 a b c = begin - a ∙ (b ∙ c) ≈⟨ sym (assoc _ _ _) ⟩ - (a ∙ b) ∙ c ≈⟨ ∙-congʳ (comm _ _) ⟩ - (b ∙ a) ∙ c ≈⟨ assoc _ _ _ ⟩ - b ∙ (a ∙ c) ∎ - lemma : ∀ l m {d b c} (p : d ≈ b ∙ c) → - fold d (a ∙_) (l + m) ≈ fold b (a ∙_) l ∙ fold c (a ∙_) m - lemma zero zero p = p - lemma zero (suc m) p = trans (∙-congˡ (lemma zero m p)) (flip12 _ _ _) - lemma (suc l) m p = trans (∙-congˡ (lemma l m p)) (sym (assoc a _ _)) - +-- DEPRECATED NAMES ------------------------------------------------------------------------ --- Normalization - --- A normaliser. - -normalise : Expr n → Normal n -normalise (var x) = sg x -normalise id = empty -normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂ - --- The normaliser preserves the semantics of the expression. - -normalise-correct : (e : Expr n) (ρ : Env n) → - ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ -normalise-correct (var x) ρ = sg-correct x ρ -normalise-correct id ρ = empty-correct ρ -normalise-correct (e₁ ⊕ e₂) ρ = begin - - ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ - - ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ - - ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ - - ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩ - - ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ - ∎ - ------------------------------------------------------------------------- --- "Tactic. - -open module R = Reflection - setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct - public using (solve; _⊜_) - --- We can decide if two normal forms are /syntactically/ equal. - -infix 5 _≟_ - -_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂) - where open Pointwise - --- We can also give a sound, but not necessarily complete, procedure --- for determining if two expressions have the same semantics. - -prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) -prove′ e₁ e₂ = - Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)) - where - lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ - lemma eq ρ = - R.prove ρ e₁ e₂ (begin - ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ - ⟦ normalise e₂ ⟧⇓ ρ ∎) - --- This procedure can be combined with from-just. +-- Please use the new names as continuing support for the old names is +-- not guaranteed. -prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂) -prove _ e₁ e₂ = from-just (prove′ e₁ e₂) +-- Version 2.2 --- prove : ∀ n (es : Expr n × Expr n) → --- From-just (uncurry prove′ es) --- prove _ = from-just ∘ uncurry prove′ +{-# WARNING_ON_USAGE normalise-correct +"Warning: normalise-correct was deprecated in v2.2. +Please use Algebra.Solver.CommutativeMonoid.Normal.correct instead." +#-} diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda new file mode 100644 index 0000000000..2d75ec21fe --- /dev/null +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -0,0 +1,161 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Normal forms in commutative monoids +-- +-- Adapted from Algebra.Solver.Monoid.Normal +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (CommutativeMonoid) + +module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where + +import Algebra.Properties.CommutativeSemigroup as CSProperties +import Algebra.Properties.Monoid.Mult as MultProperties +open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Nat as ℕ using (ℕ; zero; suc; _+_) +open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith) +import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +open import Relation.Binary.Definitions using (DecidableEquality) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Nullary.Decidable as Dec + +open CommutativeMonoid M +open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+) +open CSProperties commutativeSemigroup using (interchange) +open ≈-Reasoning setoid + +private + variable + n : ℕ + + +------------------------------------------------------------------------ +-- Monoid expressions + +open import Algebra.Solver.Monoid.Expression rawMonoid public + hiding (NormalAPI) + +------------------------------------------------------------------------ +-- Normal forms + +-- A normal form is a vector of multiplicities (a bag). + +Normal : ℕ → Set +Normal n = Vec ℕ n + +-- The semantics of a normal form. + +⟦_⟧⇓ : Normal n → Env n → Carrier +⟦ [] ⟧⇓ _ = ε +⟦ n ∷ v ⟧⇓ (a ∷ ρ) = (n × a) ∙ (⟦ v ⟧⇓ ρ) + +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : DecidableEquality (Normal n) +nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂) + where open Pointwise using (Pointwise-≡↔≡; decidable) + +------------------------------------------------------------------------ +-- Constructions on normal forms + +-- The empty bag. + +empty : Normal n +empty = replicate _ 0 + +-- A singleton bag. + +singleton : (i : Fin n) → Normal n +singleton zero = 1 ∷ empty +singleton (suc i) = 0 ∷ singleton i + +-- The composition of normal forms. +infixr 10 _•_ + +_•_ : (v w : Normal n) → Normal n +_•_ = zipWith _+_ + +------------------------------------------------------------------------ +-- Correctness of the constructions on normal forms + +-- The empty bag stands for the unit ε. + +empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε +empty-correct [] = refl +empty-correct (a ∷ ρ) = begin + ε ∙ ⟦ empty ⟧⇓ ρ ≈⟨ identityˡ _ ⟩ + ⟦ empty ⟧⇓ ρ ≈⟨ empty-correct ρ ⟩ + ε ∎ + +-- The singleton bag stands for a single variable. + +singleton-correct : (x : Fin n) (ρ : Env n) → + ⟦ singleton x ⟧⇓ ρ ≈ lookup ρ x +singleton-correct zero (x ∷ ρ) = begin + (1 × x) ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congʳ (×-homo-1 _) ⟩ + x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ + x ∙ ε ≈⟨ identityʳ _ ⟩ + x ∎ +singleton-correct (suc x) (m ∷ ρ) = begin + ε ∙ ⟦ singleton x ⟧⇓ ρ ≈⟨ identityˡ _ ⟩ + ⟦ singleton x ⟧⇓ ρ ≈⟨ singleton-correct x ρ ⟩ + lookup ρ x ∎ + +-- Normal form composition corresponds to the composition of the monoid. + +comp-correct : ∀ v w (ρ : Env n) → + ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) +comp-correct [] [] _ = sym (identityˡ _) +comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = begin + ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ ≈⟨ ∙-congʳ (×-homo-+ a l m) ⟩ + (l × a) ∙ (m × a) ∙ ⟦ v • w ⟧⇓ ρ ≈⟨ ∙-congˡ (comp-correct v w ρ) ⟩ + (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ interchange _ _ _ _ ⟩ + ⟦ l ∷ v ⟧⇓ (a ∷ ρ) ∙ ⟦ m ∷ w ⟧⇓ (a ∷ ρ) ∎ + +------------------------------------------------------------------------ +-- Normalization + +-- A normaliser. + +normalise : Expr n → Normal n +normalise (var x) = singleton x +normalise id = empty +normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂ + +-- The normaliser preserves the semantics of the expression. + +correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ +correct (var x) ρ = singleton-correct x ρ +correct id ρ = empty-correct ρ +correct (e₁ ⊕ e₂) ρ = begin + ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ + ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ + ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ + ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ + ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ + ∎ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +sg = singleton +{-# WARNING_ON_USAGE sg +"Warning: sg was deprecated in v2.2. +Please use singleton instead." +#-} +sg-correct = singleton-correct +{-# WARNING_ON_USAGE sg-correct +"Warning: sg-correct was deprecated in v2.2. +Please use singleton-correct instead." +#-} diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index 00b8824975..d5cac0585f 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -10,208 +10,39 @@ open import Algebra.Bundles using (IdempotentCommutativeMonoid) -open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_) -open import Data.Fin.Base using (Fin; zero; suc) -open import Data.Maybe.Base as Maybe - using (Maybe; From-just; from-just) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_) -open import Data.Product.Base using (_×_; uncurry) -open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate) - -open import Function.Base using (_∘_) - -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Relation.Binary.Reflection as Reflection -import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise - -open import Relation.Binary.Consequences using (dec⇒weaklyDec) -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) -open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) -open import Relation.Nullary.Decidable as Dec using (Dec) - - module Algebra.Solver.IdempotentCommutativeMonoid - {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where - -open IdempotentCommutativeMonoid M -open ≈-Reasoning setoid - -private - variable - n : ℕ - ------------------------------------------------------------------------- --- Monoid expressions - --- There is one constructor for every operation, plus one for --- variables; there may be at most n variables. - -infixr 5 _⊕_ -infixr 10 _•_ + {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where -data Expr (n : ℕ) : Set where - var : Fin n → Expr n - id : Expr n - _⊕_ : Expr n → Expr n → Expr n +import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal +import Algebra.Solver.Monoid.Solver as Solver --- An environment contains one value for every variable. +open IdempotentCommutativeMonoid M using (monoid) -Env : ℕ → Set _ -Env n = Vec Carrier n - --- The semantics of an expression is a function from an environment to --- a value. +private + module N = Normal M -⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier -⟦ var x ⟧ ρ = lookup ρ x -⟦ id ⟧ ρ = ε -⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ------------------------------------------------------------------------ -- Normal forms --- A normal form is a vector of bits (a set). - -Normal : ℕ → Set -Normal n = Vec Bool n - --- The semantics of a normal form. - -⟦_⟧⇓ : Normal n → Env n → Carrier -⟦ [] ⟧⇓ _ = ε -⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ) - ------------------------------------------------------------------------- --- Constructions on normal forms - --- The empty set. - -empty : Normal n -empty = replicate _ false - --- A singleton set. - -sg : (i : Fin n) → Normal n -sg zero = true ∷ empty -sg (suc i) = false ∷ sg i - --- The composition of normal forms. - -_•_ : (v w : Normal n) → Normal n -[] • [] = [] -(l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w +open N public + renaming (correct to normalise-correct) ------------------------------------------------------------------------ --- Correctness of the constructions on normal forms - --- The empty set stands for the unit ε. - -empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε -empty-correct [] = refl -empty-correct (a ∷ ρ) = empty-correct ρ - --- The singleton set stands for a single variable. - -sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x -sg-correct zero (x ∷ ρ) = begin - x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ - x ∙ ε ≈⟨ identityʳ _ ⟩ - x ∎ -sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ - --- Normal form composition corresponds to the composition of the monoid. +-- Proof procedures -flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c) -flip12 a b c = begin - a ∙ (b ∙ c) ≈⟨ sym (assoc _ _ _) ⟩ - (a ∙ b) ∙ c ≈⟨ ∙-congʳ (comm _ _) ⟩ - (b ∙ a) ∙ c ≈⟨ assoc _ _ _ ⟩ - b ∙ (a ∙ c) ∎ +open Solver monoid (record { N }) public -distr : ∀ a b c → a ∙ (b ∙ c) ≈ (a ∙ b) ∙ (a ∙ c) -distr a b c = begin - a ∙ (b ∙ c) ≈⟨ ∙-cong (sym (idem a)) refl ⟩ - (a ∙ a) ∙ (b ∙ c) ≈⟨ assoc _ _ _ ⟩ - a ∙ (a ∙ (b ∙ c)) ≈⟨ ∙-congˡ (sym (assoc _ _ _)) ⟩ - a ∙ ((a ∙ b) ∙ c) ≈⟨ ∙-congˡ (∙-congʳ (comm _ _)) ⟩ - a ∙ ((b ∙ a) ∙ c) ≈⟨ ∙-congˡ (assoc _ _ _) ⟩ - a ∙ (b ∙ (a ∙ c)) ≈⟨ sym (assoc _ _ _) ⟩ - (a ∙ b) ∙ (a ∙ c) ∎ - -comp-correct : ∀ (v w : Normal n) (ρ : Env n) → - ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) -comp-correct [] [] ρ = sym (identityˡ _) -comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) = - trans (∙-congˡ (comp-correct v w ρ)) (distr _ _ _) -comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) = - trans (∙-congˡ (comp-correct v w ρ)) (sym (assoc _ _ _)) -comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) = - trans (∙-congˡ (comp-correct v w ρ)) (flip12 _ _ _) -comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) = - comp-correct v w ρ ------------------------------------------------------------------------ --- Normalization - --- A normaliser. - -normalise : Expr n → Normal n -normalise (var x) = sg x -normalise id = empty -normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂ - --- The normaliser preserves the semantics of the expression. - -normalise-correct : (e : Expr n) (ρ : Env n) → - ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ -normalise-correct (var x) ρ = sg-correct x ρ -normalise-correct id ρ = empty-correct ρ -normalise-correct (e₁ ⊕ e₂) ρ = begin - - ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ - - ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ - - ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ - - ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩ - - ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ - ∎ - +-- DEPRECATED NAMES ------------------------------------------------------------------------ --- "Tactic. - -open module R = Reflection - setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct - public using (solve; _⊜_) - --- We can decide if two normal forms are /syntactically/ equal. - -infix 5 _≟_ - -_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) - where open Pointwise - --- We can also give a sound, but not necessarily complete, procedure --- for determining if two expressions have the same semantics. - -prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) -prove′ e₁ e₂ = - Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)) - where - lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ - lemma eq ρ = - R.prove ρ e₁ e₂ (begin - ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ - ⟦ normalise e₂ ⟧⇓ ρ ∎) - --- This procedure can be combined with from-just. +-- Please use the new names as continuing support for the old names is +-- not guaranteed. -prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂) -prove _ e₁ e₂ = from-just (prove′ e₁ e₂) +-- Version 2.2 --- prove : ∀ n (es : Expr n × Expr n) → --- From-just (uncurry prove′ es) --- prove _ = from-just ∘ uncurry prove′ +{-# WARNING_ON_USAGE normalise-correct +"Warning: normalise-correct was deprecated in v2.2. +Please use Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct instead." +#-} diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda new file mode 100644 index 0000000000..bb90c66c72 --- /dev/null +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -0,0 +1,168 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Solver for equations in idempotent commutative monoids +-- +-- Adapted from Algebra.Solver.CommutativeMonoid +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (IdempotentCommutativeMonoid) + +module Algebra.Solver.IdempotentCommutativeMonoid.Normal + {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where + +import Algebra.Properties.CommutativeSemigroup as CSProperties +open import Algebra.Properties.IdempotentCommutativeMonoid M using (∙-distrˡ-∙) +open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_) +open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith) +import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise +open import Relation.Binary.Definitions using (DecidableEquality) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Nullary.Decidable as Dec + +open IdempotentCommutativeMonoid M +open CSProperties commutativeSemigroup using (x∙yz≈xy∙z; x∙yz≈y∙xz) +open ≈-Reasoning setoid + +private + variable + n : ℕ + + +------------------------------------------------------------------------ +-- Monoid expressions + +open import Algebra.Solver.Monoid.Expression rawMonoid public + hiding (NormalAPI) + +------------------------------------------------------------------------ +-- Normal forms + +-- A normal form is a vector of bits (a set). + +Normal : ℕ → Set +Normal n = Vec Bool n + +-- The semantics of a normal form. + +⟦_⟧⇓ : Normal n → Env n → Carrier +⟦ [] ⟧⇓ _ = ε +⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ) + +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : DecidableEquality (Normal n) +nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) + where open Pointwise using (Pointwise-≡↔≡; decidable) + +------------------------------------------------------------------------ +-- Constructions on normal forms + +-- The empty set. + +empty : Normal n +empty = replicate _ false + +-- A singleton set. + +singleton : (i : Fin n) → Normal n +singleton zero = true ∷ empty +singleton (suc i) = false ∷ singleton i + +-- The composition of normal forms. +infixr 10 _•_ + +_•_ : (v w : Normal n) → Normal n +_•_ = zipWith _∨_ + +------------------------------------------------------------------------ +-- Correctness of the constructions on normal forms + +-- The empty set stands for the unit ε. + +empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε +empty-correct [] = refl +empty-correct (a ∷ ρ) = empty-correct ρ + +-- The singleton set stands for a single variable. + +singleton-correct : (x : Fin n) (ρ : Env n) → + ⟦ singleton x ⟧⇓ ρ ≈ lookup ρ x +singleton-correct zero (x ∷ ρ) = begin + x ∙ ⟦ empty ⟧⇓ ρ ≈⟨ ∙-congˡ (empty-correct ρ) ⟩ + x ∙ ε ≈⟨ identityʳ _ ⟩ + x ∎ +singleton-correct (suc x) (m ∷ ρ) = singleton-correct x ρ + +-- Normal form composition corresponds to the composition of the monoid. + +comp-correct : ∀ v w (ρ : Env n) → + ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) +comp-correct [] [] ρ = sym (identityˡ _) +comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) = + trans (∙-congˡ (comp-correct v w ρ)) (∙-distrˡ-∙ _ _ _) +comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) = + trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈xy∙z _ _ _) +comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) = + trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈y∙xz _ _ _) +comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) = + comp-correct v w ρ + +------------------------------------------------------------------------ +-- Normalization + +-- A normaliser. + +normalise : Expr n → Normal n +normalise (var x) = singleton x +normalise id = empty +normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂ + +-- The normaliser preserves the semantics of the expression. + +correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ +correct (var x) ρ = singleton-correct x ρ +correct id ρ = empty-correct ρ +correct (e₁ ⊕ e₂) ρ = begin + ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ + ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ + ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ + ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ + ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ + ∎ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.2 + +flip12 = x∙yz≈y∙xz +{-# WARNING_ON_USAGE flip12 +"Warning: flip12 was deprecated in v2.2. +Please use Algebra.Properties.CommutativeSemigroup.x∙yz≈y∙xz instead." +#-} +distr = ∙-distrˡ-∙ +{-# WARNING_ON_USAGE distr +"Warning: distr was deprecated in v2.2. +Please use Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙ instead." +#-} +sg = singleton +{-# WARNING_ON_USAGE sg +"Warning: sg was deprecated in v2.2. +Please use singleton instead." +#-} +sg-correct = singleton-correct +{-# WARNING_ON_USAGE sg-correct +"Warning: sg-correct was deprecated in v2.2. +Please use singleton-correct instead." +#-} diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index 7debc4e1aa..f0ee5ca799 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -6,133 +6,51 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra +open import Algebra.Bundles using (Monoid) -module Algebra.Solver.Monoid {m₁ m₂} (M : Monoid m₁ m₂) where +module Algebra.Solver.Monoid {c ℓ} (M : Monoid c ℓ) where -open import Data.Fin.Base as Fin -import Data.Fin.Properties as Fin -open import Data.List.Base hiding (lookup) -import Data.List.Relation.Binary.Equality.DecPropositional as ListEq +import Algebra.Solver.Monoid.Normal as Normal +import Algebra.Solver.Monoid.Solver as Solver open import Data.Maybe.Base as Maybe - using (Maybe; From-just; from-just) -open import Data.Nat.Base using (ℕ) + using (From-just; from-just) open import Data.Product.Base using (_×_; uncurry) -open import Data.Vec.Base using (Vec; lookup) -open import Function.Base using (_∘_; _$_) -open import Relation.Binary.Consequences using (dec⇒weaklyDec) -open import Relation.Binary.Definitions using (DecidableEquality) +open import Function.Base using (_∘_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) -import Relation.Binary.Reflection -import Relation.Nullary.Decidable.Core as Dec +private + module N = Normal M -open Monoid M -open import Relation.Binary.Reasoning.Setoid setoid - ------------------------------------------------------------------------- --- Monoid expressions - --- There is one constructor for every operation, plus one for --- variables; there may be at most n variables. - -infixr 5 _⊕_ - -data Expr (n : ℕ) : Set where - var : Fin n → Expr n - id : Expr n - _⊕_ : Expr n → Expr n → Expr n - --- An environment contains one value for every variable. - -Env : ℕ → Set _ -Env n = Vec Carrier n - --- The semantics of an expression is a function from an environment to --- a value. - -⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier -⟦ var x ⟧ ρ = lookup ρ x -⟦ id ⟧ ρ = ε -⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ------------------------------------------------------------------------ -- Normal forms --- A normal form is a list of variables. - -Normal : ℕ → Set -Normal n = List (Fin n) - --- The semantics of a normal form. - -⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier -⟦ [] ⟧⇓ ρ = ε -⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ - --- A normaliser. - -normalise : ∀ {n} → Expr n → Normal n -normalise (var x) = x ∷ [] -normalise id = [] -normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂ - --- The normaliser is homomorphic with respect to _++_/_∙_. - -homomorphic : ∀ {n} (nf₁ nf₂ : Normal n) (ρ : Env n) → - ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) -homomorphic [] nf₂ ρ = begin - ⟦ nf₂ ⟧⇓ ρ ≈⟨ sym $ identityˡ _ ⟩ - ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ -homomorphic (x ∷ nf₁) nf₂ ρ = begin - lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (homomorphic nf₁ nf₂ ρ) ⟩ - lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ≈⟨ sym $ assoc _ _ _ ⟩ - lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∎ - --- The normaliser preserves the semantics of the expression. - -normalise-correct : - ∀ {n} (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ -normalise-correct (var x) ρ = begin - lookup ρ x ∙ ε ≈⟨ identityʳ _ ⟩ - lookup ρ x ∎ -normalise-correct id ρ = begin - ε ∎ -normalise-correct (e₁ ⊕ e₂) ρ = begin - ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ homomorphic (normalise e₁) (normalise e₂) ρ ⟩ - ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩ - ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ +open N public + renaming (comp-correct to homomorphic; correct to normalise-correct) ------------------------------------------------------------------------ --- "Tactic. +-- Tactic -open module R = Relation.Binary.Reflection - setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct - public using (solve; _⊜_) +open Solver M (record { N }) public + hiding (prove) --- We can decide if two normal forms are /syntactically/ equal. - -infix 5 _≟_ +prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es) +prove _ = from-just ∘ uncurry prove′ -_≟_ : ∀ {n} → DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) - where open ListEq Fin._≟_ --- We can also give a sound, but not necessarily complete, procedure --- for determining if two expressions have the same semantics. +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. -prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) -prove′ e₁ e₂ = - Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) - where - lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ - lemma eq ρ = - R.prove ρ e₁ e₂ (begin - ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ - ⟦ normalise e₂ ⟧⇓ ρ ∎) +-- Version 2.2 --- This procedure can be combined with from-just. +{-# WARNING_ON_USAGE homomorphic +"Warning: homomorphic was deprecated in v2.2. +Please use Algebra.Solver.Monoid.Normal.comp-correct instead." +#-} -prove : ∀ n (es : Expr n × Expr n) → - From-just (uncurry prove′ es) -prove _ = from-just ∘ uncurry prove′ +{-# WARNING_ON_USAGE normalise-correct +"Warning: normalise-correct was deprecated in v2.2. +Please use Algebra.Solver.Monoid.Normal.correct instead." +#-} diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda new file mode 100644 index 0000000000..7b71c9e9c2 --- /dev/null +++ b/src/Algebra/Solver/Monoid/Expression.agda @@ -0,0 +1,69 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles.Raw using (RawMonoid) + +module Algebra.Solver.Monoid.Expression {c ℓ} (M : RawMonoid c ℓ) where + +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (Vec; lookup) +open import Level using (suc; _⊔_) +open import Relation.Binary.Definitions using (DecidableEquality) + +open RawMonoid M + +private + variable + n : ℕ + +------------------------------------------------------------------------ +-- Monoid expressions + +-- There is one constructor for every operation, plus one for +-- variables; there may be at most n variables. + +infixr 5 _⊕_ + +data Expr (n : ℕ) : Set where + var : Fin n → Expr n + id : Expr n + _⊕_ : Expr n → Expr n → Expr n + +-- An environment contains one value for every variable. + +Env : ℕ → Set _ +Env n = Vec Carrier n + +-- The semantics of an expression is a function from an environment to +-- a value. + +⟦_⟧ : Expr n → Env n → Carrier +⟦ var x ⟧ ρ = lookup ρ x +⟦ id ⟧ ρ = ε +⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ + +------------------------------------------------------------------------ +-- API for normal expressions + +record NormalAPI a : Set (suc a ⊔ c ⊔ ℓ) where + infix 5 _≟_ + + field + +-- The type of normal forms. + Normal : ℕ → Set a +-- We can decide if two normal forms are /syntactically/ equal. + _≟_ : DecidableEquality (Normal n) +-- A normaliser. + normalise : Expr n → Normal n +-- The semantics of a normal form. + ⟦_⟧⇓ : Normal n → Env n → Carrier +-- The normaliser preserves the semantics of the expression. + correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ + diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda new file mode 100644 index 0000000000..6fd4f3e839 --- /dev/null +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -0,0 +1,89 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Monoid) + +module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where + +open import Data.Fin.Base using (Fin) +import Data.Fin.Properties as Fin +open import Data.List.Base using (List; [] ; _∷_; _++_) +import Data.List.Relation.Binary.Equality.DecPropositional as ≋ +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (lookup) +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.Definitions using (DecidableEquality) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Nullary.Decidable as Dec + +open Monoid M +open ≈-Reasoning setoid + +private + variable + n : ℕ + + +------------------------------------------------------------------------ +-- Monoid expressions + +open import Algebra.Solver.Monoid.Expression rawMonoid public + +------------------------------------------------------------------------ +-- Normal forms + +-- A normal form is a list of variables. + +Normal : ℕ → Set _ +Normal n = List (Fin n) + +-- The semantics of a normal form. + +⟦_⟧⇓ : Normal n → Env n → Carrier +⟦ [] ⟧⇓ ρ = ε +⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ + +-- We can decide if two normal forms are /syntactically/ equal. + +infix 5 _≟_ + +_≟_ : DecidableEquality (Normal n) +nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) + where open ≋ Fin._≟_ using (_≋?_; ≋⇒≡; ≡⇒≋) + +-- A normaliser. + +normalise : Expr n → Normal n +normalise (var x) = x ∷ [] +normalise id = [] +normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂ + +-- The normaliser is homomorphic with respect to _++_/_∙_. + +comp-correct : ∀ nf₁ nf₂ (ρ : Env n) → + ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) +comp-correct [] nf₂ ρ = begin + ⟦ nf₂ ⟧⇓ ρ ≈⟨ identityˡ _ ⟨ + ε ∙ ⟦ nf₂ ⟧⇓ ρ ∎ +comp-correct (x ∷ nf₁) nf₂ ρ = begin + lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈⟨ ∙-congˡ (comp-correct nf₁ nf₂ ρ) ⟩ + lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ) ≈⟨ assoc _ _ _ ⟨ + lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ ∎ + +-- The normaliser preserves the semantics of the expression. + +correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ +correct (var x) ρ = begin + lookup ρ x ∙ ε ≈⟨ identityʳ _ ⟩ + lookup ρ x ∎ +correct id ρ = begin + ε ∎ +correct (e₁ ⊕ e₂) ρ = begin + ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ + ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ + ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ diff --git a/src/Algebra/Solver/Monoid/Solver.agda b/src/Algebra/Solver/Monoid/Solver.agda new file mode 100644 index 0000000000..a1281e9639 --- /dev/null +++ b/src/Algebra/Solver/Monoid/Solver.agda @@ -0,0 +1,57 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Monoid) +import Algebra.Solver.Monoid.Expression as Expression + +module Algebra.Solver.Monoid.Solver {a c ℓ} (M : Monoid c ℓ) + (open Monoid M using (rawMonoid; setoid; _≈_)) + (open Expression rawMonoid using (Expr; Env; var; ⟦_⟧; NormalAPI)) + (N : NormalAPI a) where + +open import Data.Maybe.Base as Maybe + using (Maybe; From-just; from-just) +open import Data.Nat.Base using (ℕ) +open import Function.Base using (_∘_; _$_) +open import Relation.Binary.Consequences using (dec⇒weaklyDec) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) +import Relation.Binary.Reflection as Reflection + +open NormalAPI N + +private + variable + n : ℕ + module + R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct + + +------------------------------------------------------------------------ +-- Proof procedures + +-- Re-export the existing solver machinery from `Reflection` + +open R public + using (solve; _⊜_) + +-- We can also give a sound, but not necessarily complete, procedure +-- for determining if two expressions have the same semantics. + +prove′ : ∀ e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) +prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) + where + open import Relation.Binary.Reasoning.Setoid setoid + lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ + lemma eq ρ = R.prove ρ e₁ e₂ $ begin + ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ + ⟦ normalise e₂ ⟧⇓ ρ ∎ + +-- This procedure can then be combined with from-just. + +prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂) +prove _ e₁ e₂ = from-just $ prove′ e₁ e₂ diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda index a2a982d5c2..4d31bf5442 100644 --- a/src/Algebra/Solver/Ring.agda +++ b/src/Algebra/Solver/Ring.agda @@ -58,6 +58,11 @@ infixl 8 _:*_ _*N_ _*H_ _*NH_ _*HN_ infixl 7 _:+_ _:-_ _+H_ _+N_ infix 4 _≈H_ _≈N_ +private + variable + n : ℕ + + ------------------------------------------------------------------------ -- Polynomials @@ -76,16 +81,16 @@ data Polynomial (m : ℕ) : Set r₁ where -- Short-hand notation. -_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n +_:+_ : Polynomial n → Polynomial n → Polynomial n _:+_ = op [+] -_:*_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n +_:*_ : Polynomial n → Polynomial n → Polynomial n _:*_ = op [*] -_:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n +_:-_ : Polynomial n → Polynomial n → Polynomial n x :- y = x :+ :- y -_:×_ : ∀ {n} → ℕ → Polynomial n → Polynomial n +_:×_ : ℕ → Polynomial n → Polynomial n zero :× p = con C.0# suc m :× p = p :+ m :× p @@ -95,7 +100,12 @@ sem : Op → Op₂ Carrier sem [+] = _+_ sem [*] = _*_ -⟦_⟧ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier +-- An environment contains one value for every variable. + +Env : ℕ → Set _ +Env = Vec Carrier + +⟦_⟧ : Polynomial n → Env n → Carrier ⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ ⟦ con c ⟧ ρ = ⟦ c ⟧′ ⟦ var x ⟧ ρ = lookup ρ x @@ -132,12 +142,12 @@ mutual -- degree. data HNF : ℕ → Set r₁ where - ∅ : ∀ {n} → HNF (suc n) - _*x+_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n) + ∅ : HNF (suc n) + _*x+_ : HNF (suc n) → Normal n → HNF (suc n) data Normal : ℕ → Set r₁ where con : C.Carrier → Normal zero - poly : ∀ {n} → HNF (suc n) → Normal (suc n) + poly : HNF (suc n) → Normal (suc n) -- Note that the data types above do /not/ ensure uniqueness of -- normal forms: the zero polynomial of degree one can be @@ -147,11 +157,11 @@ mutual -- Semantics. - ⟦_⟧H : ∀ {n} → HNF (suc n) → Vec Carrier (suc n) → Carrier + ⟦_⟧H : HNF (suc n) → Env (suc n) → Carrier ⟦ ∅ ⟧H _ = 0# ⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ - ⟦_⟧N : ∀ {n} → Normal n → Vec Carrier n → Carrier + ⟦_⟧N : Normal n → Env n → Carrier ⟦ con c ⟧N _ = ⟦ c ⟧′ ⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ @@ -162,12 +172,12 @@ mutual -- Equality. - data _≈H_ : ∀ {n} → HNF n → HNF n → Set (r₁ ⊔ r₃) where - ∅ : ∀ {n} → _≈H_ {suc n} ∅ ∅ + data _≈H_ : HNF n → HNF n → Set (r₁ ⊔ r₃) where + ∅ : _≈H_ {suc n} ∅ ∅ _*x+_ : ∀ {n} {p₁ p₂ : HNF (suc n)} {c₁ c₂ : Normal n} → p₁ ≈H p₂ → c₁ ≈N c₂ → (p₁ *x+ c₁) ≈H (p₂ *x+ c₂) - data _≈N_ : ∀ {n} → Normal n → Normal n → Set (r₁ ⊔ r₃) where + data _≈N_ : Normal n → Normal n → Set (r₁ ⊔ r₃) where con : ∀ {c₁ c₂} → ⟦ c₁ ⟧′ ≈ ⟦ c₂ ⟧′ → con c₁ ≈N con c₂ poly : ∀ {n} {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → poly p₁ ≈N poly p₂ @@ -177,7 +187,7 @@ mutual infix 4 _≟H_ _≟N_ - _≟H_ : ∀ {n} → WeaklyDecidable (_≈H_ {n = n}) + _≟H_ : WeaklyDecidable (_≈H_ {n = n}) ∅ ≟H ∅ = just ∅ ∅ ≟H (_ *x+ _) = nothing (_ *x+ _) ≟H ∅ = nothing @@ -186,7 +196,7 @@ mutual ... | _ | nothing = nothing ... | nothing | _ = nothing - _≟N_ : ∀ {n} → WeaklyDecidable (_≈N_ {n = n}) + _≟N_ : WeaklyDecidable (_≈N_ {n = n}) con c₁ ≟N con c₂ with c₁ coeff≟ c₂ ... | just c₁≈c₂ = just (con c₁≈c₂) ... | nothing = nothing @@ -198,7 +208,7 @@ mutual -- The semantics respect the equality relations defined above. - ⟦_⟧H-cong : ∀ {n} {p₁ p₂ : HNF (suc n)} → + ⟦_⟧H-cong : {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → ∀ ρ → ⟦ p₁ ⟧H ρ ≈ ⟦ p₂ ⟧H ρ ⟦ ∅ ⟧H-cong _ = refl ⟦ p₁≈p₂ *x+ c₁≈c₂ ⟧H-cong (x ∷ ρ) = @@ -206,9 +216,8 @@ mutual ⟨ +-cong ⟩ ⟦ c₁≈c₂ ⟧N-cong ρ - ⟦_⟧N-cong : - ∀ {n} {p₁ p₂ : Normal n} → - p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ + ⟦_⟧N-cong : {p₁ p₂ : Normal n} → + p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ ⟦ con c₁≈c₂ ⟧N-cong _ = c₁≈c₂ ⟦ poly p₁≈p₂ ⟧N-cong ρ = ⟦ p₁≈p₂ ⟧H-cong ρ @@ -217,10 +226,10 @@ mutual -- Zero. -0H : ∀ {n} → HNF (suc n) +0H : HNF (suc n) 0H = ∅ -0N : ∀ {n} → Normal n +0N : Normal n 0N {zero} = con C.0# 0N {suc n} = poly 0H @@ -228,16 +237,16 @@ mutual -- One. - 1H : ∀ {n} → HNF (suc n) + 1H : HNF (suc n) 1H {n} = ∅ *x+ 1N {n} - 1N : ∀ {n} → Normal n + 1N : Normal n 1N {zero} = con C.1# 1N {suc n} = poly 1H -- A simplifying variant of _*x+_. -_*x+HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n) +_*x+HN_ : HNF (suc n) → Normal n → HNF (suc n) (p *x+ c′) *x+HN c = (p *x+ c′) *x+ c ∅ *x+HN c with c ≟N 0N ... | just c≈0 = ∅ @@ -247,49 +256,49 @@ mutual -- Addition. - _+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n) + _+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n) ∅ +H p = p p +H ∅ = p (p₁ *x+ c₁) +H (p₂ *x+ c₂) = (p₁ +H p₂) *x+HN (c₁ +N c₂) - _+N_ : ∀ {n} → Normal n → Normal n → Normal n + _+N_ : Normal n → Normal n → Normal n con c₁ +N con c₂ = con (c₁ C.+ c₂) poly p₁ +N poly p₂ = poly (p₁ +H p₂) -- Multiplication. -_*x+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n) +_*x+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n) p₁ *x+H (p₂ *x+ c) = (p₁ +H p₂) *x+HN c ∅ *x+H ∅ = ∅ (p₁ *x+ c) *x+H ∅ = (p₁ *x+ c) *x+ 0N mutual - _*NH_ : ∀ {n} → Normal n → HNF (suc n) → HNF (suc n) + _*NH_ : Normal n → HNF (suc n) → HNF (suc n) c *NH ∅ = ∅ c *NH (p *x+ c′) with c ≟N 0N ... | just c≈0 = ∅ ... | nothing = (c *NH p) *x+ (c *N c′) - _*HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n) + _*HN_ : HNF (suc n) → Normal n → HNF (suc n) ∅ *HN c = ∅ (p *x+ c′) *HN c with c ≟N 0N ... | just c≈0 = ∅ ... | nothing = (p *HN c) *x+ (c′ *N c) - _*H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n) + _*H_ : HNF (suc n) → HNF (suc n) → HNF (suc n) ∅ *H _ = ∅ (_ *x+ _) *H ∅ = ∅ (p₁ *x+ c₁) *H (p₂ *x+ c₂) = ((p₁ *H p₂) *x+H (p₁ *HN c₂ +H c₁ *NH p₂)) *x+HN (c₁ *N c₂) - _*N_ : ∀ {n} → Normal n → Normal n → Normal n + _*N_ : Normal n → Normal n → Normal n con c₁ *N con c₂ = con (c₁ C.* c₂) poly p₁ *N poly p₂ = poly (p₁ *H p₂) -- Exponentiation. -_^N_ : ∀ {n} → Normal n → ℕ → Normal n +_^N_ : Normal n → ℕ → Normal n p ^N zero = 1N p ^N suc n = p *N (p ^N n) @@ -297,25 +306,25 @@ mutual -- Negation. - -H_ : ∀ {n} → HNF (suc n) → HNF (suc n) + -H_ : HNF (suc n) → HNF (suc n) -H p = (-N 1N) *NH p - -N_ : ∀ {n} → Normal n → Normal n + -N_ : Normal n → Normal n -N con c = con (C.- c) -N poly p = poly (-H p) ------------------------------------------------------------------------ -- Normalisation -normalise-con : ∀ {n} → C.Carrier → Normal n +normalise-con : C.Carrier → Normal n normalise-con {zero} c = con c normalise-con {suc n} c = poly (∅ *x+HN normalise-con c) -normalise-var : ∀ {n} → Fin n → Normal n +normalise-var : Fin n → Normal n normalise-var zero = poly ((∅ *x+ 1N) *x+ 0N) normalise-var (suc i) = poly (∅ *x+HN normalise-var i) -normalise : ∀ {n} → Polynomial n → Normal n +normalise : Polynomial n → Normal n normalise (op [+] t₁ t₂) = normalise t₁ +N normalise t₂ normalise (op [*] t₁ t₂) = normalise t₁ *N normalise t₂ normalise (con c) = normalise-con c @@ -325,7 +334,7 @@ normalise (:- t) = -N normalise t -- Evaluation after normalisation. -⟦_⟧↓ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier +⟦_⟧↓ : Polynomial n → Env n → Carrier ⟦ p ⟧↓ ρ = ⟦ normalise p ⟧N ρ ------------------------------------------------------------------------ @@ -502,7 +511,7 @@ mutual ------------------------------------------------------------------------ -- Correctness -correct-con : ∀ {n} (c : C.Carrier) (ρ : Vec Carrier n) → +correct-con : ∀ {n} (c : C.Carrier) (ρ : Env n) → ⟦ normalise-con c ⟧N ρ ≈ ⟦ c ⟧′ correct-con c [] = refl correct-con c (x ∷ ρ) = begin diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 48303dec37..76bbd8beaf 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -17,6 +17,7 @@ import Data.List.Membership.Setoid as Membership import Data.List.Relation.Binary.Equality.Setoid as Equality open import Data.List.Relation.Unary.All as All using (All) open import Data.List.Relation.Unary.Any as Any using (Any; here; there) +import Data.List.Relation.Unary.All.Properties.Core as All import Data.List.Relation.Unary.Any.Properties as Any import Data.List.Relation.Unary.Unique.Setoid as Unique open import Data.Nat.Base using (suc; z_ diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index 3f06fef070..45fc85a00f 100644 --- a/src/Reflection/AST/Definition.agda +++ b/src/Reflection/AST/Definition.agda @@ -15,12 +15,13 @@ open import Relation.Nullary.Decidable.Core using (map′; _×-dec_; open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) -import Reflection.AST.Argument as Arg -import Reflection.AST.Name as Name -import Reflection.AST.Term as Term +import Reflection.AST.Argument as Arg +import Reflection.AST.Argument.Quantity as Quantity +import Reflection.AST.Name as Name +import Reflection.AST.Term as Term ------------------------------------------------------------------------ --- Re-exporting type publically +-- Re-exporting type publicly open import Agda.Builtin.Reflection public using ( Definition @@ -56,8 +57,14 @@ record′-injective₂ refl = refl record′-injective : ∀ {c c′ fs fs′} → record′ c fs ≡ record′ c′ fs′ → c ≡ c′ × fs ≡ fs′ record′-injective = < record′-injective₁ , record′-injective₂ > -constructor′-injective : ∀ {c c′} → constructor′ c ≡ constructor′ c′ → c ≡ c′ -constructor′-injective refl = refl +constructor′-injective₁ : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′ +constructor′-injective₁ refl = refl + +constructor′-injective₂ : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → q ≡ q′ +constructor′-injective₂ refl = refl + +constructor′-injective : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′ × q ≡ q′ +constructor′-injective = < constructor′-injective₁ , constructor′-injective₂ > infix 4 _≟_ @@ -70,39 +77,40 @@ data-type pars cs ≟ data-type pars′ cs′ = record′ c fs ≟ record′ c′ fs′ = map′ (uncurry (cong₂ record′)) record′-injective (c Name.≟ c′ ×-dec List.≡-dec (Arg.≡-dec Name._≟_) fs fs′) -constructor′ d ≟ constructor′ d′ = - map′ (cong constructor′) constructor′-injective (d Name.≟ d′) +constructor′ d q ≟ constructor′ d′ q′ = + map′ (uncurry (cong₂ constructor′)) constructor′-injective + (d Name.≟ d′ ×-dec q Quantity.≟ q′) axiom ≟ axiom = yes refl primitive′ ≟ primitive′ = yes refl -- antidiagonal function cs ≟ data-type pars cs₁ = no (λ ()) function cs ≟ record′ c fs = no (λ ()) -function cs ≟ constructor′ d = no (λ ()) +function cs ≟ constructor′ d q = no (λ ()) function cs ≟ axiom = no (λ ()) function cs ≟ primitive′ = no (λ ()) data-type pars cs ≟ function cs₁ = no (λ ()) data-type pars cs ≟ record′ c fs = no (λ ()) -data-type pars cs ≟ constructor′ d = no (λ ()) +data-type pars cs ≟ constructor′ d q = no (λ ()) data-type pars cs ≟ axiom = no (λ ()) data-type pars cs ≟ primitive′ = no (λ ()) record′ c fs ≟ function cs = no (λ ()) record′ c fs ≟ data-type pars cs = no (λ ()) -record′ c fs ≟ constructor′ d = no (λ ()) +record′ c fs ≟ constructor′ d q = no (λ ()) record′ c fs ≟ axiom = no (λ ()) record′ c fs ≟ primitive′ = no (λ ()) -constructor′ d ≟ function cs = no (λ ()) -constructor′ d ≟ data-type pars cs = no (λ ()) -constructor′ d ≟ record′ c fs = no (λ ()) -constructor′ d ≟ axiom = no (λ ()) -constructor′ d ≟ primitive′ = no (λ ()) +constructor′ d q ≟ function cs = no (λ ()) +constructor′ d q ≟ data-type pars cs = no (λ ()) +constructor′ d q ≟ record′ c fs = no (λ ()) +constructor′ d q ≟ axiom = no (λ ()) +constructor′ d q ≟ primitive′ = no (λ ()) axiom ≟ function cs = no (λ ()) axiom ≟ data-type pars cs = no (λ ()) axiom ≟ record′ c fs = no (λ ()) -axiom ≟ constructor′ d = no (λ ()) +axiom ≟ constructor′ d q = no (λ ()) axiom ≟ primitive′ = no (λ ()) primitive′ ≟ function cs = no (λ ()) primitive′ ≟ data-type pars cs = no (λ ()) primitive′ ≟ record′ c fs = no (λ ()) -primitive′ ≟ constructor′ d = no (λ ()) +primitive′ ≟ constructor′ d q = no (λ ()) primitive′ ≟ axiom = no (λ ()) diff --git a/src/Reflection/AST/Instances.agda b/src/Reflection/AST/Instances.agda index cb7cc014d5..27a766076d 100644 --- a/src/Reflection/AST/Instances.agda +++ b/src/Reflection/AST/Instances.agda @@ -17,6 +17,7 @@ import Reflection.AST.Abstraction as Abstraction import Reflection.AST.Argument as Argument import Reflection.AST.Argument.Visibility as Visibility import Reflection.AST.Argument.Relevance as Relevance +import Reflection.AST.Argument.Quantity as Quantity import Reflection.AST.Argument.Information as Information import Reflection.AST.Pattern as Pattern import Reflection.AST.Term as Term @@ -37,6 +38,7 @@ instance Meta-≡-isDecEquivalence = isDecEquivalence Meta._≟_ Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≟_ Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≟_ + Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≟_ ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≟_ Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≟_ Clause-≡-isDecEquivalence = isDecEquivalence Term._≟-Clause_ diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda index a9de9a2993..8757e3aef1 100644 --- a/src/Reflection/AST/Show.agda +++ b/src/Reflection/AST/Show.agda @@ -24,6 +24,7 @@ open import Relation.Nullary.Decidable.Core using (yes; no) open import Reflection.AST.Abstraction hiding (map) open import Reflection.AST.Argument hiding (map) +open import Reflection.AST.Argument.Quantity open import Reflection.AST.Argument.Relevance open import Reflection.AST.Argument.Visibility open import Reflection.AST.Argument.Modality @@ -58,6 +59,10 @@ showVisibility visible = "visible" showVisibility hidden = "hidden" showVisibility instance′ = "instance" +showQuantity : Quantity → String +showQuantity quantity-0 = "quantity-0" +showQuantity quantity-ω = "quantity-ω" + showLiteral : Literal → String showLiteral (nat x) = ℕ.show x showLiteral (word64 x) = ℕ.show (Word64.toℕ x) @@ -144,6 +149,6 @@ showDefinition (data-type pars cs) = "datatype" <+> ℕ.show pars <+> braces (intersperse ", " (map showName cs)) showDefinition (record′ c fs) = "record" <+> showName c <+> braces (intersperse ", " (map (showName ∘′ unArg) fs)) -showDefinition (constructor′ d) = "constructor" <+> showName d +showDefinition (constructor′ d q) = "constructor" <+> showName d <+> showQuantity q showDefinition axiom = "axiom" showDefinition primitive′ = "primitive" diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda index 12665df8cc..cf7cf77e11 100644 --- a/src/Relation/Binary/Reflection.agda +++ b/src/Relation/Binary/Reflection.agda @@ -10,11 +10,10 @@ open import Data.Fin.Base using (Fin) open import Data.Nat.Base using (ℕ) open import Data.Vec.Base as Vec using (Vec; allFin) -open import Function.Base using (id; _⟨_⟩_) +open import Function.Base using (id) open import Function.Bundles using (module Equivalence) open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) -import Relation.Binary.PropositionalEquality.Core as ≡ -- Think of the parameters as follows: -- @@ -33,18 +32,17 @@ import Relation.Binary.PropositionalEquality.Core as ≡ module Relation.Binary.Reflection {e a s} {Expr : ℕ → Set e} {A : Set a} - (Sem : Setoid a s) + (Sem : Setoid a s) (open Setoid Sem using (Carrier; _≈_)) (var : ∀ {n} → Fin n → Expr n) - (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Setoid.Carrier Sem) - (correct : ∀ {n} (e : Expr n) ρ → - ⟦ e ⇓⟧ ρ ⟨ Setoid._≈_ Sem ⟩ ⟦ e ⟧ ρ) + (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Carrier) + (correct : ∀ {n} (e : Expr n) ρ → ⟦ e ⇓⟧ ρ ≈ ⟦ e ⟧ ρ) where open import Data.Vec.N-ary open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) +import Relation.Binary.PropositionalEquality.Core as ≡ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open Setoid Sem open ≈-Reasoning Sem -- If two normalised expressions are semantically equal, then their @@ -54,7 +52,7 @@ prove : ∀ {n} (ρ : Vec A n) e₁ e₂ → ⟦ e₁ ⇓⟧ ρ ≈ ⟦ e₂ ⇓⟧ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ prove ρ e₁ e₂ hyp = begin - ⟦ e₁ ⟧ ρ ≈⟨ sym (correct e₁ ρ) ⟩ + ⟦ e₁ ⟧ ρ ≈⟨ correct e₁ ρ ⟨ ⟦ e₁ ⇓⟧ ρ ≈⟨ hyp ⟩ ⟦ e₂ ⇓⟧ ρ ≈⟨ correct e₂ ρ ⟩ ⟦ e₂ ⟧ ρ ∎ diff --git a/src/Tactic/RingSolver.agda b/src/Tactic/RingSolver.agda index 59475a3129..9c6cb29e8e 100644 --- a/src/Tactic/RingSolver.agda +++ b/src/Tactic/RingSolver.agda @@ -20,7 +20,6 @@ open import Data.Unit.Base using (⊤) open import Data.String.Base as String using (String; _++_; parens) open import Data.Product.Base using (_,_; proj₁) open import Function.Base -open import Relation.Nullary.Decidable open import Reflection open import Reflection.AST.Argument diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda index cc0b747037..fb33a2b9e0 100644 --- a/src/Tactic/RingSolver/NonReflective.agda +++ b/src/Tactic/RingSolver/NonReflective.agda @@ -33,9 +33,7 @@ open import Algebra.Properties.Semiring.Exp.TCOptimised semiring module Ops where zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x - zero-homo x _ with 0≟ x - zero-homo x _ | just p = p - zero-homo x () | nothing + zero-homo x _ with just p ← 0≟ x = p homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂ homo = record