[ fix #395 ] creating Data.X.Solver

CHANGELOG.md

@@ -95,6 +95,30 @@ Non-backwards compatible changes
   and exports all the old names, but may be removed in some
   future version.
 
+### Rearrangement of algebraic Solvers
+
+* Standardised and moved the generic solver modules as follows:
+  ```agda
+  Algebra.RingSolver                        ↦ Algebra.Solver.Ring
+  Algebra.Monoid-solver                     ↦ Algebra.Solver.Monoid
+  Algebra.CommutativeMonoidSolver           ↦ Algebra.Solver.CommutativeMonoidx
+  Algebra.IdempotentCommutativeMonoidSolver ↦ Algebra.Solver.IdempotentCommutativeMonoid
+  ```
+
+* In order to avoid dependency cycles, special instances of solvers for the following
+  data types have been moved from `Data.X.Properties` to new modules `Data.X.Solver`.
+  The naming conventions for these solver modules have also been standardised.
+  ```agda
+  Data.Bool.Properties.RingSolver          ↦  Data.Bool.Solver.∨-∧-Solver
+  Data.Bool.Properties.XorRingSolver       ↦  Data.Bool.Solver.xor-∧-Solver
+  Data.Integer.Properties.RingSolver       ↦  Data.Integer.Solver.+-*-Solver
+  Data.List.Properties.List-solver         ↦  Data.List.Solver.++-Solver
+  Data.Nat.Properties.SemiringSolver       ↦  Data.Nat.Solver.+-*-Solver
+  Function.Related.TypeIsomorphisms.Solver ↦ Function.Related.TypeIsomorphisms.Solver.×-⊎-Solver
+  ```
+
+* Renamed `Algebra.Solver.Ring.Natural-coefficients` to `Algebra.Solver.Ring.NaturalCoefficients`.
+
 ### Overhaul of `Data.X.Categorical`
 
 * Created `Category.Comonad`:

README.agda

@@ -125,7 +125,7 @@ import Relation.Binary.PropositionalEquality
 import Relation.Binary.PreorderReasoning
 
 -- Solver for commutative ring or semiring equalities:
-import Algebra.RingSolver
+import Algebra.Solver.Ring
 
 -- • Properties of functions, sets and relations
 

README/Integer.agda

@@ -57,11 +57,13 @@ ex₆ i j = begin
   i * j          ≡⟨ ℤₚ.*-comm i j ⟩
   j * i          ∎
 
--- The module RingSolver in Data.Integer.Properties contains a solver
+-- The module RingSolver in Data.Integer.Solver contains a solver
 -- for integer equalities involving variables, constants, _+_, _*_, -_
 -- and _-_.
 
+open import Data.Integer.Solver using (module +-*-Solver)
+open +-*-Solver
+
 ex₇ : ∀ i j → i * - j - j * i ≡ - + 2 * i * j
 ex₇ = solve 2 (λ i j → i :* :- j :- j :* i  :=  :- con (+ 2) :* i :* j)
               P.refl
-  where open ℤₚ.RingSolver

README/Nat.agda

@@ -42,11 +42,12 @@ ex₄ m n = begin
   m * n        ≡⟨ Nat.*-comm m n ⟩
   n * m        ∎
 
--- The module SemiringSolver in Data.Nat.Properties contains a solver
+-- The module SemiringSolver in Data.Nat.Solver contains a solver
 -- for natural number equalities involving variables, constants, _+_
 -- and _*_.
 
-open Nat.SemiringSolver
+open import Data.Nat.Solver using (module +-*-Solver)
+open +-*-Solver
 
 ex₅ : ∀ m n → m * (n + 0) ≡ n * m
 ex₅ = solve 2 (λ m n → m :* (n :+ con 0)  :=  n :* m) refl

src/Algebra/Properties/CommutativeMonoid.agda

@@ -9,7 +9,7 @@ open import Algebra
 module Algebra.Properties.CommutativeMonoid {g₁ g₂} (M : CommutativeMonoid g₁ g₂) where
 
 open import Algebra.Operations.CommutativeMonoid M
-open import Algebra.CommutativeMonoidSolver M
+open import Algebra.Solver.CommutativeMonoid M
 open import Relation.Binary as B using (_Preserves_⟶_)
 open import Function
 open import Function.Equality using (_⟨$⟩_)

src/Algebra/CommutativeMonoidSolver.agda → src/Algebra/Solver/CommutativeMonoid.agda

@@ -26,7 +26,7 @@ import Data.Vec.Relation.Pointwise.Inductive as Pointwise
 open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
 open import Relation.Nullary using (Dec)
 
-module Algebra.CommutativeMonoidSolver {m₁ m₂} (M : CommutativeMonoid m₁ m₂) where
+module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁ m₂) where
 
 open CommutativeMonoid M
 open EqReasoning setoid

