Mercurial > hg > Members > kono > Proof > HyperReal
changeset 16:cd52a72d4fca
ℕ → ℕ ∧ ℕ bijection done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Jul 2021 11:02:41 +0900 |
| parents | ded4bd888817 |
| children | 02847b697be9 |
| files | src/HyperReal.agda |
| diffstat | 1 files changed, 80 insertions(+), 106 deletions(-) [+] |
line wrap: on
line diff
--- a/src/HyperReal.agda Mon Jul 05 09:18:37 2021 +0900 +++ b/src/HyperReal.agda Mon Jul 05 11:02:41 2021 +0900 @@ -49,8 +49,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 @@ -114,14 +114,15 @@ nxn→n (suc (suc i)) (suc j) ∎ where open ≡-Reasoning - nn004 : {k k0 : ℕ} → nxn→n 0 k ≡ nxn→n 0 k0 → k ≡ k0 - nn004 {zero} {zero} eq = refl - nn004 {zero} {suc k0} eq = {!!} - nn004 {suc k} {zero} eq = {!!} - nn004 {suc k} {suc k0} eq = begin - suc k ≡⟨ cong suc (nn004 {k} {k0} {!!} ) ⟩ -- k + suc (nxn→n zero k) ≡ k0 + suc (nxn→n zero k0) → nxn→n 0 k ≡ nxn→n 0 k0 - suc k0 ∎ where - open ≡-Reasoning + nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) + nid00 zero = refl + nid00 (suc i) = begin + suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩ + suc (suc (i + (nxn→n 0 (suc i)))) ≡⟨ refl ⟩ + suc (suc (i + (i + suc (nxn→n 0 i)))) ≡⟨ cong suc (sym ( +-assoc 1 i (i + suc (nxn→n 0 i)))) ⟩ + suc ((1 + i) + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (k + (i + suc (nxn→n 0 i)))) (+-comm 1 i) ⟩ + suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩ + suc (i + suc (i + suc (nxn→n 0 i))) ∎ 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 @@ -164,9 +165,21 @@ suc 0 ≤⟨ s≤s z≤n ⟩ suc y ≡⟨ sym (cong proj2 eq1) ⟩ proj2 (n→nxn i) ∎ )) where open ≤-Reasoning - -- nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j + -- nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (NN.sum (nn i)) ⟫ ≡ ⟪ j0 , k0 ⟫ - nn04 {zero} {suc k0} eq = {!!} -- k0 + suc (nxn→n zero k0) ≡ suc i -- + nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- + nn07 : nxn→n k0 0 ≡ i + nn07 = cong pred ( begin + suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩ + nxn→n 0 (suc k0 ) ≡⟨ eq1 ⟩ + suc i ∎ ) where open ≡-Reasoning + nn08 : k0 ≡ sum + nn08 = begin + k0 ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩ + NN.j (nn i) ≡⟨ +-comm 0 _ ⟩ + NN.j (nn i) + 0 ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ + NN.j (nn i) + NN.k (nn i) ≡⟨ NN.nn (nn i) ⟩ + sum ∎ where open ≡-Reasoning nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where nn05 : nxn→n j0 (suc k0) ≡ i nn05 = begin @@ -177,106 +190,67 @@ i ∎ where open ≡-Reasoning nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ nn06 = NN.nn-unique (nn i) - ... | 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 = {!!} } + ... | 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 = nn10 + ; ni = cong suc (NN.ni (nn i)) ; k1 = nn11 ; k0 = nn12 ; nn-unique = nn13 } where + nn10 : suc (NN.j (nn i)) + k ≡ NN.sum (nn i) + nn10 = begin + suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _) ⟩ + (NN.j (nn i) + 1) + k ≡⟨ +-assoc (NN.j (nn i)) 1 k ⟩ + NN.j (nn i) + suc k ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ + NN.j (nn i) + NN.k (nn i) ≡⟨ NN.nn (nn i) ⟩ + NN.sum (nn i) ∎ where open ≡-Reasoning + nn11 : nxn→n (suc (NN.j (nn i))) k ≡ suc i -- nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i + nn11 = begin + nxn→n (suc (NN.j (nn i))) k ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩ + suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k → suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩ + suc (nxn→n ( NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i)) ⟩ + suc i ∎ where open ≡-Reasoning + nn18 : zero < NN.k (nn i) + nn18 = subst (λ k → 0 < k ) ( begin + suc k ≡⟨ sym eq ⟩ + NN.k (nn i) ∎ ) (s≤s z≤n ) where open ≡-Reasoning + nn12 : n→nxn (suc i) ≡ ⟪ suc (NN.j (nn i)) , k ⟫ -- n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ + nn12 with n→nxn i | inspect n→nxn i + ... | ⟪ x , zero ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 eq1)) + (subst (λ k → 0 < k ) ( begin + suc k ≡⟨ sym eq ⟩ + NN.k (nn i) ≡⟨ cong proj2 (sym (NN.k0 (nn i)) ) ⟩ + proj2 (n→nxn i) ∎ ) (s≤s z≤n )) ) where open ≡-Reasoning -- eq1 n→nxn i ≡ ⟪ x , zero ⟫ + ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = begin -- n→nxn i ≡ ⟪ x , suc y ⟫ + ⟪ suc x , y ⟫ ≡⟨ refl ⟩ + ⟪ suc x , pred (suc y) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin + ⟪ x , suc y ⟫ ≡⟨ sym eq1 ⟩ + n→nxn i ≡⟨ NN.k0 (nn i) ⟩ + ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ∎ ) ⟩ + ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫) eq ⟩ + ⟪ suc (NN.j (nn i)) , k ⟫ ∎ where open ≡-Reasoning + nn13 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫ + nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where -- (nxn→n zero (suc k0)) ≡ suc i + nn16 : nxn→n k0 zero ≡ i + nn16 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid00 k0 )) eq1 ) + nn17 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ k0 , zero ⟫ + nn17 = NN.nn-unique (nn i) nn16 + nn13 {suc j0} {k0} eq1 = begin + ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩ + ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin + ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡⟨ nn15 ⟩ + ⟪ j0 , suc k0 ⟫ ∎ ) ⟩ + ⟪ suc j0 , k0 ⟫ ∎ where -- nxn→n (suc j0) k0 ≡ suc i + open ≡-Reasoning + nn14 : nxn→n j0 (suc k0) ≡ i + nn14 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid2 j0 k0 )) eq1 ) + nn15 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ + nn15 = NN.nn-unique (nn i) nn14 - 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)) + 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 + 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) - ... | ⟪ x , zero ⟫ = ⊥-elim ( nat-≤> 0<p2 a<sa ) - ... | ⟪ x , suc y ⟫ = refl - 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 - 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 = {!!} - 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) - 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 = {!!} open NxN