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

nxn : NxN
nxn = record {
     nxn→n = λ p → nxn→n (proj1 p) (proj2 p)
   ; n→nxn =  n→nxn 
   ; nn-id = nn-id
   ; n-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 ⟫
     nid0 : (i : ℕ) → 0 ≡ proj2 (n→nxn i) → n→nxn (suc i) ≡ ⟪ 0 , suc ( proj1 ( n→nxn i )) ⟫
     nid0 zero eq = refl
     nid0 (suc i) eq with n→nxn (suc i)
     ... | ⟪ x , zero ⟫ = refl
     nid1 : (i : ℕ) → 0 < proj2 (n→nxn i) → n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
     nid1 (suc i) 0<p2 with  n→nxn (suc i) 
     ... | ⟪ x , zero ⟫ = ⊥-elim ( nat-≤> 0<p2 a<sa )
     ... | ⟪ x , suc y ⟫ = refl
     nid4 : {i j : ℕ} →  i + 1 + j ≡ i + suc j
     nid4 {zero} {j} = refl
     nid4 {suc i} {j} = cong suc (nid4 {i} {j} )
     nid5 : {i j k : ℕ} →  i + suc (suc j) + suc k ≡ i + suc j + suc (suc k )
     nid5 {zero} {j} {k} = begin
          suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩
          1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩
          (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩
          suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩
          suc j + suc (suc k) ∎ where open ≡-Reasoning
     nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
     nid20 : (i : ℕ) →  i +  (nxn→n 0 i) ≡ nxn→n i 0
     nid20 i = {!!}
     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
     nid2 zero zero = refl
     nid2 zero (suc j) = refl
     nid2 (suc i) zero = begin
          suc (nxn→n (suc i) 1)  ≡⟨ refl ⟩
          suc (suc (i + 1 + suc (nxn→n i 1)))  ≡⟨ cong (λ k → suc (suc k)) nid4  ⟩
          suc (suc (i + suc (suc (nxn→n i 1))))  ≡⟨ cong (λ k →  suc (suc (i + suc (suc k)))) (nid3 i) ⟩
          suc (suc (i + suc (suc (i + suc (nxn→n i 0)))))  ≡⟨ refl ⟩
          nxn→n (suc (suc i)) zero ∎ where
             open ≡-Reasoning
             nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0)
             nid3 zero = refl
             nid3 (suc i) = begin
                 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
                 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k →  suc (i + suc (suc k))) (nid3 i) ⟩
                 suc (i + suc (suc (i + suc (nxn→n i 0))))
              ∎
     nid2 (suc i) (suc j) = begin
          suc (nxn→n (suc i) (suc (suc j)))  ≡⟨ refl ⟩
          suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j)))))  ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩
          suc (suc (i + suc (suc j) + suc      (i + suc j + suc (nxn→n i (suc j)))))  ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩
          suc (suc (i + suc j       + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩
          nxn→n (suc (suc i)) (suc j) ∎ where
             open ≡-Reasoning
     nid6 : {i : ℕ } → 0 < i  → suc (pred i) ≡ i
     nid6 {suc i} 0<i = refl
     n-id :  (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
     n-id 0 = refl
     n-id (suc i) with proj2 (n→nxn (suc i))  | inspect  proj2 (n→nxn (suc i))  -- ⟪ pred n , 1 ⟫  → ⟪ n , 0 ⟫
     ... | zero  | record { eq = eq } with  proj1 (n→nxn (suc i)) | inspect  proj1 (n→nxn (suc i))
     ... | zero | record { eq = eqx } = {!!} where
         nid14 :  {i x y : ℕ} → n→nxn i ≡ ⟪ x , suc y ⟫ →  suc x ≡ proj2 (n→nxn (suc (suc i)))
         nid14 = {!!}
         nid13 : (i : ℕ) → proj1 (n→nxn (suc i)) ≡ 0  →  proj2 (n→nxn (suc i)) ≡ 0  → ⊥
         nid13 (suc i) eq eq1 with n→nxn i | inspect  n→nxn i
         ... | ⟪ x , suc y ⟫ | record { eq = eq2 } = nat-≡< (sym eq1) ( begin
             1 ≤⟨ s≤s z≤n ⟩
             suc x ≡⟨ nid14 {i} {x} {y} eq2 ⟩
             {!!} ≡⟨ {!!} ⟩
             _ ∎ ) where open ≤-Reasoning
     ... | suc x | record { eq = eqx } with proj2 (n→nxn i) | inspect  proj2 (n→nxn i)
     -- i +  (nxn→n 0 i) ≡ nxn→n i 0
     ... | zero | record { eq = eqy } = begin
         suc (x + suc (nxn→n x 0)) ≡⟨ {!!}  ⟩
         suc (pred (proj1 (n→nxn (suc i))) + suc (nxn→n (pred (proj1 (n→nxn (suc i)))) 0))  ≡⟨ {!!}  ⟩
         suc (nxn→n (proj1 (n→nxn i)) 0) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) k)) (sym eqy) ⟩
         suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩
         suc i ∎ where
             open ≡-Reasoning
     ... | suc y | record { eq = eqy } = begin
         nxn→n (suc x) 0 ≡⟨ sym (nid2 x 0) ⟩
         suc (nxn→n x 1)  ≡⟨ cong₂ (λ j k → suc (nxn→n j k) ) nid9 nid10 ⟩
         suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩
         suc i ∎   where
             open ≡-Reasoning
             nid11 : 0 < proj2 (n→nxn i)
             nid11 = subst (λ k → 0 < k ) (sym eqy) (s≤s z≤n)
             nid9 :  x ≡ proj1 (n→nxn i)
             nid9 = begin
               x ≡⟨ sym (cong pred eqx) ⟩
               pred (proj1 (n→nxn (suc i))) ≡⟨ cong pred (cong proj1  (nid1 i nid11)) ⟩
               pred (suc (proj1 (n→nxn i)))  ≡⟨ refl  ⟩
               proj1 (n→nxn i)  ∎   
             nid10 :  1 ≡ proj2 (n→nxn i)
             nid10 = begin
               1  ≡⟨ cong suc (sym eq) ⟩
               suc ( proj2 (n→nxn (suc i)))  ≡⟨ cong suc (cong proj2  (nid1 i nid11)) ⟩
               suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid11 ⟩
               proj2 (n→nxn i)  ∎   
     n-id (suc i) | suc x | record { eq = eq } with  proj2 (n→nxn i) | inspect proj2 (n→nxn i)  -- ⟪ x , 0 ⟫ → ⟪ 0 , suc x ⟫
     -- eqy : proj2 (n→nxn i) ≡ zero
     -- eq  : proj2 (n→nxn (suc i) | n→nxn i) ≡ suc x
     ... | zero  | record { eq = eqy } = begin
          nxn→n (proj1 (n→nxn (suc i) )) (suc x) ≡⟨ {!!} ⟩
          nxn→n zero (suc x) ≡⟨ {!!} ⟩
          pred (suc x) + suc (nxn→n 0 (pred (suc x))) ≡⟨ cong (λ k → pred k +  suc (nxn→n 0 (pred k))) (sym eq) ⟩
          pred (proj2 (n→nxn (suc i) )) + suc (nxn→n 0 (pred (proj2 (n→nxn (suc i) )))) ≡⟨ {!!} ⟩
          suc i ∎ where
             open ≡-Reasoning
     ... | suc y | record { eq = eqy } = begin
          nxn→n (proj1 (n→nxn (suc i))) (suc x)   ≡⟨ cong (λ k → nxn→n (proj1 k) (suc x)) (nid1 i nid7 ) ⟩
          nxn→n (suc (proj1 (n→nxn i))) (suc x)   ≡⟨ sym (nid2 (proj1 (n→nxn i)) (suc x) ) ⟩
          suc (nxn→n (proj1 (n→nxn i)) (suc (suc x))) ≡⟨  cong (λ k → suc (nxn→n  (proj1 (n→nxn i)) (suc k))) (sym eq) ⟩
          suc (nxn→n (proj1 (n→nxn i)) (suc (proj2  (n→nxn (suc i))))) ≡⟨  cong (λ k → suc (nxn→n  (proj1 (n→nxn i)) k)) ( begin
              suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7)) ⟩
              suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩
              proj2 (n→nxn i) ∎ )⟩
          suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩ 
          suc i ∎ where
             open ≡-Reasoning
             nid7 :  0 < proj2 (n→nxn i) 
             nid7 = subst (λ k → 0 < k ) (sym eqy) (s≤s z≤n)
             nid8 : suc (proj2  (n→nxn (suc i)))  ≡ proj2 (n→nxn i)
             nid8 = begin
                suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7 )) ⟩
                suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩
                proj2 (n→nxn i) ∎  
     f : (i : ℕ) → Set
     f i = n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
     g : (i j : ℕ) → Set
     g i j = suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
     h : (i : ℕ) → Set
     h i = i +  (nxn→n 0 i) ≡ nxn→n i 0
     h1  : ( i : ℕ ) → Set
     h1 i = (pred (proj1 (n→nxn (suc i))) + suc (nxn→n (pred (proj1 (n→nxn (suc i)))) 0))  ≡ suc (nxn→n (proj1 (n→nxn i)) 0) 
     nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
     nn-id = {!!}

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