Merge remote-tracking branch 'origin/fwellen/tactical-initiative' int…

…o fwellen/tactical-initiative
agda · Feb 2, 2024 · dccd154 · dccd154
2 parents c70e1d3 + 29a9dee
commit dccd154
Show file tree

Hide file tree

Showing 27 changed files with 402 additions and 571 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/Instances/Unit.agda b/Cubical/Algebra/CommAlgebra/Instances/Unit.agda
@@ -56,9 +56,9 @@ module _ (R : CommRing ℓ) where
           where S = CommAlgebra→CommRing A
                 open CommRingStr (snd S) renaming (_·_ to _·s_)
                 step1 : (x : ⟨ A ⟩) → 0r ≡ x ·s 0r
-                step1 = solve S
+                step1 x = solve! S
                 step2 : (x : ⟨ A ⟩) → x ·s 1r ≡ x
-                step2 = solve S
+                step2 x = solve! S
 
       equivFrom1≡0 : CommAlgebraEquiv A UnitCommAlgebra
       equivFrom1≡0 = isContr→Equiv 1≡0→isContr isContrUnit*  ,

diff --git a/Cubical/Algebra/CommAlgebra/Localisation.agda b/Cubical/Algebra/CommAlgebra/Localisation.agda
@@ -311,7 +311,7 @@ module DoubleAlgLoc (R : CommRing ℓ) (f g : (fst R)) where
      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
+      useSolver _ _ _ = 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ᶠᵍ)))

diff --git a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
@@ -246,4 +246,4 @@ module _
       where
         open CommAlgebraStr (snd A)
         step : (x : ⟨ A ⟩) → x ≡ x - 0a
-        step = solve (CommAlgebra→CommRing A)
+        step x = solve! (CommAlgebra→CommRing A)
diff --git a/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda b/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda
@@ -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 -}

diff --git a/Cubical/Algebra/CommRing/BinomialThm.agda b/Cubical/Algebra/CommRing/BinomialThm.agda
@@ -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ⁿ⁺¹
@@ -86,7 +86,7 @@ module BinomialThm (R' : CommRing ℓ) where
   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'
+  solve1 x nci xⁱ yⁿ⁻ⁱ = solve! R'
 
   xVecPath : ∀ (i : Fin (suc n)) → x · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ xVec i
   xVecPath i = solve1 _ _ _ _
@@ -95,7 +95,7 @@ module BinomialThm (R' : CommRing ℓ) where
   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'
+  solve2 y nci xⁱ yⁿ⁻ⁱ = solve! R'
 
   yVecPath : ∀ (i : Fin (suc n)) → y · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ yVec i
   yVecPath i = solve2 _ _ _ _
@@ -111,7 +111,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)
@@ -129,4 +129,4 @@ module BinomialThm (R' : CommRing ℓ) where
            ∙ 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'
+   solve4 nci ncsi xxⁱ yⁿ⁻ⁱ = solve! R'
diff --git a/Cubical/Algebra/CommRing/FGIdeal.agda b/Cubical/Algebra/CommRing/FGIdeal.agda
@@ -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)

diff --git a/Cubical/Algebra/CommRing/Ideal/Base.agda b/Cubical/Algebra/CommRing/Ideal/Base.agda
@@ -82,9 +82,9 @@ 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) useSolver (·Closed (snd I) (- 1r) x∈I)
+   where useSolver : - 1r · x ≡ - x
+         useSolver = solve! R'
 
  ∑Closed : (I : CommIdeal) {n : ℕ} (V : FinVec R n)
          → (∀ i → V i ∈ I) → ∑ V ∈ I
@@ -132,7 +132,7 @@ module _ {R : CommRing ℓ} where
   -closed (snd (CommIdeal→Ideal I)) =  λ x∈pI → subst-∈p (fst I) (useSolver _)
                                                            (·Closed (snd I) (- 1r) x∈pI)
                                          where useSolver : (x : fst R) → - 1r · x ≡ - x
-                                               useSolver = solve R
+                                               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 →

diff --git a/Cubical/Algebra/CommRing/Ideal/Sum.agda b/Cubical/Algebra/CommRing/Ideal/Sum.agda
@@ -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)

diff --git a/Cubical/Algebra/CommRing/LocalRing.agda b/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) ⟩

