```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]

```