# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1625721816 -32400
# Node ID f0763f51631ef2d899d68a3a809f0d3f15624be1
# Parent  9fefd6c7fb7796ad5a15c90b80ee7eea103adde6
...

diff -r 9fefd6c7fb77 -r f0763f51631e src/HyperReal.agda
--- a/src/HyperReal.agda	Thu Jul 08 11:55:40 2021 +0900
+++ b/src/HyperReal.agda	Thu Jul 08 14:23:36 2021 +0900
@@ -4,7 +4,7 @@
 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 Level renaming ( suc to succ ; zero to Zero ; _⊔_ to _L⊔_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Binary.Definitions
 open import Relation.Binary.Structures
@@ -56,15 +56,18 @@
    field 
       <-map : Bijection ℕ ℕ
       <-m : ℕ
-      is-<≤ : (k : ℕ ) → k > <-m → i k < j (fun→ <-map  k)
+      is-n< : (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≤_ = {!!}
 
+¬hn<0 : {x : HyperNat } → ¬ ( x n< h 0 )
+¬hn<0 {x} x<0 = ⊥-elim ( nat-≤> (is-n< x<0 (suc (<-m x<0)) a<sa) 0<s )
+
 postulate
-   _cmpn_  : Trichotomous {Level.zero} _n=_  _n<_ 
+   <-cmpn  : Trichotomous {Level.zero} _n=_  _n<_ 
 
 n=IsEquivalence : IsEquivalence _n=_
 n=IsEquivalence = record { refl = record {=-map = bid ℕ ; =-m = 0 ; is-n= = λ _ _ → refl}
@@ -82,7 +85,7 @@
       open import Data.Sum.Base using (_⊎_)
       open _⊎_
       total : (x y : HyperNat ) → (x n≤ y) ⊎ (y n≤ x)
-      total x y with x cmpn y
+      total x y with <-cmpn x y 
       ... | tri< a ¬b ¬c = inj₁ {!!}
       ... | tri≈ ¬a b ¬c = {!!}
       ... | tri> ¬a ¬b c = {!!}
@@ -114,20 +117,33 @@
 _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) 
+<-cmpz  : Trichotomous {Level.zero}  _z=_ _z<_
+<-cmpz (hz x0 y0) (hz x1 y1)  = <-cmpn (x0 n+ y1) (x1 n+ y0) 
 
 import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
+---    x*y    ...... 0 0 0 0 ...
+---    x      ...... 0 0 1 0 1 ....
+---    y      ...... 0 1 0 1 0 ....
+
 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 
-
+HNnzero* {x} {y} nzx nzy xy0 = hn1 where
+   hn2 : ( h 0 n< x ) → ( h 0 n< y  ) →  ¬ ( (x n* y) n= h 0 )
+   hn2 0<x 0<y  xy0 = ⊥-elim ( nat-≡< (sym (is-n= xy0 (suc mxy) {!!} )) {!!}  ) where
+       mxy : ℕ
+       mxy = <-m 0<x ⊔ <-m 0<y ⊔ =-m xy0
+   hn1 : ⊥
+   hn1 with <-cmpn x (h 0)
+   ... | tri≈ ¬a b ¬c = nzx b
+   ... | tri< a ¬b ¬c = ⊥-elim ( ¬hn<0 a)
+   hn1 | tri> ¬a ¬b c with <-cmpn y (h 0)
+   ... | tri< a ¬b₁ ¬c = ⊥-elim ( ¬hn<0 a)
+   ... | tri≈ ¬a₁ b ¬c = nzy b
+   ... | tri> ¬a₁ ¬b₁ c₁ = hn2 c c₁ xy0
 
 HZzero : HyperZ → Set
-HZzero (hz i j ) = ( k : ℕ ) →  i k ≡ j k 
+HZzero z = hZ 0 0 z= z
 
 HZzero? : ( i : HyperZ ) → Dec (HZzero i)
 HZzero? = {!!}
@@ -136,10 +152,7 @@
    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 = {!!}
+HZnzero* {x} {y} nzx nzy nzx*y = {!!}
 
 HRzero : HyperR → Set
 HRzero (hr i j nz ) = HZzero i
@@ -147,11 +160,20 @@
 hR :  ℕ → ℕ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR
 hR x y k ne = hr (hZ x y) k ne
 
+--
+--  z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0
+--
 _h=_ :  (i j : HyperR ) → Set
-_h=_ = {!!}
+hr z0 k0 ne0 h= hr z1 k1 ne1  = (z0 z* (hz k1 (h 0))) z= (z1 z* (hz k0 (h 0)))
 
 _h≤_ :  (i j : HyperR ) → Set
-_h≤_ = {!!}
+hr z0 k0 ne0 h≤ hr z1 k1 ne1  = (z0 z* (hz k1 (h 0))) z≤ (z1 z* (hz k0 (h 0)))
+
+_h<_ :  (i j : HyperR ) → Set
+hr z0 k0 ne0 h< hr z1 k1 ne1  = (z0 z* (hz k1 (h 0))) z< (z1 z* (hz k0 (h 0)))
+
+<-cmph  : Trichotomous {Level.zero}  _h=_ _h<_
+<-cmph (hr z0 k0 ne0 ) ( hr z1 k1 ne1 ) = <-cmpz  (z0 z* (hz k1 (h 0)))  (z1 z* (hz k0 (h 0)))
 
 _h*_ : (i j : HyperR) → HyperR
 hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁)
@@ -170,4 +192,4 @@
    factor : HyperNat 
    factor n = {!!}
    fne : (n : ℕ) → ¬ (factor n= h 0)
-   fne = ?
+   fne = {!!}