Make the RingSolver work with generic rings (#1116)

src/Data/Integer/Tactic/RingSolver.agda

@@ -4,7 +4,7 @@
 -- Automatic solvers for equations over integers
 ------------------------------------------------------------------------
 
--- See README.Integer for examples of how to use this solver
+-- See README.Data.Integer for examples of how to use this solver
 
 {-# OPTIONS --without-K --safe #-}
 

src/Reflection/AST/DeBruijn.agda

@@ -10,7 +10,9 @@ module Reflection.AST.DeBruijn where
 
 open import Data.Bool.Base using (Bool; true; false; _∨_; if_then_else_)
 open import Data.Nat.Base as Nat using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_)
-open import Data.List.Base using (List; []; _∷_; _++_)
+open import Data.List.Base using (List; []; _∷_; _++_; foldr; reverse; map)
+open import Data.Product using (_×_; _,_)
+open import Data.String as String using (String)
 open import Data.Maybe.Base using (Maybe; nothing; just)
 import Data.Maybe.Effectful as Maybe
 import Function.Identity.Effectful as Identity
@@ -53,6 +55,16 @@ module _ where
   weakenClauses : (by : ℕ) → Clauses → Clauses
   weakenClauses = weakenFrom′ traverseClauses 0
 
+-- Apply Weakening to substitute under lambdas
+
+prependLams : List (String × Visibility) → Term → Term
+prependLams xs t = foldr (λ (s , v) t → lam v (abs s t)) t (reverse xs)
+
+prependHLams : List String → Term → Term
+prependHLams vs = prependLams (map (_, hidden) vs)
+
+prependVLams : List String → Term → Term
+prependVLams vs = prependLams (map (_, visible) vs)
 
 ------------------------------------------------------------------------
 -- η-expansion

src/Reflection/AST/Term.agda

@@ -96,15 +96,6 @@ stripPis : Term → List (String × Arg Type) × Term
 stripPis (Π[ s ∶ t ] x) = map₁ ((s , t) ∷_) (stripPis x)
 stripPis x              = [] , x
 
-prependLams : List (String × Visibility) → Term → Term
-prependLams xs t = foldr (λ {(s , v) t → lam v (abs s t)}) t (reverse xs)
-
-prependHLams : List String → Term → Term
-prependHLams vs = prependLams (List.map (_, hidden) vs)
-
-prependVLams : List String → Term → Term
-prependVLams vs = prependLams (List.map (_, visible) vs)
-
 ------------------------------------------------------------------------
 -- Decidable equality
 

src/Tactic/RingSolver.agda

@@ -27,6 +27,7 @@ open import Reflection.AST.Argument
 open import Reflection.AST.Term as Term
 open import Reflection.AST.AlphaEquality
 open import Reflection.AST.Name as Name
+open import Reflection.AST.DeBruijn using (prependVLams; prependHLams)
 open import Reflection.TCM.Syntax
 open import Data.Nat.Reflection
 open import Data.List.Reflection

src/Tactic/RingSolver/Examples.agda

@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some simple use cases of the ring solver
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Tactic.RingSolver.Examples where
+
+open import Algebra
+
+open import Data.Integer.Base using (ℤ)
+open import Data.Integer.Properties
+open import Data.Maybe
+
+open import Agda.Builtin.Equality using (_≡_ ; refl)
+
+open import Tactic.RingSolver
+open import Tactic.RingSolver.Core.AlmostCommutativeRing
+
+
+module IntegerExamples where
+  ℤAsCRing : CommutativeRing _ _
+  ℤAsCRing = record
+               { Carrier = ℤ
+               ; isCommutativeRing = +-*-isCommutativeRing
+               }
+
+  ℤAsAlmostCRing : _
+  ℤAsAlmostCRing = fromCommutativeRing ℤAsCRing (λ _ → nothing)
+  open AlmostCommutativeRing ℤAsAlmostCRing
+
+  works : ∀ x y → x + y ≡ y + x
+  works = solve-∀ ℤAsAlmostCRing
+
+  {-
+  nope : ∀ x y → (x + y) * (x - y) ≡ (x * x) - (y * y)
+  nope = solve-∀ ℤAsAlmostCRing
+  -}
+
+module GenericExamples {r s} (R : CommutativeRing r s) where
+  RAsAlmostCRing = fromCommutativeRing R (λ _ → nothing)
+  open AlmostCommutativeRing RAsAlmostCRing
+
+  works : ∀ x y → x + y ≈ y + x
+  works = solve-∀ RAsAlmostCRing
+
+  {-
+  nope : ∀ x y → (x + y) * (x - y) ≡ (x * x) - (y * y)
+  nope = solve-∀ RAsAlmostCRing
+  -}
+
+module SolverCanOnlyUseNames {r s} (R : CommutativeRing r s) where
+  RAsAlmostCRing = fromCommutativeRing R (λ _ → nothing)
+  open AlmostCommutativeRing RAsAlmostCRing
+
+  {-
+  nope : ∀ x y → x + y ≈ y + x
+  nope = solve-∀ (fromCommutativeRing R (λ _ → nothing))
+  -}
+
+  {-
+    to make this work, one has to lift deBruijn indices in the expression defining the ring
+  -}