149 lines
4.4 KiB
Text
149 lines
4.4 KiB
Text
load "nat.quox"
|
||
|
||
namespace int {
|
||
|
||
def0 Sign : ★ = {pos, neg-succ}
|
||
def0 ℤ : ★ = Sign × ℕ
|
||
|
||
def from-ℕ : ℕ → ℤ = λ n ⇒ ('pos, n)
|
||
|
||
def neg-ℕ : ℕ → ℤ =
|
||
λ n ⇒ case n return ℤ of { 0 ⇒ ('pos, 0); succ n ⇒ ('neg-succ, n) }
|
||
|
||
def zeroℤ : ℤ = ('pos, 0)
|
||
|
||
|
||
def match : 0.(A : ★) → ω.(pos neg : ℕ → A) → ℤ → A =
|
||
λ A pos neg x ⇒
|
||
case x return A of { (s, x) ⇒
|
||
case s return A of { 'pos ⇒ pos x; 'neg-succ ⇒ neg x }
|
||
}
|
||
|
||
def negate : ℤ → ℤ =
|
||
match ℤ neg-ℕ (λ x ⇒ from-ℕ (succ x))
|
||
|
||
def minus-ℕ-ℕ : ℕ → ℕ → ℤ =
|
||
λ m n ⇒
|
||
letω f : ω.ℕ → ω.ℕ → ℤ = λ m n ⇒
|
||
bool.if ℤ (nat.ge m n) (from-ℕ (nat.minus m n))
|
||
(neg-ℕ (nat.minus n m)) in
|
||
getω ℤ (app2ω ℕ ℕ ℤ f (nat.dup m) (nat.dup n))
|
||
|
||
def plus-ℕ : ℤ → ℕ → ℤ =
|
||
match (ℕ → ℤ) (λ x n ⇒ from-ℕ (nat.plus x n))
|
||
(λ x n ⇒ minus-ℕ-ℕ n (succ x))
|
||
|
||
def minus-ℕ : ℤ → ℕ → ℤ =
|
||
match (ℕ → ℤ) minus-ℕ-ℕ (λ x n ⇒ ('neg-succ, nat.plus x n))
|
||
|
||
|
||
def plus : ℤ → ℤ → ℤ =
|
||
match (ℤ → ℤ) (λ x y ⇒ plus-ℕ y x) (λ x y ⇒ minus-ℕ y (succ x))
|
||
|
||
def minus : ℤ → ℤ → ℤ = λ x y ⇒ plus x (negate y)
|
||
|
||
|
||
def dup-sign : Sign → [ω. Sign] =
|
||
λ s ⇒ case s return [ω. Sign] of {
|
||
'pos ⇒ ['pos];
|
||
'neg-succ ⇒ ['neg-succ]
|
||
}
|
||
|
||
def0 dup-sign-ok : (s : Sign) → dup-sign s ≡ [s] : [ω. Sign] =
|
||
λ s ⇒ case s return s' ⇒ dup-sign s' ≡ [s'] : [ω. Sign] of {
|
||
'pos ⇒ δ 𝑖 ⇒ ['pos];
|
||
'neg-succ ⇒ δ 𝑖 ⇒ ['neg-succ]
|
||
}
|
||
|
||
def dup : ℤ → [ω.ℤ] =
|
||
λ x ⇒ case x return [ω.ℤ] of { (s, n) ⇒
|
||
app2ω Sign ℕ ℤ (λ s n ⇒ (s, n)) (dup-sign s) (nat.dup n)
|
||
}
|
||
|
||
def0 dup-ok : (x : ℤ) → dup x ≡ [x] : [ω.ℤ] =
|
||
λ x ⇒
|
||
case x return x' ⇒ dup x' ≡ [x'] : [ω.ℤ] of { (s, n) ⇒ δ 𝑖 ⇒
|
||
app2ω Sign ℕ ℤ (λ s n ⇒ (s, n)) (dup-sign-ok s @𝑖) (nat.dup-ok n @𝑖)
|
||
}
|
||
|
||
|
||
def times-ℕ : ℤ → ℕ → ℤ =
|
||
match (ℕ → ℤ)
|
||
(λ m n ⇒ from-ℕ (nat.times m n))
|
||
(λ m' n ⇒ neg-ℕ (nat.times (succ m') n))
|
||
|
||
def times : ℤ → ℤ → ℤ =
|
||
match (ℤ → ℤ) (λ p x ⇒ times-ℕ x p) (λ n x ⇒ negate (times-ℕ x (succ n)))
|
||
|
||
|
||
def abs : ℤ → ℕ = match ℕ (λ p ⇒ p) (λ n ⇒ succ n)
|
||
|
||
|
||
def pair-eq? : 0.(A B : ★) → ω.(DecEq A) → ω.(DecEq B) → DecEq (A × B) =
|
||
λ A B eqA? eqB? x y ⇒
|
||
let0 Ret : ★ = x ≡ y : (A × B) in
|
||
letω a0 = fst x; a1 = fst y;
|
||
b0 = snd x; b1 = snd y in
|
||
dec.elim (a0 ≡ a1 : A) (λ _ ⇒ Dec Ret)
|
||
(λ ya ⇒
|
||
dec.elim (b0 ≡ b1 : B) (λ _ ⇒ Dec Ret)
|
||
(λ yb ⇒ Yes Ret (δ 𝑖 ⇒ (ya @𝑖, yb @𝑖)))
|
||
(λ nb ⇒ No Ret (λ eq ⇒ nb (δ 𝑖 ⇒ snd (eq @𝑖))))
|
||
(eqB? b0 b1))
|
||
(λ na ⇒ No Ret (λ eq ⇒ na (δ 𝑖 ⇒ fst (eq @𝑖))))
|
||
(eqA? a0 a1)
|
||
|
||
|
||
def sign-eq? : DecEq Sign =
|
||
λ x y ⇒
|
||
let0 disc : Sign → ★ =
|
||
λ s ⇒ case s return ★ of { 'pos ⇒ True; 'neg-succ ⇒ False } in
|
||
case x return x' ⇒ Dec (x' ≡ y : Sign) of {
|
||
'pos ⇒
|
||
case y return y' ⇒ Dec ('pos ≡ y' : Sign) of {
|
||
'pos ⇒ dec.yes-refl Sign 'pos;
|
||
'neg-succ ⇒
|
||
No ('pos ≡ 'neg-succ : Sign)
|
||
(λ eq ⇒ coe (𝑖 ⇒ disc (eq @𝑖)) 'true)
|
||
};
|
||
'neg-succ ⇒
|
||
case y return y' ⇒ Dec ('neg-succ ≡ y' : Sign) of {
|
||
'neg-succ ⇒ dec.yes-refl Sign 'neg-succ;
|
||
'pos ⇒
|
||
No ('neg-succ ≡ 'pos : Sign)
|
||
(λ eq ⇒ coe (𝑖 ⇒ disc (eq @𝑖)) @1 @0 'true)
|
||
}
|
||
}
|
||
|
||
#[compile-scheme "(lambda% (x y) (if (equal? x y) Yes No))"]
|
||
def eq? : DecEq ℤ = pair-eq? Sign ℕ sign-eq? nat.eq?
|
||
|
||
def eq : ω.ℤ → ω.ℤ → Bool =
|
||
λ x y ⇒ dec.bool (x ≡ y : ℤ) (eq? x y)
|
||
|
||
}
|
||
|
||
def0 ℤ = int.ℤ
|
||
|
||
|
||
namespace scheme-int {
|
||
postulate0 Int : ★
|
||
|
||
#[compile-scheme "(lambda (x) x)"]
|
||
postulate from-ℕ : ℕ → Int
|
||
|
||
#[compile-scheme "(lambda% (x y) (+ x y))"]
|
||
postulate plus : Int → Int → Int
|
||
|
||
#[compile-scheme "(lambda% (x y) (- x y))"]
|
||
postulate minus : Int → Int → Int
|
||
|
||
#[compile-scheme "(lambda% (x y) (* x y))"]
|
||
postulate times : Int → Int → Int
|
||
|
||
#[compile-scheme "(lambda% (x y) (if (= x y) 'true 'false))"]
|
||
postulate eq : Int → Int → Bool
|
||
|
||
#[compile-scheme "abs"]
|
||
postulate abs : Int → ℕ
|
||
}
|