\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.StrictlyOrdered
\import Algebra.Pointed
\import Algebra.Semiring
\import Arith.Int
\import Arith.Rat
\import Arith.Real.LowerReal
\import Arith.Real.UpperReal
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta

\record InfReal \extends LowerReal, ExUpperReal {
  | LU-disjoint {q : Rat} : L q -> U q -> Empty
  | LU-located {q r : Rat} : q < r -> L q || U r
  | LU-focus-bound (B : Rat) {eps : Rat} : eps >  -> L B || Given (a : L) (U (a + eps))

  \default LU-located {q} {r} q<r => \case LU-focus-bound q {r - q} (RatField.pos_>0 q<r) \with {
    | byLeft p => byLeft p
    | byRight (s,Ls,Us+r-q) => \case LinearOrder.trichotomy q s \with {
      | less q<s => byLeft (L-closed Ls q<s)
      | equals q=s => byLeft (transportInv L q=s Ls)
      | greater s<q => byRight $ U-closed Us+r-q $ transport (_ <) (equation : q + (r - q) = r) (<_+-left (r - q) s<q)
    }
  }

  \default L-inh => \case LU-focus-bound  {} idp \with {
    | byLeft p => inP (,p)
    | byRight p => inP (p.,p.)
  }

  \default LU-focus-bound \as LU-focus-bound-impl (B : Rat) {eps : Rat} (eps>0 : eps > ) : L B || Given (a : L) (U (a + eps)) => \case L-inh, LU-located {\this} {B} {B + } linarith \with {
    | _, byLeft LB => byLeft LB
    | inP (q,Lq), byRight Ur =>
      \let | m r q => (r - q) * finv 
           | LU-less {q} {r} (Lq : L q) (Ur : U r) : q < r => \case LinearOrder.dec<_<= q r \with {
             | inl q<r => q<r
             | inr r<=q => absurd $ LU-disjoint Lq (U_<= Ur r<=q)
           }
           | r => B + 
      \in \case focus-iter (ratio  ) rat_<=-dec (\lam q r => \Sigma (L q) (U r)) (\lam q r (Lq,Ur) => \case LU-located (linarith (usingOnly (LU-less Lq Ur))) \with {
        | byLeft Lq+m => inP (q + m r q, r, (Lq+m,Ur), linarith)
        | byRight Ur-m => inP (q, r - m r q, (Lq,Ur-m), linarith)
      }) (iabs $ rat_ceiling $ finv eps * (r - q)) q r (Lq,Ur) \with {
        | inP (q',r',(Lq',Ur'),p) => byRight (q', Lq', U-closed Ur'
            \have | r-q>0 {q} {r} (Lq : L q) (Ur : U r) :  < r - q => linarith (usingOnly (LU-less Lq Ur))
                  | pr>0 => RatField.<_*_positive_positive (RatField.finv>0 eps>0) (r-q>0 Lq Ur)
                  | c>0 => fromInt_<.conv $ pr>0 <∘l rat_ceiling>=id
                  | s : (r' - q') * (finv eps * (r - q)) < r - q
                  => <_*_positive-right (r-q>0 Lq' Ur') (rat_ceiling>=id <∘r fromInt_<= (=_<= $ inv $ iabs.ofPos $ LinearOrder.<_<= c>0) <∘r pow>id _) <∘l p
                  | t => transport (_ <) (pmap (_ *) RatField.finv_* *> inv *-assoc *> pmap (`* _) (finv-right $ RatField.>_/= $ r-q>0 Lq Ur) *> ide-left *> RatField.finv_finv) (RatField.<_rotate-right pr>0 s)
            \in linarith (usingOnly t))
      }
  }

  \lemma LU-less {q r : Rat} (Lq : L q) (Ur : U r) : q < r
    => \case LinearOrder.dec<_<= q r \with {
      | inl q<r => q<r
      | inr r<=q => absurd $ LU-disjoint Lq (U_<= Ur r<=q)
    }
} \where {
  \use \coerce fromRat (x : Rat) : InfReal \cowith
    | LowerReal => LowerReal.fromRat x
    | ExUpperReal => ExUpperReal.fromRat x
    | LU-disjoint q<x x<q => <-irreflexive (q<x <∘ x<q)
    | LU-focus-bound B {eps} eps>0 => byRight (x - eps * finv , linarith, linarith)

  \lemma pow>id (n : Nat) : Monoid.pow (ratio  ) n > n \elim n
    |  => idp
    |  => idp
    |  => idp
    | suc (suc (suc n)) => linarith <∘r <_*_positive-left (pow>id (suc (suc n))) idp

  \lemma focus-iter (rat : Rat) (rat>=0 :  <= rat) (P : Rat -> Rat -> \Prop) (f : \Pi (q r : Rat) -> P q r -> ∃ (q' r' : P) ((r' - q') * rat <= r - q)) (n : Nat) (q r : Rat) (Pqr : P q r) : ∃ (q' r' : P) ((r' - q') * Monoid.pow rat n <= r - q) \elim n
    |  => inP (q, r, Pqr, transportInv (`<= _) ide-right <=-refl)
    | suc n => \case f q r Pqr \with {
      | inP (q',r',Pq'r',c) => \case focus-iter rat rat>=0 P f n q' r' Pq'r' \with {
        | inP (q'',r'',Pq''r'',d) => inP (q'', r'', Pq''r'', =_<= (inv *-assoc) <=∘ RatField.<=_*_positive-left d rat>=0 <=∘ c)
      }
    }

  \lemma real-ext {x y : InfReal} (p : \Pi {a : Rat} -> x.L a <-> y.L a) : x = y
    => exts (\lam a => ext p, \lam b =>
        \have lem {x y : InfReal} (p : \Pi {a : Rat} -> x.L a <-> y.L a) (x<b : x.U b) : y.U b => \case U-rounded x<b \with {
          | inP (a,x<a,a<b) => \case y.LU-located a<b \with {
            | byLeft a<y => absurd $ x.LU-disjoint {a} (p. a<y) x<a
            | byRight y<b => y<b
          }
        }
        \in ext (lem p, lem (\lam {_} => (p.,p.))))

  \lemma real-lower-ext {x y : InfReal} (p : x = {LowerReal} y) : x = y
    => real-ext \lam {a} => transport (\lam (y : LowerReal) => x.L a <-> y.L a) p <->refl
}

\instance InfRealAbMonoid : LinearlyBiorderedAbMonoid InfReal
  | zro => InfReal.fromRat 
  | + => +
  | zro-left => InfReal.real-lower-ext $ +-lower *> {LowerReal} zro-left
  | +-comm => InfReal.real-lower-ext $ +-lower *> {LowerReal} +-comm *> {LowerReal} inv {LowerReal} +-lower
  | +-assoc => InfReal.real-lower-ext $ +-lower *> {LowerReal} pmap {LowerReal} (LowerRealAbMonoid.`+ _) +-lower *> {LowerReal} +-assoc *> {LowerReal} pmap (_ LowerRealAbMonoid.+) (inv {LowerReal} +-lower) *> {LowerReal} inv {LowerReal} +-lower
  | < => <
  | <-irreflexive (inP (a,x<a,a<x)) => LU-disjoint a<x x<a
  | <-transitive (inP (a,x<a,a<y)) (inP (b,y<b,b<z)) => inP (a, x<a, L-closed b<z $ InfReal.LU-less a<y y<b)
  | meet => meet
  | meet-left (inP (a,x<a,a<xy)) => absurd $ LU-disjoint (meet_L. a<xy). x<a
  | meet-right (inP (a,y<a,a<xy)) => absurd $ LU-disjoint (meet_L. a<xy). y<a
  | meet-univ z<=x z<=y (inP (a,xy<a,a<z)) => \case meet_U. xy<a \with {
    | byLeft x<a => z<=x $ inP (a,x<a,a<z)
    | byRight y<a => z<=y $ inP (a,y<a,a<z)
  }
  | join => join
  | join-left (inP (a,xy<a,a<x)) => LU-disjoint a<x (join_U. xy<a).
  | join-right (inP (a,xy<a,a<y)) => LU-disjoint a<y (join_U. xy<a).
  | join-univ x<=z y<=z (inP (a,z<a,a<xy)) => \case join_L. a<xy \with {
    | byLeft a<x => x<=z $ inP (a,z<a,a<x)
    | byRight a<y => y<=z $ inP (a,z<a,a<y)
  }
  | <-comparison y (inP (a,x<a,a<z)) => \case L-rounded a<z \with {
    | inP (b,b<z,a<b) => \case LU-located a<b \with {
      | byLeft a<y => byLeft $ inP (a,x<a,a<y)
      | byRight b<y => byRight $ inP (b,b<y,b<z)
    }
  }
  | <-connectedness p q => InfReal.real-ext \lam {a} => (\lam a<x => \case L-rounded a<x \with {
    | inP (b,b<x,a<b) => \case LU-located a<b \with {
      | byLeft a<y => a<y
      | byRight y<b => absurd $ q $ inP (b,y<b,b<x)
    }
  }, \lam a<y => \case L-rounded a<y \with {
    | inP (b,b<y,a<b) => \case LU-located a<b \with {
      | byLeft a<x => a<x
      | byRight x<b => absurd $ p $ inP (b,x<b,b<y)
    }
  })
  | <=_+ a<=b c<=d (inP (x,b+d<x,x<a+c)) => \case +_L. x<a+c, +_U. b+d<x \with {
    | inP (q,q<a,r,r<c,x<q+r), inP (s,b<s,t,d<t,s+t<x) => <-irreflexive $ x<q+r <∘ RatField.<_+ (InfReal.LU-less q<a $ <=_U. a<=b b<s) (InfReal.LU-less r<c $ <=_U. c<=d d<t) <∘ s+t<x
  }
  | meet_+-left => InfReal.real-lower-ext $ +-lower *> {LowerReal} pmap (_ LowerRealAbMonoid.+) meet-lower *> {LowerReal} meet_+-left *> {LowerReal} inv (pmap2 LowerRealAbMonoid.meet +-lower +-lower) *> {LowerReal} inv {LowerReal} meet-lower
  | join_+-left => InfReal.real-lower-ext $ +-lower *> {LowerReal} pmap (_ LowerRealAbMonoid.+) join-lower *> {LowerReal} join_+-left *> {LowerReal} inv (pmap2 LowerRealAbMonoid.join +-lower +-lower) *> {LowerReal} inv {LowerReal} join-lower
  \where {
    \sfunc \infixl  + (x y : InfReal) : InfReal \cowith
      | LowerReal => x LowerRealAbMonoid.+ y
      | ExUpperReal => x ExUpperReal.+ y
      | LU-disjoint r1 r2 => \case LowerRealAbMonoid.+_L. r1, ExUpperReal.+_U. r2 \with {
        | inP (a,a<x,b,b<y,q<a+b), inP (c,x<c,d,y<d,c+d<q) => linarith (x.LU-less a<x x<c, y.LU-less b<y y<d)
      }
      | LU-focus-bound B {eps} eps>0 =>
        \have eps/4>0 :  RatField.< eps * ratio   => linarith
        \in \case x.LU-focus-bound  eps/4>0, y.LU-focus-bound B eps/4>0 \with {
          | byLeft x>1, byLeft y>B => byLeft $ LowerRealAbMonoid.+_L. $ inP (, x>1, B, y>B, linarith)
          | byLeft _, byRight (y',y'<y,y<y'+eps/4) => \case x.LU-focus-bound (B - y' RatField.+ ) eps/4>0 \with {
            | byLeft B-y'+1<x => byLeft $ LowerRealAbMonoid.+_L. $ inP (_, B-y'+1<x, y', y'<y, linarith)
            | byRight (x',x'<x,x<x'+eps/4) => byRight (x' RatField.+ y' - eps * ratio  , LowerRealAbMonoid.+_L. $ inP (x', x'<x, y', y'<y, linarith), ExUpperReal.+_U. $ inP (_, x<x'+eps/4, _, y<y'+eps/4, linarith))
          }
          | byRight (x',x'<x,x<x'+eps/4), byLeft _ => \case y.LU-focus-bound (B - x' RatField.+ ) eps/4>0 \with {
            | byLeft r => byLeft $ LowerRealAbMonoid.+_L. $ inP (x', x'<x, _, r, linarith)
            | byRight (y',y'<y,y<y'+eps/4) => byRight (x' RatField.+ y' - eps * ratio  , LowerRealAbMonoid.+_L. $ inP (x', x'<x, y', y'<y, linarith), ExUpperReal.+_U. $ inP (_, x<x'+eps/4, _, y<y'+eps/4, linarith))
          }
          | byRight (x',x'<x,x<x'+eps/4), byRight (y',y'<y,y<y'+eps/4) => byRight (x' RatField.+ y' - eps * ratio  , LowerRealAbMonoid.+_L. $ inP (x', x'<x, y', y'<y, linarith), ExUpperReal.+_U. $ inP (_, x<x'+eps/4, _, y<y'+eps/4, linarith))
        }

    \lemma +-lower {x y : InfReal} : x + y = {LowerReal} x LowerRealAbMonoid.+ y
      => \peval _ + _

    \lemma +-rat {x y : Rat} : InfReal.fromRat x + InfReal.fromRat y = InfReal.fromRat (x RatField.+ y)
      => InfReal.real-ext \lam {a} => <->trans +_L (\lam (inP (b,b<x,c,c<y,a<b+c)) => linarith, \lam a<x+y =>
          \let eps => (x RatField.+ y - a) * ratio  
          \in inP (x - eps, linarith, y - eps, linarith, linarith))

    \lemma +_L {x y : InfReal} {a : Rat} : InfReal.L {x + y} a <-> ∃ (b : x.L) (c : y.L) (a RatField.< b RatField.+ c)
      => <->trans (<->_=. $ pmap {LowerReal} (\lam t => InfReal.L {t} a) +-lower) LowerRealAbMonoid.+_L

    \lemma +_L_<= {x y : InfReal} {a b : Rat} (b<x : x.L b) {c : Rat} (c<y : y.L c) (a<=b+c : a RatField.<= b RatField.+ c) : InfReal.L {x + y} a
      => \case L-rounded b<x \with {
        | inP (b',x<b',b<b') => +_L. $ inP (b', x<b', c, c<y, a<=b+c <∘r <_+-left c b<b')
      }

    \lemma +-upper {x y : InfReal} : x + y = x ExUpperReal.+ y
      => \peval _ + _

    \lemma +_U {x y : InfReal} {a : Rat} : InfReal.U {x + y} a <-> ∃ (b : x.U) (c : y.U) (b RatField.+ c RatField.< a)
      => <->trans (<->_=. $ pmap (\lam t => InfReal.U {t} a) +-upper) ExUpperReal.+_U

    \lemma +_U_<= {x y : InfReal} {a b : Rat} (x<b : x.U b) {c : Rat} (y<c : y.U c) (b+c<=a : b RatField.+ c RatField.<= a) : InfReal.U {x + y} a
      => \case U-rounded x<b \with {
        | inP (b',x<b',b'<b) => +_U. $ inP (b', x<b', c, y<c, <_+-left c b'<b <∘l b+c<=a)
      }

    \type \infix  < (x y : InfReal) => ∃ (a : Rat) (x.U a) (y.L a)

    \lemma <=_L {x y : InfReal} : Not (y < x) <-> ∀ {a : x.L} (y.L a)
      => (\lam p a<x => \case L-rounded a<x \with {
        | inP (b,b<x,a<b) => \case y.LU-located a<b \with {
          | byLeft a<y => a<y
          | byRight y<b => $ absurd $ p $ inP (b,y<b,b<x)
        }
      }, \lam p (inP (a,y<a,x<a)) => y.LU-disjoint (p x<a) y<a)

    \lemma <=_U {x y : InfReal} : Not (y < x) <-> ∀ {b : y.U} (x.U b)
      => (\lam p y<b => \case U-rounded y<b \with {
        | inP (a,y<a,a<b) => \case x.LU-located a<b \with {
          | byLeft a<x => absurd $ p $ inP (a,y<a,a<x)
          | byRight x<b => x<b
        }
      }, \lam p (inP (a,y<a,x<a)) => x.LU-disjoint x<a (p y<a))

    \sfunc meet (x y : InfReal) : InfReal \cowith
      | LowerReal => LowerRealAbMonoid.meet x y
      | ExUpperReal => ExUpperReal.meet x y
      | LU-disjoint s r => \case ExUpperReal.meet_U. r \with {
        | byLeft x<q => <-irreflexive (x.LU-less (LowerRealAbMonoid.meet_L. s). x<q)
        | byRight y<q => <-irreflexive (y.LU-less (LowerRealAbMonoid.meet_L. s). y<q)
      }
      | LU-located q<r => \case x.LU-located q<r, y.LU-located q<r \with {
        | byLeft q<x, byLeft q<y => byLeft $ LowerRealAbMonoid.meet_L. (q<x,q<y)
        | _, byRight y<r => byRight $ ExUpperReal.meet_U. (byRight y<r)
        | byRight x<r, _ => byRight $ ExUpperReal.meet_U. (byLeft x<r)
      }

    \lemma meet-lower {x y : InfReal} : meet x y = {LowerReal} LowerRealAbMonoid.meet x y
      => \peval meet _ _

    \lemma meet_L {x y : InfReal} {a : Rat} : InfReal.L {meet x y} a <-> (\Sigma (x.L a) (y.L a))
      => rewrite (\peval meet x y, \peval LowerRealAbMonoid.meet x y) <->refl

    \lemma meet_U {x y : InfReal} {a : Rat} : InfReal.U {meet x y} a <-> x.U a || y.U a
      => rewrite (\peval meet x y, \peval ExUpperReal.meet x y) <->refl

    \sfunc join (x y : InfReal) : InfReal \cowith
      | LowerReal => LowerRealAbMonoid.join x y
      | ExUpperReal => ExUpperReal.join x y
      | LU-disjoint e s => \case LowerRealAbMonoid.join_L. e \with {
        | byLeft q<x => <-irreflexive $ x.LU-less q<x (ExUpperReal.join_U. s).
        | byRight q<y => <-irreflexive $ y.LU-less q<y (ExUpperReal.join_U. s).
      }
      | LU-located q<r => \case x.LU-located q<r, y.LU-located q<r \with {
        | byLeft q<x, _ => byLeft $ LowerRealAbMonoid.join_L. (byLeft q<x)
        | _, byLeft q<y => byLeft $ LowerRealAbMonoid.join_L. (byRight q<y)
        | byRight x<r, byRight y<r => byRight $ ExUpperReal.join_U. (x<r,y<r)
      }

    \lemma join-lower {x y : InfReal} : join x y = {LowerReal} LowerRealAbMonoid.join x y
      => \peval join _ _

    \lemma join_L {x y : InfReal} {a : Rat} : InfReal.L {join x y} a <-> x.L a || y.L a
      => rewrite (\peval join x y, \peval LowerRealAbMonoid.join x y) <->refl

    \lemma join_U {x y : InfReal} {a : Rat} : InfReal.U {join x y} a <-> (\Sigma (x.U a) (y.U a))
      => rewrite (\peval join x y, \peval ExUpperReal.join x y) <->refl

    \lemma zro<ide : InfReal.fromRat  < InfReal.fromRat 
      => inP (ratio  , idp, idp)

    \lemma <_L {a : Rat} {x : InfReal} : (a : InfReal) < x <-> x.L a
      => (\lam (inP (b,a<b,b<x)) => L-closed b<x a<b, \lam a<x => \case L-rounded a<x \with {
        | inP (b,b<x,a<b) => inP (b,a<b,b<x)
      })

    \lemma <_U {a : Rat} {x : InfReal} : x < a <-> x.U a
      => (\lam (inP (b,x<b,b<a)) => U-closed x<b b<a, \lam x<a => \case U-rounded x<a \with {
        | inP (b,x<b,b<a) => inP (b,x<b,b<a)
      })

    \lemma <_+ {a b c d : InfReal} (p : a < c) (q : b < d) : a + b < c + d \elim p, q
      | inP (q,a<q,q<c), inP (r,b<r,r<d) => inP (q RatField.+ r, +_U_<= a<q b<r <=-refl, +_L_<= q<c r<d <=-refl)
  }

\lemma inf-real_<_LowerReal {x y : InfReal} : x < y <-> x LowerRealAbMonoid.< y
  => (\lam (inP (a,x<a,a<y)) => inP (a, a<y, \lam {b} b<x => x.LU-less b<x x<a), \lam (inP (b,b<y,x<=b)) => \case L-rounded b<y \with {
    | inP (a,a<y,b<a) => inP (a, \case x.LU-located b<a \with {
      | byLeft b<x => absurd $ <-irreflexive (x<=b b<x)
      | byRight x<a => x<a
    }, a<y)
  })