\import Algebra.Domain
\import Algebra.Field
\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Nat
\import Data.Or
\import Function.Meta
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\open Monoid(Inv)
\class OrderedAddMonoid \extends StrictPoset, AddMonoid {
| <_+-left (z : E) {x y : E} : x < y -> x + z < y + z
| <_+-right (z : E) {x y : E} : x < y -> z + x < z + y
\lemma <_+ {a b c d : E} (p : a < c) (q : b < d) : a + b < c + d
=> <-transitive (<_+-left b p) (<_+-right c q)
}
\class OrderedAbMonoid \extends OrderedAddMonoid, AbMonoid
| <_+-right z x<y => transport2 (<) +-comm +-comm (<_+-left z x<y)
\class PreorderedAddGroup \extends AddGroup
| isPos : E -> \Prop
| zro/>0 : Not (isPos zro)
| positive_+ {x y : E} : isPos x -> isPos y -> isPos (x + y)
\class OrderedAddGroup \extends OrderedAddMonoid, PreorderedAddGroup {
| < => <
| <-irreflexive x<x => zro/>0 (transport isPos negative-right x<x)
| <-transitive x<y y<z => transport isPos diff_+ (positive_+ y<z x<y)
| <_+-left z {x} {y} x<y => transport isPos (inv (
(y + z) - (x + z) ==< pmap ((y + z) +) negative_+ >==
(y + z) + (negative z - x) ==< +-assoc >==
y + (z + (negative z - x)) ==< inv (pmap (y +) +-assoc) >==
y + ((z - z) - x) ==< pmap (y + (__ - x)) negative-right >==
y + (zro - x) ==< pmap (y +) zro-left >==
y - x `qed)) x<y
| isNeg : E -> \Prop
| isNeg x => isPos (negative x)
\lemma fromNeg {x y : E} (x-y<0 : isNeg (x - y)) : x < y
=> transport isPos (negative_+ *> pmap (`- x) negative-isInv) x-y<0
\lemma toNeg {x y : E} (x<y : x < y) : isNeg (x - y)
=> transport isPos (inv (negative_+ *> pmap (`- x) negative-isInv)) x<y
\lemma pos_>0 {x : E} (p : isPos x) : x > zro
=> transportInv (\lam y => isPos (x + y)) negative_zro $ transportInv isPos zro-right p
\lemma >0_pos {x : E} (x>0 : x > zro) : isPos x
=> transport isPos zro-right $ transport (\lam y => isPos (x + y)) negative_zro x>0
\lemma neg_<0 {x : E} (p : isNeg x) : x < zro
=> rewriteF negative-isInv $ positive_negative $ pos_>0 p
\lemma <0_neg {x : E} (x<0 : x < zro) : isNeg x
=> >0_pos (negative_positive x<0)
\lemma positive_negative' {x : E} (x>0 : isPos x) : isNeg (negative x)
=> unfold (simplify x>0)
\lemma positive_negative {x : E} (x>0 : x > zro) : negative x < zro
=> transport isPos (unfold (-) $ rewrite (negative-isInv,negative_zro) (zro-right *> inv zro-left)) x>0
\lemma negative_positive' {x : E} (-x<0 : isNeg (negative x)) : isPos x
=> transport isPos negative-isInv -x<0
\lemma negative_positive {x : E} (x<0 : x < zro) : negative x > zro
=> transport isPos (unfold (-) $ rewrite negative_zro (zro-left *> inv zro-right)) x<0
\lemma negative_< {x y : E} (x<y : x < y) : negative y < negative x
=> transportInv (\lam y => isPos (_ + y)) negative-isInv $ >0_pos $ rewriteF negative-left $ <_+-right (negative x) x<y
\lemma negative_<-inv {x y : E} (p : negative x < negative y) : y < x
=> transport2 (<) negative-isInv negative-isInv (negative_< p)
\lemma negative_<-left {x y : E} (p : negative x < y) : negative y < x
=> transport (_ <) negative-isInv (negative_< p)
\lemma negative_<-right {x y : E} (p : x < negative y) : y < negative x
=> transport (`< _) negative-isInv (negative_< p)
} \where {
\type \infix 4 < {A : PreorderedAddGroup} (x y : A) => isPos (y - x)
}
\class OrderedAbGroup \extends OrderedAbMonoid, OrderedAddGroup, AbGroup
\class OrderedSemiring \extends Semiring, OrderedAbMonoid {
| zro<ide : zro < ide
| <_*_positive-left {x y z : E} : x < y -> z > zro -> x * z < y * z
| <_*_positive-right {x y z : E} : x > zro -> y < z -> x * y < x * z
| <_*_negative-left {x y z : E} : x < y -> z < zro -> x * z > y * z
| <_*_negative-right {x y z : E} : x < zro -> y < z -> x * y > x * z
\lemma natCoef_< {n m : Nat} (p : n NatSemiring.< m) : natCoef n < natCoef m \elim n, m, p
| 0, 1, NatSemiring.zero<suc => rewrite (natCoefZero,natCoefSuc,natCoefZero,zro-left) zro<ide
| 0, suc (suc m), NatSemiring.zero<suc => rewrite (natCoefZero,natCoefSuc) $ transport (`< _) (zro-right *> natCoefZero) $ <_+ (natCoef_< NatSemiring.zero<suc) zro<ide
| suc n, suc m, NatSemiring.suc<suc p => rewrite (natCoefSuc,natCoefSuc) $ <_+-left ide (natCoef_< p)
\lemma <_*_positive_positive {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) : 0 < x * y
=> transport (`< _) zro_*-right (<_*_positive-right x>0 y>0)
\lemma <_*_negative_negative {x y : E} (x<0 : x < 0) (y<0 : y < 0) : 0 < x * y
=> 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)
\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)
}
\class LinearlyOrderedSemiring \extends OrderedSemiring, LinearOrder {
| <_+-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))
\lemma <=_+ {a b c d : E} (a<=b : a <= b) (c<=d : c <= d) : a + c <= b + d
=> \case <-comparison (b + c) __ \with {
| byLeft b+d<b+c => c<=d (<_+-cancel-left b b+d<b+c)
| byRight b+c<a+c => a<=b (<_+-cancel-right c b+c<a+c)
}
\lemma <=_+-left {a b c d : E} (p : a <= c) (q : b < d) : a + b < c + d
=> <-transitive-left (<_+-right a q) (<=_+ p <=-refl)
\lemma <=_+-right {a b c d : E} (p : a < c) (q : b <= d) : a + b < c + d
=> <-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 {
| byLeft (_,y<x) => x<=y y<x
| byRight (z<0,_) => 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 {
| byLeft (_,z<y) => y<=z z<y
| byRight (x<0,_) => 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 {
| 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 {
| byLeft (x>0,_) => x<=0 x>0
| byRight (_,z<y) => y<=z z<y
}
\lemma <=_*_positive_positive {x y : E} (x>=0 : 0 <= x) (y>=0 : 0 <= y) : 0 <= x * y
=> transport (`<= _) zro_*-right (<=_*_positive-right x>=0 y>=0)
\lemma <=_*_negative_negative {x y : E} (x<=0 : x <= 0) (y<=0 : y <= 0) : 0 <= x * y
=> 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)
\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)
\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
\lemma <_+-invert-left {a b c d : E} (p : b + d < a + c) (q : c <= d) : b < a
=> <_+-cancel-right c $ <-transitive-right (<=_+ <=-refl q) p
\lemma BigSum_<= {n : Nat} {l l' : Array E n} (p : \Pi (j : Fin n) -> l j <= l' j) : BigSum l <= BigSum l' \elim n, l, l'
| 0, nil, nil => <=-refl
| 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<ide) \with {
| byLeft q => q.2
| byRight q => absurd (<-irreflexive (<-transitive p q.1))
}
\func mid (t : Inv (1 + 1)) (a b : E) => (a + b) * t.inv
\lemma mid>left (t : Inv (1 + 1)) {a b : E} (p : a < b) : a < mid t a b
=> \have | t>0 : t.inv > 0 => inv-positive t $ <-transitive zro<ide $ transport (`< _) zro-left (<_+-left 1 zro<ide)
| a2<a+b : a * (1 + 1) < a + b => rewrite (ldistr,ide-right) (<_+-right a p)
\in transport (`< _) (*-assoc *> pmap (a *) t.inv-right *> ide-right) $ <_*_positive-left a2<a+b t>0
\lemma mid<right (t : Inv (1 + 1)) {a b : E} (p : a < b) : mid t a b < b
=> \have | t>0 : t.inv > 0 => inv-positive t $ <-transitive zro<ide $ transport (`< _) zro-left (<_+-left 1 zro<ide)
| a+b<b2 : a + b < b * (1 + 1) => rewrite (ldistr,ide-right) (<_+-left b p)
\in transport (_ <) (*-assoc *> pmap (b *) t.inv-right *> ide-right) (<_*_positive-left a+b<b2 t>0)
\func denseOrder (t : Inv (1 + 1)) : DenseLinearOrder \cowith
| LinearOrder => \this
| isDense {x} {z} p => inP (mid t x z, mid>left t p, mid<right t p)
\lemma natCoef>=0 {n : Nat} : zro <= natCoef n \elim n
| 0 => rewrite natCoefZero <=-refl
| suc n => transport2 (<=) zro-left (inv (natCoefSuc n)) $ <=_+ natCoef>=0 (<_<= zro<ide)
\lemma natCoef>0 {n : Nat} (p : 0 NatSemiring.< n) : zro < natCoef n \elim n
| 0 => \case p
| suc n => rewrite natCoefSuc $ transport (`< _) zro-left $ <=_+-left natCoef>=0 zro<ide
\lemma natCoef_<= {n m : Nat} (p : n NatSemiring.<= m) : natCoef n <= natCoef m
=> rewrite (inv (<=_exists p), natCoef_+) $ transport (`<= _) zro-right $ <=_+ <=-refl natCoef>=0
\class Dec \extends LinearlyOrderedSemiring, LinearOrder.Dec {
| <_+-cancel-left x {y} {z} x+y<x+z => \case trichotomy y z \with {
| equals y=z => absurd (<-irreflexive (rewriteF y=z x+y<x+z))
| less y<z => y<z
| greater y>z => absurd (<-irreflexive (<-transitive (<_+-right x y>z) x+y<x+z))
}
| <_+-cancel-right z {x} {y} x+z<y+z => \case trichotomy x y \with {
| equals x=y => absurd (<-irreflexive (rewriteF x=y x+z<y+z))
| less x<y => x<y
| greater x>y => absurd (<-irreflexive (<-transitive (<_+-left z x>y) x+z<y+z))
}
| <_*-cancel-left x y z x*y<x*z => \case trichotomy x zro, trichotomy y z \with {
| equals x=0, _ => absurd (<-irreflexive (transport2 (<) zro_*-left zro_*-left (rewriteF x=0 x*y<x*z)))
| _, equals y=z => absurd (<-irreflexive (rewriteF y=z x*y<x*z))
| less x<0, less y<z => absurd (<-irreflexive (<-transitive (<_*_negative-right x<0 y<z) x*y<x*z))
| greater x>0, less y<z => byLeft (x>0, y<z)
| less x<0, greater y>z => byRight (x<0, y>z)
| greater x>0, greater y>z => absurd (<-irreflexive (<-transitive (<_*_positive-right x>0 y>z) x*y<x*z))
}
| <_*-cancel-right x y z x*z<y*z => \case trichotomy x y, trichotomy z zro \with {
| equals x=y, _ => absurd (<-irreflexive (rewriteF x=y x*z<y*z))
| _, equals z=0 => absurd (<-irreflexive (transport2 (<) zro_*-right zro_*-right (rewriteF z=0 x*z<y*z)))
| less x<y, less z<0 => absurd (<-irreflexive (<-transitive x*z<y*z (<_*_negative-left x<y z<0)))
| less x<y, greater z>0 => byLeft (z>0, x<y)
| greater x>y, less z<0 => byRight (z<0, x>y)
| greater x>y, greater z>0 => absurd (<-irreflexive (<-transitive x*z<y*z (<_*_positive-left x>y z>0)))
}
\lemma splitSum {x y a b : E} (p : x + y <= a + b) : x <= a || y <= b
=> \case dec<_<= a x, dec<_<= b y \with {
| inr x<=a, _ => byLeft x<=a
| _, inr y<=b => byRight y<=b
| inl a<x, inl b<y => absurd (<-irreflexive (<-transitive-left (OrderedAddMonoid.<_+ a<x b<y) p))
}
\lemma meet_+-left {a b c : E} : (a + b) ∧ (a + c) = a + b ∧ c
=> \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<x => absurd $ <-irreflexive $ <-transitive-right p $ <_*_positive-right z>0 y<x
| inr x<=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<x => absurd $ <-irreflexive $ <-transitive-right p $ <_*_positive-left y<x z>0
| inr x<=y => x<=y
}
}
} \where \open LinearOrder
\class OrderedCSemiring \extends OrderedSemiring, CSemiring, OrderedAbMonoid
| <_*_positive-right x>0 y<z => transport2 (<) *-comm *-comm (<_*_positive-left y<z x>0)
| <_*_negative-right x<0 y<z => transport2 (>) *-comm *-comm (<_*_negative-left y<z x<0)
\class LinearlyOrderedCSemiring \extends LinearlyOrderedSemiring, OrderedCSemiring, OrderedAbMonoid
| <_+-cancel-right z x+z<y+z => <_+-cancel-left z (transport2 (<) +-comm +-comm x+z<y+z)
| <_*-cancel-right x y z x*z<y*z => <_*-cancel-left z x y (transport2 (<) *-comm *-comm x*z<y*z)
\where
\class Dec \extends OrderedCSemiring, LinearlyOrderedSemiring.Dec
{- | An ordered ring is a linearly ordered domain such that the product of positive elements is positive
- and an element is apart from {zro} if and only if it is either positive or negative.
-}
\class OrderedRing \extends Domain, LinearlyOrderedSemiring, OrderedAbGroup {
| ide>zro : isPos ide
| <_+-comparison (x y : E) : isPos (x + y) -> isPos x || isPos y
| <_+-connectedness {x : E} : Not (isPos x) -> Not (isNeg x) -> x = zro
| positive_* {x y : E} : isPos x -> isPos y -> isPos (x * y)
| positive_*-cancel {x y : E} : isPos (x * y) -> (\Sigma (isPos x) (isPos y)) || (\Sigma (isNeg x) (isNeg y))
| positive=>#0 {x : E} : isPos x -> x `#0
| negative=>#0 {x : E} : isNeg x -> x `#0
\field #0=>eitherPosOrNeg {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))
| 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)
| 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_* {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)
| zro<ide => transport isPos (inv minus_zro) ide>zro
| <-comparison y {x} {z} x<z => \case <_+-comparison (z - y) (y - x) (transport isPos (inv OrderedAddGroup.diff_+) x<z) \with {
| byLeft p => byRight p
| byRight p => byLeft p
}
| <-connectedness x/<y y/<x => fromZero $ <_+-connectedness (y/<x __) $ \lam p => x/<y (fromNeg p)
| <_*_positive-left {x} {y} {z} x<y z>0 =>
transport isPos (rdistr *> pmap (y * z +) Ring.negative_*-left)
(positive_* x<y (transport isPos minus_zro z>0))
| <_*_positive-right {x} {y} {z} x>0 y<z =>
transport isPos (ldistr *> pmap (x * z +) Ring.negative_*-right)
(positive_* (transport isPos minus_zro x>0) y<z)
| <_*_negative-left {x} {y} {z} x<y z<0 =>
transport isPos (rdistr *> pmap (x * z +) Ring.negative_*-left)
(negative_* (toNeg x<y) (transport isPos zro-left z<0))
| <_*_negative-right {x} {y} {z} x<0 y<z =>
transport isPos (ldistr *> pmap (x * y +) Ring.negative_*-right)
(negative_* (transport isPos zro-left x<0) (toNeg y<z))
| <_+-cancel-left x {y} {z} x+y<x+z =>
transport2 (<)
(inv +-assoc *> pmap (`+ y) negative-left *> zro-left)
(inv +-assoc *> pmap (`+ z) negative-left *> zro-left)
(<_+-right (negative x) x+y<x+z)
| <_+-cancel-right z {x} {y} x+z<y+z =>
transport2 (<)
(+-assoc *> pmap (x +) negative-right *> zro-right)
(+-assoc *> pmap (y +) negative-right *> zro-right)
(<_+-left (negative z) x+z<y+z)
| <_*-cancel-left x y z x*y<x*z =>
\have x*[z-y]>0 => transport isPos (inv (ldistr *> pmap (x * z +) Ring.negative_*-right)) x*y<x*z
\in \case positive_*-cancel x*[z-y]>0 \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<y*z =>
\have [y-x]*z>0 => transport isPos (inv (rdistr *> pmap (y * z +) Ring.negative_*-left)) x*z<y*z
\in \case positive_*-cancel [y-x]*z>0 \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)
}
| #0-zro zro#0 => \case #0=>eitherPosOrNeg zro#0 \with {
| byLeft zro>0 => zro/>0 zro>0
| byRight zro>0 => zro/>0 (transport isPos negative_zro zro>0)
}
| #0-+ {x} {y} x+y#0 => \case #0=>eitherPosOrNeg x+y#0 \with {
| byLeft x+y>0 => ||.map positive=>#0 positive=>#0 (<_+-comparison x y x+y>0)
| byRight x+y<0 => \case <_+-comparison (negative y) (negative x) (transport isPos negative_+ x+y<0) \with {
| byLeft y<0 => byRight (negative=>#0 y<0)
| byRight x<0 => byLeft (negative=>#0 x<0)
}
}
| #0-tight x/#0 => <_+-connectedness (\lam x>0 => x/#0 (positive=>#0 x>0)) (\lam x<0 => x/#0 (negative=>#0 x<0))
| #0-*-left x*y#0 => \case #0=>eitherPosOrNeg x*y#0 \with {
| byLeft x*y>0 =>
\case positive_*-cancel x*y>0 \with {
| byLeft (x>0, _) => positive=>#0 x>0
| byRight (x<0, _) => negative=>#0 x<0
}
| byRight x*y<0 =>
\case negative_*-cancel x*y<0 \with {
| byLeft (x>0, _) => positive=>#0 x>0
| byRight (x<0, _) => negative=>#0 x<0
}
}
| #0-*-right x*y#0 => \case #0=>eitherPosOrNeg x*y#0 \with {
| byLeft x*y>0 =>
\case positive_*-cancel x*y>0 \with {
| byLeft (_, y>0) => positive=>#0 y>0
| byRight (_, y<0) => negative=>#0 y<0
}
| byRight x*y<0 =>
\case negative_*-cancel x*y<0 \with {
| byLeft (_, y<0) => negative=>#0 y<0
| byRight (_, y>0) => positive=>#0 y>0
}
}
| zro#ide => positive=>#0 ide>zro
| #0-* x#0 y#0 => \case #0=>eitherPosOrNeg x#0, #0=>eitherPosOrNeg y#0 \with {
| byLeft x>0, byLeft y>0 => positive=>#0 (positive_* x>0 y>0)
| byLeft x>0, byRight y<0 => negative=>#0 (positive_negative_* x>0 y<0)
| byRight x<0, byLeft y>0 => negative=>#0 (negative_positive_* x<0 y>0)
| byRight x<0, byRight y<0 => positive=>#0 (negative_* x<0 y<0)
}
\default #0 x : \Prop => isPos x || isNeg x
\default positive=>#0 \as positive=>#0Impl {x} : isPos x -> #0 x => byLeft
\default negative=>#0 \as negative=>#0Impl {x} : isNeg x -> #0 x => byRight
\default #0=>eitherPosOrNeg \as #0=>eitherPosOrNegImpl {x} (x#0 : #0 x) => x#0
\lemma positive_*-cancel-left {x y : E} (x*y>0 : isPos (x * y)) (y>0 : isPos y) : isPos x
=> \case positive_*-cancel x*y>0 \with {
| byLeft (x>0, _) => x>0
| byRight (_, -y>0) => absurd (zro/>0 (transport isPos negative-right (positive_+ y>0 -y>0)))
}
\lemma negative_<= {x y : E} (x<=y : x <= y) : negative y <= negative x
=> \lam -x<-y => x<=y $ repeat {2} (rewriteF negative-isInv) (negative_< -x<-y)
\func denseOrder (t : Inv (1 + 1)) : UnboundedDenseLinearOrder \cowith
| DenseLinearOrder => LinearlyOrderedSemiring.denseOrder t
| withoutUpperBound x => inP (x + 1, transport (`< _) zro-right $ <_+-right x zro<ide)
| withoutLowerBound x => inP (x - 1, transport (_ <) zro-right $ <_+-right x (positive_negative zro<ide))
} \where {
\class Dec \extends Domain.Dec, OrderedRing, LinearlyOrderedSemiring.Dec {
\field +_trichotomy (x : E) : Tri x zro
| trichotomy x y => \case +_trichotomy (x - y) \with {
| less x-y<0 => less $ fromNeg $ <0_neg x-y<0
| equals x-y=0 => equals (fromZero x-y=0)
| greater x-y>0 => greater $ >0_pos x-y>0
}
| <_+-comparison x y x+y>0 => \case +_trichotomy x \with {
| less x<0 => byRight $ transport isPos (inv +-assoc *> pmap (`+ y) negative-left *> zro-left) $ positive_+ (<0_neg x<0) x+y>0
| equals x=0 => byRight $ transport isPos (pmap (`+ y) x=0 *> zro-left) x+y>0
| greater x>0 => byLeft $ >0_pos x>0
}
| <_+-connectedness {x} x/>0 x/<0 => \case +_trichotomy x \with {
| less x<0 => absurd $ x/<0 $ <0_neg x<0
| equals x=0 => x=0
| greater x>0 => absurd $ x/>0 $ >0_pos x>0
}
| positive_*-cancel {x} {y} x*y>0 => \case +_trichotomy x, +_trichotomy y \with {
| equals x=0, _ => absurd (zro/>0 (transport isPos (pmap (`* y) x=0 *> zro_*-left) x*y>0))
| _, equals y=0 => absurd (zro/>0 (transport isPos (pmap (x *) y=0 *> zro_*-right) x*y>0))
| greater x>0, greater y>0 => byLeft (>0_pos x>0, >0_pos y>0)
| greater x>0, less y<0 => absurd $ zro/>0 $ transport isPos negative-right $ positive_+ x*y>0 $ positive_negative_* (>0_pos x>0) (<0_neg y<0)
| less x<0, greater y>0 => absurd $ zro/>0 $ transport isPos negative-right $ positive_+ x*y>0 $ negative_positive_* (<0_neg x<0) (>0_pos y>0)
| less x<0, less y<0 => byRight (<0_neg x<0, <0_neg y<0)
}
| nonZeroApart {x} x/=0 => \case +_trichotomy x \with {
| less x<0 => negative=>#0 (<0_neg x<0)
| equals x=0 => absurd (x/=0 x=0)
| greater x>0 => positive=>#0 (>0_pos x>0)
}
\default positive=>#0 {x} (x>0 : isPos x) : x /= zro => \lam x=0 => zro/>0 (transport isPos x=0 x>0)
\default negative=>#0 {x} (x<0 : isNeg x) : x /= zro => \lam x=0 => zro/>0 (transport isPos (pmap negative x=0 *> negative_zro) x<0)
\default #0=>eitherPosOrNeg {x} (x#0 : x /= zro) : isPos x || isNeg x => \case +_trichotomy x \with {
| less x<0 => byRight (<0_neg x<0)
| equals x=0 => absurd (transport (`/= zro) x=0 x#0 idp)
| greater x>0 => byLeft (>0_pos x>0)
}
\lemma join_negative {x y : E} : negative x ∨ negative y = negative (x ∧ y)
=> \case totality x y \with {
| byLeft x<=y => rewrite (meet_<= x<=y) $ join-comm *> join_<= (negative_<= x<=y)
| byRight y<=x => rewrite (meet-comm *> meet_<= y<=x) $ join_<= (negative_<= y<=x)
}
\lemma meet_negative {x y : E} : negative x ∧ negative y = negative (x ∨ y)
=> \case totality x y \with {
| byLeft x<=y => rewrite (join_<= x<=y) $ meet-comm *> meet_<= (negative_<= x<=y)
| byRight y<=x => rewrite (join-comm *> join_<= y<=x) $ meet_<= (negative_<= y<=x)
}
}
}
\class OrderedCRing \extends OrderedRing, IntegralDomain, OrderedCSemiring
\where
\class Dec \extends OrderedRing.Dec, OrderedCRing, LinearlyOrderedCSemiring.Dec, IntegralDomain.Dec
\class OrderedField \extends OrderedCRing, Field {
| zro/=ide _0=1 => <-irreflexive (transport (`< ide) _0=1 zro<ide)
| locality x => \case <_+-comparison (x + ide) (negative x) (transport isPos (inv (pmap (`- x) +-comm *> +-assoc *> pmap (ide +) negative-right *> zro-right)) ide>zro) \with {
| 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 =>
\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))))
| byRight x<0, byLeft y>0 => absurd (zro/>0 (transport isPos negative-right (positive_+ x*y>0 (negative_positive_* x<0 y>0))))
| byRight x<0, byRight y<0 => byRight (x<0, y<0)
}
| negative=>#0 x<0 => transport #0 negative-isInv (Ring.negative_inv (positive=>#0 x<0))
}
\class DiscreteOrderedField \extends OrderedCRing.Dec, OrderedField, DiscreteField {
| positive=>#0 {x} x>0 => \case eitherZeroOrInv x \with {
| byLeft x=0 => absurd (zro/>0 (transport isPos x=0 x>0))
| byRight x-isInv => x-isInv
}
| +_trichotomy x => \case eitherZeroOrInv x \with {
| byLeft x=0 => equals x=0
| byRight x-isInv => \case #0=>eitherPosOrNeg x-isInv \with {
| byLeft x>0 => greater $ pos_>0 x>0
| byRight x<0 => less $ neg_<0 x<0
}
}
\lemma finv>0 {x : E} (x>0 : 0 < x) : 0 < finv x
=> inv-positive (nonZero-Inv (>_/= x>0)) x>0
\lemma <_rotate-right {x y z : E} (y>0 : 0 < y) (xy<z : x * y < z) : x < z * finv y
=> transport (`< _) (*-assoc *> pmap (x *) (finv-right (>_/= y>0)) *> ide-right) (<_*_positive-left xy<z (finv>0 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)
}