Mercurial > hg > Members > kono > Proof > HyperReal

comparison src/HyperReal.agda @ 4:f094694aeec5

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:00:15 +0900
parents 04f0b553db34
children ebc18df12f5a
comparison
equal deleted inserted replaced
3:04f0b553db34 4:f094694aeec5
6 open import Relation.Nullary using (¬_; Dec; yes; no) 6 open import Relation.Nullary using (¬_; Dec; yes; no)
7 open import Level renaming ( suc to succ ; zero to Zero ) 7 open import Level renaming ( suc to succ ; zero to Zero )
8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
9 open import Relation.Binary.Definitions 9 open import Relation.Binary.Definitions
10 open import Function.Bijection 10 open import Function.Bijection
11 open import Relation.Binary.Structures
11 open import nat 12 open import nat
12 open import logic 13 open import logic
13 14
14 HyperNat : Set 15 HyperNat : Set
15 HyperNat = ℕ → ℕ 16 HyperNat = ℕ → ℕ
102 is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (≤-map k) 103 is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (≤-map k)
103 104
104 postulate 105 postulate
105 _cmpn_ : ( i j : HyperNat ) → Dec ( i n≤ j ) 106 _cmpn_ : ( i j : HyperNat ) → Dec ( i n≤ j )
106 107
108 HNTotalOrder : IsTotalPreorder HyperNat ? _n≤_
109 HNTotalOrder = ?
110
107 111
108 data HyperZ : Set where 112 data HyperZ : Set where
109 hz : HyperNat → HyperNat → HyperZ 113 hz : HyperNat → HyperNat → HyperZ
110 114
111 _z*_ : (i j : HyperZ ) → HyperZ 115 _z*_ : (i j : HyperZ ) → HyperZ
120 HNzero i = ( k : ℕ ) → i k ≡ 0 124 HNzero i = ( k : ℕ ) → i k ≡ 0
121 125
122 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j 126 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
123 ≤→= {0} {0} z≤n z≤n = refl 127 ≤→= {0} {0} z≤n z≤n = refl
124 ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i ) 128 ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
129
130
125 131
126 HNzero? : ( i : HyperNat ) → Dec (HNzero i) 132 HNzero? : ( i : HyperNat ) → Dec (HNzero i)
127 HNzero? i with i cmpn hzero | hzero cmpn i 133 HNzero? i with i cmpn hzero | hzero cmpn i
128 ... | no s | t = no (λ n → s {!!}) -- (k₁ : ℕ) → i k₁ ≡ 0 → i k ≤ 0 134 ... | no s | t = no (λ n → s {!!}) -- (k₁ : ℕ) → i k₁ ≡ 0 → i k ≤ 0
129 ... | s | no t = no (λ n → t {!!}) 135 ... | s | no t = no (λ n → t {!!})