Mercurial > hg > Members > kono > Proof > HyperReal

comparison src/HyperReal.agda @ 5:ebc18df12f5a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Jul 2021 22:58:09 +0900
parents f094694aeec5
children b7c2a67befdf
comparison
equal deleted inserted replaced
4:f094694aeec5 5:ebc18df12f5a
13 open import logic 13 open import logic
14 14
15 HyperNat : Set 15 HyperNat : Set
16 HyperNat = ℕ → ℕ 16 HyperNat = ℕ → ℕ
17 17
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
18 record NxN : Set where 26 record NxN : Set where
19 field 27 field
20 nxn→n : ℕ ∧ ℕ → ℕ 28 nxn→n : ℕ ∧ ℕ → ℕ
21 n→nxn : ℕ → ℕ ∧ ℕ 29 n→nxn : ℕ → ℕ ∧ ℕ
22 nn-id : (i j : ℕ) → n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫ 30 nn-id : (i j : ℕ) → n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫
23 n-id : (i : ℕ) → nxn→n (n→nxn i ) ≡ i 31 n-id : (i : ℕ) → nxn→n (n→nxn i ) ≡ i
24
25 32
26 open _∧_ 33 open _∧_
27 34
28 -- t1 : nxn→n 0 1 ≡ 1 35 -- t1 : nxn→n 0 1 ≡ 1
29 -- t1 = refl 36 -- t1 = refl
92 i n* j = λ k → i (n1 k) * j (n2 k) 99 i n* j = λ k → i (n1 k) * j (n2 k)
93 100
94 hzero : HyperNat 101 hzero : HyperNat
95 hzero _ = 0 102 hzero _ = 0
96 103
104 record _n=_ (i j : HyperNat ) : Set where
105 field
106 =-map : IsoN
107 =-m : ℕ
108 is-n= : (k : ℕ ) → k > =-m → i k ≡ j (m→ =-map k)
109
97 -- 110 --
98 -- 111 --
99 record _n≤_ (i j : HyperNat ) : Set where 112 record _n≤_ (i j : HyperNat ) : Set where
100 field 113 field
101 ≤-map : ℕ → ℕ 114 ≤-map : IsoN
102 ≤-m : ℕ 115 ≤-m : ℕ
103 is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (≤-map k) 116 is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (m→ ≤-map k)
104 117
105 postulate 118 postulate
106 _cmpn_ : ( i j : HyperNat ) → Dec ( i n≤ j ) 119 _cmpn_ : ( i j : HyperNat ) → Dec ( i n≤ j )
107 120
108 HNTotalOrder : IsTotalPreorder HyperNat ? _n≤_ 121 HNTotalOrder : IsTotalPreorder _n=_ _n≤_
109 HNTotalOrder = ? 122 HNTotalOrder = record {
123 isPreorder = record {
124 isEquivalence = {!!}
125 ; reflexive = {!!}
126 ; trans = {!!} }
127 ; total = {!!}
128 }
110 129
111 130
112 data HyperZ : Set where 131 data HyperZ : Set where
113 hz : HyperNat → HyperNat → HyperZ 132 hz : HyperNat → HyperNat → HyperZ
114 133
120 -- ( i - i₁ ) * ( j - j₁ ) = i * j + i₁ * j₁ - i * j₁ - i₁ * j 139 -- ( i - i₁ ) * ( j - j₁ ) = i * j + i₁ * j₁ - i * j₁ - i₁ * j
121 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 ) 140 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 )
122 141
123 HNzero : HyperNat → Set 142 HNzero : HyperNat → Set
124 HNzero i = ( k : ℕ ) → i k ≡ 0 143 HNzero i = ( k : ℕ ) → i k ≡ 0
144
145 _z=_ : (i j : HyperZ ) → Set
146 _z=_ = {!!}
147
148 _z≤_ : (i j : HyperZ ) → Set
149 _z≤_ = {!!}
125 150
126 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j 151 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
127 ≤→= {0} {0} z≤n z≤n = refl 152 ≤→= {0} {0} z≤n z≤n = refl
128 ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i ) 153 ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
129 154
173 ... | no t | no s = {!!} 198 ... | no t | no s = {!!}
174 199
175 HRzero : HyperR → Set 200 HRzero : HyperR → Set
176 HRzero (hr i j nz ) = HZzero i 201 HRzero (hr i j nz ) = HZzero i
177 202
203 _h=_ : (i j : HyperR ) → Set
204 _h=_ = {!!}
205
206 _h≤_ : (i j : HyperR ) → Set
207 _h≤_ = {!!}
208
178 _h*_ : (i j : HyperR) → HyperR 209 _h*_ : (i j : HyperR) → HyperR
179 210
180 _h+_ : (i j : HyperR) → HyperR 211 _h+_ : (i j : HyperR) → HyperR
181 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₁) 212 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₁)
182 213