|
0
|
1 module HyperReal where
|
|
|
2
|
|
|
3 open import Data.Nat
|
|
|
4 open import Data.Nat.Properties
|
|
|
5 open import Data.Empty
|
|
|
6 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
19
|
7 open import Level renaming ( suc to succ ; zero to Zero ; _⊔_ to _L⊔_ )
|
|
0
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
9 open import Relation.Binary.Definitions
|
|
4
|
10 open import Relation.Binary.Structures
|
|
1
|
11 open import nat
|
|
|
12 open import logic
|
|
17
|
13 open import bijection
|
|
0
|
14
|
|
1
|
15 HyperNat : Set
|
|
|
16 HyperNat = ℕ → ℕ
|
|
|
17
|
|
2
|
18 open _∧_
|
|
17
|
19 open Bijection
|
|
2
|
20
|
|
|
21 n1 : ℕ → ℕ
|
|
17
|
22 n1 n = proj1 (fun→ nxn n)
|
|
2
|
23
|
|
|
24 n2 : ℕ → ℕ
|
|
17
|
25 n2 n = proj2 (fun→ nxn n)
|
|
2
|
26
|
|
1
|
27 _n*_ : (i j : HyperNat ) → HyperNat
|
|
17
|
28 i n* j = λ k → i k * j k
|
|
1
|
29
|
|
|
30 _n+_ : (i j : HyperNat ) → HyperNat
|
|
17
|
31 i n+ j = λ k → i k + j k
|
|
1
|
32
|
|
|
33 hzero : HyperNat
|
|
|
34 hzero _ = 0
|
|
|
35
|
|
17
|
36 h : (n : ℕ) → HyperNat
|
|
|
37 h n _ = n
|
|
|
38
|
|
5
|
39 record _n=_ (i j : HyperNat ) : Set where
|
|
|
40 field
|
|
17
|
41 =-map : Bijection ℕ ℕ
|
|
5
|
42 =-m : ℕ
|
|
17
|
43 is-n= : (k : ℕ ) → k > =-m → i k ≡ j (fun→ =-map k)
|
|
5
|
44
|
|
17
|
45 open _n=_
|
|
|
46
|
|
3
|
47 record _n≤_ (i j : HyperNat ) : Set where
|
|
|
48 field
|
|
17
|
49 ≤-map : Bijection ℕ ℕ
|
|
3
|
50 ≤-m : ℕ
|
|
17
|
51 is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map k)
|
|
|
52
|
|
|
53 open _n≤_
|
|
|
54
|
|
18
|
55 record _n<_ (i j : HyperNat ) : Set where
|
|
|
56 field
|
|
|
57 <-map : Bijection ℕ ℕ
|
|
|
58 <-m : ℕ
|
|
19
|
59 is-n< : (k : ℕ ) → k > <-m → i k < j (fun→ <-map k)
|
|
18
|
60
|
|
|
61 open _n<_
|
|
|
62
|
|
|
63 _n<=s≤_ : (i j : HyperNat ) → (i n< j) ⇔ (( i n+ h 1 ) n≤ j )
|
|
|
64 _n<=s≤_ = {!!}
|
|
2
|
65
|
|
19
|
66 ¬hn<0 : {x : HyperNat } → ¬ ( x n< h 0 )
|
|
|
67 ¬hn<0 {x} x<0 = ⊥-elim ( nat-≤> (is-n< x<0 (suc (<-m x<0)) a<sa) 0<s )
|
|
|
68
|
|
2
|
69 postulate
|
|
19
|
70 <-cmpn : Trichotomous {Level.zero} _n=_ _n<_
|
|
17
|
71
|
|
|
72 n=IsEquivalence : IsEquivalence _n=_
|
|
|
73 n=IsEquivalence = record { refl = record {=-map = bid ℕ ; =-m = 0 ; is-n= = λ _ _ → refl}
|
|
|
74 ; sym = λ xy → record {=-map = bi-sym ℕ ℕ (=-map xy) ; =-m = =-m xy ; is-n= = λ k lt → {!!} } -- (is-n= xy k lt) }
|
|
|
75 ; trans = λ xy yz → record {=-map = bi-trans ℕ ℕ ℕ (=-map xy) (=-map yz) ; =-m = {!!} ; is-n= = λ k lt → {!!} } }
|
|
2
|
76
|
|
5
|
77 HNTotalOrder : IsTotalPreorder _n=_ _n≤_
|
|
|
78 HNTotalOrder = record {
|
|
|
79 isPreorder = record {
|
|
17
|
80 isEquivalence = n=IsEquivalence
|
|
|
81 ; reflexive = λ eq → record { ≤-map = =-map eq ; ≤-m = =-m eq ; is-n≤ = {!!} }
|
|
18
|
82 ; trans = trans1 }
|
|
|
83 ; total = total
|
|
|
84 } where
|
|
|
85 open import Data.Sum.Base using (_⊎_)
|
|
|
86 open _⊎_
|
|
|
87 total : (x y : HyperNat ) → (x n≤ y) ⊎ (y n≤ x)
|
|
19
|
88 total x y with <-cmpn x y
|
|
18
|
89 ... | tri< a ¬b ¬c = inj₁ {!!}
|
|
|
90 ... | tri≈ ¬a b ¬c = {!!}
|
|
|
91 ... | tri> ¬a ¬b c = {!!}
|
|
|
92 trans1 : {i j k : HyperNat} → i n≤ j → j n≤ k → i n≤ k
|
|
|
93 trans1 = {!!}
|
|
4
|
94
|
|
20
|
95 record n-finite (i : HyperNat ) : Set where
|
|
|
96 field
|
|
|
97 val : ℕ
|
|
|
98 is-val : i n= h val
|
|
|
99
|
|
|
100 n-infinite : (i : HyperNat ) → Set
|
|
|
101 n-infinite i = (j : ℕ ) → h j n≤ i
|
|
|
102
|
|
|
103 n-linear : HyperNat
|
|
|
104 n-linear i = i
|
|
|
105
|
|
|
106 n-linear-is-infnite : n-infinite n-linear
|
|
|
107 n-linear-is-infnite i = record { ≤-map = bid ℕ ; ≤-m = i ; is-n≤ = λ k lt → <to≤ lt }
|
|
|
108
|
|
|
109 ¬-infinite-n-finite : (i : HyperNat ) → n-finite i → ¬ n-infinite i
|
|
|
110 ¬-infinite-n-finite = {!!}
|
|
2
|
111
|
|
1
|
112 data HyperZ : Set where
|
|
|
113 hz : HyperNat → HyperNat → HyperZ
|
|
0
|
114
|
|
18
|
115 hZ : ℕ → ℕ → HyperZ
|
|
|
116 hZ x y = hz (λ _ → x) (λ _ → y )
|
|
1
|
117
|
|
|
118 _z+_ : (i j : HyperZ ) → HyperZ
|
|
|
119 hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ )
|
|
0
|
120
|
|
17
|
121 _z*_ : (i j : HyperZ ) → HyperZ
|
|
1
|
122 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 )
|
|
|
123
|
|
18
|
124 -- x0 - y0 ≡ x1 - y1
|
|
|
125 -- x0 + y1 ≡ x1 + y0
|
|
|
126 --
|
|
5
|
127 _z=_ : (i j : HyperZ ) → Set
|
|
18
|
128 _z=_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n= (x1 n+ y0)
|
|
5
|
129
|
|
|
130 _z≤_ : (i j : HyperZ ) → Set
|
|
18
|
131 _z≤_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n≤ (x1 n+ y0)
|
|
4
|
132
|
|
18
|
133 _z<_ : (i j : HyperZ ) → Set
|
|
|
134 _z<_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n< (x1 n+ y0)
|
|
2
|
135
|
|
19
|
136 <-cmpz : Trichotomous {Level.zero} _z=_ _z<_
|
|
|
137 <-cmpz (hz x0 y0) (hz x1 y1) = <-cmpn (x0 n+ y1) (x1 n+ y0)
|
|
2
|
138
|
|
20
|
139 -z : (i : HyperZ ) → HyperZ
|
|
|
140 -z (hz x y) = hz y x
|
|
|
141
|
|
|
142 z-z=0 : (i : HyperZ ) → (i z+ (-z i)) z= hZ 0 0
|
|
|
143 z-z=0 = {!!}
|
|
|
144
|
|
|
145 z+infinite : (i : HyperZ ) → Set
|
|
|
146 z+infinite i = (j : ℕ ) → hZ j 0 z≤ i
|
|
|
147
|
|
|
148 z-infinite : (i : HyperZ ) → Set
|
|
|
149 z-infinite i = (j : ℕ ) → i z≤ hZ 0 j
|
|
|
150
|
|
2
|
151 import Axiom.Extensionality.Propositional
|
|
|
152 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m
|
|
|
153
|
|
19
|
154 --- x*y ...... 0 0 0 0 ...
|
|
|
155 --- x ...... 0 0 1 0 1 ....
|
|
|
156 --- y ...... 0 1 0 1 0 ....
|
|
|
157
|
|
18
|
158 HNnzero* : {x y : HyperNat } → ¬ ( x n= h 0 ) → ¬ ( y n= h 0 ) → ¬ ( (x n* y) n= h 0 )
|
|
19
|
159 HNnzero* {x} {y} nzx nzy xy0 = hn1 where
|
|
|
160 hn2 : ( h 0 n< x ) → ( h 0 n< y ) → ¬ ( (x n* y) n= h 0 )
|
|
|
161 hn2 0<x 0<y xy0 = ⊥-elim ( nat-≡< (sym (is-n= xy0 (suc mxy) {!!} )) {!!} ) where
|
|
|
162 mxy : ℕ
|
|
|
163 mxy = <-m 0<x ⊔ <-m 0<y ⊔ =-m xy0
|
|
|
164 hn1 : ⊥
|
|
|
165 hn1 with <-cmpn x (h 0)
|
|
|
166 ... | tri≈ ¬a b ¬c = nzx b
|
|
|
167 ... | tri< a ¬b ¬c = ⊥-elim ( ¬hn<0 a)
|
|
|
168 hn1 | tri> ¬a ¬b c with <-cmpn y (h 0)
|
|
|
169 ... | tri< a ¬b₁ ¬c = ⊥-elim ( ¬hn<0 a)
|
|
|
170 ... | tri≈ ¬a₁ b ¬c = nzy b
|
|
|
171 ... | tri> ¬a₁ ¬b₁ c₁ = hn2 c c₁ xy0
|
|
1
|
172
|
|
|
173 HZzero : HyperZ → Set
|
|
19
|
174 HZzero z = hZ 0 0 z= z
|
|
0
|
175
|
|
1
|
176 HZzero? : ( i : HyperZ ) → Dec (HZzero i)
|
|
|
177 HZzero? = {!!}
|
|
|
178
|
|
|
179 data HyperR : Set where
|
|
20
|
180 hr : HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
|
|
0
|
181
|
|
1
|
182 HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
|
|
19
|
183 HZnzero* {x} {y} nzx nzy nzx*y = {!!}
|
|
1
|
184
|
|
|
185 HRzero : HyperR → Set
|
|
|
186 HRzero (hr i j nz ) = HZzero i
|
|
|
187
|
|
20
|
188 R0 : HyperR
|
|
|
189 R0 = hr (hZ 0 0) (h 1) {!!}
|
|
|
190
|
|
22
|
191 R1 : HyperR
|
|
|
192 R1 = hr (hZ 1 0) (h 1) {!!}
|
|
|
193
|
|
20
|
194 record Rational : Set where
|
|
|
195 field
|
|
|
196 rp rm k : ℕ
|
|
|
197 0<k : 0 < k
|
|
|
198
|
|
|
199 hR : ℕ → ℕ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
|
|
18
|
200 hR x y k ne = hr (hZ x y) k ne
|
|
|
201
|
|
20
|
202 rH : (r : Rational ) → HyperR
|
|
|
203 rH r = hr (hZ (Rational.rp r) (Rational.rm r)) (h (Rational.k r)) {!!}
|
|
|
204
|
|
22
|
205 nH : (r : ℕ ) → HyperR
|
|
|
206 nH r = hr (hZ r 0) (h 1) {!!}
|
|
|
207
|
|
19
|
208 --
|
|
|
209 -- z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0
|
|
|
210 --
|
|
5
|
211 _h=_ : (i j : HyperR ) → Set
|
|
19
|
212 hr z0 k0 ne0 h= hr z1 k1 ne1 = (z0 z* (hz k1 (h 0))) z= (z1 z* (hz k0 (h 0)))
|
|
5
|
213
|
|
|
214 _h≤_ : (i j : HyperR ) → Set
|
|
19
|
215 hr z0 k0 ne0 h≤ hr z1 k1 ne1 = (z0 z* (hz k1 (h 0))) z≤ (z1 z* (hz k0 (h 0)))
|
|
|
216
|
|
|
217 _h<_ : (i j : HyperR ) → Set
|
|
|
218 hr z0 k0 ne0 h< hr z1 k1 ne1 = (z0 z* (hz k1 (h 0))) z< (z1 z* (hz k0 (h 0)))
|
|
|
219
|
|
|
220 <-cmph : Trichotomous {Level.zero} _h=_ _h<_
|
|
|
221 <-cmph (hr z0 k0 ne0 ) ( hr z1 k1 ne1 ) = <-cmpz (z0 z* (hz k1 (h 0))) (z1 z* (hz k0 (h 0)))
|
|
5
|
222
|
|
1
|
223 _h*_ : (i j : HyperR) → HyperR
|
|
20
|
224 hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) {!!}
|
|
1
|
225
|
|
|
226 _h+_ : (i j : HyperR) → HyperR
|
|
20
|
227 hr x k nz h+ hr y k₁ nz₁ = hr ( (x z* (hz k hzero)) z+ (y z* (hz k₁ hzero)) ) (k n* k₁) {!!}
|
|
|
228
|
|
|
229 -h : (i : HyperR) → HyperR
|
|
|
230 -h (hr x k nz) = hr (-z x) k nz
|
|
|
231
|
|
|
232 inifinitesimal-R : (inf : HyperR) → Set
|
|
|
233 inifinitesimal-R inf = ( r : Rational ) → R0 h< rH r → ( -h (rH r) h< inf ) ∧ ( inf h< rH r)
|
|
|
234
|
|
|
235 1/x : HyperR
|
|
|
236 1/x = hr (hZ 1 0) n-linear {!!}
|
|
|
237
|
|
|
238 1/x-is-inifinitesimal : inifinitesimal-R 1/x
|
|
|
239 1/x-is-inifinitesimal r 0<r = ⟪ {!!} , {!!} ⟫
|
|
1
|
240
|
|
18
|
241 HyperReal : Set
|
|
|
242 HyperReal = ℕ → HyperR
|
|
|
243
|
|
|
244 HR→HRl : HyperR → HyperReal
|
|
|
245 HR→HRl (hr (hz x y) k ne) k1 = hr (hz (λ k2 → (x k1)) (λ k2 → (x k1))) k ne
|
|
|
246
|
|
|
247 HRl→HR : HyperReal → HyperR
|
|
|
248 HRl→HR r = hr (hz (λ k → {!!}) (λ k → {!!}) ) factor {!!} where
|
|
|
249 factor : HyperNat
|
|
|
250 factor n = {!!}
|
|
|
251 fne : (n : ℕ) → ¬ (factor n= h 0)
|
|
19
|
252 fne = {!!}
|
|
20
|
253
|
|
|
254 _≈_ : (x y : HyperR ) → Set
|
|
|
255 x ≈ y = inifinitesimal-R (x h+ ( -h y ))
|
|
|
256
|
|
21
|
257 is-inifinitesimal : {x : HyperR } → inifinitesimal-R x → x ≈ R0
|
|
|
258 is-inifinitesimal {x} inf = {!!}
|
|
|
259
|
|
|
260 record Standard : Set where
|
|
20
|
261 field
|
|
21
|
262 standard : HyperR → HyperR
|
|
|
263 is-standard : {x : HyperR } → x ≈ standard x
|
|
|
264 standard-unique : {x y : HyperR } → x ≈ y → standard x ≡ standard y
|
|
22
|
265 st-inifinitesimal : {x : HyperR } → inifinitesimal-R x → standard x ≡ R0
|
|
|
266 st-ℕ : {x : HyperR } → { i : ℕ } → x ≈ nH i → standard x ≡ nH i
|
|
21
|
267
|
|
|
268 postulate
|
|
|
269 ST : Standard
|
|
|
270
|
|
|
271 open Standard
|
|
|
272
|
|
|
273 st : HyperR → HyperR
|
|
|
274 st x = standard ST x
|
|
20
|
275
|
|
22
|
276 open import Algebra.Structures
|
|
|
277 open import Algebra.Bundles
|
|
|
278
|
|
|
279 HRing : CommutativeRing Level.zero Level.zero
|
|
|
280 HRing = record {
|
|
|
281 Carrier = HyperR
|
|
|
282 ; _≈_ = _h=_
|
|
|
283 ; _+_ = _h+_
|
|
|
284 ; _*_ = _h*_
|
|
|
285 ; -_ = -h
|
|
|
286 ; 0# = R0
|
|
|
287 ; 1# = R1
|
|
|
288 ; isCommutativeRing = {!!}
|
|
|
289 }
|
|
20
|
290
|
|
|
291
|
|
22
|
292 transfer : ( p : Rational ∨ HyperR → Set )
|
|
|
293 → ((x : Rational ) → p (case1 x) )
|
|
|
294 → ((x : HyperR ) → p (case2 x))
|
|
|
295 transfer = {!!}
|
