Add tactic-style ring solvers for rational and unnormalised rational numbers

CHANGELOG.md

@@ -129,6 +129,10 @@ Deprecated names
 New modules
 -----------
 
+* Added tactic ring solvers for rational numbers (issue #1879):
+  `Data.Rational.Tactic.RingSolver`,
+  `Data.Rational.Unnormalised.Tactic.RingSolver`.
+
 * `Algebra.Construct.Sub.Group` for the definition of subgroups.
 
 * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.

doc/README/Data/Rational.agda

@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some examples showing where the rational numbers and some related
+-- operations and properties are defined, and how they can be used
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module README.Data.Rational where
+
+open import Data.Integer using (+_)
+open import Data.Rational
+open import Data.Rational.Properties
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+1/4 : ℚ
+1/4 = + 1 / 4
+
+3/4 : ℚ
+3/4 = + 3 / 4
+
+expr : ℚ
+expr = (1/4 + ½) * 1ℚ - 0ℚ
+
+eqEx : expr ≡ 3/4
+eqEx = refl
+
+open import Data.Rational.Tactic.RingSolver
+
+lemma : ∀ (x y : ℚ) → x + y + 1/4 + ½ ≡ 3/4 + y + x
+lemma = solve-∀

doc/README/Data/Rational/Unnormalised.agda

@@ -0,0 +1,26 @@
+module README.Data.Rational.Unnormalised where
+
+open import Data.Integer using (+_)
+open import Data.Rational.Unnormalised
+open import Data.Rational.Unnormalised.Properties
+open import Relation.Binary.PropositionalEquality using (refl)
+
+1/4 : ℚᵘ
+1/4 = + 1 / 4
+
+3/4 : ℚᵘ
+3/4 = + 3 / 4
+
+6/8 : ℚᵘ
+6/8 = + 6 / 8
+
+expr : ℚᵘ
+expr = (1/4 + ½) * 1ℚᵘ - 0ℚᵘ
+
+eqEx : expr ≃ 3/4
+eqEx = *≡* refl
+
+open import Data.Rational.Unnormalised.Tactic.RingSolver
+
+lemma₁ : ∀ (x y : ℚᵘ) → x + y + 1/4 + ½ ≃ 6/8 + y + x
+lemma₁ = solve-∀

src/Data/Rational/Properties.agda

@@ -27,6 +27,7 @@ import Algebra.Lattice.Morphism.LatticeMonomorphism as LatticeMonomorphisms
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
 import Algebra.Properties.Group as GroupProperties
 open import Data.Bool.Base using (T; true; false)
+open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; +[1+_]; +0; 0ℤ; 1ℤ; _◃_)
 open import Data.Integer.Coprimality using (coprime-divisor)
 import Data.Integer.Properties as ℤ
@@ -190,6 +191,11 @@ drop-*≡* (*≡* eq) = eq
 p≡0⇒↥p≡0 : ∀ p → p ≡ 0ℚ → ↥ p ≡ 0ℤ
 p≡0⇒↥p≡0 p refl = refl
 
+0≡?-weak : (p : ℚ) → Maybe (0ℚ ≡ p)
+0≡?-weak p with ↥ p ℤ.≟ 0ℤ
+... | yes ↥p≡0 = just (sym (↥p≡0⇒p≡0 p ↥p≡0))
+... | no  _    = nothing
+
 ↥p≡↥q≡0⇒p≡q : ∀ p q → ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≡ q
 ↥p≡↥q≡0⇒p≡q p q ↥p≡0 ↥q≡0 = trans (↥p≡0⇒p≡0 p ↥p≡0) (sym (↥p≡0⇒p≡0 q ↥q≡0))
 

src/Data/Rational/Tactic/RingSolver.agda

@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over rationals
+------------------------------------------------------------------------
+
+-- See README.Tactic.RingSolver for examples of how to use this solver
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Rational.Tactic.RingSolver where
+
+open import Agda.Builtin.Reflection using (Term; TC)
+open import Data.Rational.Properties using (+-*-commutativeRing; 0≡?-weak)
+open import Level using (0ℓ)
+open import Data.Unit.Base using (⊤)
+
+import Tactic.RingSolver as Solver using (solve-macro; solve-∀-macro)
+import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equalities
+-- containing _+_ and _*_
+
+ring : ACR.AlmostCommutativeRing 0ℓ 0ℓ
+ring = ACR.fromCommutativeRing
+  +-*-commutativeRing
+  0≡?-weak
+
+macro
+  solve-∀ : Term → TC ⊤
+  solve-∀ = Solver.solve-∀-macro (quote ring)
+
+macro
+  solve : Term → Term → TC ⊤
+  solve n = Solver.solve-macro n (quote ring)

src/Data/Rational/Unnormalised/Properties.agda

@@ -28,6 +28,7 @@ open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 open import Data.Bool.Base using (T; true; false)
+open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Nat.Base as ℕ using (suc; pred)
 import Data.Nat.Properties as ℕ
   using (≤-refl; +-comm; +-identityʳ; +-assoc
@@ -185,6 +186,10 @@ p≃0⇒↥p≡0 p (*≡* eq) = begin
 ↥p≡↥q≡0⇒p≃q : ∀ p q → ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≃ q
 ↥p≡↥q≡0⇒p≃q p q ↥p≡0 ↥q≡0 = ≃-trans (↥p≡0⇒p≃0 p ↥p≡0) (≃-sym (↥p≡0⇒p≃0 _ ↥q≡0))
 
+0≃?-weak : (p : ℚᵘ) → Maybe (0ℚᵘ ≃ p)
+0≃?-weak p with ↥ p ℤ.≟ 0ℤ
+... | yes ↥p≡0 = just (≃-sym (↥p≡0⇒p≃0 p ↥p≡0))
+... | no  _    = nothing
 
 ------------------------------------------------------------------------
 -- Properties of -_

src/Data/Rational/Unnormalised/Tactic/RingSolver.agda

@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over unnormalised rationals
+------------------------------------------------------------------------
+
+-- See README.Tactic.RingSolver for examples of how to use this solver
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Rational.Unnormalised.Tactic.RingSolver where
+
+open import Agda.Builtin.Reflection using (Term; TC)
+open import Data.Rational.Unnormalised.Properties using (+-*-commutativeRing; 0≃?-weak)
+open import Level using (0ℓ)
+open import Data.Unit.Base using (⊤)
+
+import Tactic.RingSolver as Solver using (solve-∀-macro; solve-macro)
+import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equivalences
+-- containing _+_ and _*_
+
+ring : ACR.AlmostCommutativeRing 0ℓ 0ℓ
+ring = ACR.fromCommutativeRing
+  +-*-commutativeRing
+  0≃?-weak
+
+macro
+  solve-∀ : Term → TC ⊤
+  solve-∀ = Solver.solve-∀-macro (quote ring)
+
+macro
+  solve : Term → Term → TC ⊤
+  solve n = Solver.solve-macro n (quote ring)