Refactor and improve CommRingSolver (#1093)

* split reflection code of CommRingSolver, introduce detection of equal terms

* use new macro

* rename main import file for CommRingSolver

* fix

* cleanup/simplify

* fix

* collect variables in CommRingSolver, while walking through ring exprs

* fix, cleanup CommRingSolver

* Experiment

* properly handle unexpected input

* credit the 1lab

* adapt also NatSolver

* fix

* wait-for-type, simplify

* more simplification, new test for the solver

* mention a limitation

* simplify

Cubical/Algebra/CommAlgebra/Instances/Unit.agda

@@ -12,7 +12,7 @@ open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommAlgebra.Base
 open import Cubical.Algebra.CommRing.Instances.Unit
 open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom)
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 private
   variable
@@ -49,16 +49,11 @@ module _ (R : CommRing ℓ) where
 
       1≡0→isContr : isContr ⟨ A ⟩
       1≡0→isContr = 0a , λ a →
-        0a      ≡⟨ step1 a ⟩
+        0a      ≡⟨ solve! S ⟩
         a · 0a  ≡⟨ cong (λ b → a · b) (sym 1≡0) ⟩
-        a · 1a  ≡⟨ step2 a ⟩
+        a · 1a  ≡⟨ solve! S ⟩
         a       ∎
           where S = CommAlgebra→CommRing A
-                open CommRingStr (snd S) renaming (_·_ to _·s_)
-                step1 : (x : ⟨ A ⟩) → 0r ≡ x ·s 0r
-                step1 = solve S
-                step2 : (x : ⟨ A ⟩) → x ·s 1r ≡ x
-                step2 = solve S
 
       equivFrom1≡0 : CommAlgebraEquiv A UnitCommAlgebra
       equivFrom1≡0 = isContr→Equiv 1≡0→isContr isContrUnit*  ,

Cubical/Algebra/CommAlgebra/Localisation.agda

@@ -31,7 +31,7 @@ open import Cubical.Algebra.Algebra
 open import Cubical.Algebra.CommAlgebra.Base
 open import Cubical.Algebra.CommAlgebra.Properties
 
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 open import Cubical.HITs.SetQuotients as SQ
 open import Cubical.HITs.PropositionalTruncation as PT
@@ -308,10 +308,7 @@ module DoubleAlgLoc (R : CommRing ℓ) (f g : (fst R)) where
      helper2 : (α : FinVec (fst R) 1)
              → x ^ n ≡ linearCombination R α (replicateFinVec 1 y)
              → x ∈ᵢ √ ⟨ y · x ⟩
-     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ useSolver x y (α zero) ∣₁ ∣₁
-      where
-      useSolver : ∀ x y a → x · (a · y + 0r) ≡ a · (y · x) + 0r
-      useSolver = solve R
+     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ solve! R ∣₁ ∣₁
 
   toUnit2 : ∀ s → s ∈ [_ⁿ|n≥0] R g → s ⋆ 1a ∈ R[1/fg]ˣ
   toUnit2 s s∈[gⁿ|n≥0] = subst-∈ R[1/fg]ˣ (sym (·IdR (s /1ᶠᵍ)))

Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda

@@ -28,8 +28,6 @@ open import Cubical.Algebra.CommRing as CommRing hiding (_ˣ;module Units)
 open import Cubical.Algebra.CommRing.Localisation using (isMultClosedSubset)
 open import Cubical.Algebra.Ring
 
-open import Cubical.Tactics.CommRingSolver.Reflection
-
 module Cubical.Algebra.CommAlgebra.LocalisationAlgebra
   {ℓR : Level}
   (R : CommRing ℓR)

Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda

@@ -22,7 +22,7 @@ open import Cubical.Algebra.CommAlgebra.Instances.Unit
 open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom; isPropIsAlgebraHom)
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Ideal using (isIdeal)
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 open import Cubical.Algebra.Algebra.Properties
 open AlgebraHoms using (_∘a_)
 
