Mercurial > hg > Members > kono > Proof > HyperReal

comparison src/HyperReal.agda @ 0:8c492c69514c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HyperReal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Mar 2021 16:55:49 +0900
parents
children b50a277631e1
comparison
equal deleted inserted replaced
-1:000000000000 0:8c492c69514c
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)) {!!}