simplify

agda · Feb 7, 2024 · aab08fb · aab08fb
1 parent 036ada4
commit aab08fb
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 25 deletions.
diff --git a/Cubical/Algebra/Ring/Quotient.agda b/Cubical/Algebra/Ring/Quotient.agda
@@ -18,7 +18,6 @@ open import Cubical.HITs.SetQuotients.Properties
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Ideal
 open import Cubical.Algebra.Ring.Kernel
-open import Cubical.Tactics.CommRingSolver
 
 private
   variable

diff --git a/Cubical/Algebra/ZariskiLattice/Base.agda b/Cubical/Algebra/ZariskiLattice/Base.agda
@@ -33,7 +33,6 @@ open import Cubical.Algebra.CommRing.Ideal
 open import Cubical.Algebra.CommRing.Ideal.Sum
 open import Cubical.Algebra.CommRing.FGIdeal
 open import Cubical.Algebra.CommRing.RadicalIdeal
-open import Cubical.Tactics.CommRingSolver
 open import Cubical.Algebra.Semilattice
 open import Cubical.Algebra.Lattice
 open import Cubical.Algebra.DistLattice

diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
@@ -304,10 +304,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
           instance
            h⁻ᵐ : (h ^ m) /1 ∈ₚ (R[1/ h ]AsCommRing ˣ)
            h⁻ᵐ = [ 1r , h ^ m , ∣ m , refl ∣₁ ]
-               , eq/ _ _ ((1r , containsOne) , path (h ^ m))
-            where
-            path : ∀ x → 1r · (x · 1r) · 1r ≡ 1r · 1r · (1r · x)
-            path _ = solve! R'
+               , eq/ _ _ ((1r , containsOne) , solve! R')
 
           β : FinVec R[1/ h ] (suc n)
           β i = ((h ^ m) /1) ⁻¹ · α i /1
@@ -360,12 +357,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
       pres1 (snd (coneOut /1/1Cone (pair i j i<j))) = refl
       pres+ (snd (coneOut /1/1Cone (pair i j i<j))) x y =
         cong [_] (≡-× (cong [_] (≡-×
-                      (cong₂ _+_ (useSolver x) (useSolver y))
-                      (Σ≡Prop (λ _ → isPropPropTrunc) (useSolver 1r))))
+                      (cong₂ _+_ (solve! R') (solve! R'))
+                      (Σ≡Prop (λ _ → isPropPropTrunc) (solve! R'))))
                       (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r))))
-        where
-        useSolver : ∀ a → a ≡ a · 1r · (1r · 1r)
-        useSolver _ = solve! R'
       pres· (snd (coneOut /1/1Cone (pair i j i<j))) x y =
         cong [_] (≡-× (cong [_] (≡-× refl
                       (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r)))))

diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda
@@ -314,16 +314,9 @@ module _ (R' : CommRing ℓ) where
         path = eq/ _ _ ((1r , ∣ 0 , refl ∣₁) , bigPath)
              ∙ cong (β zero · (f /1) +_) (sym (+IdR (β (suc zero) · (g /1))))
          where
-         useSolver1 : ∀ hn → 1r · 1r · ((hn · 1r) · (hn · 1r)) ≡ hn · hn
-         useSolver1 _ = solve! R'
-
-         useSolver2 : ∀ az f hn as g → hn · (az · f + (as · g + 0r))
-                                      ≡ 1r · (az · f · (hn · 1r) + as · g · (hn · 1r)) · 1r
-         useSolver2 _ _ _ _ _ = solve! R'
-
          bigPath : 1r · 1r · ((h ^ n · 1r) · (h ^ n · 1r))
                  ≡ 1r · (α zero · f · (h ^ n · 1r) + α (suc zero) · g · (h ^ n · 1r)) · 1r
-         bigPath = useSolver1 (h ^ n) ∙ cong (h ^ n ·_) p ∙ useSolver2 _ _ _ _ _
+         bigPath = solve! R' ∙ cong (h ^ n ·_) p ∙ solve! R'
 
     {-
 
@@ -371,12 +364,9 @@ module _ (R' : CommRing ℓ) where
     pres0 (snd /1/1AsCommRingHomFG) = refl
     pres1 (snd /1/1AsCommRingHomFG) = refl
     pres+ (snd /1/1AsCommRingHomFG) x y = cong [_] (≡-× (cong [_] (≡-×
-                                         (cong₂ _+_ (useSolver x) (useSolver y))
-                                         (Σ≡Prop (λ _ → isPropPropTrunc) (useSolver 1r))))
+                                         (cong₂ _+_ (solve! R') (solve! R'))
+                                         (Σ≡Prop (λ _ → isPropPropTrunc) (solve! R'))))
                                          (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r))))
-      where
-      useSolver : ∀ a → a ≡ a · 1r · (1r · 1r)
-      useSolver _ = solve! R'
     pres· (snd /1/1AsCommRingHomFG) x y = cong [_] (≡-× (cong [_] (≡-× refl
                                             (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r)))))
                                             (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·IdR 1r))))

diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
@@ -33,7 +33,6 @@ open import Cubical.Algebra.CommRing.BinomialThm
 open import Cubical.Algebra.CommRing.Ideal
 open import Cubical.Algebra.CommRing.FGIdeal
 open import Cubical.Algebra.CommRing.RadicalIdeal
-open import Cubical.Tactics.CommRingSolver
 open import Cubical.Algebra.Semilattice
 open import Cubical.Algebra.Lattice
 open import Cubical.Algebra.DistLattice