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

HyperNat : Set
HyperNat = ℕ → ℕ

record IsoN : Set where
  field
     m→ m← : ℕ → ℕ 
     id→← : (i  : ℕ) →  m→ (m← i ) ≡ i
     id←→ : (i  : ℕ) →  m← (m→ i ) ≡ i

open IsoN 

record NxN : Set where
  field
     nxn→n : ℕ ∧ ℕ → ℕ
     n→nxn : ℕ → ℕ ∧ ℕ 
     nn-id : (i j : ℕ) →  n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫
     n-id : (i  : ℕ) →  nxn→n (n→nxn i ) ≡ i

open _∧_

     -- t1 :  nxn→n 0 1 ≡ 1
     -- t1 = refl
     -- t2 :  nxn→n 1 0 ≡ 2
     -- t2 = refl
     -- t3 :  nxn→n 0 2 ≡ 3
     -- t3 = refl
     -- t4 :  nxn→n 1 1 ≡ 4
     -- t4 = refl
     -- t5 :  nxn→n 2 0 ≡ 5
     -- t5 = refl
     -- t6 :  nxn→n 0 3 ≡ 6
     -- t6 = refl
     -- t7 :  nxn→n 1 2 ≡ 7
     -- t7 = refl
     -- t8 :  nxn→n 2 1 ≡ 8
     -- t8 = refl
     -- t9 :  nxn→n 3 0 ≡ 9
     -- t9 = refl
     -- t10 :  nxn→n 0 4 ≡ 10
     -- t10 = refl

nxn : NxN
nxn = record {
     nxn→n = λ p → nxn→n (proj1 p) (proj2 p)
   ; n→nxn =  n→nxn 
   ; nn-id = {!!}
   ; n-id = {!!}
  } where
     nxn→n :  ℕ →  ℕ → ℕ
     nxn→n zero zero = zero
     nxn→n zero (suc j) = j + suc (nxn→n zero j)
     nxn→n (suc i) zero = suc i + suc (nxn→n i zero)
     nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j))
     n→nxn : ℕ → ℕ ∧ ℕ
     n→nxn zero = ⟪ 0 , 0 ⟫
     n→nxn (suc i) with n→nxn i
     ... | ⟪ x , zero ⟫ = ⟪ zero  , suc x ⟫
     ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
     nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
     nn-id zero zero = refl
     nn-id zero (suc j) with  n→nxn (j + (nxn→n 0 j))
     ... | ⟪ x , zero ⟫ = {!!}
     ... | ⟪ x , suc y ⟫ = {!!}
     --= begin
     --   n→nxn (nxn→n zero (suc j)) ≡⟨ refl ⟩ --  n→nxn (nxn→n zero j) ≡ ⟪ zero , j ⟫ : nn-id zero j
     --   n→nxn (j + suc (nxn→n 0 j))  ≡⟨  {!!}  ⟩
     --   n→nxn (suc (j + (nxn→n 0 j)))  ≡⟨  {!!}  ⟩
     --   {!!}  ≡⟨  {!!}  ⟩
     --   ⟪ zero , suc j ⟫ ∎  where open ≡-Reasoning
     nn-id (suc i) j = {!!}

open NxN

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

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

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

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

i n* j = λ k → i (n1 k) * j (n2 k)

hzero : HyperNat
hzero _ = 0 

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

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

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

HNTotalOrder : IsTotalPreorder _n=_ _n≤_ 
HNTotalOrder = record {
     isPreorder = record {
              isEquivalence = {!!}
            ; reflexive     = {!!}
            ; trans         = {!!} }
    ; total = {!!}
  }


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 

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

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

≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
≤→= {0} {0} z≤n z≤n = refl
≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )



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

m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl
m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl

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