\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.QModule
\import Arith.Int
\import Arith.Nat
\import Arith.Rat
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set

\class PosetDivAbGroup \extends PosetAbGroup, TorsionFreeGroup {
  | <=_*n-div {n : Nat} (n/=0 : n /= ) {a : E} :  <= n *n a ->  <= a
  \default noTorsion n/=0 na=0 => <=-antisymmetric (negative-to<=0 $ <=_*n-div n/=0 $ transportInv ( <=) *n_negative $ negative>=0 $ =_<= na=0) (<=_*n-div n/=0 $ =_<= $ inv na=0)

  \lemma <=_*n-cancel-left {n : Nat} (n/=0 : n /= ) {a b : E} (na<=nb : n *n a <= n *n b) : a <= b
    => from>=0 $ <=_*n-div n/=0 $ transportInv ( <=) *n-ldistr_- (to>=0 na<=nb)
}

\class PosetQModule \extends QModule, PosetDivAbGroup {
  \lemma *q_>=0 {q : Rat} (q>=0 : RatField.zro RatField.<= q) {a : E} (a>=0 :  <= a) :  <= q *q a
    => <=_*n-div ratDenom/=0 $ transport ( <=) (pmap (`*i a) (iabs.ofPos $ <=_ratNom.conv q>=0) *> inv *q_*i *> pmap (`*q a) (inv rat*denom-left) *> *q-assoc *> *q_*n) (*n_>=0 a>=0)

  \lemma *q_>=0-cancel {q : Rat} (q>0 :  < q) {a : E} (qa>=0 :  <= q *q a) :  <= a
    => transport ( <=) (inv *q-assoc *> pmap (`*q a) (RatField.finv-left $ RatField.>_/= q>0) *> ide_*q) $ *q_>=0 (<=-less $ RatField.finv>0 q>0) qa>=0

  \lemma <=_*q-left {q r : Rat} (q<=r : q RatField.<= r) {a : E} (a>=0 :  <= a) : q *q a <= r *q a
    => from>=0 $ transport ( <=) toRatModule.*c-rdistr_- $ *q_>=0 (RatField.to>=0 q<=r) a>=0

  \lemma <=_*q-right {q : Rat} (q>=0 : RatField.zro RatField.<= q) {a b : E} (a<=b : a <= b) : q *q a <= q *q b
    => from>=0 $ transport (_ <=) toRatModule.*c-ldistr_- $ *q_>=0 q>=0 (to>=0 a<=b)

  \lemma <=_*q-cancel-left {q : Rat} (q>0 :  < q) {a b : E} (qa<=qb : q *q a <= q *q b) : a <= b
    => from>=0 $ *q_>=0-cancel q>0 $ transportInv ( <=) toRatModule.*c-ldistr_- (to>=0 qa<=qb)

  \lemma <=_*q-rotate-left {q : Rat} (q>0 :  < q) {a b : E} (a<=qb : a <= RatField.finv q *q b) : q *q a <= b
    => transport (__ *q a <= b) RatField.finv_finv $ <=_*q-rotate_finv-left (RatField.finv>0 q>0) a<=qb

  \lemma <=_*q-rotate-right {q : Rat} (q>0 :  < q) {a b : E} (p : RatField.finv q *q a <= b) : a <= q *q b
    => transport (`<= _) (inv *q-assoc *> pmap (`*q a) (RatField.finv-right $ RatField.>_/= q>0) *> ide_*q) $ <=_*q-right (<=-less q>0) p

  \lemma <=_*q-rotate_finv-left {q : Rat} (q>0 :  < q) {a b : E} (a<=qb : a <= q *q b) : RatField.finv q *q a <= b
    => <=_*q-right (<=-less $ RatField.finv>0 q>0) a<=qb <=∘ =_<= (inv *q-assoc *> pmap (`*q b) (RatField.finv-left $ RatField.>_/= q>0) *> ide_*q)
}

\class RieszSpace \extends PosetQModule, AbsAbGroup, LatticeAbGroup.FromJoin {
  -- <=_*n-div is equivalent to conjunction of noTorsion and abs>=0.
  \default abs>=0 => <=_*n-div {_} {} suc/=0 $ rewrite zro-left $ transportInv ( <=) join_+-left $ transportInv ( <=) join_+-right (=_<= (inv negative-left) <=∘ join-right) <=∘ join-left
  \default <=_*n-div n/=0 na>=0 => transport ( <=) (noTorsion-div n/=0 (abs_*n *> abs-ofPos na>=0)) abs>=0

  \lemma join_*q {q : Rat} (q>=0 : RatField.zro RatField.<= q) {x y : E} : q *q (x ∨ y) = (q *q x) ∨ (q *q y)
    => noTorsion-div ratDenom/=0 $ inv *q_*n *> inv *q-assoc *> pmap (`*q _) rat*denom-left *> *q_*i *> pmap (`*i _) (inv $ iabs.ofPos $ <=_ratNom.conv q>=0) *> join_*n *> pmap2 (∨) (pmap (`*i x) (iabs.ofPos $ <=_ratNom.conv q>=0) *> inv *q_*i *> pmap (`*q x) (inv rat*denom-left) *> *q-assoc *> *q_*n) (pmap (`*i y) (iabs.ofPos $ <=_ratNom.conv q>=0) *> inv *q_*i *> pmap (`*q y) (inv rat*denom-left) *> *q-assoc *> *q_*n) *> inv join_*n

  \lemma abs_*q {q : Rat} (q>=0 : RatField.zro RatField.<= q) {x : E} : abs (q *q x) = q *q abs x
    => inv $ join_*q q>=0 *> pmap (_ ∨) toRatModule.*c_negative-right

  \lemma meet_*q {q : Rat} {x y : E} (q>=0 : RatField.zro RatField.<= q) : q *q (x ∧ y) = (q *q x) ∧ (q *q y)
    => inv negative-isInv *> pmap negative (inv toRatModule.*c_negative-right *> pmap (q *q) meet_negative *> join_*q q>=0 *> pmap2 (∨) toRatModule.*c_negative-right toRatModule.*c_negative-right *> inv meet_negative) *> negative-isInv

  \lemma join_abs {x y : E} : x ∨ y = ratio   *q (x + y + abs (x - y))
    => *q-cancel {_} {} /=-dec $ *q_*2 *> join_+-comm *> pmap2 (∨) equation.abGroup equation.abGroup *> inv join_+-left *> inv ide_*q *> *q-assoc

  \lemma meet_abs {x y : E} : x ∧ y = ratio   *q (x + y - abs (x - y))
    => inv negative-isInv *> pmap negative (meet_negative *> join_abs) *> inv toRatModule.*c_negative-right *> pmap (_ *q) (later $ rewrite (pmap abs (pmap (_ +) negative-isInv *> +-comm) *> abs_-) equation.abGroup)
} \where {
  \func fromAbs {A : PosetQModule} (abs : \Pi (a : A) -> ∃ (b : A) (a <= b) (negative a <= b) ∀ {c} (a <= c -> negative a <= c -> b <= c)) : RieszSpace \cowith
    | PosetQModule => A
    | join => join
    | join-left => transportInv (_ <=) (\peval join _ _) $ A.<=_*q-cancel-left {} idp $ transport2 (<=) (inv A.*q_*2) (inv +-assoc *> inv A.ide_*q *> A.*q-assoc) $ <=_+ <=-refl $ =_<= equation.abGroup <=∘ <=_+ <=-refl (getAbs _).
    | join-right => transportInv (_ <=) (\peval join _ _) $ A.<=_*q-cancel-left {} idp $ transport2 (<=) (inv A.*q_*2) (inv +-assoc *> pmap (`+ _) +-comm *> inv A.ide_*q *> A.*q-assoc) $ <=_+ <=-refl $ =_<= equation.abGroup <=∘ <=_+ <=-refl (getAbs _).
    | join-univ {x} {y} x<=z y<=z => transportInv (`<= _) (\peval join _ _) $ A.<=_*q-cancel-left {} idp $ transport2 (<=) (inv A.ide_*q *> A.*q-assoc) (inv A.*q_*2) $ A.<=_+-cancel-left (negative (x + y)) $ transportInv (`<= _) (inv +-assoc *> pmap (`+ _) negative-left *> zro-left) $ (getAbs _).
      -- TODO: Use solver for PosetAbGroup
      (A.from>=0 $ transport (A.zro <=) equation.abGroup $ A.<=_+-positive (A.to>=0 x<=z) (A.to>=0 x<=z))
      (A.from>=0 $ transport (A.zro <=) equation.abGroup $ A.<=_+-positive (A.to>=0 y<=z) (A.to>=0 y<=z))
    \where {
      \private \lemma getAbs (a : A) : Given (b : A) (a <= b) (negative a <= b) ∀ {c} (a <= c -> negative a <= c -> b <= c)
        => TruncP.remove (\lam s s' => ext $ <=-antisymmetric (s. s'. s'.) (s'. s. s.)) (abs a)

      \protected \sfunc join (a b : A) : A
        => ratio   A.*q (a + b + (getAbs (a - b)).)
    }
}