Mercurial > hg > Members > kono > Proof > HyperReal
view src/HyperReal.agda @ 10:a4e441b7493b
too complex invariant
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Jul 2021 15:47:18 +0900 |
| parents | d7d7016764b5 |
| children | 2ce1c67dde0f |
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 ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Binary.Definitions open import Function.Bijection open import Relation.Binary.Structures open import nat open import logic HyperNat : Set HyperNat = ℕ → ℕ record IsoN : Set where field m→ m← : ℕ → ℕ id→← : (i : ℕ) → m→ (m← i ) ≡ i id←→ : (i : ℕ) → m← (m→ i ) ≡ i open IsoN record NxN : Set where field nxn→n : ℕ ∧ ℕ → ℕ n→nxn : ℕ → ℕ ∧ ℕ nn-id : (i j : ℕ) → n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫ n-id : (i : ℕ) → nxn→n (n→nxn i ) ≡ i open _∧_ record NN ( i j k : ℕ) : Set where field nn : (k + j ) * (k + suc j ) + j * 2 ≡ i * 2 ni : i ≡ 0 → j ≡ 0 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0 i≤0→i≡0 {0} z≤n = refl nxn : NxN nxn = record { nxn→n = λ p → nxn→n (proj1 p) (proj2 p) ; n→nxn = n→nxn ; nn-id = nn-id ; n-id = n-id } where nxn→n : ℕ → ℕ → ℕ nxn→n zero zero = zero nxn→n zero (suc j) = j + suc (nxn→n zero j) nxn→n (suc i) zero = suc i + suc (nxn→n i zero) nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j)) n→nxn : ℕ → ℕ ∧ ℕ n→nxn zero = ⟪ 0 , 0 ⟫ n→nxn (suc i) with n→nxn i ... | ⟪ x , zero ⟫ = ⟪ zero , suc x ⟫ ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫ nn→ : {i j k : ℕ } → NN i j k → NN (suc i) (proj1 (n→nxn (suc k))) (proj2 (n→nxn (suc k))) nn→ = {!!} nn←0 : {i j k : ℕ } → NN i j k → NN (nxn→n (suc j) k) (suc j) k nn←0 = {!!} nn←1 : {i j k : ℕ } → NN i j k → NN (nxn→n j (suc k)) j (suc k) nn←1 = {!!} nn= : {i j k : ℕ } → NN i j k → ( n→nxn i ≡ ⟪ j , k ⟫ ) ∧ ( nxn→n j k ≡ i ) nn= {i} {j} {k} nn = ⟪ nn=1 i j k nn , {!!} ⟫ where nn=1 : (i j k : ℕ ) → NN i j k → n→nxn i ≡ ⟪ j , k ⟫ nn=1 zero j k nn = cong₂ (λ x y → ⟪ x , y ⟫) (sym (NN.ni nn refl)) (sym (nn=2 {j} {k} {!!})) where nn=3 : {!!} nn=3 = NN.nn nn nn=2 : { j k : ℕ } → j + k ≡ 0 + j → k ≡ 0 nn=2 {zero} {k} eq = eq nn=2 {suc j} {k} eq = nn=2 {j} {k} (cong pred eq) nn=1 (suc i) j k nn = {!!} nn=4 : (i j k : ℕ ) → NN i j k → nxn→n j k ≡ i nn=4 i zero zero nn = subst (λ k → 0 ≡ k) (+-comm _ 0) {!!} nn=4 i zero (suc k) nn = begin -- 0 + suc k ≡ i + 0 nxn→n zero (suc k) ≡⟨ {!!} ⟩ k + suc (nxn→n 0 k) ≡⟨ {!!} ⟩ i ∎ where open ≡-Reasoning nn=4 i (suc j) k nn = {!!} nid1 : (i : ℕ) → 0 < proj2 (n→nxn i) → n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫ nid1 (suc i) 0<p2 with n→nxn (suc i) ... | ⟪ x , zero ⟫ = ⊥-elim ( nat-≤> 0<p2 a<sa ) ... | ⟪ x , suc y ⟫ = refl nid4 : {i j : ℕ} → i + 1 + j ≡ i + suc j nid4 {zero} {j} = refl nid4 {suc i} {j} = cong suc (nid4 {i} {j} ) nid5 : {i j k : ℕ} → i + suc (suc j) + suc k ≡ i + suc j + suc (suc k ) nid5 {zero} {j} {k} = begin suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩ 1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩ (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩ suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩ suc j + suc (suc k) ∎ where open ≡-Reasoning nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} ) nid0 : (i : ℕ) → 0 ≡ proj2 (n→nxn i) → n→nxn (suc i) ≡ ⟪ 0 , suc ( proj1 ( n→nxn i )) ⟫ nid0 zero eq = refl nid0 (suc i) eq with n→nxn (suc i) ... | ⟪ x , zero ⟫ = refl nid20 : (i : ℕ) → i + (nxn→n 0 i) ≡ nxn→n i 0 nid20 i = {!!} nid-case0 : (i : ℕ) → suc (pred (proj2 (n→nxn (suc i))) + suc (nxn→n ( pred (proj2 (n→nxn (suc i)))) 0)) ≡ suc (nxn→n (proj1 (n→nxn i)) 0) nid-case0 = {!!} nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j nid2 zero zero = refl nid2 zero (suc j) = refl nid2 (suc i) zero = begin suc (nxn→n (suc i) 1) ≡⟨ refl ⟩ suc (suc (i + 1 + suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (suc k)) nid4 ⟩ suc (suc (i + suc (suc (nxn→n i 1)))) ≡⟨ cong (λ k → suc (suc (i + suc (suc k)))) (nid3 i) ⟩ suc (suc (i + suc (suc (i + suc (nxn→n i 0))))) ≡⟨ refl ⟩ nxn→n (suc (suc i)) zero ∎ where open ≡-Reasoning nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0) nid3 zero = refl nid3 (suc i) = begin suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩ suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (i + suc (suc k))) (nid3 i) ⟩ suc (i + suc (suc (i + suc (nxn→n i 0)))) ∎ nid2 (suc i) (suc j) = begin suc (nxn→n (suc i) (suc (suc j))) ≡⟨ refl ⟩ suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j))))) ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩ suc (suc (i + suc (suc j) + suc (i + suc j + suc (nxn→n i (suc j))))) ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩ suc (suc (i + suc j + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩ nxn→n (suc (suc i)) (suc j) ∎ where open ≡-Reasoning nid6 : {i : ℕ } → 0 < i → suc (pred i) ≡ i nid6 {suc i} 0<i = refl n-id : (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i n-id 0 = refl n-id (suc i) with proj2 (n→nxn (suc i)) | inspect proj2 (n→nxn (suc i)) ... | zero | record { eq = eq } with proj1 (n→nxn (suc i)) | inspect proj1 (n→nxn (suc i)) ... | zero | record { eq = eqx } = ⊥-elim (nid13 i eqx eq) where -- ⟪ 0 , 0 ⟫ will not happen nid13 : (i : ℕ) → proj1 (n→nxn (suc i)) ≡ 0 → proj2 (n→nxn (suc i)) ≡ 0 → ⊥ nid13 (suc i) eq eq1 with n→nxn (suc i) | inspect n→nxn (suc i) ... | ⟪ x , suc y ⟫ | record { eq = eq2 } = nat-≡< (sym eq) (s≤s z≤n) ... | suc x | record { eq = eqx } with proj2 (n→nxn i) | inspect proj2 (n→nxn i) ... | zero | record { eq = eqy } = begin -- ⟪ m , 0 ⟫ → ⟪ 0 , suc x ⟫ suc (x + suc (nxn→n x 0)) ≡⟨ cong (λ k → suc (k + suc (nxn→n k 0))) refl ⟩ suc (pred (suc x) + suc (nxn→n (pred (suc x)) 0)) ≡⟨ cong (λ k → suc (pred k + suc (nxn→n (pred k) 0))) (sym eqx) ⟩ suc (pred (proj1 (n→nxn (suc i))) + suc (nxn→n ( pred (proj1 (n→nxn (suc i)))) 0)) ≡⟨ {!!} ⟩ suc (nxn→n (proj1 (n→nxn i)) 0) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) k )) (sym eqy) ⟩ suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩ suc i ∎ where open ≡-Reasoning ... | suc y | record { eq = eqy } = begin -- ⟪ pred n , 1 ⟫ → ⟪ n , 0 ⟫ nxn→n (suc x) 0 ≡⟨ sym (nid2 x 0) ⟩ suc (nxn→n x 1) ≡⟨ cong₂ (λ j k → suc (nxn→n j k) ) nid9 nid10 ⟩ suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩ suc i ∎ where open ≡-Reasoning nid11 : 0 < proj2 (n→nxn i) nid11 = subst (λ k → 0 < k ) (sym eqy) (s≤s z≤n) nid9 : x ≡ proj1 (n→nxn i) nid9 = begin x ≡⟨ sym (cong pred eqx) ⟩ pred (proj1 (n→nxn (suc i))) ≡⟨ cong pred (cong proj1 (nid1 i nid11)) ⟩ pred (suc (proj1 (n→nxn i))) ≡⟨ refl ⟩ proj1 (n→nxn i) ∎ nid10 : 1 ≡ proj2 (n→nxn i) nid10 = begin 1 ≡⟨ cong suc (sym eq) ⟩ suc ( proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid11)) ⟩ suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid11 ⟩ proj2 (n→nxn i) ∎ n-id (suc i) | suc x | record { eq = eqx } with proj2 (n→nxn i) | inspect proj2 (n→nxn i) -- eqy : proj2 (n→nxn i) ≡ zero -- eq : proj2 (n→nxn (suc i) | n→nxn i) ≡ suc x ... | zero | record { eq = eqy } = begin -- ⟪ x , 0 ⟫ → ⟪ 0 , suc x ⟫ nxn→n (proj1 (n→nxn (suc i))) (suc x) ≡⟨ {!!} ⟩ suc (x + suc (nxn→n x 0)) ≡⟨ {!!} ⟩ suc (x + suc (nxn→n x 0)) ≡⟨ cong (λ k → suc (k + suc (nxn→n k 0))) refl ⟩ suc (pred (suc x) + suc (nxn→n (pred (suc x)) 0)) ≡⟨ cong (λ k → suc (pred k + suc (nxn→n (pred k) 0))) (sym eqx) ⟩ suc (pred (proj2 (n→nxn (suc i))) + suc (nxn→n ( pred (proj2 (n→nxn (suc i)))) 0)) ≡⟨ nid-case0 i ⟩ suc (nxn→n (proj1 (n→nxn i)) 0) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) k )) (sym eqy) ⟩ suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩ suc i ∎ where open ≡-Reasoning ... | suc y | record { eq = eqy } = begin -- ⟪ pred n , suc y ⟫ → ⟪ n , y ⟫ nxn→n (proj1 (n→nxn (suc i))) (suc x) ≡⟨ cong (λ k → nxn→n (proj1 k) (suc x)) (nid1 i nid7 ) ⟩ nxn→n (suc (proj1 (n→nxn i))) (suc x) ≡⟨ sym (nid2 (proj1 (n→nxn i)) (suc x) ) ⟩ suc (nxn→n (proj1 (n→nxn i)) (suc (suc x))) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) (suc k))) (sym eqx) ⟩ suc (nxn→n (proj1 (n→nxn i)) (suc (proj2 (n→nxn (suc i))))) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) k)) ( begin suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7)) ⟩ suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩ proj2 (n→nxn i) ∎ )⟩ suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩ suc i ∎ where open ≡-Reasoning nid7 : 0 < proj2 (n→nxn i) nid7 = subst (λ k → 0 < k ) (sym eqy) (s≤s z≤n) nid8 : suc (proj2 (n→nxn (suc i))) ≡ proj2 (n→nxn i) nid8 = begin suc (proj2 (n→nxn (suc i))) ≡⟨ cong suc (cong proj2 (nid1 i nid7 )) ⟩ suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩ proj2 (n→nxn i) ∎ f : (i : ℕ) → Set f i = (k + j ) * (k + suc j ) ≡ (i - j) * 2 where -- 0 n ... Σ n = (n + 1 ) n / 2 = j = proj1 (n→nxn i) k = proj2 (n→nxn i) nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫ nn-id = {!!} open NxN n1 : ℕ → ℕ n1 n = proj1 (n→nxn nxn n) n2 : ℕ → ℕ n2 n = proj2 (n→nxn nxn n) _n*_ : (i j : HyperNat ) → HyperNat _n+_ : (i j : HyperNat ) → HyperNat i n+ j = λ k → i (n1 k) + j (n2 k) i n* j = λ k → i (n1 k) * j (n2 k) hzero : HyperNat hzero _ = 0 record _n=_ (i j : HyperNat ) : Set where field =-map : IsoN =-m : ℕ is-n= : (k : ℕ ) → k > =-m → i k ≡ j (m→ =-map k) -- -- record _n≤_ (i j : HyperNat ) : Set where field ≤-map : IsoN ≤-m : ℕ is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (m→ ≤-map k) postulate _cmpn_ : ( i j : HyperNat ) → Dec ( i n≤ j ) HNTotalOrder : IsTotalPreorder _n=_ _n≤_ HNTotalOrder = record { isPreorder = record { isEquivalence = {!!} ; reflexive = {!!} ; trans = {!!} } ; total = {!!} } data HyperZ : Set where hz : HyperNat → HyperNat → HyperZ _z*_ : (i j : HyperZ ) → HyperZ _z+_ : (i j : HyperZ ) → HyperZ hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ ) -- ( i - i₁ ) * ( j - j₁ ) = i * j + i₁ * j₁ - i * j₁ - i₁ * j 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 ) HNzero : HyperNat → Set HNzero i = ( k : ℕ ) → i k ≡ 0 _z=_ : (i j : HyperZ ) → Set _z=_ = {!!} _z≤_ : (i j : HyperZ ) → Set _z≤_ = {!!} ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j ≤→= {0} {0} z≤n z≤n = refl ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i ) HNzero? : ( i : HyperNat ) → Dec (HNzero i) HNzero? i with i cmpn hzero | hzero cmpn i ... | no s | t = no (λ n → s {!!}) -- (k₁ : ℕ) → i k₁ ≡ 0 → i k ≤ 0 ... | s | no t = no (λ n → t {!!}) ... | yes s | yes t = yes (λ k → {!!} ) record HNzeroK ( x : HyperNat ) : Set where field nonzero : ℕ isNonzero : ¬ ( x nonzero ≡ 0 ) postulate HNnzerok : (x : HyperNat ) → ¬ ( HNzero x ) → HNzeroK x import Axiom.Extensionality.Propositional postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 ) m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl HNnzero* : {x y : HyperNat } → ¬ ( HNzero x ) → ¬ ( HNzero y ) → ¬ ( HNzero (x n* y) ) HNnzero* {x} {y} nzx nzy nzx*y with HNnzerok x nzx | HNnzerok y nzy ... | s | t = {!!} where hnz0 : ( k : ℕ ) → x k * y k ≡ 0 → (x k ≡ 0) ∨ (y k ≡ 0) hnz0 k x*y = m*n=0⇒m=0∨n=0 x*y HZzero : HyperZ → Set HZzero (hz i j ) = ( k : ℕ ) → i k ≡ j k HZzero? : ( i : HyperZ ) → Dec (HZzero i) HZzero? = {!!} data HyperR : Set where hr : HyperZ → (k : HyperNat ) → ¬ HNzero k → HyperR HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) ) HZnzero* {x} {y} nzx nzy nzx*y with HZzero? x | HZzero? y ... | yes t | s = ⊥-elim ( nzx t ) ... | t | yes s = ⊥-elim ( nzy s ) ... | no t | no s = {!!} HRzero : HyperR → Set HRzero (hr i j nz ) = HZzero i _h=_ : (i j : HyperR ) → Set _h=_ = {!!} _h≤_ : (i j : HyperR ) → Set _h≤_ = {!!} _h*_ : (i j : HyperR) → HyperR _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₁) hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁)