|
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)
|
|
|
7 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
9 open import Relation.Binary.Definitions
|
|
3
|
10 open import Function.Bijection
|
|
4
|
11 open import Relation.Binary.Structures
|
|
1
|
12 open import nat
|
|
|
13 open import logic
|
|
0
|
14
|
|
1
|
15 HyperNat : Set
|
|
|
16 HyperNat = ℕ → ℕ
|
|
|
17
|
|
5
|
18 record IsoN : Set where
|
|
|
19 field
|
|
|
20 m→ m← : ℕ → ℕ
|
|
|
21 id→← : (i : ℕ) → m→ (m← i ) ≡ i
|
|
|
22 id←→ : (i : ℕ) → m← (m→ i ) ≡ i
|
|
|
23
|
|
|
24 open IsoN
|
|
|
25
|
|
2
|
26 record NxN : Set where
|
|
|
27 field
|
|
|
28 nxn→n : ℕ ∧ ℕ → ℕ
|
|
|
29 n→nxn : ℕ → ℕ ∧ ℕ
|
|
|
30 nn-id : (i j : ℕ) → n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫
|
|
|
31 n-id : (i : ℕ) → nxn→n (n→nxn i ) ≡ i
|
|
|
32
|
|
|
33 open _∧_
|
|
|
34
|
|
|
35 nxn : NxN
|
|
|
36 nxn = record {
|
|
|
37 nxn→n = λ p → nxn→n (proj1 p) (proj2 p)
|
|
|
38 ; n→nxn = n→nxn
|
|
6
|
39 ; nn-id = nn-id
|
|
|
40 ; n-id = n-id
|
|
2
|
41 } where
|
|
|
42 nxn→n : ℕ → ℕ → ℕ
|
|
|
43 nxn→n zero zero = zero
|
|
|
44 nxn→n zero (suc j) = j + suc (nxn→n zero j)
|
|
|
45 nxn→n (suc i) zero = suc i + suc (nxn→n i zero)
|
|
|
46 nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j))
|
|
|
47 n→nxn : ℕ → ℕ ∧ ℕ
|
|
|
48 n→nxn zero = ⟪ 0 , 0 ⟫
|
|
|
49 n→nxn (suc i) with n→nxn i
|
|
|
50 ... | ⟪ x , zero ⟫ = ⟪ zero , suc x ⟫
|
|
|
51 ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
|
|
6
|
52 nid1 : (i : ℕ) → 0 < proj2 ( n→nxn i) → n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
|
|
7
|
53 nid1 (suc i) 0<p2 with n→nxn (suc i)
|
|
|
54 ... | ⟪ x , zero ⟫ = ⊥-elim ( nat-≤> 0<p2 a<sa )
|
|
|
55 ... | ⟪ x , suc y ⟫ = refl
|
|
|
56 nid4 : {i j : ℕ} → i + 1 + j ≡ i + suc j
|
|
|
57 nid4 {zero} {j} = refl
|
|
|
58 nid4 {suc i} {j} = cong suc (nid4 {i} {j} )
|
|
|
59 nid5 : {i j k : ℕ} → i + suc (suc j) + suc k ≡ i + suc j + suc (suc k )
|
|
|
60 nid5 {zero} {j} {k} = begin
|
|
|
61 suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩
|
|
|
62 1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩
|
|
|
63 (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩
|
|
|
64 suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩
|
|
|
65 suc j + suc (suc k) ∎ where open ≡-Reasoning
|
|
|
66 nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
|
|
6
|
67 nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
|
|
|
68 nid2 zero zero = refl
|
|
|
69 nid2 zero (suc j) = refl
|
|
7
|
70 nid2 (suc i) zero = begin
|
|
|
71 suc (nxn→n (suc i) 1) ≡⟨ refl ⟩
|
|
|
72 suc (suc (i + 1 + suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (suc k)) nid4 ⟩
|
|
|
73 suc (suc (i + suc (suc (nxn→n i 1)))) ≡⟨ cong (λ k → suc (suc (i + suc (suc k)))) (nid3 i) ⟩
|
|
|
74 suc (suc (i + suc (suc (i + suc (nxn→n i 0))))) ≡⟨ refl ⟩
|
|
|
75 nxn→n (suc (suc i)) zero ∎ where
|
|
|
76 open ≡-Reasoning
|
|
|
77 nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0)
|
|
|
78 nid3 zero = refl
|
|
|
79 nid3 (suc i) = begin
|
|
|
80 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
|
|
|
81 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (i + suc (suc k))) (nid3 i) ⟩
|
|
|
82 suc (i + suc (suc (i + suc (nxn→n i 0))))
|
|
|
83 ∎
|
|
|
84 nid2 (suc i) (suc j) = begin
|
|
|
85 suc (nxn→n (suc i) (suc (suc j))) ≡⟨ refl ⟩
|
|
|
86 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)) ⟩
|
|
|
87 suc (suc (i + suc (suc j) + suc (i + suc j + suc (nxn→n i (suc j))))) ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩
|
|
|
88 suc (suc (i + suc j + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩
|
|
|
89 nxn→n (suc (suc i)) (suc j) ∎ where
|
|
|
90 open ≡-Reasoning
|
|
|
91 nid6 : {i : ℕ } → 0 < i → suc (pred i) ≡ i
|
|
|
92 nid6 {suc i} 0<i = refl
|
|
6
|
93 n-id : (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
|
|
|
94 n-id 0 = refl
|
|
7
|
95 n-id (suc i) with proj2 (n→nxn (suc i)) | inspect proj2 (n→nxn (suc i))
|
|
|
96 ... | zero | record { eq = eq } = {!!}
|
|
|
97 ... | suc x | record { eq = eq } with proj2 (n→nxn i) | inspect proj2 (n→nxn i)
|
|
|
98 ... | zero | record { eq = eqy } = {!!}
|
|
|
99 ... | suc y | record { eq = eqy } = begin
|
|
|
100 nxn→n (proj1 (n→nxn (suc i))) (suc x) ≡⟨ cong (λ k → nxn→n (proj1 k) (suc x)) (nid1 i nid7 ) ⟩
|
|
|
101 nxn→n (suc (proj1 (n→nxn i))) (suc x) ≡⟨ sym (nid2 (proj1 (n→nxn i)) (suc x) ) ⟩
|
|
|
102 suc (nxn→n (proj1 (n→nxn i)) (suc (suc x))) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) (suc k))) (sym eq) ⟩
|
|
|
103 suc (nxn→n (proj1 (n→nxn i)) (suc (proj2 (n→nxn (suc i))))) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) k)) ( begin
|
|
|
104 suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7)) ⟩
|
|
|
105 suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩
|
|
|
106 proj2 (n→nxn i) ∎ )⟩
|
|
|
107 suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩
|
|
|
108 suc i ∎ where
|
|
|
109 open ≡-Reasoning
|
|
|
110 nid7 : 0 < proj2 (n→nxn i)
|
|
|
111 nid7 = subst (λ k → 0 < k ) (sym eqy) (s≤s z≤n)
|
|
|
112 nid8 : suc (proj2 (n→nxn (suc i))) ≡ proj2 (n→nxn i)
|
|
|
113 nid8 = begin
|
|
|
114 suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7 )) ⟩
|
|
|
115 suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩
|
|
|
116 proj2 (n→nxn i) ∎
|
|
6
|
117 f : (i : ℕ) → Set
|
|
|
118 f i = n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
|
|
|
119 g : (i j : ℕ) → Set
|
|
|
120 g i j = suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
|
|
2
|
121 nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
|
|
6
|
122 nn-id = {!!}
|
|
2
|
123
|
|
|
124 open NxN
|
|
|
125
|
|
|
126 n1 : ℕ → ℕ
|
|
|
127 n1 n = proj1 (n→nxn nxn n)
|
|
|
128
|
|
|
129 n2 : ℕ → ℕ
|
|
|
130 n2 n = proj2 (n→nxn nxn n)
|
|
|
131
|
|
1
|
132 _n*_ : (i j : HyperNat ) → HyperNat
|
|
|
133
|
|
|
134 _n+_ : (i j : HyperNat ) → HyperNat
|
|
2
|
135 i n+ j = λ k → i (n1 k) + j (n2 k)
|
|
1
|
136
|
|
2
|
137 i n* j = λ k → i (n1 k) * j (n2 k)
|
|
1
|
138
|
|
|
139 hzero : HyperNat
|
|
|
140 hzero _ = 0
|
|
|
141
|
|
5
|
142 record _n=_ (i j : HyperNat ) : Set where
|
|
|
143 field
|
|
|
144 =-map : IsoN
|
|
|
145 =-m : ℕ
|
|
|
146 is-n= : (k : ℕ ) → k > =-m → i k ≡ j (m→ =-map k)
|
|
|
147
|
|
3
|
148 --
|
|
|
149 --
|
|
|
150 record _n≤_ (i j : HyperNat ) : Set where
|
|
|
151 field
|
|
5
|
152 ≤-map : IsoN
|
|
3
|
153 ≤-m : ℕ
|
|
5
|
154 is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (m→ ≤-map k)
|
|
2
|
155
|
|
|
156 postulate
|
|
|
157 _cmpn_ : ( i j : HyperNat ) → Dec ( i n≤ j )
|
|
|
158
|
|
5
|
159 HNTotalOrder : IsTotalPreorder _n=_ _n≤_
|
|
|
160 HNTotalOrder = record {
|
|
|
161 isPreorder = record {
|
|
|
162 isEquivalence = {!!}
|
|
|
163 ; reflexive = {!!}
|
|
|
164 ; trans = {!!} }
|
|
|
165 ; total = {!!}
|
|
|
166 }
|
|
4
|
167
|
|
2
|
168
|
|
1
|
169 data HyperZ : Set where
|
|
|
170 hz : HyperNat → HyperNat → HyperZ
|
|
0
|
171
|
|
1
|
172 _z*_ : (i j : HyperZ ) → HyperZ
|
|
|
173
|
|
|
174 _z+_ : (i j : HyperZ ) → HyperZ
|
|
|
175 hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ )
|
|
0
|
176
|
|
1
|
177 -- ( i - i₁ ) * ( j - j₁ ) = i * j + i₁ * j₁ - i * j₁ - i₁ * j
|
|
|
178 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 )
|
|
|
179
|
|
|
180 HNzero : HyperNat → Set
|
|
|
181 HNzero i = ( k : ℕ ) → i k ≡ 0
|
|
0
|
182
|
|
5
|
183 _z=_ : (i j : HyperZ ) → Set
|
|
|
184 _z=_ = {!!}
|
|
|
185
|
|
|
186 _z≤_ : (i j : HyperZ ) → Set
|
|
|
187 _z≤_ = {!!}
|
|
|
188
|
|
2
|
189 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
|
|
|
190 ≤→= {0} {0} z≤n z≤n = refl
|
|
|
191 ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
|
|
|
192
|
|
4
|
193
|
|
|
194
|
|
1
|
195 HNzero? : ( i : HyperNat ) → Dec (HNzero i)
|
|
2
|
196 HNzero? i with i cmpn hzero | hzero cmpn i
|
|
3
|
197 ... | no s | t = no (λ n → s {!!}) -- (k₁ : ℕ) → i k₁ ≡ 0 → i k ≤ 0
|
|
|
198 ... | s | no t = no (λ n → t {!!})
|
|
|
199 ... | yes s | yes t = yes (λ k → {!!} )
|
|
2
|
200
|
|
|
201 record HNzeroK ( x : HyperNat ) : Set where
|
|
|
202 field
|
|
|
203 nonzero : ℕ
|
|
|
204 isNonzero : ¬ ( x nonzero ≡ 0 )
|
|
|
205
|
|
|
206 postulate
|
|
|
207 HNnzerok : (x : HyperNat ) → ¬ ( HNzero x ) → HNzeroK x
|
|
|
208
|
|
|
209 import Axiom.Extensionality.Propositional
|
|
|
210 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m
|
|
|
211
|
|
|
212 m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
|
|
|
213 m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl
|
|
|
214 m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl
|
|
0
|
215
|
|
1
|
216 HNnzero* : {x y : HyperNat } → ¬ ( HNzero x ) → ¬ ( HNzero y ) → ¬ ( HNzero (x n* y) )
|
|
2
|
217 HNnzero* {x} {y} nzx nzy nzx*y with HNnzerok x nzx | HNnzerok y nzy
|
|
|
218 ... | s | t = {!!} where
|
|
|
219 hnz0 : ( k : ℕ ) → x k * y k ≡ 0 → (x k ≡ 0) ∨ (y k ≡ 0)
|
|
|
220 hnz0 k x*y = m*n=0⇒m=0∨n=0 x*y
|
|
0
|
221
|
|
1
|
222
|
|
|
223 HZzero : HyperZ → Set
|
|
|
224 HZzero (hz i j ) = ( k : ℕ ) → i k ≡ j k
|
|
0
|
225
|
|
1
|
226 HZzero? : ( i : HyperZ ) → Dec (HZzero i)
|
|
|
227 HZzero? = {!!}
|
|
|
228
|
|
|
229 data HyperR : Set where
|
|
|
230 hr : HyperZ → (k : HyperNat ) → ¬ HNzero k → HyperR
|
|
0
|
231
|
|
1
|
232 HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
|
|
|
233 HZnzero* {x} {y} nzx nzy nzx*y with HZzero? x | HZzero? y
|
|
|
234 ... | yes t | s = ⊥-elim ( nzx t )
|
|
|
235 ... | t | yes s = ⊥-elim ( nzy s )
|
|
|
236 ... | no t | no s = {!!}
|
|
|
237
|
|
|
238 HRzero : HyperR → Set
|
|
|
239 HRzero (hr i j nz ) = HZzero i
|
|
|
240
|
|
5
|
241 _h=_ : (i j : HyperR ) → Set
|
|
|
242 _h=_ = {!!}
|
|
|
243
|
|
|
244 _h≤_ : (i j : HyperR ) → Set
|
|
|
245 _h≤_ = {!!}
|
|
|
246
|
|
1
|
247 _h*_ : (i j : HyperR) → HyperR
|
|
|
248
|
|
|
249 _h+_ : (i j : HyperR) → HyperR
|
|
|
250 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₁)
|
|
|
251
|
|
|
252 hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁)
|
