module cauchyRealsToSignedDigitsVers3 where

open import MiniLibrary.Base
open import MiniLibrary.Nat
open import MiniLibrary.Natplus
-- open import MiniLibrary.DivMod
open import MiniLibrary.Integer
open import MiniLibrary.Rational
open import MiniLibrary.Real
open import MiniLibrary.Codata




data Cauchyℝ (r : ) : Set where 
  cauchy : (f :    Rat)
            (p : (n :  )  || (Rat2ℝ (f n)) -ℝ r  || <ℝ 2↑- n)
            Cauchyℝ r


postulate lemConstantCauchy : (r : )  (n : )  || r  -ℝ  r || <ℝ 2↑- n 

Rat2Cauchyℝ : (q : Rat)  Cauchyℝ (Rat2ℝ q)
Rat2Cauchyℝ  q  = cauchy  n  q) (lemConstantCauchy (Rat2ℝ q))

postulate lemCauchyClosed+  : (q q' : Rat)
                               (r r' : ) 
                               (n : ) 
                               || Rat2ℝ q  -ℝ r  || <ℝ 2↑- (suc n) 
                               || Rat2ℝ q' -ℝ r' || <ℝ 2↑- (suc n) 
                               || Rat2ℝ (q +Rat q') -ℝ (r +ℝ r') || <ℝ 2↑- n

cauchyℝClosed+ : (r s : )  Cauchyℝ r  Cauchyℝ s  Cauchyℝ  (r +ℝ  s)
cauchyℝClosed+ r s (cauchy f p) (cauchy g q) = cauchy 
                                                n  (f (suc n) +Rat g (suc n))) 
                                                n  (lemCauchyClosed+
                                                       (f (suc n))
                                                       (g (suc n))
                                                       r
                                                       s
                                                       n
                                                       (p (suc n))
                                                       (q (suc n))))




data Digit : Set where
  -1d   : Digit
  0d   : Digit
  1d   : Digit


digit2ℝ  : Digit   
digit2ℝ -1d = -1ℝ
digit2ℝ 0d = 0ℝ 
digit2ℝ 1d = 1ℝ 

digit2ℤ  : Digit   
digit2ℤ -1d = -1ℤ
digit2ℤ 0d = 0ℤ 
digit2ℤ 1d = 1ℤ 

digit2Rat  : Digit  Rat 
digit2Rat -1d = -1Rat
digit2Rat 0d = 0Rat 
digit2Rat 1d = 1Rat 


postulate lemCauchyℝClosed2*q-r : (q : Rat)  
                                  (r :  )  
                                  (n : )  
                                  (d : Digit)  
                                  || Rat2ℝ q -ℝ r || <ℝ  2↑- (suc n)  
                                  || Rat2ℝ (2Rat *Rat q -Rat digit2Rat d)  -ℝ (2ℝ *ℝ r -ℝ digit2ℝ d)||
                                   <ℝ 2↑- n


cauchyℝClosed2*q-r : (d : Digit)  (r : )  Cauchyℝ r  Cauchyℝ (2ℝ  *ℝ r -ℝ digit2ℝ d)
cauchyℝClosed2*q-r d  r (cauchy f p) = cauchy  n  2Rat *Rat f (suc n) -Rat digit2Rat d) 
                                               n  lemCauchyℝClosed2*q-r (f (suc n)) r n d (p (suc n)))





data SignedDigit :    Set where
  signedDigit : (r : ) 
                 (r ∈[-1,1]ℝ)
                 (s : )
                 (r ==ℝ s)
                 (d : Digit)
                  (SignedDigit (2ℝ *ℝ r -ℝ  digit2ℝ d))
                 SignedDigit r

{- We decide for cauchy reals whether they are
   >= 0 or <= 1/4>
   >= -1/4 or <= 0 
   Possible because we have overlapping intervals -}

postulate postulateCauchyToSignedDigit1 : (r : ) 
                                      (q : Rat) 
                                      || Rat2ℝ q -ℝ  r || <ℝ  2↑- 2 
                                      q ≤Rat 1/4Rat 
                                      r ≤ℝ  1/2ℝ

postulate postulateCauchyToSignedDigit2 : (r : ) 
                                      (q : Rat) 
                                      || Rat2ℝ q -ℝ  r || <ℝ  2↑- 2 
                                      q  ≥Rat 1/4Rat
                                      r  ≥ℝ  0ℝ


postulate postulateCauchyToSignedDigit3 : (r : ) 
                                      (q : Rat) 
                                      || Rat2ℝ q -ℝ  r || <ℝ  2↑- 2 
                                      q ≤Rat -1/4Rat 
                                      r ≤ℝ  0ℝ

