quox/examples/nat.quox

113 lines
3.4 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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 @𝑖)] @0 @1 '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')
};
}