Mercurial > hg > Members > kono > Proof > HyperReal
view src/HyperReal.agda @ 14:7264f8749369
... uniquness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Jul 2021 08:55:20 +0900 |
| parents | 4b3dfce33fa3 |
| children | ded4bd888817 |
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 : ℕ) (nxn→n : ℕ → ℕ → ℕ) (n→nxn : ℕ → ℕ ∧ ℕ) : Set where field 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 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 ⟫ 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 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} ) 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 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 = nn03 ; 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) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NN.nn (nn i))) ⟩ suc (nxn→n (NN.j (nn i) + (NN.k (nn i)) ) 0) ≡⟨ cong₂ (λ j k → suc (nxn→n (NN.j (nn i) + j) k )) eq (sym eq) ⟩ suc (nxn→n (NN.j (nn i) + 0 ) (NN.k (nn i))) ≡⟨ cong (λ k → suc ( nxn→n k (NN.k (nn i)))) (+-comm (NN.j (nn i)) 0) ⟩ suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩ suc i ∎ where open ≡-Reasoning nn03 : n→nxn (suc i) ≡ ⟪ 0 , suc (NN.sum (nn i)) ⟫ -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫ nn03 with n→nxn i | inspect n→nxn i ... | ⟪ x , zero ⟫ | record { eq = eq1 } = begin ⟪ zero , suc x ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (sym (cong proj1 eq1)) ⟩ ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (cong proj1 (NN.k0 (nn i))) ⟩ ⟪ zero , suc (NN.j (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (+-comm 0 _ ) ⟩ ⟪ zero , suc (NN.j (nn i) + 0) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc (NN.j (nn i) + k) ⟫ ) (sym eq) ⟩ ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫ ) (NN.nn (nn i)) ⟩ ⟪ 0 , suc sum ⟫ ∎ where open ≡-Reasoning ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 (NN.k0 (nn i)))) (begin suc (NN.k (nn i)) ≡⟨ cong suc eq ⟩ 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 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 {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 nxn→n j0 (suc k0) ≡⟨ cong pred ( begin suc (nxn→n j0 (suc k0)) ≡⟨ nid2 j0 k0 ⟩ nxn→n (suc j0) k0 ≡⟨ eq1 ⟩ suc i ∎ ) ⟩ 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 = {!!} } 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) ... | ⟪ 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 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₁)