src/Algebra/CommutativeMonoidSolver/Example.agda → src/Algebra/Solver/CommutativeMonoid/Example.agda

@@ -4,7 +4,7 @@
 -- An example of how Algebra.CommutativeMonoidSolver can be used
 ------------------------------------------------------------------------
 
-module Algebra.CommutativeMonoidSolver.Example where
+module Algebra.Solver.CommutativeMonoid.Example where
 
 open import Relation.Binary.PropositionalEquality using (_≡_)
 
@@ -14,7 +14,7 @@ open import Data.Bool.Properties using (∨-commutativeMonoid)
 open import Data.Fin using (zero; suc)
 open import Data.Vec using ([]; _∷_)
 
-open import Algebra.CommutativeMonoidSolver ∨-commutativeMonoid
+open import Algebra.Solver.CommutativeMonoid ∨-commutativeMonoid
 
 test : ∀ x y z → (x ∨ y) ∨ (x ∨ z) ≡ (z ∨ y) ∨ (x ∨ x)
 test a b c = let _∨_ = _⊕_ in

src/Algebra/IdempotentCommutativeMonoidSolver.agda → src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -26,7 +26,7 @@ import Data.Vec.Relation.Pointwise.Inductive as Pointwise
 open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
 open import Relation.Nullary using (Dec)
 
-module Algebra.IdempotentCommutativeMonoidSolver
+module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
 
 open IdempotentCommutativeMonoid M

src/Algebra/IdempotentCommutativeMonoidSolver/Example.agda → src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda

@@ -5,7 +5,7 @@
 -- used
 ------------------------------------------------------------------------
 
-module Algebra.IdempotentCommutativeMonoidSolver.Example where
+module Algebra.Solver.IdempotentCommutativeMonoid.Example where
 
 open import Relation.Binary.PropositionalEquality using (_≡_)
 
@@ -15,7 +15,7 @@ open import Data.Bool.Properties using (∨-idempotentCommutativeMonoid)
 open import Data.Fin using (zero; suc)
 open import Data.Vec using ([]; _∷_)
 
-open import Algebra.IdempotentCommutativeMonoidSolver
+open import Algebra.Solver.IdempotentCommutativeMonoid
   ∨-idempotentCommutativeMonoid
 
 test : ∀ x y z → (x ∨ y) ∨ (x ∨ z) ≡ (z ∨ y) ∨ x

src/Algebra/Monoid-solver.agda → src/Algebra/Solver/Monoid.agda

@@ -6,7 +6,7 @@
 
 open import Algebra
 
-module Algebra.Monoid-solver {m₁ m₂} (M : Monoid m₁ m₂) where
+module Algebra.Solver.Monoid {m₁ m₂} (M : Monoid m₁ m₂) where
 
 open import Data.Fin as Fin hiding (_≟_)
 import Data.Fin.Properties as Fin

src/Algebra/RingSolver.agda → src/Algebra/Solver/Ring.agda

@@ -10,19 +10,19 @@
 -- Horner normal forms are not sparse).
 
 open import Algebra
-open import Algebra.RingSolver.AlmostCommutativeRing
+open import Algebra.Solver.Ring.AlmostCommutativeRing
 
 open import Relation.Binary
 
-module Algebra.RingSolver
+module Algebra.Solver.Ring
   {r₁ r₂ r₃}
   (Coeff : RawRing r₁)               -- Coefficient "ring".
   (R : AlmostCommutativeRing r₂ r₃)  -- Main "ring".
   (morphism : Coeff -Raw-AlmostCommutative⟶ R)
   (_coeff≟_ : Decidable (Induced-equivalence morphism))
   where
 
