load "misc.quox"; load "bool.quox"; load "either.quox"; namespace nat { def dup : 1.ℕ → [ω.ℕ] = λ n ⇒ case1 n return [ω.ℕ] of { zero ⇒ [zero]; succ _, 1.d ⇒ case1 d return [ω.ℕ] of { [d] ⇒ [succ d] } }; def plus : 1.ℕ → 1.ℕ → ℕ = λ m n ⇒ case1 m return ℕ of { zero ⇒ n; succ _, 1.p ⇒ succ p }; def timesω : 1.ℕ → ω.ℕ → ℕ = λ m n ⇒ case1 m return ℕ of { zero ⇒ zero; succ _, 1.t ⇒ plus n t }; def times : 1.ℕ → 1.ℕ → ℕ = λ m n ⇒ case1 dup n return ℕ of { [n] ⇒ timesω m n }; def pred : 1.ℕ → ℕ = λ n ⇒ case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n }; def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ = λ n ⇒ δ 𝑖 ⇒ n; def0 succ-inj : 0.(m n : ℕ) → 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ = λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖); def0 IsSucc : 0.ℕ → ★⁰ = λ n ⇒ caseω n return ★⁰ of { zero ⇒ False; succ _ ⇒ True }; def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) = λ n ⇒ caseω n return n' ⇒ Dec (IsSucc n') of { zero ⇒ No (IsSucc zero) (λ v ⇒ v); succ n ⇒ Yes (IsSucc (succ n)) 'true }; def zero-not-succ : 0.(m : ℕ) → Not (zero ≡ succ m : ℕ) = λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) @1 @0 'true; def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) = λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) 'true; def0 not-succ-self : 0.(m : ℕ) → Not (m ≡ succ m : ℕ) = λ m ⇒ caseω m return m' ⇒ Not (m' ≡ succ m' : ℕ) of { zero ⇒ zero-not-succ 0; succ n, ω.ih ⇒ λ eq ⇒ ih (succ-inj n (succ n) eq) } def eq? : DecEq ℕ = λ m ⇒ caseω m return m' ⇒ ω.(n : ℕ) → Dec (m' ≡ n : ℕ) of { zero ⇒ λ n ⇒ caseω n return n' ⇒ Dec (zero ≡ n' : ℕ) of { zero ⇒ Yes (zero ≡ zero : ℕ) (δ _ ⇒ zero); succ n' ⇒ No (zero ≡ succ n' : ℕ) (λ eq ⇒ zero-not-succ n' eq) }; succ m', ω.ih ⇒ λ n ⇒ caseω n return n' ⇒ Dec (succ m' ≡ n' : ℕ) of { zero ⇒ No (succ m' ≡ zero : ℕ) (λ eq ⇒ succ-not-zero m' eq); succ n' ⇒ dec.elim (m' ≡ n' : ℕ) (λ _ ⇒ Dec (succ m' ≡ succ n' : ℕ)) (λ y ⇒ Yes (succ m' ≡ succ n' : ℕ) (δ 𝑖 ⇒ succ (y @𝑖))) (λ n ⇒ No (succ m' ≡ succ n' : ℕ) (λ eq ⇒ n (succ-inj m' n' eq))) (ih n') } }; def eqb : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq? m n); def0 plus-zero : 0.(m : ℕ) → m ≡ plus m 0 : ℕ = λ m ⇒ caseω m return m' ⇒ m' ≡ plus m' 0 : ℕ of { zero ⇒ δ _ ⇒ zero; succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖) }; def0 plus-succ : 0.(m n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ = λ m n ⇒ caseω m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of { zero ⇒ δ _ ⇒ succ n; succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖) }; def0 plus-comm : 0.(m n : ℕ) → plus m n ≡ plus n m : ℕ = λ m n ⇒ caseω m return m' ⇒ plus m' n ≡ plus n m' : ℕ of { zero ⇒ plus-zero n; succ m', ω.ih ⇒ trans ℕ (succ (plus m' n)) (succ (plus n m')) (plus n (succ m')) (δ 𝑖 ⇒ succ (ih @𝑖)) (plus-succ n m') }; }