From d6cf2a47e8ed67fd8e7b35c6f694ca1043b066a3 Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Tue, 6 Feb 2024 17:41:35 +0100
Subject: [PATCH] more simplification, new test for the solver

---
 .../CommRing/Localisation/PullbackSquare.agda | 14 +------
 .../Localisation/UniversalProperty.agda       | 10 +----
 .../Algebra/CommRing/Quotient/IdealSum.agda   |  5 +--
 Cubical/Algebra/CommRing/RadicalIdeal.agda    |  4 +-
 Cubical/Tactics/CommRingSolver/Examples.agda  | 42 ++++++++++---------
 5 files changed, 28 insertions(+), 47 deletions(-)

diff --git a/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda b/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda
index 7b1a1ae69c..231223071b 100644
--- a/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda
+++ b/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda
@@ -383,21 +383,11 @@ module _ (R' : CommRing ℓ) (f g : (fst R')) where
       z/1≡y/gⁿ : (z /1ᵍ) ≡ [ y , g ^ n , ∣ n , refl ∣₁ ]
       z/1≡y/gⁿ = eq/ _ _ ((g ^ (n +ℕ m) , ∣ n +ℕ m , refl ∣₁) , path)
        where
-       useSolver1 : ∀ x y α₀ α₁ fⁿ⁺ᵐ gⁿ⁺ᵐ gⁿ
-                  → gⁿ⁺ᵐ · (α₀ · x · fⁿ⁺ᵐ + α₁ · y · gⁿ⁺ᵐ) · gⁿ
-                  ≡ α₀ · (x · gⁿ · (fⁿ⁺ᵐ · gⁿ⁺ᵐ)) + gⁿ⁺ᵐ · (α₁ · y · (gⁿ · gⁿ⁺ᵐ))
-       useSolver1 _ _ _ _ _ _ _ = solve! R'
-
-       useSolver2 : ∀ y α₀ α₁ gⁿ⁺ᵐ g²ⁿ⁺ᵐ f²ⁿ⁺ᵐ
-                  → α₀ · (y · f²ⁿ⁺ᵐ · gⁿ⁺ᵐ) + gⁿ⁺ᵐ · (α₁ · y · g²ⁿ⁺ᵐ)
-                  ≡ gⁿ⁺ᵐ · y · (α₀ · f²ⁿ⁺ᵐ + α₁ · g²ⁿ⁺ᵐ)
-       useSolver2 _ _ _ _ _ _ = solve! R'
-
        path : g ^ (n +ℕ m) · z · g ^ n ≡ g ^ (n +ℕ m) · y · 1r
        path =
            g ^ (n +ℕ m) · z · g ^ n
 
-         ≡⟨ useSolver1 _ _ _ _ _ _ _ ⟩
+         ≡⟨ solve! R' ⟩
 
            α₀ · (x · g ^ n · (f ^ (n +ℕ m) · g ^ (n +ℕ m))) + g ^ (n +ℕ m) · (α₁ · y · (g ^ n · g ^ (n +ℕ m)))
 
@@ -424,7 +414,7 @@ module _ (R' : CommRing ℓ) (f g : (fst R')) where
 
            α₀ · (y · f ^ 2n+m · g ^ (n +ℕ m)) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)
 
-         ≡⟨ useSolver2 _ _ _ _ _ _ ⟩
+         ≡⟨ solve! R' ⟩
 
            g ^ (n +ℕ m) · y · (α₀ · f ^ 2n+m + α₁ · g ^ 2n+m)
 
diff --git a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
index ef9cd26ff0..0c89652f21 100644
--- a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
+++ b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
@@ -84,10 +84,7 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
 
   S⁻¹Rˣ = S⁻¹RAsCommRing ˣ
   S/1⊆S⁻¹Rˣ : ∀ s → s ∈ S' → (s /1) ∈ S⁻¹Rˣ
