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 Relation.Binary.Structures
open import nat
open import logic
open import bijection

HyperNat : Set
HyperNat = ℕ → ℕ

open _∧_
open Bijection

n1 : ℕ → ℕ
n1 n = proj1 (fun→ nxn n)

n2 : ℕ → ℕ
n2 n = proj2 (fun→ nxn n)

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

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

hzero : HyperNat
hzero _ = 0 

h : (n : ℕ) → HyperNat
h n _ = n 

record _n=_  (i j : HyperNat ) :  Set where 
   field 
      =-map : Bijection ℕ ℕ 
      =-m : ℕ
      is-n= : (k : ℕ ) → k > =-m → i k ≡ j (fun→ =-map  k)

open _n=_

record _n≤_  (i j : HyperNat ) :  Set where 
   field 
      ≤-map : Bijection ℕ ℕ
      ≤-m : ℕ
      is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map  k)

open _n≤_

_n<_ :  (i j : HyperNat ) → Set
i n< j = ( i n+ h 1 ) n≤ j 

postulate
   _cmpn_  : ( i j : HyperNat ) → Dec ( i n< j )

n=IsEquivalence : IsEquivalence _n=_
n=IsEquivalence = record { refl = record {=-map = bid ℕ ; =-m = 0 ; is-n= = λ _ _ → refl}
  ; sym = λ xy →  record {=-map = bi-sym ℕ ℕ (=-map xy) ; =-m =  =-m xy ; is-n= = λ k lt → {!!} } -- (is-n= xy k lt) }
  ; trans =  λ xy yz →  record {=-map = bi-trans ℕ ℕ ℕ (=-map xy) (=-map yz) ; =-m =  {!!} ; is-n= = λ k lt → {!!} } }

HNTotalOrder : IsTotalPreorder _n=_ _n≤_ 
HNTotalOrder = record {
     isPreorder = record {
              isEquivalence = n=IsEquivalence
            ; reflexive     = λ eq → record { ≤-map = =-map eq ; ≤-m = =-m eq ; is-n≤ = {!!} }
            ; trans         = {!!} }
    ; total = {!!}
  }


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


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

_z*_ : (i j : HyperZ ) → HyperZ
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 

_z=_ :  (i j : HyperZ ) → Set
_z=_ = {!!}

_z≤_ :  (i j : HyperZ ) → Set
_z≤_ = {!!}


HNzero? : ( i : HyperNat ) → Dec (HNzero i)
HNzero? i with i cmpn hzero | hzero cmpn i
... | no s | t = no (λ n → s {!!}) --  (k₁ : ℕ) → i k₁ ≡ 0  → i k ≤ 0
... | s | no t = no (λ n → t {!!})
... | yes s | yes t = yes (λ k → {!!} )

record HNzeroK ( x : HyperNat ) : Set where
  field
     nonzero : ℕ
     isNonzero : ¬ ( x nonzero ≡ 0 )

postulate 
   HNnzerok : (x  : HyperNat ) → ¬ ( HNzero x ) → HNzeroK x

import Axiom.Extensionality.Propositional
postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m

HNnzero* : {x y : HyperNat } → ¬ ( HNzero x ) → ¬ ( HNzero y ) → ¬ ( HNzero (x n* y) )
HNnzero* {x} {y} nzx nzy nzx*y with HNnzerok x nzx | HNnzerok y nzy
... | s | t = {!!} where
   hnz0 : ( k : ℕ ) → x k * y k ≡ 0  → (x k ≡ 0) ∨ (y k ≡ 0)
   hnz0 k x*y = m*n=0⇒m=0∨n=0 x*y 


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 ) → Set
_h=_ = {!!}

_h≤_ :  (i j : HyperR ) → Set
_h≤_ = {!!}

_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₁)