Ordered

\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Nat
\import Data.Array
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Subset

\class PosetAddMonoid \extends AddMonoid, Poset {
  | <=_+ {a b c d : E} : a <= b -> c <= d -> a + c <= b + d

  \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 BigSum_>=0 {l : Array E} (q : \Pi (j : Fin l.len) -> 0 <= l j) : 0 <= BigSum l
    => transport (`<= _) BigSum_replicate0 $ BigSum_<= {_} {_} {replicate l.len zro} q

  \lemma <=_+-positive {a b : E} (a>=0 : 0 <= a) (b>=0 : 0 <= b) : 0 <= a + b
    => transport (`<= _) zro-left $ <=_+ a>=0 b>=0

  \lemma *n_<= {n : Nat} {a b : E} (a<=b : a <= b) : n *n a <= n *n b \elim n
    | 0 => <=-refl
    | suc n => <=_+ (*n_<= a<=b) a<=b

  \lemma *n_>=0 {n : Nat} {a : E} (a>=0 : 0 <= a) : 0 <= n *n a \elim n
    | 0 => <=-refl
    | suc n => <=_+-positive (*n_>=0 a>=0) a>=0
}

\class PosetAbMonoid \extends PosetAddMonoid, AbMonoid

\class JoinSemilatticeAddMonoid \extends PosetAddMonoid, JoinSemilattice
  | join_+-left {a b c : E} : a + (b ∨ c) = (a + b) ∨ (a + c)
  | join_+-right {a b c : E} : (a ∨ b) + c = (a + c) ∨ (b + c)

\class MeetSemilatticeAddMonoid \extends PosetAddMonoid, MeetSemilattice
  | meet_+-left {a b c : E} : a + b ∧ c = (a + b) ∧ (a + c)
  | meet_+-right {a b c : E} : a ∧ b + c = (a + c) ∧ (b + c)

\class JoinSemilatticeAbMonoid \extends JoinSemilatticeAddMonoid, PosetAbMonoid
  | join_+-right => +-comm *> join_+-left *> pmap2 (∨) +-comm +-comm

\class MeetSemilatticeAbMonoid \extends MeetSemilatticeAddMonoid, PosetAbMonoid
  | meet_+-right => +-comm *> meet_+-left *> pmap2 (∧) +-comm +-comm

\class PosetAddGroup \extends PosetAddMonoid, AddGroup {
  \lemma from>=0 {x y : E} (p : 0 <= y - x) : x <= y
    => transport2 (<=) zro-left (+-assoc *> pmap (y +) negative-left *> zro-right) (<=_+ p <=-refl)

  \lemma to>=0 {x y : E} (p : x <= y) : 0 <= y - x
    => transport (`<= _) negative-right (<=_+ p <=-refl)

  \lemma from<=0 {x y : E} (p : x - y <= 0) : x <= y
    => transport2 (<=) (+-assoc *> pmap (x +) negative-left *> zro-right) zro-left (<=_+ p <=-refl)

  \lemma to<=0 {x y : E} (p : x <= y) : x - y <= 0
    => transport (_ <=) negative-right (<=_+ p <=-refl)

  \lemma negative_<= {x y : E} (x<=y : x <= y) : negative y <= negative x
    => transport2 (<=) (inv +-assoc *> pmap (`- y) negative-left *> zro-left) zro-right $ <=_+ <=-refl (to<=0 x<=y)

  \lemma negative_<=-conv {x y : E} (p : negative y <= negative x) : x <= y
    => transport2 (<=) negative-isInv negative-isInv (negative_<= p)

  \lemma negative>=0 {x : E} (x<=0 : x <= 0) : 0 <= negative x
    => transport (`<= _) negative_zro (negative_<= x<=0)

  \lemma negative-to<=0 {x : E} (p : 0 <= negative x) : x <= 0
    => negative_<=-conv $ transportInv (`<= _) negative_zro p

  \lemma negative<=0 {x : E} (x>=0 : 0 <= x) : negative x <= 0
    => transport (_ <=) negative_zro (negative_<= x>=0)

  \lemma negative-to>=0 {x : E} (p : negative x <= 0) : 0 <= x
    => negative_<=-conv $ transportInv (_ <=) negative_zro p

  \lemma <=_+-cancel-left (x : E) {y z : E} (p : x + y <= x + z) : y <= z
    => transport2 (<=) (inv +-assoc *> pmap (`+ y) negative-left *> zro-left) (inv +-assoc *> pmap (`+ z) negative-left *> zro-left) (<=_+ <=-refl p)

  \lemma <=_+-cancel-right (z : E) {x y : E} (p : x + z <= y + z) : x <= y
    => transport2 (<=) (+-assoc *> pmap (x +) negative-right *> zro-right) (+-assoc *> pmap (y +) negative-right *> zro-right) (<=_+ p <=-refl)
}

