Mercurial > hg > Members > kono > Proof > HyperReal

changeset 9:d7d7016764b5

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 Sat, 03 Jul 2021 23:37:41 +0900
parents e423b498f3fe
children a4e441b7493b
files src/HyperReal.agda
diffstat 1 files changed, 16 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/HyperReal.agda	Sat Jul 03 21:40:29 2021 +0900
+++ b/src/HyperReal.agda	Sat Jul 03 23:37:41 2021 +0900
@@ -100,11 +100,21 @@
      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 ⟫
      ... | zero  | record { eq = eq } with  proj1 (n→nxn (suc i)) | inspect  proj1 (n→nxn (suc i))
-     ... | zero | record { eq = eqx } = {!!}
+     ... | zero | record { eq = eqx } = {!!} where
+         nid14 :  {i x y : ℕ} → n→nxn i ≡ ⟪ x , suc y ⟫ →  suc x ≡ proj2 (n→nxn (suc (suc i)))
+         nid14 = {!!}
+         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
      ... | 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 (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) ⟩
          suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩
          suc i ∎ where
@@ -135,8 +145,8 @@
      ... | zero  | record { eq = eqy } = begin
           nxn→n (proj1 (n→nxn (suc i) )) (suc x) ≡⟨ {!!} ⟩
           nxn→n zero (suc x) ≡⟨ {!!} ⟩
-          x + suc (nxn→n 0 x) ≡⟨ {!!} ⟩
-          x + suc (nxn→n 0 (pred (proj1 (n→nxn i)))) ≡⟨ {!!} ⟩
+          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
              open ≡-Reasoning
      ... | suc y | record { eq = eqy } = begin
@@ -163,6 +173,8 @@
      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) 
      nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
      nn-id = {!!}