WIP Add Rational RingSolver

CHANGELOG.md

@@ -2050,6 +2050,12 @@ New modules
   Data.Rational.Unnormalised.Show
   ```
 
+* Added RingSolver for Data.Rational (issue #1879):
+  ```
+  Data.Rational.Tactic.RingSolver
+  Data.Rational.Unnormalised.Tactic.RingSolver
+  ```
+
 * Membership relations for maps and sets
   ```
   Data.Tree.AVL.Map.Membership.Propositional

doc/README/Data/Rational.agda

@@ -0,0 +1,52 @@
+------------------------------------------------------------------------
+-- 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
+
+-- The rational numbers and various arithmetic operations are defined in
+-- Data.Rational.
+
+open import Data.Integer using (+_)
+open import Data.Rational
+open import Data.Rational.Properties
+
+1/4 : ℚ
+1/4 = + 1 / 4
+
+3/4 : ℚ
+3/4 = + 3 / 4
+
+-- Some binary operators are also defined, including addition,
+-- subtraction and multiplication.
+
+expr : ℚ
+expr = (1/4 + ½) * 1ℚ - 0ℚ
+
+-- We can use PropositionalEquality with rational numbers
+
+open import Relation.Binary.PropositionalEquality -- using (_≡_; refl)
+
+eqEx : expr ≡ 3/4
+eqEx = refl
+
+-- or use equality defined for rational numbers
+
+eqEx' : expr ≃ 3/4
+eqEx' = *≡* refl
+
+-- we can automaticaly prove equations using RingSolver
+
+open import Data.Rational.Tactic.RingSolver
+
+lemma : ∀ (x y : ℚ) → x + y + 1/4 + ½ ≃ 3/4 + y + x
+{-
+Malformed call to solve.Expected target type to be like: ∀ x y → x + y ≈ y + x.Instead: _19
+when checking that the expression unquote solve-∀ has type _19
+-}
+lemma = {! solve-∀  !}

doc/README/Data/Rational/Unnormalised.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some examples showing where the unnormalised rational numbers and some
+-- related operations and properties are defined, and how they can be used
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module README.Data.Rational.Unnormalised where
+
+-- The rational numbers and various arithmetic operations are defined in
+-- Data.Rational.
+
+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
+
+-- Some binary operators are also defined, including addition,
+-- subtraction and multiplication.
+
+expr : ℚᵘ
+expr = (1/4 + ½) * 1ℚᵘ - 0ℚᵘ
+
+-- We can use defined for rational numbers
+
+expr2 : expr ≃ 3/4
+expr2 = *≡* refl
+
+-- We can automatically proove equations using Ring
+
+open import Data.Rational.Unnormalised.Tactic.RingSolver
+
+lemma₁ : ∀ (x y : ℚᵘ) → (x + y) ≡ (y + x) -- TODO should we use ≃
+{-
+TODO fails with:
+Malformed call to solve.Expected target type to be like: ∀ x y → x + y ≈ y + x.Instead: _25
+when checking that the expression unquote solve-∀ has type _25
+-}
+lemma₁ = {! solve-∀  !}

src/Data/Rational/Tactic/RingSolver.agda

@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over rationals
+------------------------------------------------------------------------
+
+-- See README.Integer 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 Agda.Builtin.Int using (Int; negsuc; pos)
+open import Data.Nat.Base using (zero; suc)
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.Rational.Base using (ℚ; 0ℚ; mkℚ)
+open import Data.Rational.Properties using (+-*-commutativeRing)
+open import Level using (0ℓ)
+open import Data.Unit using (⊤)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+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 f
+  where
+   f : (x : ℚ) → Maybe (0ℚ ≡ x)
+   f (mkℚ (pos 0)       0       _) = just refl
+   f (mkℚ (pos 0)       (suc _) _) = nothing
+   f (mkℚ (pos (suc _)) _       _) = nothing
+   f (mkℚ (negsuc _)    _       _) = nothing
+
+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/Tactic/RingSolver.agda

@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over unnormalised rationals
+------------------------------------------------------------------------
+
+-- See README.Integer for examples of how to use this solver
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Rational.Unnormalised.Tactic.RingSolver where
+
+open import Agda.Builtin.Reflection
+
+open import Agda.Builtin.Int using (Int; negsuc; pos)
+open import Data.Nat.Base using (zero; suc)
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.Rational.Unnormalised.Base using (ℚᵘ; 0ℚᵘ; _≃_; mkℚᵘ; *≡*)
+open import Data.Rational.Unnormalised.Properties using (+-*-commutativeRing)
+open import Level using (0ℓ)
+open import Data.Unit using (⊤)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+import Tactic.RingSolver as Solver
+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 f
+  where
+   f : (x : ℚᵘ) → Maybe (0ℚᵘ ≃ x)
+   f (mkℚᵘ (pos zero)    _) = just (*≡* refl)
+   f (mkℚᵘ (pos (suc _)) _) = nothing
+   f (mkℚᵘ (negsuc _)    _) = nothing
+
+macro
+  solve-∀ : Term → TC ⊤
+  solve-∀ = Solver.solve-∀-macro (quote ring)
+
+macro
+  solve : Term → Term → TC ⊤
+  solve n = Solver.solve-macro n (quote ring)