-open import Algebra.RingSolver.Lemmas Coeff R morphism
+open import Algebra.Solver.Ring.Lemmas Coeff R morphism
 private module C = RawRing Coeff
 open AlmostCommutativeRing R
   renaming (zero to *-zero; zeroˡ to *-zeroˡ; zeroʳ to *-zeroʳ)

src/Algebra/RingSolver/AlmostCommutativeRing.agda → src/Algebra/Solver/Ring/AlmostCommutativeRing.agda

@@ -5,7 +5,7 @@
 -- commutative rings), used by the ring solver
 ------------------------------------------------------------------------
 
-module Algebra.RingSolver.AlmostCommutativeRing where
+module Algebra.Solver.Ring.AlmostCommutativeRing where
 
 open import Relation.Binary
 open import Algebra

src/Algebra/RingSolver/Lemmas.agda → src/Algebra/Solver/Ring/Lemmas.agda

@@ -7,9 +7,9 @@
 -- Note that these proofs use all "almost commutative ring" properties.
 
 open import Algebra
-open import Algebra.RingSolver.AlmostCommutativeRing
+open import Algebra.Solver.Ring.AlmostCommutativeRing
 
-module Algebra.RingSolver.Lemmas
+module Algebra.Solver.Ring.Lemmas
   {r₁ r₂ r₃}
   (coeff : RawRing r₁)
   (r : AlmostCommutativeRing r₂ r₃)

src/Algebra/RingSolver/Natural-coefficients.agda → src/Algebra/Solver/Ring/NaturalCoefficients.agda

@@ -9,15 +9,15 @@ open import Algebra
 import Algebra.Operations.Semiring as SemiringOps
 open import Relation.Nullary
 
