fix, cleanup CommRingSolver

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 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,10 @@ 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 _)
+      1≢0 (sym 0x≡1 ∙ useSolver)
       where
-        useSolver : (x : ⟨ R ⟩) → 0r · x ≡ 0r
-        useSolver = solve R
+        useSolver : 0r · x ≡ 0r
+        useSolver = solve! R
     ·Closed nonInvertiblesFormIdeal {x = x} r xNonInv rxInv =
       xNonInv (snd (RˣMultDistributing r x rxInv))
 
@@ -163,7 +163,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,10 +205,10 @@ 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)
+          binSum x (1r - x) (subst (_∈ R ˣ) (1≡x+1-x) RˣContainsOne)
           where
-          1≡x+1-x : (x : ⟨ R ⟩) → 1r ≡ x + (1r - x)
-          1≡x+1-x = solve R
+          1≡x+1-x : 1r ≡ x + (1r - x)
+          1≡x+1-x = solve! R
           open Units R
 
         oneMinus→BinSum : OneMinus → BinSum.BinSum
@@ -220,7 +220,7 @@ module _ (R : CommRing ℓ) where
             (oneMinus (x · s⁻¹))
           where
           solveStep : (a b c : ⟨ R ⟩) → (a + b) · c - a · c ≡ b · c
-          solveStep = solve R
+          solveStep _ _ _ = solve! R
           1-xs⁻¹≡ys⁻¹ : 1r - x · s⁻¹ ≡ y · s⁻¹
           1-xs⁻¹≡ys⁻¹ =
             (1r - x · s⁻¹)             ≡⟨ cong (_- _) (sym ss⁻¹≡1) ⟩

Cubical/Tactics/CommRingSolver/Reflection.agda

@@ -37,12 +37,6 @@ private
   variable
     ℓ : Level
 
-
-  -- we walk through expression collecting terms we will treat as variables in "vars : Vars"
-  -- when done, we look how many variables (=n) we have assign each an index 0,...,n-1
-  -- these indicies are used in the Hornerforms/Polynomials
-
-
   _==_ = primQNameEquality
   {-# INLINE _==_ #-}
 
@@ -80,14 +74,13 @@ private
           is- = buildMatcher (quote (CommRingStr.-_)) (getName -altName)
         }
 
-  private
-    solverCallAsTerm : Term → Arg Term → Term → Term → Term
-    solverCallAsTerm R varList lhs rhs =
-      def
-         (quote ringSolve)
-         (R v∷ lhs v∷ rhs
-           v∷ varList
-           ∷ (def (quote refl) []) v∷ [])
+  solverCallAsTerm : Term → Arg Term → Term → Term → Term
+  solverCallAsTerm R varList lhs rhs =
+    def
+       (quote ringSolve)
+       (R v∷ lhs v∷ rhs
+         v∷ varList
+         ∷ (def (quote refl) []) v∷ [])
 
   solverCallWithVars : ℕ → Vars → Term → Term → Term → Term
   solverCallWithVars n vars R lhs rhs =
@@ -123,41 +116,41 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   `1` (_ h∷ xs) = `1` xs
   `1` _ = ((λ _ → unknown) , [])
 