@@ -242,8 +242,6 @@ module _
     unfolding quotientHom
 
     isZeroFromIdeal : (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
-    isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (step x) x∈I )
+    isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (solve! (CommAlgebra→CommRing A)) x∈I )
       where
         open CommAlgebraStr (snd A)
-        step : (x : ⟨ A ⟩) → x ≡ x - 0a
-        step = solve (CommAlgebra→CommRing A)

Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda

@@ -17,7 +17,7 @@ open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList
 open import Cubical.Algebra.Polynomials.UnivariateList.Base
 open import Cubical.Algebra.Polynomials.UnivariateList.Properties
 
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 private variable
   ℓ ℓ' : Level
@@ -217,7 +217,7 @@ module _ (R : CommRing ℓ) where
             (is-set _ _)
           where
             useSolver : (r : ⟨ R ⟩) → r ≡ (r · 1r) + 0r
-            useSolver = solve R
+            useSolver r = solve! R
 
 
     {- Reforumlation in terms of the R-AlgebraHom from R[X] to A -}

Cubical/Algebra/CommRing/BinomialThm.agda

@@ -15,7 +15,7 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Algebra.Monoid.BigOp
 open import Cubical.Algebra.Ring.BigOps
 open import Cubical.Algebra.CommRing
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 private
   variable