-  S/1⊆S⁻¹Rˣ s s∈S' = [ 1r , s , s∈S' ] , eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path s)
-   where
-   path : ∀ s → 1r · (s · 1r) · 1r ≡ 1r · 1r · (1r  · s)
-   path _ = solve! R'
+  S/1⊆S⁻¹Rˣ s s∈S' = [ 1r , s , s∈S' ] , eq/ _ _ ((1r , SMultClosedSubset .containsOne) , solve! R')
 
   S⁻¹RHasUniversalProp : hasLocUniversalProp S⁻¹RAsCommRing /1AsCommRingHom S/1⊆S⁻¹Rˣ
   S⁻¹RHasUniversalProp B' ψ ψS⊆Bˣ = (χ , funExt χcomp) , χunique
@@ -313,10 +310,7 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
 
      s-inv : ⦃ s/1∈S⁻¹Rˣ : s /1 ∈ S⁻¹Rˣ ⦄ → s /1 ⁻¹ˡ ≡ [ 1r , s , s∈S' ]
      s-inv ⦃ s/1∈S⁻¹Rˣ ⦄ = PathPΣ (S⁻¹RInverseUniqueness (s /1) s/1∈S⁻¹Rˣ
-                           (_ , eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path s))) .fst
-      where
-      path : ∀ s → 1r · (s · 1r) · 1r ≡ 1r · 1r · (1r · s)
-      path _ = solve! R'
+                           (_ , eq/ _ _ ((1r , SMultClosedSubset .containsOne) , solve! R'))) .fst
 
      ·ₗ-path : [ r , s , s∈S' ] ≡   [ r , 1r , SMultClosedSubset .containsOne ]
                                  ·ₗ [ 1r , s , s∈S' ]
diff --git a/Cubical/Algebra/CommRing/Quotient/IdealSum.agda b/Cubical/Algebra/CommRing/Quotient/IdealSum.agda
index ae23b46491..937c8e0edc 100644
--- a/Cubical/Algebra/CommRing/Quotient/IdealSum.agda
+++ b/Cubical/Algebra/CommRing/Quotient/IdealSum.agda
@@ -93,12 +93,9 @@ module Construction {R : CommRing ℓ} (I J : IdealsIn R) where
               (subst (λ K → b - x ∈ K) (kernel≡I I)
                   (kernelFiber R (R / I) π₁ b x π₁b≡π₁x))
 
-          useSolver : (b : ⟨ R ⟩) → x ≡ - (b - x) + b
-          useSolver _ = solve! R
-
           step2 : ∀ b → b ∈ J → fst π₁ b ≡ fst π₁ x → x ∈ (I +i J)
           step2 b b∈J π₁b≡π₁x =
-            ∣ (- (b - x) , b) , (step1 b π₁b≡π₁x) , (b∈J , (x ≡⟨ useSolver b ⟩ (- (b - x) + b) ∎)) ∣₁
+            ∣ (- (b - x) , b) , (step1 b π₁b≡π₁x) , (b∈J , (x ≡⟨ solve! R ⟩ (- (b - x) + b) ∎)) ∣₁
 
   ψ : CommRingHom (R / (I +i J)) ((R / I) / π₁J)
   ψ = UniversalProperty.inducedHom R ((R / I) / π₁J) (I +i J) π πI+J≡0
diff --git a/Cubical/Algebra/CommRing/RadicalIdeal.agda b/Cubical/Algebra/CommRing/RadicalIdeal.agda
index dd0bb19b0f..0fdabfb3e7 100644
--- a/Cubical/Algebra/CommRing/RadicalIdeal.agda
+++ b/Cubical/Algebra/CommRing/RadicalIdeal.agda
@@ -54,8 +54,6 @@ module RadicalIdeal (R' : CommRing ℓ) where
    binomialCoeff∈I i with ≤-+-split n m (toℕ i) (pred-≤-pred (toℕ<n i))
    ... | inl n≤i = subst-∈ I (sym path) (·Closed (I .snd) _ xⁿ∈I)
     where
-    useSolver : ∀ a b c d → a · (b · c) · d ≡ a · b · d · c
-    useSolver a b c d = solve! R'
     path : ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
          ≡ ((n +ℕ m) choose toℕ i) · x ^ (toℕ i ∸ n) · y ^ (n +ℕ m ∸ toℕ i) · x ^ n
     path = ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
@@ -65,7 +63,7 @@ module RadicalIdeal (R' : CommRing ℓ) where
          ≡⟨ cong (λ z → ((n +ℕ m) choose toℕ i) · z · y ^ (n +ℕ m ∸ toℕ i))
                  (sym (·-of-^-is-^-of-+ x (toℕ i ∸ n) n)) ⟩
            ((n +ℕ m) choose toℕ i) · (x ^ (toℕ i ∸ n) · x ^ n) · y ^ (n +ℕ m ∸ toℕ i)
-         ≡⟨ useSolver _ _ _ _ ⟩
+         ≡⟨ solve! R' ⟩
            ((n +ℕ m) choose toℕ i) · x ^ (toℕ i ∸ n) · y ^ (n +ℕ m ∸ toℕ i) · x ^ n ∎
 
    ... | inr m≤n+m-i = subst-∈ I (sym path) (·Closed (I .snd) _ yᵐ∈I)
diff --git a/Cubical/Tactics/CommRingSolver/Examples.agda b/Cubical/Tactics/CommRingSolver/Examples.agda
index ac0e7dd3a4..158a4b0879 100644
--- a/Cubical/Tactics/CommRingSolver/Examples.agda
+++ b/Cubical/Tactics/CommRingSolver/Examples.agda
@@ -35,10 +35,13 @@ module TestErrors (R : CommRing ℓ) where
 module TestWithℤ where
   open CommRingStr (ℤCommRing .snd)
 
+  ex13 : (x y : ℤ) → (x · y) · 1r ≡ 1r · (y · x)
+  ex13 x y = solve! ℤCommRing
+
   ex0 : (a b : fst ℤCommRing) → a + b ≡ b + a
   ex0 a b = solve! ℤCommRing
 
-module Test (R : CommRing ℓ) where
+module Test (R : CommRing ℓ) (x y z : fst R) where
   open CommRingStr (snd R)
 
   _ : 0r ≡ 0r
@@ -52,41 +55,41 @@ module Test (R : CommRing ℓ) where
       ≡ 0r - 0r
   _ = solve! R
 
-  ex1 : ∀ x → x ≡ x
-  ex1 x = solve! R
+  ex1 : x ≡ x
+  ex1 = solve! R
 
-  ex2 : (x y : fst R) → x ≡ x
-  ex2 x y = solve! R
+  ex2 : x ≡ x
+  ex2 = solve! R
 
-  ex3 : ∀ x y → x + y ≡ y + x
-  ex3 x y = solve! R
+  ex3 : x + y ≡ y + x
+  ex3 = solve! R
 
-  ex4 : ∀ x y → y ≡ (y - x) + x
-  ex4 x y = solve! R
+  ex4 : y ≡ (y - x) + x
+  ex4 = solve! R
 
-  ex5 : ∀ x y → x ≡ (x - y) + y
-  ex5 x y = solve! R
+  ex5 : x ≡ (x - y) + y
+  ex5 = solve! R
 
-  ex6 : ∀ x y → (x + y) · (x - y) ≡ x · x - y · y
-  ex6 x y = solve! R
+  ex6 : (x + y) · (x - y) ≡ x · x - y · y
+  ex6 = solve! R
 
   {-
     A bigger example:
   -}
-  ex7 : (x y z : (fst R)) → (x + y) · (x + y) · (x + y) · (x + y)
+  ex7 : (x + y) · (x + y) · (x + y) · (x + y)
                 ≡ x · x · x · x + (scalar R 4) · x · x · x · y + (scalar R 6) · x · x · y · y
                   + (scalar R 4) · x · y · y · y + y · y · y · y
-  ex7 x y z = solve! R
+  ex7 = solve! R
 
   {-
     Examples that used to fail (see #513):
   -}
 
-  ex8 : (x : (fst R)) → x · 0r ≡ 0r
-  ex8 x = solve! R
+  ex8 : x · 0r ≡ 0r
+  ex8 = solve! R
 
-  ex9 : (x y z : (fst R)) → x · (y - z) ≡ x · y - x · z
-  ex9 x y z = solve! R
+  ex9 : x · (y - z) ≡ x · y - x · z
+  ex9 = solve! R
 
   {-
     The solver should also deal with non-trivial terms in equations.
@@ -115,7 +118,6 @@ module _ (R : CommRing ℓ) (A : CommAlgebra R ℓ') where
   ex12 : (x y : ⟨ A ⟩) → x + y ≡ y + x
   ex12 x y = solve! (CommAlgebra→CommRing A)
 
-
 module TestInPlaceSolving (R : CommRing ℓ) where
    open CommRingStr (snd R)