\class PosetAbGroup \extends PosetAddGroup, PosetAbMonoid, AbGroup

\class LatticeAbGroup \extends PosetAbGroup, MeetSemilatticeAbMonoid, JoinSemilatticeAbMonoid, DistributiveLattice {
  | meet_+-left {a} {b} {c} => <=-antisymmetric (meet-univ (<=_+ <=-refl meet-left) (<=_+ <=-refl meet-right)) $ <=_+-cancel-left (negative a) $ meet-univ (<=_+ <=-refl meet-left <=∘ =_<= (inv +-assoc *> pmap (`+ b) negative-left *> zro-left)) (<=_+ <=-refl meet-right <=∘ =_<= (inv +-assoc *> pmap (`+ c) negative-left *> zro-left)) <=∘ =_<= (inv zro-left *> pmap (`+ _) (inv negative-left) *> +-assoc)
  | join_+-left {a} {b} {c} => <=-antisymmetric (<=_+-cancel-left (negative a) $ =_<= (inv +-assoc *> pmap (`+ _) negative-left *> zro-left) <=∘ join-univ (<=_+-cancel-left a $ join-left <=∘ =_<= (inv zro-left *> pmap (`+ _) (inv negative-right) *> +-assoc)) (<=_+-cancel-left a $ join-right <=∘ =_<= (inv zro-left *> pmap (`+ _) (inv negative-right) *> +-assoc))) $ join-univ (<=_+ <=-refl join-left) (<=_+ <=-refl join-right)
  | ldistr>= {x} {y} {z} => =_<= (inv $ meet_+-right *> pmap2 (∧) (+-assoc *> pmap (x +) (negative-left {_} {y ∨ z}) *> zro-right) zro-left) <=∘ <=_+-cancel-left _ (=_<= (inv +-assoc *> pmap (`+ _) negative-left *> zro-left) <=∘ join-univ (<=_+-cancel-left _ $ =_<= meet_+-right <=∘ meet-monotone (=_<= +-assoc <=∘ <=_+ <=-refl (<=_+ <=-refl join-left <=∘ =_<= negative-left) <=∘ =_<= zro-right) (=_<= zro-left) <=∘ join-left <=∘ =_<= (inv (pmap (`+ _) negative-right *> zro-left) *> +-assoc)) (<=_+-cancel-left _ $ =_<= meet_+-right <=∘ meet-monotone (=_<= +-assoc <=∘ <=_+ <=-refl (<=_+ <=-refl join-right <=∘ =_<= negative-left) <=∘ =_<= zro-right) (=_<= zro-left) <=∘ join-right <=∘ =_<= (inv (pmap (`+ _) negative-right *> zro-left) *> +-assoc)))

  \lemma meet_negative {x y : E} : negative (x ∧ y) = negative x ∨ negative y
    => <=-antisymmetric (negative_<= (meet-univ (negative_<= join-left <=∘ =_<= negative-isInv) (negative_<= join-right <=∘ =_<= negative-isInv)) <=∘ =_<= negative-isInv) $ join-univ (negative_<= meet-left) (negative_<= meet-right)

  \lemma join_negative {x y : E} : negative (x ∨ y) = negative x ∧ negative y
    => <=-antisymmetric (meet-univ (negative_<= join-left) (negative_<= join-right)) $ =_<= (inv negative-isInv) <=∘ negative_<= (join-univ (=_<= (inv negative-isInv) <=∘ negative_<= meet-left) (=_<= (inv negative-isInv) <=∘ negative_<= meet-right))

  \lemma modularity {x y : E} : x + y = (x ∨ y) + (x ∧ y)
    => cancel-right (negative (x ∧ y)) $ pmap (_ +) meet_negative *> join_+-left *> pmap2 (∨) (+-comm *> inv +-assoc *> pmap (`+ y) negative-left *> zro-left) (+-assoc *> pmap (x +) negative-right *> zro-right) *> join-comm *> inv (+-assoc *> pmap (_ +) negative-right *> zro-right)

  \func abs (x : E) => x ∨ negative x

  \lemma abs>=id {x : E} : x <= abs x
    => join-left

  \lemma abs>=neg {x : E} : negative x <= abs x
    => join-right

  \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 (rewrite negative_zro in negative_<= x<=0)

  \lemma abs_abs {x : E} : abs (abs x) = abs x
    => <=-antisymmetric (join-univ <=-refl $ negative_<= abs>=id <=∘ abs>=neg) abs>=id

  \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 (y - x)
    => pmap abs (inv negative-isInv) *> abs_negative *> simplify

  \lemma abs_-left {x y : E} : abs x - abs y <= abs (x - y)
    => transport (_ <=) (+-assoc *> pmap (_ +) negative-right *> zro-right) $ <=_+ (transport (abs __ <= _) (+-assoc *> pmap (x +) negative-left *> zro-right) abs_+) <=-refl

  \lemma abs_-right {x y : E} : abs y - abs x <= abs (x - y)
    => transport (_ <=) abs_- abs_-left

  \lemma abs_zro : abs zro = zro
    => <=-antisymmetric (join-univ <=-refl $ rewrite negative_zro <=-refl) abs>=id

  \lemma abs_zro-ext {x : E} (p : abs x = zro) : x = zro
    => <=-antisymmetric (transport (_ <=) p join-left) $ transport2 (<=) negative_zro negative-isInv $ negative_<= $ transport (_ <=) p join-right

  \lemma abs>=_- {x y : E} : y - x <= abs (x - y)
    => transportInv (_ <=) negative_+ (later $ rewrite negative-isInv <=-refl) <=∘ abs>=neg

  \lemma abs-univ {x y z : E} (p : x - y <= z) (q : y - x <= z) : abs (x - y) <= z
    => join-univ p (=_<= negative_- <=∘ q)

  \type IsSolid (U : Set E) => ∀ {y} {x : U} (abs y <= abs x -> U y)
} \where {
    -- TODO: Make constructor classes
    \protected \class FromMeet \extends LatticeAbGroup
      | join a b => negative (negative a ∧ negative b)
      | join-left => =_<= (inv negative-isInv) <=∘ negative_<= meet-left
      | join-right => =_<= (inv negative-isInv) <=∘ negative_<= meet-right
      | join-univ x<=z y<=z => negative_<= (meet-univ (negative_<= x<=z) (negative_<= y<=z)) <=∘ =_<= negative-isInv

    \protected \class FromJoin \extends LatticeAbGroup
      | meet a b => negative (negative a ∨ negative b)
      | meet-left => negative_<= join-left <=∘ =_<= negative-isInv
      | meet-right => negative_<= join-right <=∘ =_<= negative-isInv
      | meet-univ z<=x z<=y => =_<= (inv negative-isInv) <=∘ negative_<= (join-univ (negative_<= z<=x) (negative_<= z<=y))
  }

\class AbsAbGroup \extends LatticeAbGroup {
  | abs>=0 {x : E} : 0 <= abs x

  \func part+ (x : E) => x ∨ 0

  \func part- (x : E) => negative x ∨ 0

  \lemma parts_join {x : E} : part+ x ∨ part- x = abs x
    => <=-antisymmetric (join-univ (join-univ abs>=id abs>=0) (join-univ abs>=neg abs>=0)) $ join-univ (join-left <=∘ join-left) (join-left <=∘ join-right)

  \lemma parts_meet {x : E} : part+ x ∧ part- x = 0
    => cancel-left (part+ x ∨ part- x) $ inv modularity *> parts_+ *> inv (zro-right *> parts_join)

  \lemma parts_+ {x : E} : part+ x + part- x = abs x
    => join_+-right *> pmap2 (∨) (join_+-left *> join-comm *> pmap2 (∨) zro-right negative-right) zro-left *> parts_join

  \lemma parts_- {x : E} : part+ x - part- x = x
    => cancel-right (part- x) $ +-assoc *> pmap (_ +) negative-left *> zro-right *> join-comm *> inv (join_+-left *> pmap2 (∨) negative-right zro-right)

  \lemma join_+-double {x y : E} : x + y <= (x + x) ∨ (y + y)
    => transport2 (x + __ <= __) zro-left (pmap (x +) join_+-right *> join_+-left *> pmap2 (x + __ ∨ __) (+-assoc *> pmap (x +) negative-left *> zro-right) (inv +-assoc *> pmap (`+ y) (pmap (x +) negative_- *> +-comm *> +-assoc *> pmap (y +) negative-left *> zro-right))) $ <=_+ <=-refl $ <=_+ abs>=0 <=-refl

  \lemma join_+-comm {x y : E} : (x ∨ y) + (x ∨ y) = (x + x) ∨ (y + y)
    => join_+-left *> pmap2 (∨) join_+-right join_+-right *> <=-antisymmetric (join-univ (join-univ join-left $ =_<= +-comm <=∘ join_+-double) (join-univ join_+-double join-right)) (join-univ (join-left <=∘ join-left) (join-right <=∘ join-right))

  \lemma join_*n {n : Nat} {x y : E} : n *n (x ∨ y) = (n *n x) ∨ (n *n y)
    => <=-antisymmetric (<=_+-cancel-right ((NatSemiring.pow 2 n -' n) *n (x ∨ y)) $ =_<= (inv *n-rdistr *> pmap (`*n _) (<=_exists $ NatSemiring.<=-less id<pow2) *> steps *> inv (pmap2 (∨) (inv *n-rdistr *> pmap (`*n _) (<=_exists $ NatSemiring.<=-less id<pow2)) (inv *n-rdistr *> pmap (`*n _) (<=_exists $ NatSemiring.<=-less id<pow2)))) <=∘ join-univ (<=_+ join-left $ *n_<= join-left) (<=_+ join-right $ *n_<= join-right)) $ join-univ (*n_<= join-left) (*n_<= join-right)
    \where {
      \private \lemma steps {k : Nat} {x y : E} : NatSemiring.pow 2 k *n (x ∨ y) = (NatSemiring.pow 2 k *n x) ∨ (NatSemiring.pow 2 k *n y) \elim k
        | 0 => zro-left *> inv (pmap2 (∨) zro-left zro-left)
        | suc k => *n-rdistr *> pmap2 (+) steps steps *> join_+-comm *> inv (pmap2 (∨) (pmap (`*n x) (NatSemiring.*-comm {_} {2}) *> *n-assoc *> +-assoc *> zro-left) (pmap (`*n y) (NatSemiring.*-comm {_} {2}) *> *n-assoc *> +-assoc *> zro-left))
    }

  \lemma abs_*n {n : Nat} {x : E} : n *n abs x = abs (n *n x)
    => join_*n *> pmap (_ ∨) *n_negative

  \lemma meet_*n {n : Nat} {x y : E} : n *n (x ∧ y) = (n *n x) ∧ (n *n y)
    => inv negative-isInv *> pmap negative (inv *n_negative *> pmap (n *n) meet_negative *> join_*n *> pmap2 (∨) *n_negative *n_negative *> inv meet_negative) *> negative-isInv
}

\class PosetSemiring \extends Semiring, PosetAbMonoid {
  | zro<=ide : 0 <= 1
  | <=_*_positive-left {x y z : E} (x<=y : x <= y) (z>=0 : 0 <= z) : x * z <= y * z
  | <=_*_positive-right {x y z : E} (x>=0 : 0 <= x) (y<=z : y <= z) : x * y <= x * z

  \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 <=_*_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 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_<= {n m : Nat} (p : n NatSemiring.<= m) : natCoef n <= natCoef m
    => rewrite (inv (<=_exists p), natCoef_+) $ transport (`<= _) zro-right $ <=_+ <=-refl natCoef>=0

  \lemma pow>=0 {a : E} {k : Nat} (a>=0 : 0 <= a) : 0 <= pow a k \elim k
    | 0 => zro<=ide
    | suc k => <=_*_positive_positive (pow>=0 a>=0) a>=0

  \lemma pow_<=-monotone {a b : E} {k : Nat} (a>=0 : 0 <= a) (a<=b : a <= b) : pow a k <= pow b k \elim k
    | 0 => <=-refl
    | suc k => <=_*_positive-right (pow>=0 a>=0) a<=b <=∘ <=_*_positive-left (pow_<=-monotone a>=0 a<=b) (a>=0 <=∘ a<=b)

  \lemma pow<=id {a : E} (a>=0 : 0 <= a) (a<=1 : a <= 1) {k : Nat} (k/=0 : k /= 0) : pow a k <= a \elim k
    | 0 => \case k/=0 idp
    | 1 => transportInv (`<= _) ide-left <=-refl
    | suc (suc k) => transport (_ <=) ide-right $ <=_*_positive-right (pow>=0 {_} {a} {suc k} a>=0) a<=1 <=∘ <=_*_positive-left (pow<=id a>=0 a<=1 suc/=0) (a>=0 <=∘ a<=1)

  \lemma pow>=id {a : E} (a>=1 : 1 <= a) {k : Nat} (k/=0 : k /= 0) : a <= pow a k \elim k
    | 0 => \case k/=0 idp
    | 1 => transportInv (a <=) ide-left <=-refl
    | suc (suc k) =>
      \have a>=0 => zro<=ide <=∘ a>=1
      \in transport (`<= _) ide-right $ <=_*_positive-right a>=0 a>=1 <=∘ <=_*_positive-left (pow>=id a>=1 suc/=0) a>=0

  \lemma pow<=1 {a : E} (a>=0 : 0 <= a) (a<=1 : a <= 1) {k : Nat} : pow a k <= 1 \elim k
    | 0 => <=-refl
    | suc k => pow<=id a>=0 a<=1 {suc k} (\case __) <=∘ a<=1

  \lemma pow_<=-degree {a : E} (a>=0 : 0 <= a) (a<=1 : a <= 1) {n k : Nat} (n<=k : n NatSemiring.<= k) : pow a k <= pow a n
    => rewrite (inv (<=_exists n<=k), pow_+) $ transport (_ <=) ide-right $ <=_*_positive-right (pow>=0 a>=0) $ pow<=1 a>=0 a<=1
}

\class PosetRing \extends PosetSemiring, Ring, PosetAbGroup
  | <=_*-positive {x y : E} (x>=0 : 0 <= x) (y>=0 : 0 <= y) : 0 <= x * y
  | <=_*_positive-left x<=y z>=0 => from>=0 $ transport (0 <=) rdistr_- $ <=_*-positive (to>=0 x<=y) z>=0
  | <=_*_positive-right x>=0 y<=z => from>=0 $ transport (0 <=) ldistr_- $ <=_*-positive x>=0 (to>=0 y<=z)