aoc2023/lib/nat.quox
2023-12-01 18:52:23 +01:00

196 lines
5.9 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 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
}
}
def elim-pair :
0.(P : → ★) →
ω.(P 0 0) →
ω.(0.(n : ) → P 0 n → P 0 (succ n)) →
ω.(0.(m : ) → P m 0 → P (succ m) 0) →
ω.(0.(m n : ) → P m n → P (succ m) (succ n)) →
ω.(m : ) → (n : ) → P m n =
λ P zz zs sz ss m ⇒
caseω m return m' ⇒ (n : ) → P m' n of {
0 ⇒ λ n ⇒ case n return n' ⇒ P 0 n' of {
0 ⇒ zz;
succ n', ihn ⇒ zs n' ihn
};
succ m', ω.ihm ⇒ λ n ⇒ case n return n' ⇒ P (succ m') n' of {
0 ⇒ sz m' (ihm 0);
succ n' ⇒ ss m' n' (ihm n')
}
}
#[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))
(λ n' ⇒ sing.app n (λ n ⇒ succ n) n') d
};
def dup : → [ω.] =
λ n ⇒ appω (Sing n) (λ n' ⇒ sing.val n 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')
}
};
def0 Ordering : ★ = {lt, eq, gt}
def from-ordering : 0.(A : ★) → ω.A → ω.A → ω.A → Ordering → A =
λ A lt eq gt o ⇒
case o return A of { 'lt ⇒ lt; 'eq ⇒ eq; 'gt ⇒ gt }
def drop-ordering : 0.(A : ★) → Ordering → A → A =
λ A o x ⇒ case o return A of { 'lt ⇒ x; 'eq ⇒ x; 'gt ⇒ x }
def compareω : ω. → Ordering =
elim-pair (λ _ _ ⇒ Ordering)
'eq
(λ _ o ⇒ drop-ordering Ordering o 'lt)
(λ _ o ⇒ drop-ordering Ordering o 'gt)
(λ _ _ x ⇒ x)
def compare : → Ordering =
λ m n ⇒
case dup m return Ordering of { [m] ⇒
case dup n return Ordering of { [n] ⇒ compareω m n } }
def lt : ω. → ω. → Bool =
λ m n ⇒ from-ordering Bool 'true 'false 'false (compare m n)
def le : ω. → ω. → Bool =
λ m n ⇒ from-ordering Bool 'true 'true 'false (compare m n)
def eq : ω. → ω. → Bool =
λ m n ⇒ from-ordering Bool 'false 'true 'false (compare m n)
def gt : ω. → ω. → Bool =
λ m n ⇒ from-ordering Bool 'false 'false 'true (compare m n)
def ge : ω. → ω. → Bool =
λ m n ⇒ from-ordering Bool 'false 'true 'true (compare 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 times-zero : (m : ) → 0 ≡ timesω m 0 : =
λ m ⇒
case m return m' ⇒ 0 ≡ timesω m' 0 : of {
zero ⇒ δ _ ⇒ zero;
succ m', ih ⇒ ih
};
}