postulate postulateCauchyToSignedDigit4 : (r : ) 
                                      (q : Rat) 
                                      || Rat2ℝ q -ℝ  r || <ℝ  2↑- 2 
                                      q ≥Rat -1/4Rat 
                                      r ≥ℝ  -1/2ℝ 

lemCauchyToSignedDigit1 : (r : ) 
                           (q : Rat) 
                           || Rat2ℝ q -ℝ  r || <ℝ  2↑- 2
                           (q ≤Rat 1/4Rat)  (q ≥Rat 1/4Rat )
                           r ≤ℝ  1/2ℝ  r ≥ℝ 0ℝ
lemCauchyToSignedDigit1 r q p1 (inl p2) = inl (postulateCauchyToSignedDigit1 r q p1 p2)
lemCauchyToSignedDigit1 r q p1 (inr p2) = inr (postulateCauchyToSignedDigit2 r q p1 p2)


lemCauchyToSignedDigit2 : (r : ) 
                           (q : Rat) 
                           || Rat2ℝ q -ℝ  r || <ℝ  2↑- 2
                           (q ≤Rat -1/4Rat)  (q ≥Rat -1/4Rat )
                           r ≤ℝ  0ℝ  r ≥ℝ -1/2ℝ
lemCauchyToSignedDigit2 r q p1 (inl p2) = inl (postulateCauchyToSignedDigit3 r q p1 p2)
lemCauchyToSignedDigit2 r q p1 (inr p2) = inr (postulateCauchyToSignedDigit4 r q p1 p2)

lemCauchyToSignedDigit3 : (r : )  Cauchyℝ r  r ≤ℝ  1/2ℝ  r ≥ℝ 0ℝ
lemCauchyToSignedDigit3 r (cauchy f p) = lemCauchyToSignedDigit1 r (f 2) (p 2) (decideRat≤ (f 2) 1/4Rat)      


lemCauchyToSignedDigit4 : (r : )  Cauchyℝ r  r ≤ℝ  0ℝ  r ≥ℝ -1/2ℝ 
lemCauchyToSignedDigit4 r (cauchy f p) = lemCauchyToSignedDigit2 r (f 2) (p 2) (decideRat≤ (f 2) -1/4Rat)     



{- the first digit d of a cauchy real r will be
   1 if  r >= 0
   0 if  -1/2 <= r <= 1/2
   -1 if r <= 0
   we show that if r ∈ [-1,1]ℝ, then 2 * r - d ∈ [-1,1]ℝ -}


postulate postulateCauchyToSignedDigit5 : (r : ) 
                                           r ∈[-1,1]ℝ
                                           r ≥ℝ  0ℝ 
                                           (2ℝ *ℝ r -ℝ  1ℝ ) ∈[-1,1]ℝ

postulate postulateCauchyToSignedDigit6 : (r : ) 
                                           r ∈[-1,1]ℝ
                                           r ≤ℝ  1/2ℝ 
                                           r ≥ℝ  -1/2ℝ 
                                           (2ℝ *ℝ r -ℝ  0ℝ ) ∈[-1,1]ℝ

postulate postulateCauchyToSignedDigit7 : (r : ) 
                                           r ∈[-1,1]ℝ
                                           r ≤ℝ  0ℝ 
                                           (2ℝ *ℝ r -ℝ  -1ℝ) ∈[-1,1]ℝ

