Add solvers for rationals (#1394)

Co-authored-by: MatthewDaggitt <[email protected]>

Author: uzytkownik

CHANGELOG.md

@@ -291,6 +291,12 @@ New modules
   Algebra.Morphism.LatticeMonomorphism
   ```
 
+* Solvers for rationals
+  ```
+  Data.Rational.Solver
+  Data.Rational.Unnormalised.Solver
+  ```
+
 * New ternary relation on lists:
   ```
   Data.List.Relation.Ternary.Appending

src/Data/Rational/Solver.agda

@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over rationals
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Rational.Solver where
+
+import Algebra.Solver.Ring.Simple as Solver
+import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
+open import Data.Rational.Properties using (_≟_; +-*-commutativeRing)
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equivalences
+-- containing _+_ and _*_
+
+module +-*-Solver =
+  Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≟_

src/Data/Rational/Unnormalised/Solver.agda

@@ -0,0 +1,21 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over rationals
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Rational.Unnormalised.Solver where
+
+import Algebra.Solver.Ring.Simple as Solver
+import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
+open import Data.Rational.Unnormalised.Properties using (_≃?_; +-*-commutativeRing)
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equivalences
+-- containing _+_ and _*_
+
+module +-*-Solver =
+  Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≃?_
+