-  buildExpression' : Term → Vars → Template × Vars
-
-  private
-    op2 : Name → Term → Term → Vars → Template × Vars
-    op2 op x y vars = ((λ ass → con op (fst r1 ass v∷ fst r2 ass v∷ [])) ,
-                        appendWithoutRepetition (snd r1) (snd r2))
-      where
-      r1 = buildExpression' x vars
-      r2 = buildExpression' y vars
-
-    op1 : Name → Term → Vars → Template × Vars
-    op1 op x vars = ((λ ass → con op (fst r1 ass v∷ [])) , snd r1)
-      where
-      r1 = buildExpression' x vars
-
-  `_·_` : List (Arg Term) → Vars → Template × Vars
-  `_·_` (_ h∷ xs) vars = `_·_` xs vars
-  `_·_` (x v∷ y v∷ []) vars = op2 (quote _·'_) x y vars
-  `_·_` (_ v∷ x v∷ y v∷ []) vars = op2 (quote _·'_) x y vars
-  `_·_` _ vars = ((λ _ → unknown) , vars)
-
-  `_+_` : List (Arg Term) → Vars → Template × Vars
-  `_+_` (_ h∷ xs) vars = `_+_` xs vars
-  `_+_` (x v∷ y v∷ []) vars = op2 (quote _+'_) x y vars
-  `_+_` (_ v∷ x v∷ y v∷ []) vars = op2 (quote _+'_) x y vars
-  `_+_` _ vars = ((λ _ → unknown) , vars)
-
-  `-_` : List (Arg Term) → Vars → Template × Vars
-  `-_` (_ h∷ xs) vars = `-_` xs vars
-  `-_` (x v∷ []) vars = op1 (quote -'_) x vars
-  `-_` (_ v∷ x v∷ []) vars = op1 (quote -'_) x vars
-  `-_` _ vars = ((λ _ → unknown) , vars)
-
-  K' : List (Arg Term) → Vars → Template × Vars
-  K' xs vars = ((λ ass → con (quote K) xs) , vars)
+  buildExpression' : Term → Template × Vars
+
+  op2 : Name → Term → Term → Template × Vars
+  op2 op x y =
+    ((λ ass → con op (fst r1 ass v∷ fst r2 ass v∷ [])) ,
+     appendWithoutRepetition (snd r1) (snd r2))
+    where
+    r1 = buildExpression' x
+    r2 = buildExpression' y
+
+  op1 : Name → Term → Template × Vars
+  op1 op x = ((λ ass → con op (fst r1 ass v∷ [])) , snd r1)
+    where
+    r1 = buildExpression' x
+
+  `_·_` : List (Arg Term) → Template × Vars
+  `_·_` (_ h∷ xs) = `_·_` xs
+  `_·_` (x v∷ y v∷ []) = op2 (quote _·'_) x y
+  `_·_` (_ v∷ x v∷ y v∷ []) = op2 (quote _·'_) x y
+  `_·_` _ = ((λ _ → unknown) , [])
+
+  `_+_` : List (Arg Term) → Template × Vars
+  `_+_` (_ h∷ xs) = `_+_` xs
+  `_+_` (x v∷ y v∷ []) = op2 (quote _+'_) x y
+  `_+_` (_ v∷ x v∷ y v∷ []) = op2 (quote _+'_) x y
+  `_+_` _ = ((λ _ → unknown) , [])
+
+  `-_` : List (Arg Term) → Template × Vars
+  `-_` (_ h∷ xs) = `-_` xs
+  `-_` (x v∷ []) = op1 (quote -'_) x
+  `-_` (_ v∷ x v∷ []) = op1 (quote -'_) x
+  `-_` _ = ((λ _ → unknown) , [])
+
+  K' : List (Arg Term) → Template × Vars
+  K' xs = ((λ ass → con (quote K) xs) , [])
 
   finiteNumberAsTerm : Maybe ℕ → Term
   finiteNumberAsTerm (just ℕ.zero) = con (quote fzero) []
@@ -167,42 +160,41 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   polynomialVariable : Maybe ℕ → Term
   polynomialVariable n = con (quote ∣) (finiteNumberAsTerm n v∷ [])
 
-  -- buildExpression' : Term → Vars → Template × Vars
-  buildExpression' v@(var _ _) vars =
+  -- buildExpression' : Term → Template × Vars
+  buildExpression' v@(var _ _) =
     ((λ ass → polynomialVariable (ass v)) ,
-     addWithoutRepetition v vars)
-  buildExpression' t@(def n xs) vars =
+     v ∷ [])
+  buildExpression' t@(def n xs) =
     switch (λ f → f n) cases
       case is0 ⇒ `0` xs         break
       case is1 ⇒ `1` xs         break
-      case is· ⇒ `_·_` xs vars  break
-      case is+ ⇒ `_+_` xs vars  break
-      case is- ⇒ `-_` xs vars   break
-      default⇒ ((λ ass → polynomialVariable (ass t)) , addWithoutRepetition t vars)
-  buildExpression' t@(con n xs) vars =
+      case is· ⇒ `_·_` xs       break
+      case is+ ⇒ `_+_` xs       break
+      case is- ⇒ `-_` xs        break
+      default⇒ ((λ ass → polynomialVariable (ass t)) , t ∷ [])
+  buildExpression' t@(con n xs) =
     switch (λ f → f n) cases
       case is0 ⇒ `0` xs         break
       case is1 ⇒ `1` xs         break
-      case is· ⇒ `_·_` xs vars  break
-      case is+ ⇒ `_+_` xs vars  break
-      case is- ⇒ `-_` xs vars   break
-      default⇒ ((λ ass → polynomialVariable (ass t)) , addWithoutRepetition t vars)
-  buildExpression' t vars = ((λ _ → unknown) , vars)
+      case is· ⇒ `_·_` xs       break
+      case is+ ⇒ `_+_` xs       break
+      case is- ⇒ `-_` xs        break
+      default⇒ ((λ ass → polynomialVariable (ass t)) , t ∷ [])
+  buildExpression' t = ((λ _ → unknown) , [])
   -- there should be cases for variables which are functions, those should be detectable by having visible args
   -- there should be cases for definitions (with arguments)
 
   toAlgebraExpression : Term × Term → TC (Term × Term × Vars)
   toAlgebraExpression (lhs , rhs) = do
-      r1 ← returnTC (buildExpression' lhs [])
-      r2 ← returnTC (buildExpression' rhs [])
+      r1 ← returnTC (buildExpression' lhs)
+      r2 ← returnTC (buildExpression' rhs)
       vars ← returnTC (appendWithoutRepetition (snd r1) (snd r2))
       returnTC (
         let ass : VarAss
             ass n = indexOf n vars
         in (fst r1 ass , fst r2 ass , vars ))
 
 private
-
   checkIsRing : Term → TC Term
   checkIsRing ring = checkType ring (def (quote CommRing) (unknown v∷ []))
 
@@ -223,25 +215,6 @@ private
       let solution = solverCallWithVars (length vars) vars commRing lhs' rhs'
       unify hole solution
 
-  solve!-deb : Term → Term → TC Unit
-  solve!-deb uncheckedCommRing hole =
-    do
-      commRing ← checkIsRing uncheckedCommRing
-      goal ← inferType hole >>= normalise
-      names ← findRingNames commRing
-      just (lhs , rhs) ← get-boundary goal
-        where
-          nothing
-            → typeError(strErr "The CommRingSolver failed to parse the goal"
-                               ∷ termErr goal ∷ [])
-
-      (lhs' , rhs' , vars) ← CommRingReflection.toAlgebraExpression commRing names (lhs , rhs)
-      let solution = solverCallWithVars (length vars) vars commRing lhs' rhs'
-      typeError(termErr solution ∷ [])
-
 macro
   solve! : Term → Term → TC _
   solve! = solve!-macro
-
-  solve!-db : Term → Term → TC _
-  solve!-db = solve!-deb

Cubical/Tactics/Reflection/Variables.agda

@@ -1,4 +1,12 @@
 {-# OPTIONS --safe #-}
+{-
+  This code contains some helper functions for solvers.
+  Variables in the sense of this files are things that are treated like variables by a solver.
+  A ring solver might want to treat "f x" in an equation "f x + 0 ≡ f x" like a variable "y".
+  During the inspection of the lhs and rhs of an equation, terms like "f x" are found and saved
+  and later, indices are assigned to them. These indices will be the indices of the variables
+  in the normal forms the solver uses.
+-}
 module Cubical.Tactics.Reflection.Variables where
 
 open import Cubical.Foundations.Prelude hiding (Type)
@@ -64,6 +72,7 @@ appendWithoutRepetition : Vars → Vars → Vars
 appendWithoutRepetition (x ∷ l) l' = appendWithoutRepetition l (addWithoutRepetition x l')
 appendWithoutRepetition [] l' = l'
 
+-- this can be used to get a map from variables to numbers 0,...,n
 indexOf : Term → Vars → Maybe ℕ
 indexOf t (t' ∷ l) =
   if (t =T t')