Refactor ordered rings and define abs for them

JetBrains · Mar 12, 2024 · 2a13fb2 · 2a13fb2
1 parent 265b563
commit 2a13fb2
Show file tree

Hide file tree

Showing 9 changed files with 223 additions and 84 deletions.
diff --git a/src/Algebra/Domain.ard b/src/Algebra/Domain.ard
@@ -31,7 +31,7 @@
   | #0-* {x y : E} : x `#0 -> y `#0 -> (x * y) `#0
 
   | isReduced p => #0-tight $ \lam a#0 => #0-zro $ transport #0 p (#0-* a#0 a#0)
-  | isImpotent {a} p => \have q : a * (1 - a) = 0 => ldistr *> rewrite negative_*-right (toZero $ ide-right *> inv p)
+  | isImpotent {a} p => \have q : a * (1 - a) = 0 => ldistr_- *> toZero (ide-right *> inv p)
                         \in \case #0-+ (transportInv #0 (+-comm *> +-assoc *> pmap (1 +) negative-left *> zro-right) zro#ide) \with {
                           | byLeft a#0 => byRight $ inv $ fromZero $ #0-tight \lam zro-a#0 => apartNonZero (#0-* a#0 zro-a#0) q
                           | byRight zro-a#0 => byLeft $ #0-tight \lam a#0 => apartNonZero (#0-* a#0 zro-a#0) q
@@ -51,10 +51,10 @@
     => separatedEq (nonZero_* __ y/=0 x*y=0)
 
   \lemma nonZero-cancel-left {x y z : E} (x/=0 : x /= zro) (x*y=x*z : x * y = x * z) : y = z
-    => fromZero (nonZero-left x/=0 (ldistr *> pmap (x * y +) Ring.negative_*-right *> toZero x*y=x*z))
+    => fromZero (nonZero-left x/=0 (ldistr_- *> toZero x*y=x*z))
 
   \lemma nonZero-cancel-right {x y z : E} (z/=0 : z /= zro) (x*z=y*z : x * z = y * z) : x = y
-    => fromZero (nonZero-right z/=0 (rdistr *> pmap (x * z +) Ring.negative_*-left *> toZero x*z=y*z))
+    => fromZero (nonZero-right z/=0 (rdistr_- *> toZero x*z=y*z))
 
   \func nonZeroMonoid : CancelMonoid \cowith
     | E => \Sigma (x : E) (x `#0)
@@ -218,7 +218,7 @@
     | byLeft r => r
     | byRight r => r
   }
-  | isImpotent {a} p => \have q : a * (a - 1) = 0 => ldistr *> rewrite negative_*-right (toZero $ p *> inv ide-right)
+  | isImpotent {a} p => \have q : a * (a - 1) = 0 => ldistr_- *> toZero (p *> inv ide-right)
                         \in \case zeroProduct q \with {
                           | byLeft r => byLeft r
                           | byRight r => byRight (fromZero r)
@@ -232,13 +232,13 @@
     }
 
   \lemma zeroOrCancel-left {x y z : E} (p : x * y = x * z) : (x = 0) || (y = z)
-    => \case zeroProduct $ ldistr *> pmap (_ +) negative_*-right *> toZero p \with {
+    => \case zeroProduct $ ldistr_- *> toZero p \with {
       | byLeft x=0 => byLeft x=0
       | byRight y-z=0 => byRight (fromZero y-z=0)
     }
 
   \lemma zeroOrCancel-right {x y z : E} (p : x * z = y * z) : (x = y) || (z = 0)
-    => \case zeroProduct $ rdistr *> pmap (_ +) negative_*-left *> toZero p \with {
+    => \case zeroProduct $ rdistr_- *> toZero p \with {
       | byLeft x-y=0 => byLeft (fromZero x-y=0)
       | byRight z=0 => byRight z=0
     }

diff --git a/src/Algebra/Domain/Euclidean.ard b/src/Algebra/Domain/Euclidean.ard
@@ -319,8 +319,8 @@
                        | no x/=0 => iabs.*-comm *> pmap (_ *) (iabs.signum_/=0 x/=0)
                      }
                  \in pmap (_ +) (pos_iabs $ transportInv (`<= iabs y) (pmap iabs p) $ transportInv (`<= iabs y) t $ <=-less $ mod<right $ \lam |y|=0 => y/=0 $ iabs.equals0 |y|=0) *>
-                     pmap (`+ _) ldistr *>
-                     pmap ((_ + __) + _) (Ring.negative_*-right *> pmap negative (inv iabs.signum_*)) *>
+                     pmap (`+ _) Ring.ldistr_- *>
+                     pmap ((_ + negative __) + _) (inv iabs.signum_*) *>
                      +-assoc *>
                      pmap (_ +) (inv (+-assoc {_} {_} {pos (iabs y)} {neg (suc n)}) *> pmap (`+ _) (IntRing.negative-right {iabs y})) *>
                      pmap (_ +) p *>

diff --git a/src/Algebra/Group/Solver.ard b/src/Algebra/Group/Solver.ard
@@ -516,7 +516,7 @@
              ((removeVar n t v withInv).2 = n -' countVar t v withInv) \elim t, n
     | t, 0 => (rewrite rdistr0 ide-right, idp)
     | var x, suc n => mcases \with {
-      | yes e => (rewrite (NatSemiring.meet_+-left {1}, ldistr0) $ ide-left *> ide-left *> rewriteI (pmap __.2 e) (pmap (\lam s => f s.1) (inv e)), inv $ <=_exists zero<=_)
+      | yes e => (rewrite (inv (NatSemiring.meet_+-left {1}), ldistr0) $ ide-left *> ide-left *> rewriteI (pmap __.2 e) (pmap (\lam s => f s.1) (inv e)), inv $ <=_exists zero<=_)
       | no q => (ide-right, idp)
     }
     | :ide, suc n => (ide-left, idp)
@@ -533,7 +533,7 @@
       \lemma sum-lem {a b c : Nat} : a ∧ (b + c) = a ∧ b + (a -' b) ∧ c \elim a, b
         | 0, b => rdistr0 *> inv (pmap2 (+) rdistr0 rdistr0)
         | suc a, 0 => idp
-        | suc a, suc b => NatSemiring.meet_+-left {1} *> pmap suc sum-lem *> inv (pmap (`+ _) (NatSemiring.meet_+-left {1}))
+        | suc a, suc b => inv (NatSemiring.meet_+-left {1}) *> pmap suc sum-lem *> pmap (`+ _) (NatSemiring.meet_+-left {1})
     }
 
   \lemma removeVar_<=-lem (t : GroupTerm V) (v : V) (withInv : Bool) {n : Nat} (p : n <= countVar t v withInv)

diff --git a/src/Algebra/Linear/Solver.ard b/src/Algebra/Linear/Solver.ard
@@ -137,7 +137,7 @@
 
   \lemma solve<Problem (p : Problem) (t1 t2 : RingTerm C V) (c : CorrectCert (toContr p t1 t2))
                        (h : DArray (\lam j => interpretEq (p j))) : interpret t1 < interpret t2
-    => \case <_*-cancel-left (natCoef (c.1 0)) (interpret t1) (interpret t2) (\case or.toOr c.4 \with {
+    => \case <_*-cancel-left (\case or.toOr c.4 \with {
         | byLeft q => <_+-invert-right (certToLeq (toContr p t1 t2) c) $ solveContrProblem.aux p (\lam j => c.1 (suc j)) (hasNegative-correct p _ q) h
         | byRight q => <_+-invert-left (certToLess (toContr p t1 t2) c q) (solveContrProblem.aux_<= p (taild c.1) h)
       }) \with {