Mercurial > hg > Members > kono > Proof > HyperReal

changeset 10:a4e441b7493b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
files src/HyperReal.agda
diffstat 1 files changed, 64 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/src/HyperReal.agda	Sat Jul 03 23:37:41 2021 +0900
+++ b/src/HyperReal.agda	Sun Jul 04 15:47:18 2021 +0900
@@ -32,6 +32,14 @@
 
 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)
@@ -49,10 +57,30 @@
      n→nxn (suc i) with n→nxn i
      ... | ⟪ x , zero ⟫ = ⟪ zero  , suc x ⟫
      ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
-     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
+     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 )
@@ -68,8 +96,14 @@
           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
@@ -98,28 +132,22 @@
      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))  -- ⟪ pred n , 1 ⟫  → ⟪ n , 0 ⟫
+     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 } = {!!} where
-         nid14 :  {i x y : ℕ} → n→nxn i ≡ ⟪ x , suc y ⟫ →  suc x ≡ proj2 (n→nxn (suc (suc i)))
-         nid14 = {!!}
+     ... | 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 i | inspect  n→nxn i
-         ... | ⟪ x , suc y ⟫ | record { eq = eq2 } = nat-≡< (sym eq1) ( begin
-             1 ≤⟨ s≤s z≤n ⟩
-             suc x ≡⟨ nid14 {i} {x} {y} eq2 ⟩
-             {!!} ≡⟨ {!!} ⟩
-             _ ∎ ) where open ≤-Reasoning
+         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)
-     -- i +  (nxn→n 0 i) ≡ nxn→n i 0
-     ... | zero | record { eq = eqy } = begin
-         suc (x + suc (nxn→n x 0)) ≡⟨ {!!}  ⟩
-         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) ⟩
+     ... | 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
+         suc i ∎   where
              open ≡-Reasoning
-     ... | suc y | record { eq = eqy } = begin
+     ... | 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) ⟩
@@ -139,20 +167,23 @@
                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 = eq } with  proj2 (n→nxn i) | inspect proj2 (n→nxn i)  -- ⟪ x , 0 ⟫ → ⟪ 0 , suc x ⟫
+     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
-          nxn→n (proj1 (n→nxn (suc i) )) (suc x) ≡⟨ {!!} ⟩
-          nxn→n zero (suc x) ≡⟨ {!!} ⟩
-          pred (suc x) + suc (nxn→n 0 (pred (suc x))) ≡⟨ cong (λ k → pred k +  suc (nxn→n 0 (pred k))) (sym eq) ⟩
-          pred (proj2 (n→nxn (suc i) )) + suc (nxn→n 0 (pred (proj2 (n→nxn (suc i) )))) ≡⟨ {!!} ⟩
-          suc i ∎ where
+     ... | 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
+     ... | 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 eq) ⟩
+          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 ⟩
@@ -168,13 +199,9 @@
                 suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid7 ⟩
                 proj2 (n→nxn i) ∎  
      f : (i : ℕ) → Set
-     f i = n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
-     g : (i j : ℕ) → Set
-     g i j = suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
-     h : (i : ℕ) → Set
-     h i = i +  (nxn→n 0 i) ≡ nxn→n i 0
-     h1  : ( i : ℕ ) → Set
-     h1 i = (pred (proj1 (n→nxn (suc i))) + suc (nxn→n (pred (proj1 (n→nxn (suc i)))) 0))  ≡ suc (nxn→n (proj1 (n→nxn i)) 0) 
+     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 = {!!}