{-# OPTIONS --type-in-type
   #-}

open import NeilPrelude
open import Logic

module PosReal where

open import StrictPosReal public

--------------------------------------------------------

infix  3  _<ℜ₀_ _≤ℜ₀_ _>ℜ₀_ _≥ℜ₀_

data ℜ₀ : Set where
  O   : ℜ₀
  _>0 : ℜ⁺  ℜ₀

_<ℜ₀_  : ℜ₀  ℜ₀  Set
_    <ℜ₀ O     = False
O  <ℜ₀ _ >0    = True
x >0 <ℜ₀ y >0  = x <ℜ⁺ y

ı₀ : ℜ₀
ı₀ = ı⁺ >0 

--------------------------------------------------------

lem-ℜ₀-eq : {x y : ℜ⁺}  x >0  y >0  x  y
lem-ℜ₀-eq refl = refl

lem-ℜ₀-neq : {x : ℜ⁺}  Not (O  x >0)
lem-ℜ₀-neq ()

>0-cong : {x y : ℜ⁺}  x  y  x >0  y >0
>0-cong = cong _>0

>0-neq-cong : {x y : ℜ⁺}  Not (x  y)  Not (x >0  y >0)
>0-neq-cong n refl = n refl

--------------------------------------------------------

<ℜ₀-trans : Transitive _<ℜ₀_
<ℜ₀-trans {_} {_} {O} p ()
<ℜ₀-trans {_} {O} {_ >0} () q
<ℜ₀-trans {O} {_ >0} {_ >0} p q = _
<ℜ₀-trans {_ >0} {_ >0} {_ >0} p q = <ℜ⁺-trans p q

<ℜ₀-trich : Trichotomous _<ℜ₀_
<ℜ₀-trich {O} {O} = inl (refl , id , id)
<ℜ₀-trich {O} {y >0} = inrl (lem-ℜ₀-neq , _ , id)
<ℜ₀-trich {x >0} {O} = inrr (lem-ℜ₀-neq  sym , id , _)
<ℜ₀-trich {x >0} {y >0} with <ℜ⁺-trich {x} {y}
... | inl p       = inl (first >0-cong p)
... | inr (inl p) = inrl (first >0-neq-cong p)
... | inr (inr p) = inrr (first >0-neq-cong p)

--------------------------------------------------------

import StrictTotalOrder
module STOℜ₀ = StrictTotalOrder _<ℜ₀_ <ℜ₀-trans <ℜ₀-trich
open STOℜ₀

Compareℜ₀ : Rel ℜ₀
Compareℜ₀ = OrdCompare

CompareLeqℜ₀ : Rel ℜ₀
CompareLeqℜ₀ = OrdCompareLeq

CompareGeqℜ₀ : Rel ℜ₀
CompareGeqℜ₀ = OrdCompareGeq

compareℜ₀ : (x y : ℜ₀)  Compareℜ₀ x y
compareℜ₀ = compare

compareLeqℜ₀ : (x y : ℜ₀)  CompareLeqℜ₀ x y
compareLeqℜ₀ = compareLeq

compareGeqℜ₀ : (x y : ℜ₀)  CompareGeqℜ₀ x y
compareGeqℜ₀ = compareGeq

_>ℜ₀_ : Rel ℜ₀
_>ℜ₀_ = _>_

_≤ℜ₀_ : Rel ℜ₀
_≤ℜ₀_ = _≤_ 

_≥ℜ₀_ : Rel ℜ₀
_≥ℜ₀_ = _≥_ 

<ℜ₀-irreflexive : Irreflexive _<ℜ₀_
<ℜ₀-irreflexive = irreflex

<ℜ₀-asym : Asymmetric _<ℜ₀_
<ℜ₀-asym = asym

≤ℜ₀-antisym : Antisymmetric _≤ℜ₀_
≤ℜ₀-antisym = antisymmetric

≤ℜ₀-refl : Reflexive _≤ℜ₀_
≤ℜ₀-refl = reflexive

≤ℜ₀-trans : Transitive _≤ℜ₀_
≤ℜ₀-trans = ≤-trans

<≤ℜ₀-trans : Trans _<ℜ₀_ _≤ℜ₀_ _<ℜ₀_
<≤ℜ₀-trans = <≤-trans

≤<ℜ₀-trans : Trans _≤ℜ₀_ _<ℜ₀_ _<ℜ₀_
≤<ℜ₀-trans = ≤<-trans

<≤ℜ₀-asym : {x y : ℜ₀}  x <ℜ₀ y  Not (y ≤ℜ₀ x)
<≤ℜ₀-asym = <≤-asym

≤<ℜ₀-asym : {x y : ℜ₀}  x ≤ℜ₀ y  Not (y <ℜ₀ x)
≤<ℜ₀-asym = ≤<-asym

--------------------------------------------------------

≤ℜ₀-min : {x : ℜ₀}  O ≤ℜ₀ x
≤ℜ₀-min {O}    = inr refl
≤ℜ₀-min {_ >0} = inl _

-----------------------------------------------------------------

<ℜ₀-subst : {x₁ y₁ x₂ y₂ : ℜ₀}  x₁  x₂  y₁  y₂  x₁ <ℜ₀ y₁  x₂ <ℜ₀ y₂
<ℜ₀-subst refl refl = id

<ℜ₀-substL : {x₁ x₂ y : ℜ₀}  x₁  x₂  x₁ <ℜ₀ y  x₂ <ℜ₀ y
<ℜ₀-substL refl = id

<ℜ₀-substR : {x y₁ y₂ : ℜ₀}  y₁  y₂  x <ℜ₀ y₁  x <ℜ₀ y₂
<ℜ₀-substR refl = id

≤ℜ₀-subst : {x₁ y₁ x₂ y₂ : ℜ₀}  x₁  x₂  y₁  y₂  x₁ ≤ℜ₀ y₁  x₂ ≤ℜ₀ y₂
≤ℜ₀-subst refl refl = id

≤ℜ₀-substL : {x₁ x₂ y : ℜ₀}  x₁  x₂  x₁ ≤ℜ₀ y  x₂ ≤ℜ₀ y
≤ℜ₀-substL refl = id

≤ℜ₀-substR : {x y₁ y₂ : ℜ₀}  y₁  y₂  x ≤ℜ₀ y₁  x ≤ℜ₀ y₂
≤ℜ₀-substR refl = id

-----------------------------------------------------------------

lem-ℜ⁺-leq : {x y : ℜ⁺}  (x >0) ≤ℜ₀ (y >0)  (x ≤ℜ⁺ y)
lem-ℜ⁺-leq = right lem-ℜ₀-eq

-----------------------------------------------------------------


infixl 10 _₀+₀_ _₀+⁺_ _⁺+₀_

_₀+₀_ : ℜ₀  ℜ₀  ℜ₀
O      ₀+₀ y      = y
x      ₀+₀ O      = x
(x >0) ₀+₀ (y >0) = (x ⁺+⁺ y) >0

_₀+⁺_ : ℜ₀  ℜ⁺  ℜ⁺
O      ₀+⁺ y  =  y
(x >0) ₀+⁺ y  =  x ⁺+⁺ y

_⁺+₀_ : ℜ⁺  ℜ₀  ℜ⁺
x ⁺+₀ O       =  x
x ⁺+₀ (y >0)  =  x ⁺+⁺ y

-----------------------------------------------------------------

₀+₀-comm : {x y : ℜ₀}  (x ₀+₀ y)  (y ₀+₀ x)
₀+₀-comm {O} {O}        = refl
₀+₀-comm {O} {y >0}     = refl
₀+₀-comm {x >0} {O}     = refl
₀+₀-comm {x >0} {y >0}  = >0-cong ⁺+⁺-comm

-----------------------------------------------------------------

lem-ℜ₀-+-<-cancellativeL : {x y z : ℜ₀}  (p : x <ℜ₀ y)  x ₀+₀ z <ℜ₀ y ₀+₀ z
lem-ℜ₀-+-<-cancellativeL {x} {O} ()
lem-ℜ₀-+-<-cancellativeL {O} {y >0} {O} _ = _
lem-ℜ₀-+-<-cancellativeL {O} {y >0} {z >0} _ = lem-ℜ⁺-+-<-increasing
lem-ℜ₀-+-<-cancellativeL {x >0} {y >0} {O} p = p
lem-ℜ₀-+-<-cancellativeL {x >0} {y >0} {z >0} p = lem-ℜ⁺-+-<-cancellativeL p

lem-ℜ₀-+-<-cancellativeR : {x y z : ℜ₀}  (p : y <ℜ₀ z)  x ₀+₀ y <ℜ₀ x ₀+₀ z
lem-ℜ₀-+-<-cancellativeR {x} {y} {z} = <ℜ₀-subst (₀+₀-comm {y}) (₀+₀-comm {z})  lem-ℜ₀-+-<-cancellativeL {y} {z} {x}

-----------------------------------------------------------------

lem-ℜ₀-+-≤-increasing : {x : ℜ₀}  (y : ℜ₀)  x ≤ℜ₀ (y ₀+₀ x)
lem-ℜ₀-+-≤-increasing {O} _         = ≤ℜ₀-min
lem-ℜ₀-+-≤-increasing {x >0} O      = ≤ℜ₀-refl
lem-ℜ₀-+-≤-increasing {x >0} (y >0) = inl lem-ℜ⁺-+-<-increasing

lem-ℜ₀-+-<-increasingR : {x : ℜ₀}  (y : ℜ₀)  x ≤ℜ₀ (x ₀+₀ y) 
lem-ℜ₀-+-<-increasingR y = ≤ℜ₀-substR (₀+₀-comm {y}) (lem-ℜ₀-+-≤-increasing y)

lem-ℜ⁺₀-+-increasing : {x : ℜ⁺}  (y : ℜ₀)  x ≤ℜ⁺ (y ₀+⁺ x)
lem-ℜ⁺₀-+-increasing O      = ≤ℜ⁺-refl
lem-ℜ⁺₀-+-increasing (y >0) = inl lem-ℜ⁺-+-<-increasing

lem-ℜ⁺₀-⁺+-increasingR : {x : ℜ⁺}  (y : ℜ₀)  x ≤ℜ⁺ (x ⁺+₀ y)
lem-ℜ⁺₀-⁺+-increasingR O      = ≤ℜ⁺-refl
lem-ℜ⁺₀-⁺+-increasingR (y >0) = inl lem-ℜ⁺-+-<-increasingR

lem-ℜ₀⁺-₀+₀-increasing : {x : ℜ₀}  (y : ℜ⁺)  x <ℜ₀ (y >0 ₀+₀ x)
lem-ℜ₀⁺-₀+₀-increasing {O} y    = _
lem-ℜ₀⁺-₀+₀-increasing {x >0} y = lem-ℜ⁺-+-<-increasing

lem-ℜ₀⁺-₀+₀-increasingR : {x : ℜ₀}  (y : ℜ⁺)  x <ℜ₀ (x ₀+₀ y >0)
lem-ℜ₀⁺-₀+₀-increasingR {O} y = _
lem-ℜ₀⁺-₀+₀-increasingR {x >0} y = lem-ℜ⁺-+-<-increasingR

-----------------------------------------------------------------

lem-ℜ⁺₀-+-≰0 : {x : ℜ⁺}  {y : ℜ₀}  Not (((x ⁺+₀ y) >0) ≤ℜ₀ O)
lem-ℜ⁺₀-+-≰0 (inl ())
lem-ℜ⁺₀-+-≰0 (inr ())

lem-ℜ⁺₀-+-x+y≰x : {x : ℜ⁺}  (y : ℜ₀)  Not ((x ⁺+₀ y) <ℜ⁺ x)
lem-ℜ⁺₀-+-x+y≰x y p = absurd (<≤ℜ⁺-asym p (lem-ℜ⁺₀-⁺+-increasingR y))

lem-ℜ⁺₀-+-x+y≰x₀ : {x : ℜ⁺}  (y : ℜ₀)  Not ((x ⁺+₀ y) >0 <ℜ₀ x >0)
lem-ℜ⁺₀-+-x+y≰x₀ y p = absurd (<≤ℜ⁺-asym p (lem-ℜ⁺₀-⁺+-increasingR y))

lem-ℜ⁺₀-+-z<x→x+y≰z : {x z : ℜ⁺}  (y : ℜ₀)  z <ℜ⁺ x  Not ((x ⁺+₀ y) ≤ℜ⁺ z)
lem-ℜ⁺₀-+-z<x→x+y≰z y lt p = <≤ℜ⁺-asym lt (≤ℜ⁺-trans (lem-ℜ⁺₀-⁺+-increasingR y) p)

lem-ℜ⁺₀-+-z<x→x+y≰z₀ : {x z : ℜ⁺}  (y : ℜ₀)  z <ℜ⁺ x  Not ((x ⁺+₀ y) >0 ≤ℜ₀ z >0)
lem-ℜ⁺₀-+-z<x→x+y≰z₀ y lt = lem-ℜ⁺₀-+-z<x→x+y≰z y lt  lem-ℜ⁺-leq

lem-ℜ⁺-+-≱-increasingR₀ : {x y : ℜ⁺}  Not (x >0 ≥ℜ₀ (x ⁺+⁺ y) >0)
lem-ℜ⁺-+-≱-increasingR₀ = lem-ℜ⁺-+-≱-increasingR  lem-ℜ⁺-leq

-----------------------------------------------------------------

lem-ℜ₀-nlt : {x : ℜ⁺}  Not (x >0 ≤ℜ₀ O)
lem-ℜ₀-nlt (inl ())
lem-ℜ₀-nlt (inr ())

ℜ₀⁺⁺-minus : (x : ℜ₀)  (y : ℜ⁺)  y >0 <ℜ₀ x  ℜ⁺
ℜ₀⁺⁺-minus O y ()
ℜ₀⁺⁺-minus (x >0) y p = ℜ⁺-minus x y p

ℜ₀⁺₀-minus : (x : ℜ₀)  (y : ℜ⁺)  y >0 ≤ℜ₀ x  ℜ₀
ℜ₀⁺₀-minus x y (inl p) = ℜ₀⁺⁺-minus x y p >0
ℜ₀⁺₀-minus .(y >0) y (inr refl) = O

ℜ⁺₀⁺-minus : (x : ℜ⁺)  (y : ℜ₀)  y <ℜ₀ x >0  ℜ⁺
ℜ⁺₀⁺-minus x O p = x
ℜ⁺₀⁺-minus x (y >0) p = ℜ⁺-minus x y p

ℜ⁺₀₀-minus : (x : ℜ⁺)  (y : ℜ₀)  y ≤ℜ₀ x >0  ℜ₀
ℜ⁺₀₀-minus x y (inl p) = ℜ⁺₀⁺-minus x y p >0
ℜ⁺₀₀-minus x .(x >0) (inr refl) = O

ℜ₀₀⁺-minus : (x y : ℜ₀)  y <ℜ₀ x  ℜ⁺
ℜ₀₀⁺-minus O y ()
ℜ₀₀⁺-minus (x >0) y p = ℜ⁺₀⁺-minus x y p

ℜ₀-minus : (x y : ℜ₀)  y ≤ℜ₀ x  ℜ₀
ℜ₀-minus x y (inl p) = ℜ₀₀⁺-minus x y p >0
ℜ₀-minus x .x (inr refl) = O

-----------------------------------------------------------------

postulate lem-ℜ₀-x⁺+₀y<z→y<z-x : {x z : ℜ⁺}  {y : ℜ₀}  (p : x <ℜ⁺ z)  (x ⁺+₀ y) <ℜ⁺ z  y <ℜ₀ ((z ⁺-⁺ x) p) >0
postulate lem-ℜ₀-x⁺+₀y≤z→y≤z-x : {x z : ℜ⁺}  {y : ℜ₀}  (p : x <ℜ⁺ z)  (x ⁺+₀ y) ≤ℜ⁺ z  y ≤ℜ₀ ((z ⁺-⁺ x) p) >0
postulate lem-ℜ₀-y<z⁺-⁺x→x⁺+₀y<z : {x z : ℜ⁺}  {y : ℜ₀}  (p : x <ℜ⁺ z)  (y <ℜ₀ ((z ⁺-⁺ x) p) >0)  (x ⁺+₀ y) <ℜ⁺ z

postulate lem-ℜ₀-minus-≤-decreasing : {x y : ℜ₀}  (p : y ≤ℜ₀ x)  ℜ₀-minus x y p ≤ℜ₀ x

lem-ℜ₀-minus-<-cancellative : {x y z : ℜ₀}  (p : z ≤ℜ₀ x)  (q : z ≤ℜ₀ y)  x <ℜ₀ y  ℜ₀-minus x z p <ℜ₀ ℜ₀-minus y z q
lem-ℜ₀-minus-<-cancellative (inl p) (inr refl) lt = absurd (<ℜ₀-asym p lt)
lem-ℜ₀-minus-<-cancellative (inr refl) (inr refl) lt = absurd (<ℜ₀-irreflexive lt)
lem-ℜ₀-minus-<-cancellative {O} (inl ()) (inl q) lt
lem-ℜ₀-minus-<-cancellative {x >0} {O} (inl p) (inl ()) ()
lem-ℜ₀-minus-<-cancellative {x >0} {y >0} {O} (inl p) (inl q) lt = lt
lem-ℜ₀-minus-<-cancellative {x >0} {y >0} {z >0} (inl p) (inl q) lt = lem-ℜ⁺-minus-<-cancellative p q lt
lem-ℜ₀-minus-<-cancellative {O} (inr refl) (inl q) lt = _
lem-ℜ₀-minus-<-cancellative {x >0} {O} (inr refl) (inl ()) ()
lem-ℜ₀-minus-<-cancellative {x >0} {y >0} (inr refl) (inl q) lt = _

lem-ℜ₀-+ı-increasing : {x : ℜ₀}  x <ℜ₀ (x ₀+₀ ı₀)
lem-ℜ₀-+ı-increasing {O}    = _
lem-ℜ₀-+ı-increasing {x >0} = lem-ℜ⁺-+-<-increasingR

-----------------------------------------------------------------

lem-ℜ₀-minus-<-pos-dif : {x y : ℜ₀}  (p : x <ℜ₀ y)  O <ℜ₀ ℜ₀-minus y x (inl p)
lem-ℜ₀-minus-<-pos-dif {O} p = _
lem-ℜ₀-minus-<-pos-dif {x >0} {O} ()
lem-ℜ₀-minus-<-pos-dif {x >0} {y >0} p = _

-----------------------------------------------------------------

infixl 11 _⁺*₀_ _₀*₀_ _₀*⁺_

_₀*⁺_  : ℜ₀  ℜ⁺  ℜ₀
O ₀*⁺ y = O
(x >0) ₀*⁺ y = (x ⁺*⁺ y) >0

_⁺*₀_  : ℜ⁺  ℜ₀  ℜ₀
x ⁺*₀ O = O
x ⁺*₀ (y >0) = (x ⁺*⁺ y) >0

_₀*₀_   : ℜ₀  ℜ₀  ℜ₀
O ₀*₀ y = O
(x >0) ₀*₀ y = x ⁺*₀ y

-----------------------------------------------------------------

open import List

sumℜ⁺ : List ℜ⁺  ℜ₀
sumℜ⁺ []       = O
sumℜ⁺ (x  xs) = (x ⁺+₀ sumℜ⁺ xs) >0 

sumℜ₀ : List ℜ₀  ℜ₀
sumℜ₀ [] = O
sumℜ₀ (x  xs) = x ₀+₀ sumℜ₀ xs


lem-ℜ⁺-sum≥₀head : {x : ℜ⁺}  (xs : List ℜ⁺)  sumℜ⁺ (x  xs) ≥ℜ₀ x >0
lem-ℜ⁺-sum≥₀head [] = inr refl
lem-ℜ⁺-sum≥₀head (y  xs) = inl lem-ℜ⁺-+-<-increasingR

-- sumℜ⁺≥0 : {r : ℜ⁺} → {rs : List ℜ⁺} → sumℜ⁺ (r ∷ rs) >ℜ₀ O
-- sumℜ⁺≥0 = _

----------------------------------------------------------------

_₀<=₀_ : ℜ₀  ℜ₀  Bool
_₀<=₀_ = _<='_

_₀>=₀_ : ℜ₀  ℜ₀  Bool
_₀>=₀_ = _>='_

_₀<₀_ : ℜ₀  ℜ₀  Bool
_₀<₀_ = _<'_

_₀>₀_ : ℜ₀  ℜ₀  Bool
_₀>₀_ = _>'_

_₀<=⁺_ : ℜ₀  ℜ⁺  Bool
x ₀<=⁺ y = x ₀<=₀ (y >0)

_₀>=⁺_ : ℜ₀  ℜ⁺  Bool
x ₀>=⁺ y = x ₀>=₀ (y >0)

_₀<⁺_ : ℜ₀  ℜ⁺  Bool
x ₀<⁺ y = x ₀<₀ (y >0)

_₀>⁺_ : ℜ₀  ℜ⁺  Bool
x ₀>⁺ y = x ₀>₀ (y >0)

_⁺<=₀_ : ℜ⁺  ℜ₀  Bool
x ⁺<=₀ y = y ₀>=⁺ x

_⁺>=₀_ : ℜ⁺  ℜ₀  Bool
x ⁺>=₀ y = y ₀<=⁺ x

_⁺<₀_ : ℜ⁺  ℜ₀  Bool
x ⁺<₀ y = y ₀>⁺ x

_⁺>₀_ : ℜ⁺  ℜ₀  Bool
x ⁺>₀ y = y ₀<⁺ x

----------------------------------------------------------------