diff --git a/src/Algebra/Domain.ard b/src/Algebra/Domain.ard index 5c556906..84507afe 100644 --- 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 index e4e00936..ad31fa9c 100644 --- 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 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 index a53f6ebf..c35c7fe0 100644 --- 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 index 7f721195..00a9d1a3 100644 --- a/src/Algebra/Linear/Solver.ard +++ b/src/Algebra/Linear/Solver.ard @@ -137,7 +137,7 @@ \lemma solve 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 { diff --git a/src/Algebra/Ordered.ard b/src/Algebra/Ordered.ard index aab29c9a..c2a2a347 100644 --- a/src/Algebra/Ordered.ard +++ b/src/Algebra/Ordered.ard @@ -9,6 +9,7 @@ \import Function.Meta \import Logic \import Meta +\import Order.Lattice \import Order.LinearOrder \import Order.StrictOrder \import Paths @@ -113,17 +114,17 @@ => transport (`< _) zro_*-right (<_*_negative-right x<0 y<0) \lemma <_*_positive_negative {x y : E} (x>0 : 0 < x) (y<0 : y < 0) : x * y < 0 - => transport (< _) zro_*-right (<_*_positive-right x>0 y<0) + => transport (_ <) zro_*-right (<_*_positive-right x>0 y<0) \lemma <_*_negative_positive {x y : E} (x<0 : x < 0) (y>0 : 0 < y) : x * y < 0 - => transport (< _) zro_*-left (<_*_positive-left x<0 y>0) + => transport (_ <) zro_*-left (<_*_positive-left x<0 y>0) } -\class LinearlyOrderedSemiring \extends OrderedSemiring, LinearOrder { +\class LinearlyOrderedSemiring \extends OrderedSemiring, LinearOrder, Lattice { | <_+-cancel-left (x : E) {y z : E} : x + y < x + z -> y < z | <_+-cancel-right (z : E) {x y : E} : x + z < y + z -> x < y - | <_*-cancel-left (x y z : E) : x * y < x * z -> (\Sigma (x > zro) (y < z)) || (\Sigma (x < zro) (y > z)) - | <_*-cancel-right (x y z : E) : x * z < y * z -> (\Sigma (z > zro) (x < y)) || (\Sigma (z < zro) (x > y)) + | <_*-cancel-left {x y z : E} : x * y < x * z -> (\Sigma (x > zro) (y < z)) || (\Sigma (x < zro) (y > z)) + | <_*-cancel-right {x y z : E} : x * z < y * z -> (\Sigma (z > zro) (x < y)) || (\Sigma (z < zro) (x > y)) \lemma <=_+ {a b c d : E} (a<=b : a <= b) (c<=d : c <= d) : a + c <= b + d => \case <-comparison (b + c) __ \with { @@ -138,25 +139,25 @@ => <-transitive-left (<_+-left b p) (<=_+ <=-refl q) \lemma <=_*_positive-left {x y z : E} (x<=y : x <= y) (z>=0 : 0 <= z) : x * z <= y * z - => \case <_*-cancel-right _ _ _ __ \with { + => \case <_*-cancel-right __ \with { | byLeft (_,y x<=y y z>=0 z<0 } \lemma <=_*_positive-right {x y z : E} (x>=0 : 0 <= x) (y<=z : y <= z) : x * y <= x * z - => \case <_*-cancel-left _ _ _ __ \with { + => \case <_*-cancel-left __ \with { | byLeft (_,z y<=z z x>=0 x<0 } \lemma <=_*_negative-left {x y z : E} (x<=y : x <= y) (z<=0 : z <= 0) : y * z <= x * z - => \case <_*-cancel-right _ _ _ __ \with { + => \case <_*-cancel-right __ \with { | byLeft (z>0,_) => z<=0 z>0 | byRight (_,x>y) => x<=y x>y } \lemma <=_*_negative-right {x y z : E} (x<=0 : x <= 0) (y<=z : y <= z) : x * z <= x * y - => \case <_*-cancel-left _ _ _ __ \with { + => \case <_*-cancel-left __ \with { | byLeft (x>0,_) => x<=0 x>0 | byRight (_,z y<=z z transport (`<= _) zro_*-right (<=_*_negative-right x<=0 y<=0) \lemma <=_*_positive_negative {x y : E} (x>=0 : 0 <= x) (y<=0 : y <= 0) : x * y <= 0 - => transport (<= _) zro_*-right (<=_*_positive-right x>=0 y<=0) + => transport (_ <=) zro_*-right (<=_*_positive-right x>=0 y<=0) \lemma <=_*_negative_positive {x y : E} (x<=0 : x <= 0) (y>=0 : 0 <= y) : x * y <= 0 - => transport (<= _) zro_*-left (<=_*_positive-left x<=0 y>=0) + => transport (_ <=) zro_*-left (<=_*_positive-left x<=0 y>=0) + + \lemma <_*_positive-cancel-left {x y z : E} (x>=0 : 0 <= x) (p : x * y < x * z) : y < z + => \case <_*-cancel-left p \with { + | byLeft (_,r) => r + | byRight (x<0,_) => absurd (x>=0 x<0) + } + + \lemma <_*_positive-cancel-right {x y z : E} (z>=0 : 0 <= z) (p : x * z < y * z) : x < y + => \case <_*-cancel-right p \with { + | byLeft (_,r) => r + | byRight (z<0,_) => absurd (z>=0 z<0) + } + + \lemma <_*_negative-cancel-left {x y z : E} (x<=0 : x <= 0) (p : x * y < x * z) : z < y + => \case <_*-cancel-left p \with { + | byLeft (x>0,_) => absurd (x<=0 x>0) + | byRight (_,r) => r + } + + \lemma <_*_negative-cancel-right {x y z : E} (z<=0 : z <= 0) (p : x * z < y * z) : y < x + => \case <_*-cancel-right p \with { + | byLeft (z>0,_) => absurd (z<=0 z>0) + | byRight (_,r) => r + } \lemma <_+-invert-right {a b c d : E} (p : b + d <= a + c) (q : c < d) : b < a => <_+-cancel-right c $ <-transitive-left (<_+-right b q) p @@ -184,7 +209,7 @@ | suc n, a :: l, a' :: l' => <=_+ (p 0) $ BigSum_<= \lam j => p (suc j) \lemma inv-positive (t : Inv {\this}) (p : t > 0) : t.inv > 0 - => \case <_*-cancel-left t 0 t.inv (transport2 (<) (inv zro_*-right) (inv t.inv-right) zro \case <_*-cancel-left (transport2 (<) (inv zro_*-right) (inv t.inv-right) zro q.2 | byRight q => absurd (<-irreflexive (<-transitive p q.1)) } @@ -220,6 +245,56 @@ | 0 => zro <_*_positive_positive (pow>0 p) p + \lemma meet/=left {a b : E} (p : a ∧ b /= a) : a ∧ b = b + => <=-antisymmetric meet-right $ meet-univ (\lam a p $ <=-antisymmetric meet-left $ meet-univ <=-refl $ <_<= a rewrite meet-comm $ meet/=left $ later $ rewrite meet-comm p + + \lemma meet_+-left {a b c : E} : a + b ∧ c = (a + b) ∧ (a + c) + => <=-antisymmetric (meet-univ (<=_+ <=-refl meet-left) (<=_+ <=-refl meet-right)) \lam p => + \have t => meet/=left $ <_/= $ <_+-cancel-left a $ <-transitive-left p meet-left + \in meet-right $ rewriteF t p + + \lemma meet_+-right {a b c : E} : a ∧ b + c = (a + c) ∧ (b + c) + => +-comm *> meet_+-left *> pmap2 (∧) +-comm +-comm + + \lemma meet_*-left {a b c : E} (a>=0 : 0 <= a) : a * (b ∧ c) = (a * b) ∧ (a * c) + => <=-antisymmetric (meet-univ (<=_*_positive-right a>=0 meet-left) (<=_*_positive-right a>=0 meet-right)) + \lam p => \have bc=b => meet/=right $ <_/= $ <_*_positive-cancel-left a>=0 $ <-transitive-left p meet-right + \in <_/= (<_*_positive-cancel-left a>=0 $ <-transitive-left p meet-left) bc=b + + \lemma meet_*-right {a b c : E} (c>=0 : 0 <= c) : (a ∧ b) * c = (a * c) ∧ (b * c) + => <=-antisymmetric (meet-univ (<=_*_positive-left meet-left c>=0) (<=_*_positive-left meet-right c>=0)) + \lam p => \have ab=a => meet/=right $ <_/= $ <_*_positive-cancel-right c>=0 $ <-transitive-left p meet-right + \in <_/= (<_*_positive-cancel-right c>=0 $ <-transitive-left p meet-left) ab=a + + \lemma join/=left {a b : E} (p : a /= a ∨ b) : a ∨ b = b + => <=-antisymmetric (join-univ (\lam b p $ <=-antisymmetric join-left (join-univ <=-refl $ <_<= b rewrite join-comm $ join/=left $ later $ rewrite join-comm p + + \lemma join_+-left {a b c : E} : a + (b ∨ c) = (a + b) ∨ (a + c) + => <=-antisymmetric (\lam p => + \have t => join/=left $ <_/= $ <_+-cancel-left a $ <-transitive-right join-left p + \in join-right $ rewriteF t p) $ join-univ (<=_+ <=-refl join-left) (<=_+ <=-refl join-right) + + \lemma join_+-right {a b c : E} : (a ∨ b) + c = (a + c) ∨ (b + c) + => +-comm *> join_+-left *> pmap2 (∨) +-comm +-comm + + \lemma join_*-left {a b c : E} (a>=0 : 0 <= a) : a * (b ∨ c) = (a * b) ∨ (a * c) + => <=-antisymmetric + (\lam p => \have bc=c => join/=left $ <_/= $ <_*_positive-cancel-left a>=0 $ <-transitive-right join-left p + \in <_/= (<_*_positive-cancel-left a>=0 $ <-transitive-right join-right p) (inv bc=c)) $ + join-univ (<=_*_positive-right a>=0 join-left) (<=_*_positive-right a>=0 join-right) + + \lemma join_*-right {a b c : E} (c>=0 : 0 <= c) : (a ∨ b) * c = (a * c) ∨ (b * c) + => <=-antisymmetric + (\lam p => \have ab=b => join/=left $ <_/= $ <_*_positive-cancel-right c>=0 $ <-transitive-right join-left p + \in <_/= (<_*_positive-cancel-right c>=0 $ <-transitive-right join-right p) (inv ab=b)) $ + join-univ (<=_*_positive-left join-left c>=0) (<=_*_positive-left join-right c>=0) + \class Dec \extends LinearlyOrderedSemiring, LinearOrder.Dec { | <_+-cancel-left x {y} {z} x+y \case trichotomy y z \with { | equals y=z => absurd (<-irreflexive (rewriteF y=z x+y xy => absurd (<-irreflexive (<-transitive (<_+-left z x>y) x+z \case trichotomy x zro, trichotomy y z \with { + | <_*-cancel-left {x} {y} {z} x*y \case trichotomy x zro, trichotomy y z \with { | equals x=0, _ => absurd (<-irreflexive (transport2 (<) zro_*-left zro_*-left (rewriteF x=0 x*y absurd (<-irreflexive (rewriteF y=z x*y absurd (<-irreflexive (<-transitive (<_*_negative-right x<0 yz => byRight (x<0, y>z) | greater x>0, greater y>z => absurd (<-irreflexive (<-transitive (<_*_positive-right x>0 y>z) x*y \case trichotomy x y, trichotomy z zro \with { + | <_*-cancel-right {x} {y} {z} x*z \case trichotomy x y, trichotomy z zro \with { | equals x=y, _ => absurd (<-irreflexive (rewriteF x=y x*z absurd (<-irreflexive (transport2 (<) zro_*-right zro_*-right (rewriteF z=0 x*z absurd (<-irreflexive (<-transitive x*z byRight y<=b | inl a absurd (<-irreflexive (<-transitive-left (OrderedAddMonoid.<_+ a \case totality b c \with { - | byLeft b<=c => rewrite (meet_<= b<=c, meet_<= $ <=_+ <=-refl b<=c) idp - | byRight c<=b => rewrite {2} meet-comm $ rewrite (meet-comm, meet_<= c<=b, meet_<= $ <=_+ <=-refl c<=b) idp - } - - \lemma meet_+-right {a b c : E} : (a + c) ∧ (b + c) = a ∧ b + c - => \case totality a b \with { - | byLeft a<=b => rewrite (meet_<= a<=b, meet_<= $ <=_+ a<=b <=-refl) idp - | byRight b<=a => rewrite {2} meet-comm $ rewrite (meet-comm, meet_<= b<=a, meet_<= $ <=_+ b<=a <=-refl) idp - } - - \lemma <=_*-cancel-left {x y z : E} (z>0 : zro < z) (p : z * x <= z * y) : x <= y - => \case dec<_<= y x \with { - | inl y absurd $ <-irreflexive $ <-transitive-right p $ <_*_positive-right z>0 y x<=y - } - - \lemma <=_*-cancel-right {x y z : E} (z>0 : zro < z) (p : x * z <= y * z) : x <= y - => \case dec<_<= y x \with { - | inl y absurd $ <-irreflexive $ <-transitive-right p $ <_*_positive-left y0 - | inr x<=y => x<=y - } } } \where \open LinearOrder @@ -287,11 +338,11 @@ \class LinearlyOrderedCSemiring \extends LinearlyOrderedSemiring, OrderedCSemiring, OrderedAbMonoid | <_+-cancel-right z x+z <_+-cancel-left z (transport2 (<) +-comm +-comm x+z <_*-cancel-left z x y (transport2 (<) *-comm *-comm x*z <_*-cancel-left (transport2 (<) *-comm *-comm x*zeitherPosOrNeg {x : E} : x `#0 -> isPos x || isNeg x | negative_*-cancel {x y : E} : isNeg (x * y) -> (\Sigma (isPos x) (isNeg y)) || (\Sigma (isNeg x) (isPos y)) - | negative_*-cancel {x} {y} x*y<0 => ||.map (\lam t => (t.1, t.2)) - (\lam t => (t.1, negative_positive' t.2)) - (positive_*-cancel (transport isPos (inv Ring.negative_*-right) x*y<0)) + | negative_*-cancel x*y<0 => ||.map (\lam t => (t.1, t.2)) + (\lam t => (t.1, negative_positive' t.2)) + (positive_*-cancel (transport isPos (inv Ring.negative_*-right) x*y<0)) | positive_negative_* {x y : E} : isPos x -> isNeg y -> isNeg (x * y) - | positive_negative_* {x} {y} x>0 y<0 => transport isPos Ring.negative_*-right (positive_* x>0 y<0) + | positive_negative_* x>0 y<0 => transport isPos Ring.negative_*-right (positive_* x>0 y<0) | negative_positive_* {x y : E} : isNeg x -> isPos y -> isNeg (x * y) - | negative_positive_* {x} {y} x<0 y>0 => transport isPos Ring.negative_*-left (positive_* x<0 y>0) + | negative_positive_* x<0 y>0 => transport isPos Ring.negative_*-left (positive_* x<0 y>0) | negative_* {x y : E} : isNeg x -> isNeg y -> isPos (x * y) - | negative_* {x} {y} x<0 y<0 => transport isPos Ring.negative_* (positive_* x<0 y<0) + | negative_* x<0 y<0 => transport isPos Ring.negative_* (positive_* x<0 y<0) | zro transport isPos (inv minus_zro) ide>zro @@ -326,18 +377,10 @@ } | <-connectedness x/ fromZero $ <_+-connectedness (y/ x/0 => - transport isPos (rdistr *> pmap (y * z +) Ring.negative_*-left) - (positive_* x0)) - | <_*_positive-right {x} {y} {z} x>0 y - transport isPos (ldistr *> pmap (x * z +) Ring.negative_*-right) - (positive_* (transport isPos minus_zro x>0) y - transport isPos (rdistr *> pmap (x * z +) Ring.negative_*-left) - (negative_* (toNeg x - transport isPos (ldistr *> pmap (x * y +) Ring.negative_*-right) - (negative_* (transport isPos zro-left x<0) (toNeg y0 => transport isPos rdistr_- (positive_* x0)) + | <_*_positive-right x>0 y transport isPos ldistr_- (positive_* (transport isPos minus_zro x>0) y transport isPos rdistr_- (negative_* (toNeg x transport isPos ldistr_- (negative_* (transport isPos zro-left x<0) (toNeg y transport2 (<) (inv +-assoc *> pmap (`+ y) negative-left *> zro-left) @@ -348,14 +391,14 @@ (+-assoc *> pmap (x +) negative-right *> zro-right) (+-assoc *> pmap (y +) negative-right *> zro-right) (<_+-left (negative z) x+z - \have x*[z-y]>0 => transport isPos (inv (ldistr *> pmap (x * z +) Ring.negative_*-right)) x*y + \have x*[z-y]>0 => transportInv isPos ldistr_- x*y0 \with { | byLeft (x>0, z-y>0) => byLeft (transport isPos (inv minus_zro) x>0, z-y>0) | byRight (x<0, z-y<0) => byRight (transport isPos (inv zro-left) x<0, fromNeg z-y<0) } - | <_*-cancel-right x y z x*z - \have [y-x]*z>0 => transport isPos (inv (rdistr *> pmap (y * z +) Ring.negative_*-left)) x*z + \have [y-x]*z>0 => transportInv isPos rdistr_- x*z0 \with { | byLeft (y-x>0, z>0) => byLeft (transport isPos (inv minus_zro) z>0, y-x>0) | byRight (y-x<0, z<0) => byRight (transport isPos (inv zro-left) z<0, fromNeg y-x<0) @@ -423,6 +466,43 @@ | DenseLinearOrder => LinearlyOrderedSemiring.denseOrder t | withoutUpperBound x => inP (x + 1, transport (`< _) zro-right $ <_+-right x zro inP (x - 1, transport (_ <) zro-right $ <_+-right x (positive_negative zro x ∨ negative x + + \lemma abs>=id {x : E} : x <= abs x + => join-left + + \lemma abs>=0 {x : E} : 0 <= abs x + => \lam p => <-irreflexive $ <-transitive (negative_positive (<-transitive-right join-left p)) (<-transitive-right join-right p) + + \lemma abs_negative {x : E} : abs (negative x) = abs x + => <=-antisymmetric (join-univ join-right $ rewrite negative-isInv join-left) (join-univ (=_<= (inv negative-isInv) <=∘ join-right) join-left) + + \lemma abs-ofPos {x : E} (x>=0 : 0 <= x) : abs x = x + => <=-antisymmetric (join-univ <=-refl $ transport2 (<=) zro-left negative-right (<=_+ x>=0 <=-refl) <=∘ x>=0) join-left + + \lemma abs-ofNeg {x : E} (x<=0 : x <= 0) : abs x = negative x + => inv abs_negative *> abs-ofPos (rewriteF negative_zro $ negative_<= x<=0) + + \lemma abs_abs {x : E} : abs (abs x) = abs x + => abs-ofPos abs>=0 + + \lemma abs_+ {x y : E} : abs (x + y) <= abs x + abs y + => join-univ (<=_+ join-left join-left) $ rewrite (negative_+,+-comm) $ <=_+ join-right join-right + + \lemma abs_* {x y : E} : abs (x * y) = abs x * abs y + => \have | lem1 {x : E} : x * y <= abs x * abs y => \lam p => + \have | t : abs x * (abs y - y) < (x - abs x) * y => rewrite (ldistr_-,rdistr_-) $ <_+-left _ p + | y<=0 => LinearOrder.<_<= $ <_*_negative-cancel-left {_} {x - abs x} {0} {y} (transport (_ <=) negative-right $ <=_+ abs>=id <=-refl) $ rewrite zro_*-right $ <-transitive-right (<=_*_positive_positive abs>=0 $ transport (`<= _) negative-right $ <=_+ abs>=id <=-refl) t + \in join-right {_} {x} {negative x} $ <_*_positive-cancel-right (rewriteF negative_zro $ negative_<= y<=0) $ later $ rewrite Ring.negative_* $ rewriteF (abs-ofNeg y<=0) p + | lem2 {x : E} : x * abs y <= abs (x * y) => \lam p => \case <_*-cancel-left (<-transitive-right join-left p) \with { + | byLeft (x>0,y<|y|) => <-irreflexive $ <-transitive-right join-right $ rewriteF (join/=left $ <_/= y<|y|, negative_*-right) p + | byRight (_,c) => abs>=id c + } + \in <=-antisymmetric (join-univ lem1 $ rewriteI negative_*-left $ rewriteF abs_negative $ lem1 {negative x}) $ + rewrite (join_*-right abs>=0) $ join-univ lem2 $ transport (_ <=) (later $ rewrite negative_*-left abs_negative) lem2 } \where { \class Dec \extends Domain.Dec, OrderedRing, LinearlyOrderedSemiring.Dec { \field +_trichotomy (x : E) : Tri x zro @@ -478,7 +558,7 @@ } } -\class OrderedCRing \extends OrderedRing, IntegralDomain, OrderedCSemiring +\class OrderedCRing \extends OrderedRing, IntegralDomain, LinearlyOrderedCSemiring \where \class Dec \extends OrderedRing.Dec, OrderedCRing, LinearlyOrderedCSemiring.Dec, IntegralDomain.Dec @@ -488,7 +568,7 @@ | byLeft x+1>0 => byRight (positive=>#0 x+1>0) | byRight x<0 => byLeft (negative=>#0 x<0) } - | positive_*-cancel {x} {y} x*y>0 => + | positive_*-cancel x*y>0 => \case #0=>eitherPosOrNeg (Inv.cfactor-left (positive=>#0 x*y>0)), #0=>eitherPosOrNeg (Inv.cfactor-right (positive=>#0 x*y>0)) \with { | byLeft x>0, byLeft y>0 => byLeft (x>0, y>0) | byLeft x>0, byRight y<0 => absurd (zro/>0 (transport isPos negative-right (positive_+ x*y>0 (positive_negative_* x>0 y<0)))) @@ -518,5 +598,5 @@ => transport (`< _) (*-assoc *> pmap (x *) (finv-right (>_/= y>0)) *> ide-right) (<_*_positive-left xy0 y>0)) \lemma <_rotate-left {x y z : E} (y>0 : 0 < y) (p : x < y * z) : finv y * x < z - => transport (< _) (inv *-assoc *> pmap (`* z) (finv-left (>_/= y>0)) *> ide-left) (<_*_positive-right (finv>0 y>0) p) + => transport (_ <) (inv *-assoc *> pmap (`* z) (finv-left (>_/= y>0)) *> ide-left) (<_*_positive-right (finv>0 y>0) p) } diff --git a/src/Algebra/Ring.ard b/src/Algebra/Ring.ard index 1d393212..36e22522 100644 --- a/src/Algebra/Ring.ard +++ b/src/Algebra/Ring.ard @@ -63,6 +63,12 @@ negative (negative (x * y)) ==< negative-isInv >== x * y `qed + \lemma ldistr_- {x y z : E} : x * (y - z) = x * y - x * z + => ldistr *> pmap (_ +) negative_*-right + + \lemma rdistr_- {x y z : E} : (x - y) * z = x * z - y * z + => rdistr *> pmap (_ +) negative_*-left + \lemma negative_inv (j : Monoid.Inv {(\this : Ring)}) : Monoid.Inv (negative j) => \new Monoid.Inv { | inv => negative j.inv @@ -218,7 +224,7 @@ } })), ((1,0), \lam (zd, red : ReducedRing) => \lam a => \case zd a \with { | inP (b, 0, p) => inP (b, equation) - | inP (b, suc n, p) => inP (b, inv ide-right *> fromZero (pmap (_ +) (inv negative_*-right) *> inv ldistr *> + | inP (b, suc n, p) => inP (b, inv ide-right *> fromZero (inv ldistr_- *> red.noNilpotent {_} {suc n} (pow_*-comm {_} {_} {_} {suc n} *> equation)) *> inv *-assoc) } ), diff --git a/src/Algebra/Ring/Localization/Field.ard b/src/Algebra/Ring/Localization/Field.ard index e44a66f3..1558348f 100644 --- a/src/Algebra/Ring/Localization/Field.ard +++ b/src/Algebra/Ring/Localization/Field.ard @@ -8,8 +8,13 @@ \import Algebra.Ring \import Algebra.Ring.Local \import Algebra.Ring.Localization +\import Algebra.Semiring +\import Function.Meta \import Logic +\import Meta +\import Order.Lattice \import Order.LinearOrder +\import Order.StrictOrder \import Paths \import Paths.Meta \import Relation.Equivalence @@ -84,7 +89,61 @@ | #0=>eitherPosOrNeg {in~ x} => \case localization-inv.converse __ \with { | inP (r, x*r>0) => ||.map __.1 __.1 (positive_*-cancel x*r>0) } + | meet (x y : Type {R} {positiveSubset R}) : Type {R} {positiveSubset R} \with { + | in~ s, in~ t => in~ ((s.1 * t.2) ∧ (t.1 * s.2), s.2 * t.2, positive_* s.3 t.3) + | in~ s, ~-equiv x y r => equals1 $ pmap (_ *) *-comm *> inv *-assoc *> pmap (`* _) (meet_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∧) equation equation *> inv (meet_*-right (<_<= $ pos_>0 x.3))) *> *-assoc *> pmap (_ *) *-comm + | ~-equiv x y r, in~ t => equals1 $ inv *-assoc *> pmap (`* _) (meet_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∧) equation equation *> inv (meet_*-right $ <_<= $ pos_>0 x.3)) *> *-assoc + } + | meet-left {x} {y} => \case \elim x, \elim y \with { + | in~ s, in~ t => \lam p => unfolds at p $ \case positive_*-cancel $ rewriteF (R.*-comm {s.2} {t.2}, inv *-assoc, inv rdistr) p \with { + | byLeft (q,_) => meet-left {_} {s.1 * t.2} $ rewriteF R.negative_*-left q + | byRight (_,c) => <-irreflexive $ <-transitive (pos_>0 s.3) (R.neg_<0 c) + } + } + | meet-right {x} {y} => \case \elim x, \elim y \with { + | in~ s, in~ t => \lam p => unfolds at p $ \case positive_*-cancel $ rewriteF (inv *-assoc, inv rdistr) p \with { + | byLeft (q,_) => meet-right {_} {s.1 * t.2} $ rewriteF R.negative_*-left q + | byRight (_,c) => <-irreflexive $ <-transitive (pos_>0 t.3) (R.neg_<0 c) + } + } + | meet-univ {x} {y} {z} => \case \elim x, \elim y, \elim z \with { + | in~ s, in~ t, in~ u => \lam u<=s u<=t p => unfolds at p $ R.meet-univ + (\have u<=s' : u.1 * s.2 <= s.1 * u.2 => \lam p => u<=s $ unfolds $ rewrite R.negative_*-left p + \in transport2 (<=) *-assoc equation $ <=_*_positive-left u<=s' $ <_<= $ pos_>0 t.3) + (\have u<=t' : u.1 * t.2 <= t.1 * u.2 => \lam p => u<=t $ unfolds $ rewrite R.negative_*-left p + \in transport2 (<=) equation equation $ <=_*_positive-left u<=t' $ <_<= $ pos_>0 s.3) + (rewriteF (R.negative_*-left, meet_*-right $ <_<= $ pos_>0 u.3) p) + } + | join (x y : Type {R} {positiveSubset R}) : Type {R} {positiveSubset R} \with { + | in~ s, in~ t => in~ ((s.1 * t.2) ∨ (t.1 * s.2), s.2 * t.2, positive_* s.3 t.3) + | in~ s, ~-equiv x y r => equals1 $ pmap (_ *) *-comm *> inv *-assoc *> pmap (`* _) (join_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∨) equation equation *> inv (join_*-right $ <_<= $ pos_>0 x.3)) *> *-assoc *> pmap (_ *) *-comm + | ~-equiv x y r, in~ t => equals1 $ inv *-assoc *> pmap (`* _) (join_*-right (<_<= $ pos_>0 y.3) *> pmap2 (∨) equation equation *> inv (join_*-right $ <_<= $ pos_>0 x.3)) *> *-assoc + } + | join-left {x} {y} => \case \elim x, \elim y \with { + | in~ s, in~ t => \lam p => unfolds at p $ \case positive_*-cancel $ rewriteF (R.*-comm {s.2} {t.2}, inv *-assoc, inv rdistr) p \with { + | byLeft (q,_) => join-left {_} {s.1 * t.2} q + | byRight (_,c) => <-irreflexive $ <-transitive (pos_>0 s.3) (R.neg_<0 c) + } + } + | join-right {x} {y} => \case \elim x, \elim y \with { + | in~ s, in~ t => \lam p => unfolds at p $ \case positive_*-cancel $ rewriteF (inv *-assoc, inv rdistr) p \with { + | byLeft (q,_) => join-right {_} {s.1 * t.2} q + | byRight (_,c) => <-irreflexive $ <-transitive (pos_>0 t.3) (R.neg_<0 c) + } + } + | join-univ {x} {y} {z} => \case \elim x, \elim y, \elim z \with { + | in~ s, in~ t, in~ u => \lam s<=u t<=u p => unfolds at p $ R.join-univ {s.1 * t.2 * u.2} {t.1 * s.2 * u.2} {u.1 * (s.2 * t.2)} + (\have s<=u' : s.1 * u.2 <= u.1 * s.2 => \lam p => s<=u $ unfolds $ rewrite R.negative_*-left p + \in transport2 (<=) equation *-assoc $ <=_*_positive-left s<=u' $ <_<= $ pos_>0 t.3) + (\have t<=u' : t.1 * u.2 <= u.1 * t.2 => \lam p => t<=u $ unfolds $ rewrite R.negative_*-left p + \in transport2 (<=) equation equation $ <=_*_positive-left t<=u' $ <_<= $ pos_>0 s.3) + (rewriteF (R.negative_*-left, join_*-right $ <_<= $ pos_>0 u.3) p) + } \where { + \open OrderedAddGroup + \open LinearOrder + \open LinearlyOrderedSemiring \hiding (Dec) + \func positiveSubset (R : OrderedCRing) : SubMonoid R \cowith | contains => isPos | contains_ide => ide>zro diff --git a/src/Algebra/Ring/Reduced.ard b/src/Algebra/Ring/Reduced.ard index b00333f7..4b445ca9 100644 --- a/src/Algebra/Ring/Reduced.ard +++ b/src/Algebra/Ring/Reduced.ard @@ -42,7 +42,7 @@ => \let | I : Ideal => Ideal.radical {Ideal.closure1 a} | (inP (k,c)) => I.contains_- (inP (n, Ideal.closure1_LDiv.2 $ inP d)) (inP (n', Ideal.closure1_LDiv.2 $ inP d')) | (inP dd) => Ideal.closure1_LDiv.1 c - \in fromZero $ div_pow_zero dd $ ldistr *> pmap (_ +) negative_*-right *> toZero p + \in fromZero $ div_pow_zero dd $ ldistr_- *> toZero p \lemma div_div-cancel {a b b' : E} (d : LDiv a b) (d' : LDiv a b') (p : LDiv (a * b) (a * b')) : LDiv b b' p.inv => div_pow_div-cancel {_} {a} {b} {b'} {1} {1} (rewrite ide-left d) (rewrite ide-left d') p diff --git a/src/Arith/Rat.ard b/src/Arith/Rat.ard index 160ce3b5..1dd3a74a 100644 --- a/src/Arith/Rat.ard +++ b/src/Arith/Rat.ard @@ -309,12 +309,6 @@ | LinearOrder.Dec => RatField | UnboundedDenseLinearOrder => RatField.denseOrder RatField.suc-inv -\func rabs (r : Rat) : Rat - | rat nom denom denom/=0 reduced => rat (iabs nom) denom denom/=0 reduced - \where - \lemma >=0 {r : Rat} : 0 <= rabs r \elim r - | rat nom denom denom/=0 reduced => \lam x<0 => signum.signum_neg/=1 (RatField.<0_neg x<0) - \func rat_floor (r : Rat) : Int | rat (pos n) d _ _ => n Nat.div d | rat (neg (suc _ \as n)) d _ _ => \case n Nat.mod d \with {