|
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
|
|
|
10
|
|
|
11 hnzero : (ℕ → ℕ) → Set
|
|
|
12 hnzero f = (x : ℕ) → ¬ ( x ≡ zero )
|
|
|
13
|
|
|
14 data HyperReal : Set where
|
|
|
15 hnat : (ℕ → ℕ) → HyperReal
|
|
|
16 hadd : HyperReal → (x : ℕ → ℕ ) → HyperReal
|
|
|
17 hsub : HyperReal → (x : ℕ → ℕ ) → HyperReal
|
|
|
18 hdiv : HyperReal → (x : ℕ → ℕ ) → hnzero x → HyperReal
|
|
|
19
|
|
|
20 data Rational : Set where
|
|
|
21 rat : ℕ → ℕ → (z : ℕ) → ¬ (z ≡ zero) → Rational -- (x - y ) / z
|
|
|
22
|
|
|
23 prat : Rational → ℕ
|
|
|
24 prat (rat x _ _ _ ) = x
|
|
|
25
|
|
|
26 mrat : Rational → ℕ
|
|
|
27 mrat (rat _ y _ _ ) = y
|
|
|
28
|
|
|
29 drat : Rational → ℕ
|
|
|
30 drat (rat _ _ z _ ) = z
|
|
|
31
|
|
|
32 zrat : (r : Rational ) → ¬ (drat r ≡ zero)
|
|
|
33 zrat (rat _ _ z ne ) = ne
|
|
|
34
|
|
|
35 HyRa←R : HyperReal → (ℕ → Rational)
|
|
|
36 HyRa←R (hnat x) i = rat (x i) 0 1 (λ ())
|
|
|
37 HyRa←R (hadd x y) i with HyRa←R x i
|
|
|
38 ... | rat w v z ne = rat (w + z * (y i)) v z ne
|
|
|
39 HyRa←R (hsub x y) i with HyRa←R x i
|
|
|
40 ... | rat w v z ne = rat w (v + z * (y i)) z ne
|
|
|
41 HyRa←R (hdiv x y nz) i with HyRa←R x i
|
|
|
42 ... | rat w v z ne = rat w v (z * (y i)) {!!}
|
|
|
43
|
|
|
44 HyR←Ra : (ℕ → Rational) → HyperReal
|
|
|
45 HyR←Ra r = hdiv (hsub (hnat (λ i → prat (r i))) (λ i → mrat (r i))) (λ i → drat (r i)) {!!}
|