mutual
  cauchyReal2SignedDigit : (r : )
                            (r ∈[-1,1]ℝ)
                            Cauchyℝ r
                            SignedDigit r
  cauchyReal2SignedDigit r p q = cauchyReal2SignedDigitaux1 r p q (lemCauchyToSignedDigit3 r q)


  cauchyReal2SignedDigitaux1 : (r : )
                            (r ∈[-1,1]ℝ)
                            Cauchyℝ r
                            r ≤ℝ  1/2ℝ  r ≥ℝ 0ℝ
                            SignedDigit r
  cauchyReal2SignedDigitaux1 r p q (inl p') = cauchyReal2SignedDigitaux2 r p q p' (lemCauchyToSignedDigit4 r q)
  cauchyReal2SignedDigitaux1 r p q (inr p') = signedDigit r p r (reflℝ r) 1d 
                                              ( cauchyReal2SignedDigit 
                                                (2ℝ *ℝ r -ℝ 1ℝ) 
                                                (postulateCauchyToSignedDigit5 r p p') 
                                                (cauchyℝClosed2*q-r 1d r q))


  cauchyReal2SignedDigitaux2 : (r : )
                            (r ∈[-1,1]ℝ)
                            Cauchyℝ r
                            r ≤ℝ  1/2ℝ
                            r ≤ℝ  0ℝ  r ≥ℝ -1/2ℝ 
                            SignedDigit r
  cauchyReal2SignedDigitaux2 r p q q' (inl q'') = signedDigit r p r (reflℝ r) -1d
                                                    (
                                                     cauchyReal2SignedDigit (2ℝ *ℝ r -ℝ -1ℝ)
                                                     (postulateCauchyToSignedDigit7 r p q'')
                                                     (cauchyℝClosed2*q-r -1d r q))
  cauchyReal2SignedDigitaux2 r p q q' (inr q'') = signedDigit r p r (reflℝ r) 0d
                                                    (
                                                     cauchyReal2SignedDigit (2ℝ *ℝ r -ℝ 0ℝ)
                                                     (postulateCauchyToSignedDigit6 r p q' q'')
                                                     (cauchyℝClosed2*q-r 0d r q))



data Stream (A : Set) : Set where
     _::_ : A   (Stream A)  Stream A


data List (A : Set) : Set where
    []     : List A
    _::_ : A  List A  List A


stream2List : {A : Set}  Stream A    List A
stream2List s 0              = []
stream2List (a :: s) (suc n) = a :: stream2List ( s) n


signedDigit2Stream : (r : )  SignedDigit r  Stream Digit
signedDigit2Stream r (signedDigit .r p s q d p') = d :: 
                                                   ( (signedDigit2Stream (2ℝ *ℝ r -ℝ digit2ℝ d) ( p')))




cauchyReal2Stream : (r : )  r ∈[-1,1]ℝ  Cauchyℝ r  Stream Digit
cauchyReal2Stream r p q = signedDigit2Stream r (cauchyReal2SignedDigit r p q)

cauchyReal2List : (r : )  r ∈[-1,1]ℝ  Cauchyℝ r    List Digit
cauchyReal2List r p q n = stream2List (cauchyReal2Stream r p q) n

rat2List : (q : Rat)  q ∈[-1,1]Rat    List Digit
rat2List q p n = cauchyReal2List (Rat2ℝ q) (∈[-1,1]Rat2ℝ q p) (Rat2Cauchyℝ q) n


{- for testing show me the reals used -}
signedDigit2StreamOfReals : (r : )  SignedDigit r  Stream  
signedDigit2StreamOfReals r (signedDigit .r p s q d p') = r :: 
                                                   ( (signedDigit2StreamOfReals (2ℝ *ℝ r -ℝ digit2ℝ d) ( p')))


cauchyReal2StreamOfReals : (r : )  r ∈[-1,1]ℝ  Cauchyℝ r  Stream  
cauchyReal2StreamOfReals r p q = signedDigit2StreamOfReals r (cauchyReal2SignedDigit r p q)


cauchyReal2ListOfReals : (r : )  r ∈[-1,1]ℝ  Cauchyℝ r    List  
cauchyReal2ListOfReals r p q n = stream2List (cauchyReal2StreamOfReals r p q) n

rat2ListOfReals : (q : Rat)  q ∈[-1,1]Rat    List  
rat2ListOfReals q p n = cauchyReal2ListOfReals (Rat2ℝ q) (∈[-1,1]Rat2ℝ q p) (Rat2Cauchyℝ q) n

rat2SignedDigit : (q : Rat)  q ∈[-1,1]Rat  SignedDigit (Rat2ℝ q)
rat2SignedDigit q p =  cauchyReal2SignedDigit (Rat2ℝ q) (∈[-1,1]Rat2ℝ q p) (Rat2Cauchyℝ q)

example1/2 :   List Digit
example1/2 n = rat2List 1/2Rat 1/2Rat∈[-1,1] n

example1/3 :   List Digit
example1/3 n = rat2List 1/3Rat 1/3Rat∈[-1,1] n

example1/4 :   List Digit
example1/4 n = rat2List 1/4Rat 1/4Rat∈[-1,1] n

example-1/4 :   List Digit
example-1/4 n = rat2List -1/4Rat -1/4Rat∈[-1,1] n

example-1/3 :   List Digit
example-1/3 n = rat2List -1/3Rat -1/3Rat∈[-1,1] n


example1/2Reals :   List  
example1/2Reals n = rat2ListOfReals 1/2Rat 1/2Rat∈[-1,1] n

example1/3Reals :   List  
example1/3Reals n = rat2ListOfReals 1/3Rat 1/3Rat∈[-1,1] n


example1/4Reals :   List  
example1/4Reals n = rat2ListOfReals 1/4Rat 1/4Rat∈[-1,1] n


example1/2SignedDigit : SignedDigit (Rat2ℝ 1/2Rat)
example1/2SignedDigit = rat2SignedDigit 1/2Rat 1/2Rat∈[-1,1]