module HyperReal where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Level renaming ( suc to succ ; zero to Zero )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Binary.Definitions
open import nat
open import logic

HyperNat : Set
HyperNat = ℕ → ℕ

_n*_ : (i j : HyperNat ) → HyperNat

_n+_ : (i j : HyperNat ) → HyperNat
i n+ j = λ k → i k + j k

i n* j = λ k → i k * j k

-- _n<_ : ?

-- postulate
--    _cmpHN_  : ( i j HyperNat ) → Dec ( i n< j )

hzero : HyperNat
hzero _ = 0 

data HyperZ : Set where
   hz : HyperNat → HyperNat → HyperZ 

_z*_ : (i j : HyperZ ) → HyperZ

_z+_ : (i j : HyperZ ) → HyperZ
hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ )

--   ( i - i₁ ) * ( j - j₁ ) = i * j + i₁ * j₁ - i * j₁ - i₁ * j
hz i i₁ z* hz j j₁ = hz (λ k → i k * j k + i₁ k * j₁ k ) (λ k →  i k * j₁ k - i₁ k * j k )

HNzero : HyperNat → Set
HNzero i = ( k : ℕ ) →  i k ≡ 0 

HNzero? : ( i : HyperNat ) → Dec (HNzero i)
HNzero? i = {!!} where
   HNz1  : ( m k : ℕ ) → k < m → Dec (( j : ℕ ) → ( j < k ) → i j ≡ 0 )
   HNz1 (suc m) zero k<m with i 0 ≟ 0
   ... | yes y  = yes {!!}
   ... | no n  = no (λ n1 → {!!} )
   HNz1 (suc m) (suc k) (s≤s k<m) with HNz1 m k k<m
   ... | yes y = yes {!!}
   ... | no n = no ( λ n1 → {!!} )

HNnzero* : {x y : HyperNat } → ¬ ( HNzero x ) → ¬ ( HNzero y ) → ¬ ( HNzero (x n* y) )
HNnzero* {x} {y} nzx nzy nzx*y with HNzero? x | HNzero? y
... | yes t | s = ⊥-elim ( nzx t )
... | t | yes s = ⊥-elim ( nzy s )
... | no t | no s = {!!}


HZzero : HyperZ → Set
HZzero (hz i j ) = ( k : ℕ ) →  i k ≡ j k 

HZzero? : ( i : HyperZ ) → Dec (HZzero i)
HZzero? = {!!}

data HyperR : Set where
   hr :  HyperZ → (k : HyperNat ) → ¬ HNzero k → HyperR

HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
HZnzero* {x} {y} nzx nzy nzx*y with HZzero? x | HZzero? y
... | yes t | s = ⊥-elim ( nzx t )
... | t | yes s = ⊥-elim ( nzy s )
... | no t | no s = {!!}

HRzero : HyperR → Set
HRzero (hr i j nz ) = HZzero i

_h*_ : (i j : HyperR) → HyperR

_h+_ : (i j : HyperR) → HyperR
hr x k nz h+ hr y k₁ nz₁ = hr ( (x z* (hz k hzero)) z+  (y z* (hz k₁ hzero)) ) (k n* k₁) (HNnzero* nz nz₁)

hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁)