162 lines
4.7 KiB
Text
162 lines
4.7 KiB
Text
load "misc.quox";
|
||
load "bool.quox";
|
||
load "either.quox";
|
||
|
||
namespace nat {
|
||
|
||
def elim-0-1 :
|
||
0.(P : ℕ → ★) →
|
||
ω.(P 0) → ω.(P 1) →
|
||
ω.(0.(n : ℕ) → P n → P (succ n)) →
|
||
(n : ℕ) → P n =
|
||
λ P p0 p1 ps n ⇒
|
||
case n return n' ⇒ P n' of {
|
||
zero ⇒ p0;
|
||
succ n' ⇒
|
||
case n' return n'' ⇒ P (succ n'') of {
|
||
zero ⇒ p1;
|
||
succ n'', IH ⇒ ps (succ n'') IH
|
||
}
|
||
}
|
||
|
||
#[compile-scheme "(lambda (n) (cons n 'erased))"]
|
||
def dup! : (n : ℕ) → [ω. Sing ℕ n] =
|
||
λ n ⇒
|
||
case n return n' ⇒ [ω. Sing ℕ n'] of {
|
||
zero ⇒ [(zero, [δ _ ⇒ zero])];
|
||
succ n, d ⇒
|
||
appω (Sing ℕ n) (Sing ℕ (succ n))
|
||
(sing.app ℕ ℕ n (λ n ⇒ succ n)) d
|
||
};
|
||
|
||
def dup : ℕ → [ω.ℕ] =
|
||
λ n ⇒ appω (Sing ℕ n) ℕ (sing.val ℕ n) (dup! n);
|
||
|
||
#[compile-scheme "(lambda% (m n) (+ m n))"]
|
||
def plus : ℕ → ℕ → ℕ =
|
||
λ m n ⇒
|
||
case m return ℕ of {
|
||
zero ⇒ n;
|
||
succ _, p ⇒ succ p
|
||
};
|
||
|
||
#[compile-scheme "(lambda% (m n) (* m n))"]
|
||
def timesω : ℕ → ω.ℕ → ℕ =
|
||
λ m n ⇒
|
||
case m return ℕ of {
|
||
zero ⇒ zero;
|
||
succ _, t ⇒ plus n t
|
||
};
|
||
|
||
def times : ℕ → ℕ → ℕ =
|
||
λ m n ⇒ case dup n return ℕ of { [n] ⇒ timesω m n };
|
||
|
||
def pred : ℕ → ℕ = λ n ⇒ case n return ℕ of { zero ⇒ zero; succ n ⇒ n };
|
||
|
||
def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
|
||
λ n ⇒ δ 𝑖 ⇒ n;
|
||
|
||
def0 succ-inj : (m n : ℕ) → succ m ≡ succ n : ℕ → m ≡ n : ℕ =
|
||
λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖);
|
||
|
||
#[compile-scheme "(lambda% (m n) (max 0 (- m n)))"]
|
||
def minus : ℕ → ℕ → ℕ =
|
||
λ m n ⇒
|
||
(case n return ℕ → ℕ of {
|
||
zero ⇒ λ m ⇒ m;
|
||
succ _, f ⇒ λ m ⇒ f (pred m)
|
||
}) m;
|
||
|
||
|
||
def0 IsSucc : ℕ → ★ =
|
||
λ 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 : (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)
|
||
}
|
||
|
||
|
||
#[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"]
|
||
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 : (m : ℕ) → m ≡ plus m 0 : ℕ =
|
||
λ m ⇒
|
||
case m return m' ⇒ m' ≡ plus m' 0 : ℕ of {
|
||
zero ⇒ δ _ ⇒ 0;
|
||
succ m', ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
|
||
};
|
||
|
||
def0 plus-succ : (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 : (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')
|
||
};
|
||
|
||
def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ =
|
||
λ m ⇒
|
||
case m return m' ⇒ 0 ≡ timesω m' 0 : ℕ of {
|
||
zero ⇒ δ _ ⇒ zero;
|
||
succ m', ih ⇒ ih
|
||
};
|
||
|
||
def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) : ℕ =
|
||
λ m n ⇒
|
||
case m
|
||
return m' ⇒ plus m' (timesω m' n) ≡ timesω m' (succ n) : ℕ
|
||
of {
|
||
zero ⇒ δ _ ⇒ 0;
|
||
succ m', ih ⇒
|
||
δ 𝑖 ⇒ plus (succ n) (ih @𝑖)
|
||
};
|
||
|
||
}
|