-module Algebra.RingSolver.Natural-coefficients
+module Algebra.Solver.Ring.NaturalCoefficients
          {r₁ r₂}
          (R : CommutativeSemiring r₁ r₂)
          (dec : let open CommutativeSemiring R
                     open SemiringOps semiring in
                 ∀ m n → Dec (m × 1# ≈ n × 1#)) where
 
-import Algebra.RingSolver
-open import Algebra.RingSolver.AlmostCommutativeRing
+import Algebra.Solver.Ring
+open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Data.Nat.Base as ℕ
 open import Data.Product using (module Σ)
 open import Function
@@ -79,4 +79,4 @@ private
 
 -- The instantiation.
 
-open Algebra.RingSolver _ _ homomorphism dec′ public
+open Algebra.Solver.Ring _ _ homomorphism dec′ public

src/Algebra/RingSolver/Simple.agda → src/Algebra/Solver/Ring/Simple.agda

@@ -5,14 +5,14 @@
 -- decidable equality
 ------------------------------------------------------------------------
 
-open import Algebra.RingSolver.AlmostCommutativeRing
+open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Relation.Binary
 
-module Algebra.RingSolver.Simple
+module Algebra.Solver.Ring.Simple
          {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂)
          (_≟_ : Decidable (AlmostCommutativeRing._≈_ R))
          where
 
 open AlmostCommutativeRing R
-import Algebra.RingSolver as RS
+import Algebra.Solver.Ring as RS
 open RS rawRing R (-raw-almostCommutative⟶ R) _≟_ public

src/Data/Bool/Properties.agda

@@ -7,8 +7,6 @@
 module Data.Bool.Properties where
 
 open import Algebra
-import Algebra.RingSolver.Simple as Solver
-import Algebra.RingSolver.AlmostCommutativeRing as ACR
 open import Data.Bool
 open import Data.Empty
 open import Data.Product
@@ -382,15 +380,6 @@ push-function-into-if :
 push-function-into-if _ true  = refl
 push-function-into-if _ false = refl
 
-------------------------------------------------------------------------
--- Modules for reasoning about boolean operations
-
-module RingSolver =
-  Solver (ACR.fromCommutativeSemiring ∨-∧-commutativeSemiring) _≟_
-
-module XorRingSolver =
-  Solver (ACR.fromCommutativeRing xor-∧-commutativeRing) _≟_
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Data/Bool/Solver.agda

@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over booleans
+------------------------------------------------------------------------
+
+-- See README.Nat for examples of how to use similar solvers
+
+module Data.Bool.Solver where
+
+import Algebra.Solver.Ring.Simple as Solver
+import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
+open import Data.Bool using (_≟_)
+open import Data.Bool.Properties
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equivalences
+-- containing _∨_ and _∧_
+
+module ∨-∧-Solver =
+  Solver (ACR.fromCommutativeSemiring ∨-∧-commutativeSemiring) _≟_
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equivalences
+-- containing _xor_ and _∧_
+
+module xor-∧-Solver =
+  Solver (ACR.fromCommutativeRing xor-∧-commutativeRing) _≟_

src/Data/BoundedVec.agda

@@ -13,8 +13,8 @@ open import Data.List.Base as List using (List)
 open import Data.Vec as Vec using (Vec)
 import Data.BoundedVec.Inefficient as Ineff
 open import Relation.Binary.PropositionalEquality
-open import Data.Nat.Properties
-open SemiringSolver
+open import Data.Nat.Solver
+open +-*-Solver
 
 ------------------------------------------------------------------------
 -- The type

src/Data/Digit.agda

@@ -8,7 +8,7 @@ module Data.Digit where
 
 open import Data.Nat using (ℕ; zero; suc; pred; _+_; _*_; _≤?_; _≤′_)
 open import Data.Nat.Properties
-open SemiringSolver
+open import Data.Nat.Solver
 open import Data.Fin as Fin using (Fin; zero; suc; toℕ)
 open import Data.Char using (Char)
 open import Data.List.Base
@@ -22,6 +22,8 @@ open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
 open import Function
 
+open +-*-Solver
+
 ------------------------------------------------------------------------
 -- Digits
 

src/Data/Integer/Properties.agda

@@ -9,15 +9,14 @@ module Data.Integer.Properties where
 open import Algebra
 import Algebra.Morphism as Morphism
 import Algebra.Properties.AbelianGroup
-import Algebra.RingSolver.Simple as Solver
-import Algebra.RingSolver.AlmostCommutativeRing as ACR
 open import Data.Integer renaming (suc to sucℤ)
 open import Data.Nat
   using (ℕ; suc; zero; _∸_; s≤s; z≤n; ≤-pred)
   hiding (module ℕ)
   renaming (_+_ to _ℕ+_; _*_ to _ℕ*_;
     _<_ to _ℕ<_; _≥_ to _ℕ≥_; _≰_ to _ℕ≰_; _≤?_ to _ℕ≤?_)
 import Data.Nat.Properties as ℕₚ
+open import Data.Nat.Solver
 open import Data.Product using (proj₁; proj₂; _,_)
 open import Data.Sum using (inj₁; inj₂)
 open import Data.Sign as Sign using () renaming (_*_ to _𝕊*_)
@@ -33,8 +32,8 @@ open import Algebra.FunctionProperties (_≡_ {A = ℤ})
 open import Algebra.FunctionProperties.Consequences (setoid ℤ)
 open import Algebra.Structures (_≡_ {A = ℤ})
 open Morphism.Definitions ℤ ℕ _≡_
-open ℕₚ.SemiringSolver
 open ≡-Reasoning
+open +-*-Solver
 
 ------------------------------------------------------------------------
 -- Equality
@@ -420,7 +419,6 @@ private
                     := c :+ b :* (con 1 :+ c) :+
                        a :* (con 1 :+ (c :+ b :* (con 1 :+ c))))
             refl
-    where open ℕₚ.SemiringSolver
 
 *-assoc : Associative _*_
 *-assoc (+ zero) _ _ = refl
@@ -860,10 +858,6 @@ n≮n { -[1+ suc n ]} (-≤- n<n) =  contradiction n<n ℕₚ.1+n≰n
 ------------------------------------------------------------------------
 -- Modules for reasoning about integer number relations
 
--- A module for automatically solving propositional equivalences
-module RingSolver =
-  Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≟_
-
 -- A module for reasoning about the _≤_ relation
 module ≤-Reasoning = POR ≤-poset hiding (_≈⟨_⟩_)
 

src/Data/Integer/Solver.agda

@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over integers
+------------------------------------------------------------------------
+
+-- See README.Integer for examples of how to use this solver
+
+module Data.Integer.Solver where
+
+import Algebra.Solver.Ring.Simple as Solver
+import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
+open import Data.Integer using (_≟_)
+open import Data.Integer.Properties using (+-*-commutativeRing)
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equivalences
+-- containing _+_ and _*_
+
+-- A module for automatically solving propositional equivalences
+module +-*-Solver =
+  Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≟_