diff --git a/Cubical/Algebra/CommRing/Localisation/Base.agda b/Cubical/Algebra/CommRing/Localisation/Base.agda
@@ -79,21 +79,13 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
    ((u · v · s') , SMultClosedSubset .multClosed (SMultClosedSubset .multClosed u∈S' v∈S') s'∈S')
    , path
   where
-  eq1 : (r s r' s' r'' s'' u v : R) → u · v · s' · r · s'' ≡ u · r · s' · v · s''
-  eq1 = solve R'
-
-  eq2 : (r s r' s' r'' s'' u v : R) → u · r' · s · v · s'' ≡ u · s · (v · r' · s'')
-  eq2 = solve R'
-
-  eq3 : (r s r' s' r'' s'' u v : R) → u · s · (v · r'' · s') ≡ u · v · s' · r'' · s
-  eq3 = solve R'
 
   path : u · v · s' · r · s'' ≡ u · v · s' · r'' · s
-  path = u · v · s' · r · s''   ≡⟨ eq1 r s r' s' r'' s'' u v ⟩ -- not just ≡⟨ solve R' ⟩
+  path = u · v · s' · r · s''   ≡⟨ solve! R' ⟩
          u · r · s' · v · s''   ≡⟨ cong (λ x → x · v · s'') p ⟩
-         u · r' · s · v · s''   ≡⟨ eq2 r s r' s' r'' s'' u v ⟩
+         u · r' · s · v · s''   ≡⟨ solve! R' ⟩
          u · s · (v · r' · s'') ≡⟨ cong (u · s ·_) q ⟩
-         u · s · (v · r'' · s') ≡⟨ eq3 r s r' s' r'' s'' u v ⟩
+         u · s · (v · r'' · s') ≡⟨ solve! R' ⟩
          u · v · s' · r'' · s   ∎
 
  locIsEquivRel : isEquivRel _≈_
@@ -116,27 +108,19 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   θ : (a a' b : R × S) → a ≈ a' → (a +ₚ b) ≈ (a' +ₚ b)
   θ (r₁ , s₁ , s₁∈S) (r'₁ , s'₁ , s'₁∈S) (r₂ , s₂ , s₂∈S) ((s , s∈S) , p) = (s , s∈S) , path
     where
-    eq1 : (r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s : R)
-        → s · (r₁ · s₂ + r₂ · s₁) · (s'₁ · s₂) ≡ s · r₁ · s'₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂
-    eq1 = solve R'
-
-    eq2 : (r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s : R)
-        → s · r'₁ · s₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂ ≡ s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂)
-    eq2 = solve R'
-
 
     path : s · (r₁ · s₂ + r₂ · s₁) · (s'₁ · s₂) ≡ s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂)
     path = s · (r₁ · s₂ + r₂ · s₁) · (s'₁ · s₂)
 
-         ≡⟨ eq1 r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s ⟩
+         ≡⟨ solve! R' ⟩
 
            s · r₁ · s'₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂
 
          ≡⟨ cong (λ x → x · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂) p ⟩
 
            s · r'₁ · s₁ · s₂ · s₂ + s · r₂ · s₁ · s'₁ · s₂
 
-         ≡⟨ eq2 r₁ s₁ r'₁ s'₁ s'₁ r₂ s₂ s ⟩
+         ≡⟨ solve! R' ⟩
 
            s · (r'₁ · s₂ + r₂ · s'₁) · (s₁ · s₂) ∎
 
@@ -151,7 +135,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
      where
      path : (r s r' s' r'' s'' : R)
           → r · (s' · s'') + (r' · s'' + r'' · s') · s ≡ (r · s' + r' · s) · s'' + r'' · (s · s')
-     path = solve R'
+     path r s r' s' r'' s'' = solve! R'
 
  0ₗ : S⁻¹R
  0ₗ = [ 0r , 1r , SMultClosedSubset .containsOne ]
@@ -163,7 +147,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   +ₗ-rid[] (r , s , s∈S) = path
    where
    eq1 : (r s : R) → r · 1r + 0r · s ≡ r
-   eq1 = solve R'
+   eq1 r s = solve! R'
 
    path : [ r · 1r + 0r · s , s · 1r , SMultClosedSubset .multClosed s∈S
                                       (SMultClosedSubset .containsOne) ]
@@ -180,10 +164,10 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   -ₗWellDef (r , s , _) (r' , s' , _) ((u , u∈S) , p) = eq/ _ _ ((u , u∈S) , path)
    where
    eq1 : (u r s' : R) → u · - r · s' ≡ - (u · r · s')
-   eq1 = solve R'
+   eq1 u r s' = solve! R'
 
    eq2 : (u r' s : R) → - (u · r' · s) ≡ u · - r' · s
-   eq2 = solve R'
+   eq2 u r' s = solve! R'
 
    path : u · - r · s' ≡ u · - r' · s
    path = eq1 u r s' ∙∙ cong -_ p ∙∙ eq2 u r' s
@@ -195,7 +179,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   +ₗ-rinv[] (r , s , s∈S) = eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path r s)
    where
    path : (r s : R) → 1r · (r · s + - r · s) · 1r ≡ 1r · 0r · (s · s)
-   path = solve R'
+   path r s = solve! R'
 
  +ₗ-comm : (x y : S⁻¹R) → x +ₗ y ≡ y +ₗ x
  +ₗ-comm = SQ.elimProp2 (λ _ _ → squash/ _ _) +ₗ-comm[]
@@ -223,11 +207,11 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
    where
    eq1 : (r₁ s₁ r'₁ s'₁ r₂ s₂ s : R)
        → s · (r₁ · r₂) · (s'₁ · s₂) ≡ s · r₁ · s'₁ · r₂ · s₂
-   eq1 = solve R'
+   eq1 r₁ s₁ r'₁ s'₁ r₂ s₂ s = solve! R'
 
    eq2 : (r₁ s₁ r'₁ s'₁ r₂ s₂ s : R)
        → s · r'₁ · s₁ · r₂ · s₂ ≡ s · (r'₁ · r₂) · (s₁ · s₂)
-   eq2 = solve R'
+   eq2 r₁ s₁ r'₁ s'₁ r₂ s₂ s = solve! R'
 
    path : s · (r₁ · r₂) · (s'₁ · s₂) ≡ s · (r'₁ · r₂) · (s₁ · s₂)
    path = eq1 r₁ s₁ r'₁ s'₁ r₂ s₂ s ∙∙ cong (λ x → x · r₂ · s₂) p ∙∙ eq2 r₁ s₁ r'₁ s'₁ r₂ s₂ s
@@ -262,7 +246,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
       path : (r s r' s' r'' s'' : R)
            → 1r · (r · (r' · s'' + r'' · s')) · (s · s' · (s · s''))
            ≡ 1r · (r · r' · (s · s'') + r · r'' · (s · s')) · (s · (s' · s''))
-      path = solve R'
+      path r s r' s' r'' s'' = solve! R'
 
  ·ₗ-comm : (x y : S⁻¹R) → x ·ₗ y ≡ y ·ₗ x
  ·ₗ-comm = SQ.elimProp2 (λ _ _ → squash/ _ _) ·ₗ-comm[]