module MiniLibrary.Real 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

infix 4 _<ℝ_ _≤ℝ_ _==ℝ_ _≥ℝ_
infixl 6 _+ℝ_
infixl 7 _*ℝ_


postulate      : Set
postulate _==ℝ_ :     Set
postulate _<ℝ_  :     Set
postulate _≤ℝ_  :     Set
postulate _#_  :     Set
postulate 0ℝ    :  
postulate 1ℝ    :  
postulate _+ℝ_  :        
postulate _*ℝ_  :        
postulate _-ℝ_  :        
postulate recip : (r : )  r # 0ℝ  
postulate ||_|| :      
postulate 2↑- :        {- 2↑- n = 2^{ -n } -}


postulate reflℝ  : (r : )  r ==ℝ r

_≥ℝ_ :     Set
r ≥ℝ s = s ≤ℝ r



neg :    
neg r = 0ℝ  -ℝ r

divℝ : (r s : )  s # 0ℝ   
divℝ  r s p = r *ℝ (recip s p)

ℕ2ℝ :    
ℕ2ℝ  zero     = 0ℝ 
ℕ2ℝ  (suc n) = ℕ2ℝ n +ℝ 1ℝ 

ℕ+2ℝ : ℕ+   
ℕ+2ℝ (suc n)  = ℕ2ℝ  n +ℝ 1ℝ 

postulate ℕ+#0 : (n : ℕ+)  ℕ+2ℝ n # 0ℝ 

ℤ2ℝ :    
ℤ2ℝ (+ n) = ℕ+2ℝ n
ℤ2ℝ zero = 0ℝ
ℤ2ℝ (- n) = neg (ℕ+2ℝ n) 

Rat2ℝ : Rat   
Rat2ℝ (z / n) = divℝ (ℤ2ℝ z) (ℕ+2ℝ n) (ℕ+#0 n)


2ℝ  :  
2ℝ  = 1ℝ +ℝ 1ℝ 

3ℝ  :  
3ℝ  = 2ℝ +ℝ 1ℝ 

4ℝ  :  
4ℝ  = 2ℝ +ℝ 2ℝ 

-1ℝ  :  
-1ℝ  = neg 1ℝ 

postulate 2ℝ#0 : 2ℝ # 0ℝ 
postulate 3ℝ#0 : 3ℝ # 0ℝ 
postulate 4ℝ#0 : 4ℝ # 0ℝ 

1/2ℝ  :  
1/2ℝ  = divℝ 1ℝ  2ℝ 2ℝ#0

1/4ℝ  :  
1/4ℝ  = divℝ 1ℝ  4ℝ 4ℝ#0



-1/2ℝ  :  
-1/2ℝ  = divℝ -1ℝ  2ℝ 2ℝ#0

-1/4ℝ  :  
-1/4ℝ  = divℝ -1ℝ  4ℝ 4ℝ#0





postulate _∈[-1,1]ℝ :   Set

postulate ∈[-1,1]ℝintro : (r : )  r ≥ℝ  -1ℝ  r ≤ℝ   1ℝ   r ∈[-1,1]ℝ
postulate ∈[-1,1]ℝelim1 : (r : )  r ∈[-1,1]ℝ  r ≥ℝ  -1ℝ  
postulate ∈[-1,1]ℝelim2 : (r : )  r ∈[-1,1]ℝ  r ≤ℝ  1ℝ


postulate ∈[-1,1]Rat2ℝ : (q : Rat)  q ∈[-1,1]Rat  Rat2ℝ q ∈[-1,1]ℝ