@@ -51,7 +51,7 @@ module BinomialThm (R' : CommRing ℓ) where
  BinomialVec n x y i = (n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)
 
  BinomialThm : ∀ (n : ℕ) (x y : R) → (x + y) ^ n ≡ ∑ (BinomialVec n x y)
- BinomialThm zero x y = solve R'
+ BinomialThm zero x y = solve! R'
  BinomialThm (suc n) x y =
      (x + y) ^ suc n
   ≡⟨ refl ⟩
@@ -70,7 +70,7 @@ module BinomialThm (R' : CommRing ℓ) where
      ∑ xVec + ∑ yVec
   ≡⟨ cong (_+ ∑ yVec) (∑Last xVec) ⟩
      ∑ (xVec ∘ weakenFin) + xⁿ⁺¹ + (yⁿ⁺¹ + ∑ (yVec ∘ suc))
-  ≡⟨ solve3 _ _ _ _ ⟩
+  ≡⟨  solve3 _ _ _ _ ⟩
      yⁿ⁺¹  + (∑ (xVec ∘ weakenFin) + ∑ (yVec ∘ suc)) + xⁿ⁺¹
   ≡⟨ cong (λ s → yⁿ⁺¹  + s + xⁿ⁺¹) (sym (∑Split _ _))  ⟩
      yⁿ⁺¹  + (∑ middleVec) + xⁿ⁺¹
@@ -85,20 +85,14 @@ module BinomialThm (R' : CommRing ℓ) where
   xVec : FinVec R (suc n)
   xVec i = (n choose (toℕ i)) · x ^ (suc (toℕ i)) · y ^ (n ∸ toℕ i)
 
-  solve1 : ∀ x nci xⁱ yⁿ⁻ⁱ → x · (nci · xⁱ · yⁿ⁻ⁱ) ≡ nci · (x · xⁱ) · yⁿ⁻ⁱ
-  solve1 = solve R'
-
   xVecPath : ∀ (i : Fin (suc n)) → x · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ xVec i
-  xVecPath i = solve1 _ _ _ _
+  xVecPath i = solve! R'
 
   yVec : FinVec R (suc n)
   yVec i = (n choose (toℕ i)) · x ^ (toℕ i) · y ^ (suc (n ∸ toℕ i))
 
-  solve2 : ∀ y nci xⁱ yⁿ⁻ⁱ → y · (nci · xⁱ · yⁿ⁻ⁱ) ≡ nci · xⁱ · (y · yⁿ⁻ⁱ)
-  solve2 = solve R'
-
   yVecPath : ∀ (i : Fin (suc n)) → y · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ yVec i
-  yVecPath i = solve2 _ _ _ _
+  yVecPath i = solve! R'
 
   xⁿ⁺¹ : R
   xⁿ⁺¹ = xVec (fromℕ n)
@@ -111,7 +105,7 @@ module BinomialThm (R' : CommRing ℓ) where
                   (sym (subst (λ m → (n choose suc m) ≡ 0r) (sym (toFromId n)) (nChooseN+1 n))))
 
   solve3 : ∀ sx sy xⁿ⁺¹ yⁿ⁺¹ → sx + xⁿ⁺¹ + (yⁿ⁺¹ + sy) ≡ yⁿ⁺¹ + (sx + sy) + xⁿ⁺¹
-  solve3 = solve R'
+  solve3 sx sy xⁿ⁺¹ yⁿ⁺¹ = solve! R'
 
   middleVec : FinVec R n
   middleVec i = xVec (weakenFin i) + yVec (suc i)
@@ -122,11 +116,8 @@ module BinomialThm (R' : CommRing ℓ) where
    + (n choose suc (weakenRespToℕ i j)) · (x · x ^ (weakenRespToℕ i j)) · sym yHelper j
    ≡ ((n choose suc (toℕ (weakenFin i))) + (n choose toℕ (weakenFin i)))
    · (x · x ^ toℕ (weakenFin i)) · y ^ (n ∸ toℕ (weakenFin i)))
-   (solve4 _ _ _ _)
+   (solve! R')
    where
    yHelper : (y · y ^ (n ∸ suc (toℕ i))) ≡ y ^ (n ∸ toℕ (weakenFin i))
    yHelper = cong (λ m → y · y ^ (n ∸ suc m)) (sym (weakenRespToℕ i))
            ∙ cong (y ^_) (≤-∸-suc (subst (λ m → suc m ≤ n) (sym (weakenRespToℕ _)) (toℕ<n i)))
-
-   solve4 : ∀ nci ncsi xxⁱ yⁿ⁻ⁱ → nci · xxⁱ · yⁿ⁻ⁱ + ncsi · xxⁱ · yⁿ⁻ⁱ ≡ (ncsi + nci) · xxⁱ · yⁿ⁻ⁱ
-   solve4 = solve R'

Cubical/Algebra/CommRing/FGIdeal.agda

@@ -35,7 +35,7 @@ open import Cubical.Algebra.Ring.Quotient
 open import Cubical.Algebra.Ring.Properties
 open import Cubical.Algebra.Ring.BigOps
 open import Cubical.Algebra.Matrix
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 private
   variable
@@ -225,7 +225,7 @@ module _ (R' : CommRing ℓ) where
  sucIncl U x = PT.map λ (α , x≡∑αUsuc) → (λ { zero → 0r ; (suc i) → α i }) , x≡∑αUsuc ∙ path _ _
   where
   path : ∀ s u₀ → s ≡ 0r · u₀ + s
-  path = solve R'
+  path _ _ = solve! R'
 
  emptyFGIdeal : ∀ (V : FinVec R 0) → ⟨ V ⟩ ≡ 0Ideal
  emptyFGIdeal V = CommIdeal≡Char (λ _ →  PT.rec (is-set _ _) snd)

Cubical/Algebra/CommRing/Ideal/Base.agda

@@ -28,7 +28,7 @@ open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Ideal renaming (IdealsIn to IdealsInRing)
 open import Cubical.Algebra.Ring.BigOps
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 private
   variable
@@ -82,9 +82,7 @@ module CommIdeal (R' : CommRing ℓ) where
 
  -Closed : (I : CommIdeal) (x : R)
          → x ∈ I → (- x) ∈ I
- -Closed I x x∈I = subst (_∈ I) (useSolver x) (·Closed (snd I) (- 1r) x∈I)
-   where useSolver : (x : R) → - 1r · x ≡ - x
-         useSolver = solve R'
+ -Closed I x x∈I = subst (_∈ I) (solve! R') (·Closed (snd I) (- 1r) x∈I)
 
  ∑Closed : (I : CommIdeal) {n : ℕ} (V : FinVec R n)
          → (∀ i → V i ∈ I) → ∑ V ∈ I
@@ -129,10 +127,8 @@ module _ {R : CommRing ℓ} where
   CommIdeal→Ideal : IdealsIn R → IdealsInRing (CommRing→Ring R)
   fst (CommIdeal→Ideal I) = fst I
   +-closed (snd (CommIdeal→Ideal I)) = +Closed (snd I)
-  -closed (snd (CommIdeal→Ideal I)) =  λ x∈pI → subst-∈p (fst I) (useSolver _)
+  -closed (snd (CommIdeal→Ideal I)) =  λ x∈pI → subst-∈p (fst I) (solve! R)
                                                            (·Closed (snd I) (- 1r) x∈pI)
-                                         where useSolver : (x : fst R) → - 1r · x ≡ - x
-                                               useSolver = solve R
   0r-closed (snd (CommIdeal→Ideal I)) = contains0 (snd I)
   ·-closedLeft (snd (CommIdeal→Ideal I)) = ·Closed (snd I)
   ·-closedRight (snd (CommIdeal→Ideal I)) = λ r x∈pI →

Cubical/Algebra/CommRing/Ideal/Sum.agda

@@ -24,7 +24,7 @@ open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Ideal renaming (IdealsIn to IdealsInRing)
 open import Cubical.Algebra.Ring.BigOps
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
 
 open import Cubical.Algebra.CommRing.Ideal
 
@@ -160,10 +160,7 @@ module IdealSum (R' : CommRing ℓ) where
  ·iComm I J = CommIdeal≡Char (·iComm⊆ I J) (·iComm⊆ J I)
 
  I⊆I1 : ∀ (I : CommIdeal) → I ⊆ (I ·i 1Ideal)
- I⊆I1 I x x∈I = ∣ 1 , ((λ _ → x) , λ _ → 1r) , (λ _ → x∈I) , (λ _ → lift tt) , useSolver x ∣₁
-  where
-  useSolver : ∀ x → x ≡ x · 1r + 0r
-  useSolver = solve R'
+ I⊆I1 I x x∈I = ∣ 1 , ((λ _ → x) , λ _ → 1r) , (λ _ → x∈I) , (λ _ → lift tt) , solve! R' ∣₁
 
  ·iRid : ∀ (I : CommIdeal) → I ·i 1Ideal ≡ I
  ·iRid I = CommIdeal≡Char (·iLincl I 1Ideal) (I⊆I1 I)

Cubical/Algebra/CommRing/LocalRing.agda

@@ -38,7 +38,7 @@ open import Cubical.Algebra.CommRing.FGIdeal using (generatedIdeal; linearCombin
 open import Cubical.Algebra.CommRing.Ideal using (module CommIdeal)
 open import Cubical.Algebra.Ring.BigOps using (module Sum)
 
-open import Cubical.Tactics.CommRingSolver.Reflection using (solve)
+open import Cubical.Tactics.CommRingSolver
 
 
 private
@@ -75,13 +75,13 @@ module _ (R : CommRing ℓ) where
       x + y ∈ R ˣ →
       ∥ (x ∈ R ˣ) ⊎  (y ∈ R ˣ) ∥₁
     invertibleInBinarySum {x = x} {y = y} x+yInv =
-      ∥_∥₁.map Σ→⊎ (local {n = 2} xy (subst (_∈ R ˣ) (∑xy≡x+y x y) x+yInv))
+      ∥_∥₁.map Σ→⊎ (local {n = 2} xy (subst (_∈ R ˣ) ∑xy≡x+y x+yInv))
       where
       xy : FinVec ⟨ R ⟩ 2
       xy zero = x
       xy one = y
-      ∑xy≡x+y : (x y : ⟨ R ⟩) → x + y ≡ x + (y + 0r)
-      ∑xy≡x+y = solve R
+      ∑xy≡x+y : x + y ≡ x + (y + 0r)
+      ∑xy≡x+y = solve! R
       Σ→⊎ : Σ[ i ∈ Fin 2 ] xy i ∈ R ˣ → (x ∈ R ˣ) ⊎ (y ∈ R ˣ)
       Σ→⊎ (zero , xInv) = ⊎.inl xInv
       Σ→⊎ (one , yInv) = ⊎.inr yInv
@@ -123,10 +123,7 @@ module _ (R : CommRing ℓ) where
     +Closed nonInvertiblesFormIdeal {x = x} {y = y} xNonInv yNonInv x+yInv =
       ∥_∥₁.rec isProp⊥ (⊎.rec xNonInv yNonInv) (invertibleInBinarySum x+yInv)
     contains0 nonInvertiblesFormIdeal (x , 0x≡1) =
-      1≢0 (sym 0x≡1 ∙ useSolver _)
-      where
-        useSolver : (x : ⟨ R ⟩) → 0r · x ≡ 0r
-        useSolver = solve R
+      1≢0 (sym 0x≡1 ∙ solve! R)
     ·Closed nonInvertiblesFormIdeal {x = x} r xNonInv rxInv =
       xNonInv (snd (RˣMultDistributing r x rxInv))
 
@@ -163,7 +160,7 @@ module _ (R : CommRing ℓ) where
           ⊥.rec (1≢0 (sym 00⁻¹≡1 ∙ 0x≡0 0⁻¹))
           where
           0x≡0 : (x : ⟨ R ⟩) → 0r · x ≡ 0r
-          0x≡0 = solve R
+          0x≡0 _ = solve! R
         alternative→isLocal {n = ℕ.suc n} xxs x+∑xsInv =
           ∥_∥₁.rec
             isPropPropTrunc
@@ -205,11 +202,8 @@ module _ (R : CommRing ℓ) where
       private
         binSum→OneMinus : BinSum.BinSum → OneMinus
         binSum→OneMinus binSum x =
-          binSum x (1r - x) (subst (_∈ R ˣ) (1≡x+1-x x) RˣContainsOne)
-          where
-          1≡x+1-x : (x : ⟨ R ⟩) → 1r ≡ x + (1r - x)
-          1≡x+1-x = solve R
-          open Units R
+          binSum x (1r - x) (subst (_∈ R ˣ) (solve! R) RˣContainsOne)
+          where open Units R
 
         oneMinus→BinSum : OneMinus → BinSum.BinSum
         oneMinus→BinSum oneMinus x y (s⁻¹ , ss⁻¹≡1) =
@@ -219,12 +213,10 @@ module _ (R : CommRing ℓ) where
               (fst ∘ RˣMultDistributing y s⁻¹ ∘ subst (_∈ R ˣ) 1-xs⁻¹≡ys⁻¹))
             (oneMinus (x · s⁻¹))
           where
-          solveStep : (a b c : ⟨ R ⟩) → (a + b) · c - a · c ≡ b · c
-          solveStep = solve R
           1-xs⁻¹≡ys⁻¹ : 1r - x · s⁻¹ ≡ y · s⁻¹
           1-xs⁻¹≡ys⁻¹ =
             (1r - x · s⁻¹)             ≡⟨ cong (_- _) (sym ss⁻¹≡1) ⟩
-            ((x + y) · s⁻¹ - x · s⁻¹)  ≡⟨ solveStep x y s⁻¹ ⟩
+            ((x + y) · s⁻¹ - x · s⁻¹)  ≡⟨ solve! R ⟩
             (y · s⁻¹)                  ∎
           open Units R