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≤_

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

open _n<_

_n<=s≤_ :  (i j : HyperNat ) → (i n< j) ⇔ (( i n+ h 1 ) n≤ j )
_n<=s≤_ = {!!}

postulate
   _cmpn_  : Trichotomous {Level.zero} _n=_  _n<_ 

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         = trans1 }
    ; total = total
  } where
      open import Data.Sum.Base using (_⊎_)
      open _⊎_
      total : (x y : HyperNat ) → (x n≤ y) ⊎ (y n≤ x)
      total x y with x cmpn y
      ... | tri< a ¬b ¬c = inj₁ {!!}
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b c = {!!}
      trans1 : {i j k : HyperNat} →  i n≤ j → j n≤ k → i n≤ k
      trans1 = {!!}


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

hZ : ℕ → ℕ → HyperZ
hZ x y = hz (λ _ → x) (λ _ → y )

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

--  x0 - y0 ≡ x1 - y1
--  x0 + y1 ≡ x1 + y0
--
_z=_ :  (i j : HyperZ ) → Set
_z=_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n= (x1 n+ y0)

_z≤_ :  (i j : HyperZ ) → Set
_z≤_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n≤ (x1 n+ y0)

_z<_ :  (i j : HyperZ ) → Set
_z<_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n< (x1 n+ y0)

_cmpz_  : Trichotomous {Level.zero}  _z=_ _z<_
(hz x0 y0)  cmpz (hz x1 y1)  = (x0 n+ y1) cmpn (x1 n+ y0) 

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

HNnzero* : {x y : HyperNat } → ¬ ( x n= h 0 ) → ¬ ( y n= h 0  ) → ¬ ( (x n* y) n= h 0 )
HNnzero* {x} {y} nzx nzy nzx*y = {!!} 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 ) → ¬ (k n= h 0) → 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

hR :  ℕ → ℕ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR
hR x y k ne = hr (hZ x y) k ne

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

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

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

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

HyperReal :  Set 
HyperReal = ℕ  → HyperR

HR→HRl : HyperR → HyperReal
HR→HRl (hr (hz x y) k ne) k1 = hr (hz (λ k2 → (x k1)) (λ k2 → (x k1))) k ne

HRl→HR : HyperReal → HyperR
HRl→HR r = hr (hz (λ k → {!!}) (λ k → {!!}) ) factor {!!} where
   factor : HyperNat 
   factor n = {!!}
   fne : (n : ℕ) → ¬ (factor n= h 0)
   fne = ?