\import Algebra.Algebra
\import Algebra.Domain
\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Nat
\import Data.Array
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\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
=> <_+-left b p <∘ <_+-right c q
}
\class OrderedAbMonoid \extends OrderedAddMonoid, AbMonoid
| <_+-right z x<y => transport2 (<) +-comm +-comm (<_+-left z x<y)
\class BiorderedLatticeAbMonoid \extends BiorderedLattice, JoinSemilatticeAbMonoid, MeetSemilatticeAbMonoid, AbMonoid
\class LinearlyBiorderedAbMonoid \extends BiorderedLatticeAbMonoid, LinearLattice
\class LinearlyOrderedAbMonoid \extends LinearlyBiorderedAbMonoid, OrderedAbMonoid {
| <_+-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-right z p => <_+-cancel-left z $ transport2 (<) +-comm +-comm p
| <=_+ {a} {b} {c} {d} a<=b c<=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)
}
| meet_+-left {a} {b} {c} => <=-antisymmetric (meet-univ (<=_+ <=-refl meet-left) (<=_+ <=-refl meet-right)) \lam p =>
\have t => LinearOrder.meet/=left $ <_/= $ <_+-cancel-left a $ p <∘l meet-left
\in meet-right $ rewrite t in p
| join_+-left {a} {b} {c} => <=-antisymmetric (\lam p =>
\have t => LinearOrder.join/=left $ <_/= $ <_+-cancel-left a $ join-left <∘r p
\in join-right $ rewrite t in p) $ join-univ (<=_+ <=-refl join-left) (<=_+ <=-refl join-right)
\lemma <_+-invert-right {a b c d : E} (p : b + d <= a + c) (q : c < d) : b < a
=> <_+-cancel-right c $ <_+-right b q <∘l p
\lemma <_+-invert-left {a b c d : E} (p : b + d < a + c) (q : c <= d) : b < a
=> <_+-cancel-right c $ <=_+ <=-refl q <∘r p
\lemma <=_+-left {a b c d : E} (p : a <= c) (q : b < d) : a + b < c + d
=> <_+-right a q <∘l <=_+ p <=-refl
\lemma <=_+-right {a b c d : E} (p : a < c) (q : b <= d) : a + b < c + d
=> <_+-left b p <∘l <=_+ <=-refl q
\lemma BigSum_>0 {l : Array E} (q : \Pi (j : Fin l.len) -> 0 <= l j) (p : ∃ (j : Fin l.len) (0 < l j)) : 0 < BigSum l \elim l, p
| nil, inP ((),_)
| a :: l, inP (0, p) => transport (`< _) zro-right $ <=_+-right p $ BigSum_>=0 \lam j => q (suc j)
| a :: l, inP (suc j, p) => transport (`< _) zro-right $ <=_+-left (q 0) $ BigSum_>0 (\lam j => q (suc j)) $ inP (j,p)
\lemma Big_join-choice {n : Nat} {l : Array E (suc n)} {e : E} (e>0 : 0 < e) : ∃ (a : l) (Big (∨) (l 0) (tail l) < a + e) \elim n, l
| 0, a :: l => inP (0, transport (`< _) zro-right $ <_+-right a e>0)
| suc n, a :: l => \case <-comparison (Big (∨) a l) {l 0} {l 0 + e} $ transport (`< _) zro-right $ <_+-right (l 0) e>0 \with {
| byLeft p =>
\have t => LinearOrder.join/=left (<_/= p)
\in \case Big_join-choice {_} {n} {a :: \lam j => l (suc j)} e>0 \with {
| inP (0, q) => inP (0, transportInv (`< _) t q)
| inP (suc j, q) => inP (suc (suc j), transportInv (`< _) t q)
}
| byRight p => inP (1, p)
}
}
\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 {
| < => OrderedAddGroup.<
| <-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
=> rewrite negative-isInv in 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 $ rewrite negative-left in <_+-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)
\lemma <-diff-mid {x y z : E} (p : x - y < z) : x < z + y
=> simplify in <_+-left y p
\lemma <-diff-mid-conv {x y z : E} (p : x < z + y) : x - y < z
=> simplify in <_+-left (negative y) p
\lemma from>0 {x y : E} (p : 0 < y - x) : x < y
=> transport (`< _) (zro-left *> negative-isInv) (<-diff-mid-conv p)
\lemma to>0 {x y : E} (p : x < y) : 0 < y - x
=> <-diff-mid $ transportInv (`< _) (zro-left *> negative-isInv) p
\lemma from<0 {x y : E} (p : x - y < 0) : x < y
=> transport (x <) zro-left (<-diff-mid p)
\lemma to<0 {x y : E} (p : x < y) : x - y < 0
=> <-diff-mid-conv $ transportInv (x <) zro-left p
} \where {
\type \infix 4 < {A : PreorderedAddGroup} (x y : A) => isPos (y - x)
}
\class OrderedAbGroup \extends OrderedAbMonoid, OrderedAddGroup, AbGroup {
\lemma <-diff-left {x y z : E} (p : x - y < z) : x - z < y
=> (simplify, rewrite +-comm) in <_+-right (negative z) (<-diff-mid p)
}
\class LinearlyOrderedAbGroup \extends OrderedAbGroup, LinearlyOrderedAbMonoid, AbsAbGroup {
| <_+-comparison (x y : E) : isPos (x + y) -> isPos x || isPos y
| <_+-connectedness {x : E} : Not (isPos x) -> Not (isNeg x) -> x = zro
| <_+-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)
| <-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)
| abs>=0 => \lam p => <-irreflexive $ negative_positive (join-left <∘r p) <∘ join-right <∘r p
\lemma abs_-_< {x y z : E} (p : x - y < z) (q : y - x < z) : abs (x - y) < z
=> <_join-univ p (simplify q)
}
\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 NatOrder.< m) : natCoef n < natCoef m \elim n, m, p
| 0, 1, NatOrder.zero<suc => rewrite (natCoefZero,natCoefSuc,natCoefZero,zro-left) zro<ide
| 0, suc (suc m), NatOrder.zero<suc => rewrite (natCoefZero,natCoefSuc) $ transport (`< _) (zro-right *> natCoefZero) $ <_+ (natCoef_< NatOrder.zero<suc) zro<ide
| suc n, suc m, NatOrder.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)
\lemma <_* {a b c d : E} (a>0 : 0 < a) (c>0 : 0 < c) (a<b : a < b) (c<d : c < d) : a * c < b * d
=> <_*_positive-left a<b c>0 <∘ <_*_positive-right (a>0 <∘ a<b) c<d
\lemma pow>0 {a : E} (p : 0 < a) {k : Nat} : 0 < pow a k \elim k
| 0 => zro<ide
| suc k => <_*_positive_positive (pow>0 p) p
\lemma pow<id {a : E} (a>0 : 0 < a) (a<1 : a < 1) {k : Nat} (k>1 : 1 NatOrder.< k) : pow a k < a \elim k, k>1
| 1, NatOrder.suc<suc ()
| 2, _ => transport2 (__ * a < __) (inv ide-left) ide-right $ <_*_positive-right a>0 a<1
| suc (suc (suc k)), _ => transport (_ <) ide-right (<_*_positive-right (pow>0 a>0 {suc (suc k)}) a<1) <∘ pow<id a>0 a<1 {suc (suc k)} (NatOrder.suc<suc NatOrder.zero<suc)
}
\class LinearlyOrderedSemiring \extends OrderedSemiring, LinearlyOrderedAbMonoid, PosetSemiring {
| <_*-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))
| zro<=ide ide<zro => <-irreflexive (ide<zro <∘ zro<ide)
| <=_*_positive-left x<=y z>=0 => \case <_*-cancel-right __ \with {
| byLeft (_,y<x) => x<=y y<x
| byRight (z<0,_) => z>=0 z<0
}
| <=_*_positive-right x>=0 y<=z => \case <_*-cancel-left __ \with {
| byLeft (_,z<y) => y<=z z<y
| byRight (x<0,_) => x>=0 x<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 square_>=0 {x : E} : 0 <= x * x
=> \lam xx<0 => \case <_*-cancel-left (transportInv (_ <) zro_*-right xx<0) \with {
| byLeft (x>0,x<0) => <-irreflexive (x<0 <∘ x>0)
| byRight (x<0,x>0) => <-irreflexive (x<0 <∘ x>0)
}
\lemma sum_squares_>0 {l : Array E} (p : ∃ (j : Fin l.len) (0 < l j || l j < 0)) : 0 < BigSum (map (\lam x => x * x) l) \elim p
| inP (j,p) => BigSum_>0 (\lam j => square_>=0) $ inP $ later (j, \case \elim p \with {
| byLeft p => <_*_positive_positive p p
| byRight p => <_*_negative_negative p p
})
\lemma >0_Inv (t : Inv {\this}) (p : t > 0) : t.inv > 0
=> \case <_*-cancel-left (transport2 (<) (inv zro_*-right) (inv t.inv-right) zro<ide) \with {
| byLeft q => q.2
| byRight q => absurd (<-irreflexive (p <∘ q.1))
}
\lemma <0_Inv (t : Inv {\this}) (p : t < 0) : t.inv < 0
=> \case <_*-cancel-left (transport2 (<) (inv zro_*-right) (inv t.inv-right) zro<ide) \with {
| byLeft q => absurd (<-irreflexive (p <∘ q.1))
| byRight q => q.2
}
\lemma >=0_Inv (t : Inv {\this}) (p : 0 <= t) : 0 <= t.inv
=> \lam q => p (<0_Inv t.reverse q)
\lemma <=0_Inv (t : Inv {\this}) (p : t <= 0) : t.inv <= 0
=> \lam q => p (>0_Inv t.reverse q)
\lemma <=_Inv-cancel-left {x y z : E} (xi : Inv x) (x>=0 : 0 <= x) (p : x * y <= x * z) : y <= z
=> transport2 (<=) (inv *-assoc *> pmap (`* y) xi.inv-left *> ide-left) (inv *-assoc *> pmap (`* z) xi.inv-left *> ide-left) $ <=_*_positive-right (>=0_Inv xi x>=0) p
\lemma <=_Inv-cancel-right {x y z : E} (xi : Inv x) (p : y * x <= z * x) (x>=0 : 0 <= x) : y <= z
=> transport2 (<=) (*-assoc *> pmap (y *) xi.inv-right *> ide-right) (*-assoc *> pmap (z *) xi.inv-right *> ide-right) $ <=_*_positive-left p (>=0_Inv xi x>=0)
\func mid_inv (t : Inv (1 + 1)) (a b : E) => (a + b) * t.inv
\lemma mid_inv>left (t : Inv (1 + 1)) {a b : E} (p : a < b) : a < mid_inv t a b
=> \have | t>0 : t.inv > 0 => >0_Inv t $ 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_inv<right (t : Inv (1 + 1)) {a b : E} (p : a < b) : mid_inv t a b < b
=> \have | t>0 : t.inv > 0 => >0_Inv t $ 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_inv t x z, mid_inv>left t p, mid_inv<right t p)
\lemma natCoef>0 {n : Nat} (p : 0 NatOrder.< n) : zro < natCoef n \elim n
| 0 => \case p
| suc n => rewrite natCoefSuc $ transport (`< _) zro-left $ <=_+-left natCoef>=0 zro<ide
\lemma pow_<-monotone {a b : E} {k : Nat} (k/=0 : k /= 0) (a>=0 : 0 <= a) (a<b : a < b) : pow a k < pow b k \elim k
| 0 => absurd (k/=0 idp)
| suc k => <=_*_positive-left (pow_<=-monotone a>=0 $ <=-less a<b) a>=0 <∘r <_*_positive-right (pow>0 $ a>=0 <∘r a<b) a<b
\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 $ p <∘l meet-right
\in <_/= (<_*_positive-cancel-left a>=0 $ p <∘l 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 $ p <∘l meet-right
\in <_/= (<_*_positive-cancel-right c>=0 $ p <∘l meet-left) ab=a
\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 $ join-left <∘r p
\in <_/= (<_*_positive-cancel-left a>=0 $ join-right <∘r 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 $ join-left <∘r p
\in <_/= (<_*_positive-cancel-right c>=0 $ join-right <∘r 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<x+z => \case trichotomy y z \with {
| equals y=z => absurd (<-irreflexive (rewrite y=z in x+y<x+z))
| less y<z => y<z
| greater y>z => absurd (<-irreflexive (<_+-right x y>z <∘ x+y<x+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 (rewrite x=0 in x*y<x*z)))
| _, equals y=z => absurd (<-irreflexive (rewrite y=z in x*y<x*z))
| less x<0, less y<z => absurd (<-irreflexive (<_*_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 (<_*_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 (rewrite x=y in x*z<y*z))
| _, equals z=0 => absurd (<-irreflexive (transport2 (<) zro_*-right zro_*-right (rewrite z=0 in x*z<y*z)))
| less x<y, less z<0 => absurd (<-irreflexive (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 (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 (OrderedAddMonoid.<_+ a<x b<y <∘l p))
}
}
} \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
| <_*-cancel-right x*z<y*z => <_*-cancel-left (transport2 (<) *-comm *-comm x*z<y*z)
\where
\class Dec \extends OrderedCSemiring, LinearlyOrderedSemiring.Dec
{- | An ordered ring is a linearly ordered domain and a distributive lattice 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, LinearlyOrderedAbGroup, PosetRing {
| ide>zro : isPos ide
| positive_* {x y : E} : isPos x -> isPos y -> isPos (x * y)
| pos_*-cancel-left {x y : E} : isPos (x * y) -> isPos x -> isPos y
| pos_*-cancel-right {x y : E} : isPos (x * y) -> isPos y -> isPos x
| positive=>#0 {x : E} : isPos x -> x `#0
| negative=>#0 {x : E} : isNeg x -> x `#0
| <=_*-positive {x} {y} x>=0 y>=0 xy<0 => \case <_*-cancel-left $ transportInv (_ <) zro_*-right xy<0 \with {
| byLeft (_,y<0) => y>=0 y<0
| byRight (x<0,_) => x>=0 x<0
}
\field #0=>eitherPosOrNeg {x : E} : x `#0 -> isPos x || isNeg x
| positive_*-cancel {x y : E} : isPos (x * y) -> (\Sigma (isPos x) (isPos y)) || (\Sigma (isNeg x) (isNeg y))
| positive_*-cancel {x} {y} xy>0 => \case <-comparison x (pos_>0 xy>0) \with {
| byLeft x>0 => byLeft (>0_pos x>0, pos_*-cancel-left xy>0 $ >0_pos x>0)
| byRight x<xy => \case <_+-comparison (1 - y) y $ transportInv isPos (+-assoc *> pmap (1 +) negative-left *> zro-right) ide>zro \with {
| byLeft p => byRight
\have x<0 : isNeg x => pos_*-cancel-right (transportInv isPos negative_*-left $
transportInv isNeg (ldistr *> pmap2 (+) ide-right negative_*-right) $ toNeg x<xy) p
\in (x<0, pos_*-cancel-left (transportInv isPos Ring.negative_* xy>0) x<0)
| byRight y>0 => byLeft (pos_*-cancel-right xy>0 y>0, y>0)
}
}
| negative_*-cancel {x y : E} : isNeg (x * y) -> (\Sigma (isPos x) (isNeg y)) || (\Sigma (isNeg x) (isPos y))
| 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>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<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<0 y<0 => transport isPos Ring.negative_* (positive_* x<0 y<0)
| zro<ide => transport isPos (inv minus_zro) ide>zro
| <_*_positive-left x<y z>0 => transport isPos rdistr_- (positive_* x<y (transport isPos minus_zro z>0))
| <_*_positive-right x>0 y<z => transport isPos ldistr_- (positive_* (transport isPos minus_zro x>0) y<z)
| <_*_negative-left x<y z<0 => transport isPos rdistr_- (<_*_negative (toNeg x<y) (transport isPos zro-left z<0))
| <_*_negative-right x<0 y<z => transport isPos ldistr_- (<_*_negative (transport isPos zro-left x<0) (toNeg y<z))
| <_*-cancel-left x*y<x*z =>
\have x*[z-y]>0 => transportInv isPos ldistr_- 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*z<y*z =>
\have [y-x]*z>0 => transportInv isPos rdistr_- 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 pos#0 {x : E} (x>0 : 0 < x) : x AddGroup.`#0
=> positive=>#0 (>0_pos x>0)
\lemma neg#0 {x : E} (x<0 : x < 0) : x AddGroup.`#0
=> negative=>#0 (<0_neg x<0)
\lemma positive_*-cancel-left {x y : E} (xy>0 : 0 < x * y) (x>0 : 0 < x) : 0 < y
=> \case positive_*-cancel (>0_pos xy>0) \with {
| byLeft (_, y>0) => pos_>0 y>0
| byRight (-x>0, _) => absurd (zro/>0 (transport isPos negative-right (positive_+ (>0_pos x>0) -x>0)))
}
\lemma positive_*-cancel-right {x y : E} (x*y>0 : 0 < x * y) (y>0 : 0 < y) : 0 < x
=> pos_>0 $ pos_*-cancel-right (>0_pos x*y>0) (>0_pos y>0)
\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))
\lemma inv-negative (t : Inv {\this}) (p : t < 0) : t.inv < 0
=> transport2 (<) negative-isInv negative_zro $ negative_< $ >0_Inv (negative_inv t) (rewrite negative_zro in negative_< p)
\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 $ <=_*-positive abs>=0 (transport (`<= _) negative-right $ <=_+ abs>=id <=-refl) <∘r t
\in join-right {_} {x} {negative x} $ <_*_positive-cancel-right (rewrite negative_zro in negative_<= y<=0) $ later $ rewrite Ring.negative_* $ rewrite (abs-ofNeg y<=0) in p
| lem2 {x : E} : x * abs y <= abs (x * y) => \lam p => \case <_*-cancel-left (join-left <∘r p) \with {
| byLeft (x>0,y<|y|) => <-irreflexive $ join-right <∘r (rewrite (LinearOrder.join/=left $ <_/= y<|y|, negative_*-right) in p)
| byRight (_,c) => abs>=id c
}
\in <=-antisymmetric (join-univ lem1 $ rewriteI negative_*-left $ rewrite abs_negative in lem1 {negative x})
(rewrite (join_*-right abs>=0) $ join-univ lem2 $ transport (_ <=) (later $ rewrite negative_*-left abs_negative) lem2)
\lemma abs_ide : abs 1 = 1
=> abs-ofPos (LinearOrder.<_<= zro<ide)
\lemma abs_pow {x : E} {n : Nat} : abs (pow x n) = pow (abs x) n \elim n
| 0 => abs_ide
| suc n => abs_* *> pmap (`* _) abs_pow
} \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
}
| pos_*-cancel-left {x} {y} x*y>0 x>0 => \case +_trichotomy y \with {
| greater y>0 => >0_pos y>0
| equals y=0 => absurd (zro/>0 (transport isPos (pmap (x *) y=0 *> zro_*-right) x*y>0))
| less y<0 => absurd $ <-irreflexive $ pos_>0 x*y>0 <∘ neg_<0 (transport isPos negative_*-right $ positive_* x>0 $ >0_pos $ negative_positive 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)
}
}
}
\class OrderedCRing \extends OrderedRing, IntegralDomain, LinearlyOrderedCSemiring
| pos_*-cancel-right xy>0 => pos_*-cancel-left (transport isPos *-comm xy>0)
\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)
}
| pos_*-cancel-left x*y>0 x>0 =>
\case #0=>eitherPosOrNeg (Inv.cfactor-right (positive=>#0 x*y>0)) \with {
| byLeft y>0 => y>0
| byRight y<0 => absurd (zro/>0 (transport isPos negative-right (positive_+ x*y>0 (positive_negative_* x>0 y<0))))
}
| negative=>#0 x<0 => transport #0 negative-isInv (Ring.negative_inv (positive=>#0 x<0))
\func pinv (x : E) (\property x>0 : 0 < x) : E
=> Inv.inv {pos#0 x>0}
\lemma pinv-left {x : E} (x>0 : 0 < x) : pinv x x>0 * x = 1
=> Inv.inv-left {pos#0 x>0}
\lemma pinv-right {x : E} (x>0 : 0 < x) : x * pinv x x>0 = 1
=> Inv.inv-right {pos#0 x>0}
\lemma pinv_pos-inv {x : E} (x>0 : 0 < x) : pinv (pinv x x>0) (pinv>0 x>0) = x
=> inv $ Inv.inv-isUnique (Inv.reverse {pos#0 x>0}) (pos#0 $ pinv>0 x>0) idp
\lemma pinv_< {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) (x<y : x < y) : pinv y y>0 < pinv x x>0
=> pinv_<-conv (pinv>0 y>0) (pinv>0 x>0) $ transport2 (<) (inv $ pinv_pos-inv x>0) (inv $ pinv_pos-inv y>0) x<y
\lemma pinv_<-conv {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) (p : pinv y y>0 < pinv x x>0) : x < y
=> transport2 (<) (inv *-assoc *> pmap (`* x) (pinv-right y>0) *> ide-left) ide-right $ <_*_positive-right y>0 $ transport (_ <) (pinv-left x>0) (<_*_positive-left p x>0)
\lemma pinv_<= {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) (x<=y : x <= y) : pinv y y>0 <= pinv x x>0
=> \lam q => x<=y (pinv_<-conv y>0 x>0 q)
\lemma pinv_<=-conv {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) (p : pinv y y>0 <= pinv x x>0) : x <= y
=> \lam q => p (pinv_< y>0 x>0 q)
\lemma pinv>0 {x : E} (x>0 : 0 < x) : 0 < pinv x x>0
=> positive_*-cancel-left (transportInv (0 <) (pinv-right x>0) zro<ide) x>0
\lemma pinv>1 {x : E} (x>0 : 0 < x) (x<1 : x < 1) : 1 < pinv x x>0
=> transport (`< _) pinv_ide $ pinv_< x>0 zro<ide x<1
\lemma pinv_ide : pinv 1 zro<ide = 1
=> inv ide-left *> pinv-right zro<ide
\lemma pinv_* {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) : pinv x x>0 * pinv y y>0 = pinv (x * y) (<_*_positive_positive x>0 y>0)
=> Inv.inv-isUnique (Inv.lmake _ $ *-assoc *> pmap (_ *) (inv *-assoc *> pmap (`* x) (pinv-left y>0) *> ide-left) *> pinv-left x>0) (pos#0 $ <_*_positive_positive x>0 y>0) *-comm
\lemma pinv_pow {x : E} (x>0 : 0 < x) {n : Nat} : pow (pinv x x>0) n = pinv (pow x n) (pow>0 x>0) \elim n
| 0 => inv pinv_ide
| suc n => pmap (`* _) (pinv_pow x>0) *> pinv_* (pow>0 x>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
=> >0_Inv (nonZero-Inv (>_/= x>0)) x>0
\lemma finv<0 {x : E} (x<0 : x < 0) : finv x < 0
=> inv-negative (nonZero-Inv (<_/= x<0)) x<0
\lemma finv<1 {x : E} (x>1 : 1 < x) : finv x < 1
=> \have x>0 => zro<ide <∘ x>1
\in transport2 (<) ide-left (finv-right $ >_/= x>0) $ <_*_positive-left x>1 (finv>0 x>0)
\lemma finv>1 {x : E} (x>0 : 0 < x) (x<1 : x < 1) : 1 < finv x
=> transport2 (<) (finv-right $ >_/= x>0) ide-left $ <_*_positive-left x<1 (finv>0 x>0)
\lemma finv_< {x y : E} (x>0 : 0 < x) (x<y : x < y) : finv y < finv x
=> rewrite (finv-right $ >_/= x>0, ide-right, inv *-assoc, finv-left $ >_/= $ x>0 <∘ x<y, ide-left) in <_*_positive-right (finv>0 $ x>0 <∘ x<y) (<_*_positive-left x<y (finv>0 x>0))
\lemma finv_<-conv {x y : E} (x>0 : 0 < x) (p : finv x < finv y) : y < x
=> transport2 (<) finv_finv finv_finv $ finv_< (finv>0 x>0) p
\lemma finv_<-left {x y : E} (x>0 : 0 < x) (p : finv x < y) : finv y < x
=> transport (_ <) finv_finv $ finv_< (finv>0 x>0) p
\lemma finv_<-right {x y : E} (x>0 : 0 < x) (p : x < finv y) : y < finv x
=> transport (`< _) finv_finv $ finv_< x>0 p
\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)
\lemma <_rotate-right-conv {x y z : E} (y>0 : 0 < y) (p : x < z * finv y) : x * y < z
=> transport (`< z) (*-comm *> pmap (x *) finv_finv) $ <_rotate-left (finv>0 y>0) $ transport (x <) *-comm p
\lemma <_rotate-left-conv {x y z : E} (y>0 : 0 < y) (p : finv y * x < z) : x < y * z
=> transport (x <) (pmap (z *) finv_finv *> *-comm) $ <_rotate-right (finv>0 y>0) $ transport (`< z) *-comm p
\lemma finv_<= {x y : E} (x>0 : 0 < x) (x<=y : x <= y) : finv y <= finv x
=> \lam p => x<=y (finv_<-conv x>0 p)
\lemma finv>=0 {x : E} (x>=0 : 0 <= x) : 0 <= finv x
=> \lam p => x>=0 $ transport (`< 0) finv_finv (finv<0 p)
\lemma finv>0-diff {x : E} (x>0 : 0 < x) : finv x - finv (x + 1) = finv (x * (x + 1))
=> finv-diff (\lam x=0 => linarith) (\lam x+1=0 => linarith)
}
\class OrderedAAlgebra \extends AAlgebra, OrderedRing {
\override R : OrderedCRing
| coef_< {x y : R} : x < {R} y -> coefMap x < coefMap y
| coef_<-inv {x y : R} : coefMap x < coefMap y -> x < {R} y
\lemma coef_<= {x y : R} (p : x <= {R} y) : coefMap x <= coefMap y
=> \lam q => p (coef_<-inv q)
}
\class OrderedCAlgebra \extends OrderedAAlgebra, CAlgebra, OrderedCRing {
\override R : OrderedCRing
}
\class OrderedFieldAlgebra \extends OrderedCAlgebra, OrderedField