Mercurial > hg > Members > kono > Proof > HyperReal

changeset 12:e607f453f607

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 Sun, 04 Jul 2021 23:46:55 +0900
parents 2ce1c67dde0f
children 4b3dfce33fa3
files src/HyperReal.agda
diffstat 1 files changed, 62 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/src/HyperReal.agda	Sun Jul 04 15:53:55 2021 +0900
+++ b/src/HyperReal.agda	Sun Jul 04 23:46:55 2021 +0900
@@ -32,11 +32,14 @@
 
 open _∧_
 
-record NN ( i j k  : ℕ) : Set where
+record NN ( i  : ℕ) (nxn→n :  ℕ →  ℕ → ℕ) (n→nxn : ℕ → ℕ ∧ ℕ) : Set where
   field
-     stage : ℕ
-     nn : j + k ≡ stage
-     ni : i ≡ stage + k
+     j k sum stage : ℕ
+     nn : j + k ≡ sum
+     ni : i ≡ j + stage 
+     k1 : nxn→n j k ≡ i
+     k0 : n→nxn i ≡ ⟪ j , k ⟫ 
+     nn-unique : {j0 k0 : ℕ } →  nxn→n j0 k0 ≡ i  → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ 
 
 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0
 i≤0→i≡0 {0} z≤n = refl
@@ -45,8 +48,8 @@
 nxn = record {
      nxn→n = λ p → nxn→n (proj1 p) (proj2 p)
    ; n→nxn =  n→nxn 
-   ; nn-id = nn-id
-   ; n-id = n-id
+   ; nn-id = nn-id'
+   ; n-id = n-id'
   } where
      nxn→n :  ℕ →  ℕ → ℕ
      nxn→n zero zero = zero
@@ -58,29 +61,57 @@
      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 = {!!}
+
+     nxn→n0 : { j k : ℕ } →  nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 )
+     nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫
+     nxn→n0 {zero} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → 0 < k) (+-comm _ k) (s≤s z≤n)))
+     nxn→n0 {(suc j)} {zero} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
+     nxn→n0 {(suc j)} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
+
+     nid20 : (i : ℕ) →  i +  (nxn→n 0 i) ≡ nxn→n i 0
+     nid20 zero = refl -- suc (i + (i + suc (nxn→n 0 i))) ≡ suc (i + suc (nxn→n i 0))
+     nid20 (suc i) = begin
+         suc (i + (i + suc (nxn→n 0 i)))  ≡⟨ cong (λ k → suc (i + k)) (sym (+-assoc i 1 (nxn→n 0 i))) ⟩
+         suc (i + ((i + 1) + nxn→n 0 i))  ≡⟨ cong (λ k →  suc (i + (k + nxn→n 0 i))) (+-comm i 1)  ⟩
+         suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i)  ⟩
+         suc (i + suc (nxn→n i 0)) ∎  where open ≡-Reasoning
+
+     nn : ( i  : ℕ) → NN i nxn→n n→nxn
+     nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl
+        ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
+     nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i) 
+     ... | zero | record { eq = eq } = record { k = suc (NN.sum (nn i)) ; j = 0 ; sum = suc  (NN.sum (nn i)) ; stage = suc  (NN.sum (nn i)) + (NN.stage (nn i))
+         ; nn = refl
+         ; ni = nn01 ; k1 = nn02 ; k0 = {!!} ;  nn-unique = {!!} } where
+            sum = NN.sum (nn i)
+            stage = NN.stage (nn i)
+            j = NN.j (nn i)
+            nn01 : suc i ≡ 0 + (suc sum + stage )
+            nn01 = begin
+               suc i ≡⟨ cong suc (NN.ni (nn i)) ⟩
+               suc ((NN.j  (nn i) ) + stage )  ≡⟨ cong (λ k → suc (k + stage )) (+-comm 0 _ ) ⟩
+               suc ((NN.j  (nn i) + 0 ) + stage )  ≡⟨ cong (λ k → suc ((NN.j  (nn i) + k) + stage )) (sym eq) ⟩
+               suc ((NN.j (nn i) + NN.k  (nn i)) + stage )  ≡⟨ cong (λ k → suc ( k + stage )) (NN.nn (nn i)) ⟩
+               0 +   (suc sum + stage ) ∎  where open ≡-Reasoning
+            nn02 :  nxn→n 0 (suc sum)  ≡ suc i
+            nn02 = begin
+               sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩
+               (sum + 1) + nxn→n 0 sum  ≡⟨ cong (λ k → k + nxn→n 0 sum )  (+-comm sum 1 )⟩
+               suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩
+               suc (nxn→n sum 0) ≡⟨ {!!} ⟩
+               suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩
+               suc i ∎  where open ≡-Reasoning
+     ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = {!!} ; ni = {!!}
+         ; k1 = {!!} ; k0 = {!!} ;  nn-unique = {!!} }
+
+     n-id' :  (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
+     n-id' i = subst (λ k →  nxn→n (proj1 k) (proj2 k)  ≡ i ) (sym (NN.k0 (nn i))) (NN.k1 (nn i))
+
+     nn-id' : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫
+     nn-id' j k = begin
+          n→nxn (nxn→n j k)  ≡⟨ NN.k0 (nn (nxn→n j k))   ⟩
+          ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩
+          ⟪ j , k ⟫ ∎  where open ≡-Reasoning
 
      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) 
@@ -101,8 +132,6 @@
      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 
@@ -203,6 +232,8 @@
      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)
+     g : (i : ℕ) → Set
+     g i = i +  (nxn→n 0 i) ≡ nxn→n i 0
      nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
      nn-id = {!!}