Mercurial > hg > Members > kono > Proof > HyperReal
view src/HyperReal.agda @ 19:f0763f51631e
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 08 Jul 2021 14:23:36 +0900 |
parents | 9fefd6c7fb77 |
children | a839f149825f |
line wrap: on
line source
module HyperReal where open import Data.Nat open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary using (¬_; Dec; yes; no) open import Level renaming ( suc to succ ; zero to Zero ; _⊔_ to _L⊔_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Binary.Definitions open import Relation.Binary.Structures open import nat open import logic open import bijection HyperNat : Set HyperNat = ℕ → ℕ open _∧_ open Bijection n1 : ℕ → ℕ n1 n = proj1 (fun→ nxn n) n2 : ℕ → ℕ n2 n = proj2 (fun→ nxn n) _n*_ : (i j : HyperNat ) → HyperNat i n* j = λ k → i k * j k _n+_ : (i j : HyperNat ) → HyperNat i n+ j = λ k → i k + j k hzero : HyperNat hzero _ = 0 h : (n : ℕ) → HyperNat h n _ = n record _n=_ (i j : HyperNat ) : Set where field =-map : Bijection ℕ ℕ =-m : ℕ is-n= : (k : ℕ ) → k > =-m → i k ≡ j (fun→ =-map k) open _n=_ record _n≤_ (i j : HyperNat ) : Set where field ≤-map : Bijection ℕ ℕ ≤-m : ℕ is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map k) open _n≤_ record _n<_ (i j : HyperNat ) : Set where field <-map : Bijection ℕ ℕ <-m : ℕ is-n< : (k : ℕ ) → k > <-m → i k < j (fun→ <-map k) open _n<_ _n<=s≤_ : (i j : HyperNat ) → (i n< j) ⇔ (( i n+ h 1 ) n≤ j ) _n<=s≤_ = {!!} ¬hn<0 : {x : HyperNat } → ¬ ( x n< h 0 ) ¬hn<0 {x} x<0 = ⊥-elim ( nat-≤> (is-n< x<0 (suc (<-m x<0)) a<sa) 0<s ) postulate <-cmpn : Trichotomous {Level.zero} _n=_ _n<_ n=IsEquivalence : IsEquivalence _n=_ n=IsEquivalence = record { refl = record {=-map = bid ℕ ; =-m = 0 ; is-n= = λ _ _ → refl} ; sym = λ xy → record {=-map = bi-sym ℕ ℕ (=-map xy) ; =-m = =-m xy ; is-n= = λ k lt → {!!} } -- (is-n= xy k lt) } ; trans = λ xy yz → record {=-map = bi-trans ℕ ℕ ℕ (=-map xy) (=-map yz) ; =-m = {!!} ; is-n= = λ k lt → {!!} } } HNTotalOrder : IsTotalPreorder _n=_ _n≤_ HNTotalOrder = record { isPreorder = record { isEquivalence = n=IsEquivalence ; reflexive = λ eq → record { ≤-map = =-map eq ; ≤-m = =-m eq ; is-n≤ = {!!} } ; trans = trans1 } ; total = total } where open import Data.Sum.Base using (_⊎_) open _⊎_ total : (x y : HyperNat ) → (x n≤ y) ⊎ (y n≤ x) total x y with <-cmpn x y ... | tri< a ¬b ¬c = inj₁ {!!} ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b c = {!!} trans1 : {i j k : HyperNat} → i n≤ j → j n≤ k → i n≤ k trans1 = {!!} data HyperZ : Set where hz : HyperNat → HyperNat → HyperZ hZ : ℕ → ℕ → HyperZ hZ x y = hz (λ _ → x) (λ _ → y ) _z+_ : (i j : HyperZ ) → HyperZ hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ ) _z*_ : (i j : HyperZ ) → HyperZ 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 ) -- x0 - y0 ≡ x1 - y1 -- x0 + y1 ≡ x1 + y0 -- _z=_ : (i j : HyperZ ) → Set _z=_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n= (x1 n+ y0) _z≤_ : (i j : HyperZ ) → Set _z≤_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n≤ (x1 n+ y0) _z<_ : (i j : HyperZ ) → Set _z<_ (hz x0 y0) (hz x1 y1) = (x0 n+ y1) n< (x1 n+ y0) <-cmpz : Trichotomous {Level.zero} _z=_ _z<_ <-cmpz (hz x0 y0) (hz x1 y1) = <-cmpn (x0 n+ y1) (x1 n+ y0) import Axiom.Extensionality.Propositional postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m --- x*y ...... 0 0 0 0 ... --- x ...... 0 0 1 0 1 .... --- y ...... 0 1 0 1 0 .... HNnzero* : {x y : HyperNat } → ¬ ( x n= h 0 ) → ¬ ( y n= h 0 ) → ¬ ( (x n* y) n= h 0 ) HNnzero* {x} {y} nzx nzy xy0 = hn1 where hn2 : ( h 0 n< x ) → ( h 0 n< y ) → ¬ ( (x n* y) n= h 0 ) hn2 0<x 0<y xy0 = ⊥-elim ( nat-≡< (sym (is-n= xy0 (suc mxy) {!!} )) {!!} ) where mxy : ℕ mxy = <-m 0<x ⊔ <-m 0<y ⊔ =-m xy0 hn1 : ⊥ hn1 with <-cmpn x (h 0) ... | tri≈ ¬a b ¬c = nzx b ... | tri< a ¬b ¬c = ⊥-elim ( ¬hn<0 a) hn1 | tri> ¬a ¬b c with <-cmpn y (h 0) ... | tri< a ¬b₁ ¬c = ⊥-elim ( ¬hn<0 a) ... | tri≈ ¬a₁ b ¬c = nzy b ... | tri> ¬a₁ ¬b₁ c₁ = hn2 c c₁ xy0 HZzero : HyperZ → Set HZzero z = hZ 0 0 z= z HZzero? : ( i : HyperZ ) → Dec (HZzero i) HZzero? = {!!} data HyperR : Set where hr : HyperZ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) ) HZnzero* {x} {y} nzx nzy nzx*y = {!!} HRzero : HyperR → Set HRzero (hr i j nz ) = HZzero i hR : ℕ → ℕ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR hR x y k ne = hr (hZ x y) k ne -- -- z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0 -- _h=_ : (i j : HyperR ) → Set hr z0 k0 ne0 h= hr z1 k1 ne1 = (z0 z* (hz k1 (h 0))) z= (z1 z* (hz k0 (h 0))) _h≤_ : (i j : HyperR ) → Set hr z0 k0 ne0 h≤ hr z1 k1 ne1 = (z0 z* (hz k1 (h 0))) z≤ (z1 z* (hz k0 (h 0))) _h<_ : (i j : HyperR ) → Set hr z0 k0 ne0 h< hr z1 k1 ne1 = (z0 z* (hz k1 (h 0))) z< (z1 z* (hz k0 (h 0))) <-cmph : Trichotomous {Level.zero} _h=_ _h<_ <-cmph (hr z0 k0 ne0 ) ( hr z1 k1 ne1 ) = <-cmpz (z0 z* (hz k1 (h 0))) (z1 z* (hz k0 (h 0))) _h*_ : (i j : HyperR) → HyperR hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁) _h+_ : (i j : HyperR) → HyperR 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₁) HyperReal : Set HyperReal = ℕ → HyperR HR→HRl : HyperR → HyperReal HR→HRl (hr (hz x y) k ne) k1 = hr (hz (λ k2 → (x k1)) (λ k2 → (x k1))) k ne HRl→HR : HyperReal → HyperR HRl→HR r = hr (hz (λ k → {!!}) (λ k → {!!}) ) factor {!!} where factor : HyperNat factor n = {!!} fne : (n : ℕ) → ¬ (factor n= h 0) fne = {!!}