beginning of quox stdlib
This commit is contained in:
parent
863849e4c4
commit
5bf40755b5
|
|
@ -0,0 +1,49 @@
|
|||
load "misc.quox"
|
||||
|
||||
namespace bool {
|
||||
|
||||
def0 Bool : ★ = {true, false}
|
||||
|
||||
def if-dep : 0.(P : Bool → ★) → (b : Bool) → ω.(P 'true) → ω.(P 'false) → P b =
|
||||
λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f }
|
||||
|
||||
def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A =
|
||||
λ A ⇒ if-dep (λ _ ⇒ A)
|
||||
|
||||
def0 if-same : (A : ★) → (b : Bool) → (x : A) → if A b x x ≡ x : A =
|
||||
λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x)
|
||||
|
||||
def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B =
|
||||
λ A B ⇒ if-dep (λ b ⇒ if¹ ★ b A B)
|
||||
|
||||
def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False
|
||||
|
||||
def dup! : (b : Bool) → Dup Bool b =
|
||||
λ b ⇒
|
||||
case b return b' ⇒ Dup Bool b' of {
|
||||
'true ⇒ (['true], [δ _ ⇒ ['true]]);
|
||||
'false ⇒ (['false], [δ _ ⇒ ['false]])
|
||||
}
|
||||
|
||||
def dup : Bool → [ω.Bool] =
|
||||
λ b ⇒
|
||||
case dup! b return [ω.Bool] of {
|
||||
(b!, p0) ⇒ drop0 (b! ≡ [b] : [ω.Bool]) [ω.Bool] p0 b!
|
||||
}
|
||||
|
||||
def true-not-false : Not ('true ≡ 'false : Bool) =
|
||||
λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true
|
||||
|
||||
|
||||
-- [todo] infix
|
||||
def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false
|
||||
def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b
|
||||
def not : Bool → Bool = λ b ⇒ if Bool b 'false 'true
|
||||
|
||||
|
||||
def0 not-not : (b : Bool) → not (not b) ≡ b : Bool =
|
||||
λ b ⇒ if-dep (λ b ⇒ not (not b) ≡ b : Bool) b (δ _ ⇒ 'true) (δ _ ⇒ 'false)
|
||||
|
||||
}
|
||||
|
||||
def0 Bool = bool.Bool
|
||||
|
|
@ -0,0 +1,116 @@
|
|||
load "misc.quox"
|
||||
load "bool.quox"
|
||||
|
||||
namespace either {
|
||||
|
||||
def0 Tag : ★ = {left, right}
|
||||
|
||||
def0 Payload : ★ → ★ → Tag → ★ =
|
||||
λ A B tag ⇒ case tag return ★ of { 'left ⇒ A; 'right ⇒ B }
|
||||
|
||||
def0 Either : ★ → ★ → ★ =
|
||||
λ A B ⇒ (tag : Tag) × Payload A B tag
|
||||
|
||||
def Left : 0.(A B : ★) → A → Either A B =
|
||||
λ A B x ⇒ ('left, x)
|
||||
|
||||
def Right : 0.(A B : ★) → B → Either A B =
|
||||
λ A B x ⇒ ('right, x)
|
||||
|
||||
def elim :
|
||||
0.(A B : ★) → 0.(P : 0.(Either A B) → ★) →
|
||||
ω.((x : A) → P (Left A B x)) →
|
||||
ω.((x : B) → P (Right A B x)) →
|
||||
(x : Either A B) → P x =
|
||||
λ A B P f g e ⇒
|
||||
case e return e' ⇒ P e' of { (t, a) ⇒
|
||||
case t return t' ⇒ (a : Payload A B t') → P (t', a)
|
||||
of { 'left ⇒ f; 'right ⇒ g } a
|
||||
}
|
||||
|
||||
def elimω :
|
||||
0.(A B : ★) → 0.(P : 0.(Either A B) → ★) →
|
||||
ω.(ω.(x : A) → P (Left A B x)) →
|
||||
ω.(ω.(x : B) → P (Right A B x)) →
|
||||
ω.(x : Either A B) → P x =
|
||||
λ A B P f g e ⇒
|
||||
case fst e return t' ⇒ ω.(a : Payload A B t') → P (t', a)
|
||||
of { 'left ⇒ f; 'right ⇒ g } (snd e)
|
||||
|
||||
def fold :
|
||||
0.(A B C : ★) → ω.(A → C) → ω.(B → C) → Either A B → C =
|
||||
λ A B C ⇒ elim A B (λ _ ⇒ C)
|
||||
|
||||
def foldω :
|
||||
0.(A B C : ★) → ω.(ω.A → C) → ω.(ω.B → C) → ω.(Either A B) → C =
|
||||
λ A B C ⇒ elimω A B (λ _ ⇒ C)
|
||||
|
||||
|
||||
}
|
||||
|
||||
def0 Either = either.Either
|
||||
def Left = either.Left
|
||||
def Right = either.Right
|
||||
|
||||
|
||||
namespace dec {
|
||||
|
||||
def0 Dec : ★ → ★ = λ A ⇒ Either [0.A] [0.Not A]
|
||||
|
||||
def Yes : 0.(A : ★) → 0.A → Dec A = λ A y ⇒ Left [0.A] [0.Not A] [y]
|
||||
def No : 0.(A : ★) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]
|
||||
|
||||
def yes-refl : 0.(A : ★) → 0.(x : A) → Dec (x ≡ x : A) =
|
||||
λ A x ⇒ Yes (x ≡ x : A) (δ 𝑖 ⇒ x)
|
||||
|
||||
def0 DecEq : ★ → ★ =
|
||||
λ A ⇒ ω.(x y : A) → Dec (x ≡ y : A)
|
||||
|
||||
def elim :
|
||||
0.(A : ★) → 0.(P : 0.(Dec A) → ★) →
|
||||
ω.(0.(y : A) → P (Yes A y)) →
|
||||
ω.(0.(n : Not A) → P (No A n)) →
|
||||
(x : Dec A) → P x =
|
||||
λ A P f g ⇒
|
||||
either.elim [0.A] [0.Not A] P
|
||||
(λ y ⇒ case y return y' ⇒ P (Left [0.A] [0.Not A] y') of {[y'] ⇒ f y'})
|
||||
(λ n ⇒ case n return n' ⇒ P (Right [0.A] [0.Not A] n') of {[n'] ⇒ g n'})
|
||||
|
||||
def bool : 0.(A : ★) → Dec A → Bool =
|
||||
λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false)
|
||||
|
||||
def drop' : 0.(A : ★) → Dec A → True =
|
||||
λ A ⇒ elim A (λ _ ⇒ True) (λ _ ⇒ 'true) (λ _ ⇒ 'true)
|
||||
|
||||
def drop : 0.(A B : ★) → Dec A → B → B =
|
||||
λ A B x y ⇒ true.drop B (drop' A x) y
|
||||
|
||||
}
|
||||
|
||||
def0 Dec = dec.Dec
|
||||
def0 DecEq = dec.DecEq
|
||||
def Yes = dec.Yes
|
||||
def No = dec.No
|
||||
|
||||
|
||||
namespace dect {
|
||||
|
||||
def0 DecT : ★ → ★ = λ A ⇒ Either A [0.Not A]
|
||||
|
||||
def YesT : 0.(A : ★) → 1.A → DecT A = λ A y ⇒ Left A [0.Not A] y
|
||||
def NoT : 0.(A : ★) → 0.(Not A) → DecT A = λ A n ⇒ Right A [0.Not A] [n]
|
||||
|
||||
def elim :
|
||||
0.(A : ★) → 0.(P : 0.(DecT A) → ★) →
|
||||
ω.(1.(y : A) → P (YesT A y)) →
|
||||
ω.(0.(n : Not A) → P (NoT A n)) →
|
||||
(x : DecT A) → P x =
|
||||
λ A P f g ⇒
|
||||
either.elim A [0.Not A] P
|
||||
f
|
||||
(λ n ⇒ case n return n' ⇒ P (Right A [0.Not A] n') of {[n'] ⇒ g n'})
|
||||
}
|
||||
|
||||
def0 DecT = dect.DecT
|
||||
def YesT = dect.YesT
|
||||
def NoT = dect.NoT
|
||||
|
|
@ -0,0 +1,259 @@
|
|||
load "nat.quox"
|
||||
load "either.quox"
|
||||
load "maybe.quox"
|
||||
load "sub.quox"
|
||||
|
||||
|
||||
namespace nat.lt {
|
||||
|
||||
def0 LT : ℕ → ℕ → ★ =
|
||||
elim-pair¹ (λ _ _ ⇒ ★)
|
||||
False -- 0 ≮ 0
|
||||
(λ n p ⇒ True) -- 0 < succ n
|
||||
(λ m p ⇒ False) -- succ m ≮ 0
|
||||
(λ m n p ⇒ p) -- succ m < succ n ⇔ m < n
|
||||
|
||||
|
||||
def0 irr : sub.Irr2 ℕ ℕ LT =
|
||||
elim-pair (λ m n ⇒ (p q : LT m n) → p ≡ q : LT m n)
|
||||
false.irr (λ _ _ ⇒ true.irr) (λ _ _ ⇒ false.irr) (λ _ _ p ⇒ p)
|
||||
|
||||
|
||||
-- [todo] quantities (which will need to inline and adapt elim-pair)
|
||||
def elimω : 0.(P : (m n : ℕ) → LT m n → ★) →
|
||||
ω.(0.(n : ℕ) → P 0 (succ n) 'true) →
|
||||
ω.(0.(m n : ℕ) → 0.(lt : LT m n) →
|
||||
ω.(P m n lt) → P (succ m) (succ n) lt) →
|
||||
ω.(m n : ℕ) → 0.(lt : LT m n) → P m n lt =
|
||||
λ P p0s pss ⇒
|
||||
elim-pairω (λ m n ⇒ 0.(lt : LT m n) → P m n lt)
|
||||
(λ ff ⇒ void (P 0 0 ff) ff)
|
||||
(λ n p tt ⇒ p0s n)
|
||||
(λ m p ff ⇒ void (P (succ m) 0 ff) ff)
|
||||
(λ m n p tt ⇒ pss m n tt (p tt))
|
||||
|
||||
def0 true-ty : (m n : ℕ) → LT m n → LT m n ≡ True : ★ =
|
||||
elim-pair¹ (λ m n ⇒ LT m n → LT m n ≡ True : ★)
|
||||
(λ ff ⇒ void¹ (False ≡ True : ★) ff)
|
||||
(λ n p tt ⇒ δ _ ⇒ True)
|
||||
(λ m p ff ⇒ void¹ (False ≡ True : ★) ff)
|
||||
(λ n m p tf ⇒ p tf)
|
||||
|
||||
def0 true-val :
|
||||
(m n : ℕ) → (lt : LT m n) → Eq (𝑖 ⇒ true-ty m n lt @𝑖) lt 'true =
|
||||
let IsTrue : (m n : ℕ) → LT m n → ★ =
|
||||
λ m n lt ⇒ Eq (𝑖 ⇒ true-ty m n lt @𝑖) lt 'true in
|
||||
elim-pair (λ m n ⇒ (lt : LT m n) → IsTrue m n lt)
|
||||
(λ ff ⇒ void (IsTrue 0 0 ff) ff)
|
||||
(λ n p tt ⇒ δ _ ⇒ 'true)
|
||||
(λ m p ff ⇒ void (IsTrue (succ m) 0 ff) ff)
|
||||
(λ n m p tf ⇒ p tf)
|
||||
|
||||
def revive : 0.(m n : ℕ) → 0.(LT m n) → LT m n =
|
||||
λ m n lt ⇒ coe (𝑘 ⇒ true-ty m n lt @𝑘) @1 @0 'true
|
||||
|
||||
|
||||
def drop : 0.(A : ★) → 0.(m n : ℕ) → LT m n → A → A =
|
||||
λ A m n lt x ⇒ true.drop A (coe (𝑖 ⇒ true-ty m n lt @𝑖) lt) x
|
||||
|
||||
def0 succ-both : (m n : ℕ) → LT m n → LT (succ m) (succ n) =
|
||||
λ m n p ⇒ p
|
||||
|
||||
def0 succ-right : (m n : ℕ) → LT m n → LT m (succ n) =
|
||||
λ m n lt ⇒
|
||||
elimω (λ m n _ ⇒ LT m (succ n))
|
||||
(λ _ ⇒ 'true)
|
||||
(λ _ _ _ ih ⇒ ih)
|
||||
m n lt
|
||||
|
||||
def0 right-is-succ : (m n : ℕ) → LT m n → IsSucc n =
|
||||
λ m n lt ⇒
|
||||
elimω (λ _ n _ ⇒ IsSucc n) (λ _ ⇒ 'true) (λ _ _ _ _ ⇒ 'true) m n lt
|
||||
|
||||
def right-has-succ : 0.(m : ℕ) → (n : ℕ) → 0.(LT m n) → HasSucc n =
|
||||
λ m n lt ⇒
|
||||
case n return n' ⇒ 0.(LT m n') → HasSucc n' of {
|
||||
0 ⇒ λ lt ⇒ void (HasSucc 0) (right-is-succ m 0 lt);
|
||||
succ n ⇒ λ _ ⇒ (n, [δ _ ⇒ succ n])
|
||||
} lt
|
||||
|
||||
def0 right-not-zero : (m : ℕ) → Not (LT m 0) =
|
||||
λ m ⇒ case m return m' ⇒ Not (LT m' 0) of { 0 ⇒ λ v ⇒ v; succ _ ⇒ λ v ⇒ v }
|
||||
|
||||
def0 plus-right : (m n₀ n₁ : ℕ) → LT m n₀ → LT m (plus n₀ n₁) =
|
||||
λ m n₀ n₁ lt ⇒
|
||||
elimω (λ m n _ ⇒ LT m (plus n n₁)) (λ _ ⇒ 'true) (λ _ _ _ ih ⇒ ih) m n₀ lt
|
||||
|
||||
#[compile-scheme "(lambda% (m n) (if (< m n) dec.Yes dec.No))"]
|
||||
def lt? : ω.(m n : ℕ) → Dec (LT m n) =
|
||||
elim-pairω (λ m n ⇒ Dec (LT m n))
|
||||
(No (LT 0 0) (λ v ⇒ v))
|
||||
(λ n p ⇒ Yes (LT 0 (succ n)) 'true)
|
||||
(λ m p ⇒ No (LT (succ m) 0) (λ v ⇒ v))
|
||||
(λ m n p ⇒
|
||||
dec.elim (LT m n) (λ _ ⇒ Dec (LT (succ m) (succ n)))
|
||||
(λ yes ⇒ Yes (LT (succ m) (succ n)) yes)
|
||||
(λ no ⇒ No (LT (succ m) (succ n)) no) p)
|
||||
|
||||
|
||||
def0 irrefl : (m n : ℕ) → LT m n → Not (m ≡ n : ℕ) =
|
||||
λ m n lt ⇒
|
||||
elimω (λ m n _ ⇒ Not (m ≡ n : ℕ))
|
||||
(λ n eq ⇒ zero-not-succ n eq)
|
||||
(λ m n _ ih eq ⇒ ih (succ-inj m n eq))
|
||||
m n lt
|
||||
|
||||
def0 asym : (m n : ℕ) → LT m n → Not (LT n m) =
|
||||
λ m n lt ⇒
|
||||
elimω (λ m n _ ⇒ Not (LT n m)) (λ _ ff ⇒ ff) (λ _ _ _ ih ff ⇒ ih ff) m n lt
|
||||
|
||||
def0 trans : (n₀ n₁ n₂ : ℕ) → LT n₀ n₁ → LT n₁ n₂ → LT n₀ n₂ =
|
||||
λ n₀ n₁ n₂ lt₀₁ lt₁₂ ⇒
|
||||
elimω (λ n₀ n₁ lt₀₁ ⇒ (n₂ : ℕ) → (lt₁₂ : LT n₁ n₂) → LT n₀ n₂)
|
||||
(λ n₁ n₂ ⇒
|
||||
case n₂ return n₂' ⇒ LT (succ n₁) n₂' → LT 0 n₂' of {
|
||||
0 ⇒ λ v ⇒ v;
|
||||
succ _ ⇒ λ _ ⇒ 'true
|
||||
})
|
||||
(λ n₀ n₁ lt₀₁ ih n₂ ⇒
|
||||
case n₂ return n₂' ⇒ LT (succ n₁) n₂' → LT (succ n₀) n₂' of {
|
||||
0 ⇒ λ v ⇒ v;
|
||||
succ n₂ ⇒ λ lt₁₂ ⇒ ih n₂ lt₁₂
|
||||
})
|
||||
n₀ n₁ lt₀₁ n₂ lt₁₂
|
||||
|
||||
}
|
||||
|
||||
namespace nat {
|
||||
def0 LT = lt.LT
|
||||
def lt? = lt.lt?
|
||||
}
|
||||
|
||||
|
||||
namespace fin {
|
||||
|
||||
def0 Bounded : ℕ → ℕ → ★ = λ n i ⇒ nat.LT i n
|
||||
|
||||
def0 Fin : ℕ → ★ = λ n ⇒ Sub ℕ (Bounded n)
|
||||
|
||||
def fin : 0.(n : ℕ) → (i : ℕ) → 0.(Bounded n i) → Fin n =
|
||||
λ n ⇒ sub.sub ℕ (Bounded n)
|
||||
|
||||
def val : 0.(n : ℕ) → Fin n → ℕ =
|
||||
λ n ⇒ sub.val ℕ (Bounded n)
|
||||
|
||||
def0 val-eq : (n : ℕ) → (i j : Fin n) → val n i ≡ val n j : ℕ → i ≡ j : Fin n =
|
||||
λ n ⇒ sub.sub-eq ℕ (Bounded n) (λ i ⇒ nat.lt.irr i n)
|
||||
|
||||
def0 proof : (n : ℕ) → (i : Fin n) → nat.LT (val n i) n =
|
||||
λ n ⇒ sub.proof ℕ (Bounded n)
|
||||
|
||||
|
||||
def0 no-fin0 : Not (Fin 0) =
|
||||
λ f0 ⇒ case f0 return False of { (i, lt) ⇒
|
||||
nat.lt.right-not-zero i (get0 (nat.LT i 0) lt)
|
||||
}
|
||||
|
||||
|
||||
def fin? : ω.(n i : ℕ) → Maybe (Fin n) =
|
||||
λ n ⇒ sub.sub? ℕ (Bounded n) (λ i ⇒ nat.lt? i n)
|
||||
|
||||
def F0 : 0.(n : ℕ) → Fin (succ n) =
|
||||
λ n ⇒ fin (succ n) 0 'true
|
||||
def FS : 0.(n : ℕ) → Fin n → Fin (succ n) =
|
||||
λ n i ⇒ fin (succ n) (succ (val n i)) (proof n i)
|
||||
|
||||
def weak : 0.(m n : ℕ) → 0.(nat.LT m n) → Fin m → Fin n =
|
||||
λ m n mn i' ⇒
|
||||
let i = val m i'; 0.im = proof m i' in
|
||||
fin n i (nat.lt.trans i m n im mn)
|
||||
|
||||
|
||||
def bound-has-succ : (n : ℕ) → 0.(Fin n) → nat.HasSucc n =
|
||||
λ n i ⇒ nat.lt.right-has-succ (fst i) n (get0 (nat.LT (fst i) n) (snd i))
|
||||
|
||||
def elim' :
|
||||
0.(P : (n i : ℕ) → nat.LT i n → ★) →
|
||||
1.(pz : 0.(n : ℕ) → P (succ n) 0 'true) →
|
||||
ω.(ps : 0.(n i : ℕ) → 0.(lt : nat.LT i n) →
|
||||
P n i lt → P (succ n) (succ i) lt) →
|
||||
0.(n : ℕ) → (i : ℕ) → 0.(lt : nat.LT i n) → P n i lt =
|
||||
λ P pz ps n i lt ⇒
|
||||
case i return i' ⇒ 0.(n : ℕ) → 0.(lt : nat.LT i' n) → P n i' lt of {
|
||||
0 ⇒ λ n lt ⇒
|
||||
let0 npp = nat.lt.right-has-succ 0 n lt;
|
||||
p = nat.has-succ.val n npp;
|
||||
np = nat.has-succ.proof n npp in
|
||||
coe (𝑘 ⇒ P (np @𝑘) 0 (coe (𝑙 ⇒ nat.LT 0 (np @𝑙)) @0 @𝑘 lt)) @1 @0
|
||||
(pz p);
|
||||
succ i, ih ⇒ λ n lt ⇒
|
||||
let 0.npp = nat.lt.right-has-succ (succ i) n lt;
|
||||
0.p = nat.has-succ.val n npp;
|
||||
0.np = nat.has-succ.proof n npp;
|
||||
0.lt' : nat.LT i p = coe (𝑘 ⇒ nat.LT (succ i) (np @𝑘)) lt;
|
||||
0.lteq : Eq (𝑘 ⇒ nat.LT (succ i) (np @𝑘)) lt lt' =
|
||||
δ 𝑘 ⇒ coe (𝑙 ⇒ nat.LT (succ i) (np @𝑙)) @0 @𝑘 lt;
|
||||
1.almost : P (succ p) (succ i) lt' = ps p i lt' (ih p lt') in
|
||||
coe (𝑘 ⇒ P (np @𝑘) (succ i) (lteq @𝑘)) @1 @0 almost;
|
||||
} n lt
|
||||
|
||||
def elim : 0.(P : (n : ℕ) → Fin n → ★) →
|
||||
(pz : 0.(n : ℕ) → P (succ n) (F0 n)) →
|
||||
(ps : 0.(n : ℕ) → 0.(i : Fin n) →
|
||||
P n i → P (succ n) (FS n i)) →
|
||||
0.(n : ℕ) → (i : Fin n) → P n i =
|
||||
λ P pz ps n ilt ⇒
|
||||
case ilt return ilt' ⇒ P n ilt' of { (i, lt) ⇒
|
||||
let0 lt = get0 (nat.LT i n) lt in
|
||||
drop0 (nat.LT i n) (P n (i, [lt])) lt
|
||||
(elim' (λ n i lt ⇒ P n (i, [lt])) pz (λ n i lt ⇒ ps n (i, [lt])) n i lt)
|
||||
}
|
||||
|
||||
{-
|
||||
def elim : 0.(P : (n : ℕ) → Fin n → ★) →
|
||||
(pz : 0.(n : ℕ) → P (succ n) (F0 n)) →
|
||||
(ps : 0.(n : ℕ) → 0.(i : Fin n) →
|
||||
P n i → P (succ n) (FS n i)) →
|
||||
0.(n : ℕ) → (i : Fin n) → P n i =
|
||||
λ P pz ps n ilt ⇒
|
||||
let i = val n ilt; 0.lt : nat.LT i n = proof n ilt;
|
||||
0.pp = nat.lt.right-has-succ i n lt;
|
||||
0.p = nat.has-succ.val n pp; 0.np = nat.has-succ.proof n pp;
|
||||
0.RES : ℕ → ℕ → ★ =
|
||||
λ i n ⇒ (lt : nat.LT i n) × P n (i, [lt]);
|
||||
res : RES i (succ p) =
|
||||
case i
|
||||
return i' ⇒ 0.(p : ℕ) → 0.(nat.LT i' (succ p)) → RES i' (succ p)
|
||||
of {
|
||||
0 ⇒ λ p _ ⇒ ('true, pz p);
|
||||
succ i, IH ⇒ λ p lt ⇒
|
||||
let 0.qq = nat.lt.right-has-succ i p lt;
|
||||
0.q = nat.has-succ.val p qq; 0.pq = nat.has-succ.proof p qq;
|
||||
0.lt : nat.LT i (succ q) = coe (𝑘 ⇒ nat.LT i (pq @𝑘)) lt;
|
||||
in
|
||||
case IH q lt return RES (succ i) (succ p) of { (lt', ih') ⇒
|
||||
let lt : nat.LT (succ i) (succ p) =
|
||||
coe (𝑘 ⇒ nat.LT i (pq @𝑘)) @1 @0 lt';
|
||||
ih : P p (i, [lt]) =
|
||||
coe (𝑘 ⇒ P (pq @𝑘) (i, [coe (𝑙 ⇒ nat.LT i (pq @𝑙)) @1 @𝑘 lt']))
|
||||
@1 @0 ih';
|
||||
res : P (succ p) (succ i, [lt]) =
|
||||
ps p (i, [lt]) ih;
|
||||
in
|
||||
(lt, res)
|
||||
}
|
||||
} p (coe (𝑘 ⇒ nat.LT i (np @𝑘)) lt);
|
||||
in
|
||||
case coe (𝑘 ⇒ RES i (np @𝑘)) @1 @0 res
|
||||
return P n ilt
|
||||
of { (lt', res) ⇒
|
||||
nat.lt.drop (P n ilt) i n lt' res
|
||||
}
|
||||
-}
|
||||
|
||||
}
|
||||
|
||||
|
||||
def0 Fin = fin.Fin
|
||||
def F0 = fin.F0
|
||||
def FS = fin.FS
|
||||
|
|
@ -0,0 +1,149 @@
|
|||
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 → ℕ
|
||||
}
|
||||
|
|
@ -0,0 +1,100 @@
|
|||
load "misc.quox"
|
||||
load "maybe.quox"
|
||||
load "list.quox"
|
||||
|
||||
namespace io {
|
||||
|
||||
def0 IORes : ★ → ★ = λ A ⇒ A × IOState
|
||||
|
||||
def0 IO : ★ → ★ = λ A ⇒ IOState → IORes A
|
||||
|
||||
def pure : 0.(A : ★) → A → IO A = λ A x s ⇒ (x, s)
|
||||
|
||||
def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B =
|
||||
λ A B m k s0 ⇒
|
||||
case m s0 return IORes B of { (x, s1) ⇒ k x s1 }
|
||||
|
||||
def bindω : 0.(A B : ★) → IO [ω.A] → (ω.A → IO B) → IO B =
|
||||
λ A B m k s0 ⇒
|
||||
case m s0 return IORes B of { (x, s1) ⇒
|
||||
case x return IORes B of { [x] ⇒ k x s1 }
|
||||
}
|
||||
|
||||
def map : 0.(A B : ★) → (A → B) → IO A → IO B =
|
||||
λ A B f m ⇒ bind A B m (λ x ⇒ pure B (f x))
|
||||
|
||||
def mapω : 0.(A B : ★) → (ω.A → B) → IO [ω.A] → IO B =
|
||||
λ A B f m ⇒ bindω A B m (λ x ⇒ pure B (f x))
|
||||
|
||||
def seq : 0.(B : ★) → IO True → IO B → IO B =
|
||||
λ B x y ⇒ bind True B x (λ u ⇒ case u return IO B of { 'true ⇒ y })
|
||||
|
||||
def seq' : IO True → IO True → IO True = seq True
|
||||
|
||||
def pass : IO True = pure True 'true
|
||||
|
||||
#[compile-scheme "(lambda (str) (builtin-io (display str) 'true))"]
|
||||
postulate print : String → IO True
|
||||
|
||||
#[compile-scheme "(lambda (str) (builtin-io (write str) (newline) 'true))"]
|
||||
postulate dump : 0.(A : ★) → A → IO True
|
||||
|
||||
def newline = print "\n"
|
||||
|
||||
def println : String → IO True =
|
||||
λ str ⇒ seq' (print str) newline
|
||||
|
||||
#[compile-scheme "(builtin-io (get-line (current-input-port)))"]
|
||||
postulate readln : IO String
|
||||
|
||||
|
||||
-- [todo] errors lmao
|
||||
|
||||
{-
|
||||
postulate0 File : ★
|
||||
|
||||
#[compile-scheme "(lambda (path) (builtin-io (open-input-file path)))"]
|
||||
postulate open-read : String → IO File
|
||||
|
||||
#[compile-scheme "(lambda (file) (builtin-io (close-port file) 'true))"]
|
||||
postulate close : File → IO True
|
||||
|
||||
#[compile-scheme
|
||||
"(lambda% (file if-eof if-line)
|
||||
(builtin-io
|
||||
(let ([result (get-line file)])
|
||||
(if (eof-object? result)
|
||||
(cons if-eof file)
|
||||
(cons (if-line result) file)))))"]
|
||||
postulate prim-read-line :
|
||||
File →
|
||||
ω.(if-eof : Maybe [ω.String]) →
|
||||
ω.(if-line : ω.String → Maybe [ω.String]) →
|
||||
IO (Maybe [ω.String] × File)
|
||||
|
||||
def read-line : File → IO (Maybe [ω.String] × File) =
|
||||
λ f ⇒ prim-read-line f (Nothing [ω.String]) (λ x ⇒ Just [ω.String] [x])
|
||||
-}
|
||||
|
||||
|
||||
#[compile-scheme
|
||||
"(lambda (path) (builtin-io (call-with-input-file path get-string-all)))"]
|
||||
postulate read-fileω : ω.(path : String) → IO [ω.String]
|
||||
|
||||
def read-file : ω.(path : String) → IO String =
|
||||
λ path ⇒
|
||||
map [ω.String] String (getω String) (read-fileω path)
|
||||
|
||||
|
||||
#[compile-scheme
|
||||
"(lambda (path) (builtin-io
|
||||
(call-with-input-file path
|
||||
(lambda (file)
|
||||
(do [(line (get-line file) (get-line file))
|
||||
(acc '() (cons line acc))]
|
||||
[(eof-object? line) (reverse acc)])))))"]
|
||||
postulate read-file-lines : ω.(path : String) → IO (List String)
|
||||
|
||||
}
|
||||
|
||||
def0 IO = io.IO
|
||||
|
|
@ -0,0 +1,43 @@
|
|||
load "misc.quox"
|
||||
|
||||
def0 Irr1 : (A : ★) → (A → ★) → ★ =
|
||||
λ A P ⇒ (x : A) → (p q : P x) → p ≡ q : P x
|
||||
|
||||
def0 Sub : (A : ★) → (P : A → ★) → ★ =
|
||||
λ A P ⇒ (x : A) × [0. P x]
|
||||
|
||||
def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ =
|
||||
λ A P s ⇒ Dup A (fst s)
|
||||
-- (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]]
|
||||
|
||||
def subdup-to-dup :
|
||||
0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
|
||||
0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
|
||||
λ A P pirr s sd ⇒
|
||||
case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
|
||||
case ss0 return Dup (Sub A P) s of { [ss0] ⇒
|
||||
case sω
|
||||
return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s
|
||||
of { [s!] ⇒ λ ss' ⇒
|
||||
let ω.p : [0.P (fst s)] = revive0 (P (fst s)) (snd s);
|
||||
0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss' in
|
||||
([(s!, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @0 p)],
|
||||
[δ 𝑗 ⇒ [(ss @𝑗, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @𝑗 p)]])
|
||||
} ss0
|
||||
}}
|
||||
|
||||
def subdup : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
|
||||
((x : A) → Dup A x) →
|
||||
(s : Sub A P) → SubDup A P s =
|
||||
λ A P pirr dup s ⇒
|
||||
case s return s' ⇒ SubDup A P s' of { (x, p) ⇒
|
||||
drop0 (P x) (Dup A x) p (dup x)
|
||||
}
|
||||
|
||||
def dup : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
|
||||
((x : A) → Dup A x) →
|
||||
(s : Sub A P) → Dup (Sub A P) s =
|
||||
λ A P pirr dup s ⇒ subdup-to-dup A P pirr s (subdup A P pirr dup s)
|
||||
|
||||
def forget : 0.(A : ★) → 0.(P : A → ★) → Sub A P → A =
|
||||
λ A P s ⇒ case s return A of { (x, p) ⇒ drop0 (P x) A p x }
|
||||
|
|
@ -0,0 +1,590 @@
|
|||
load "misc.quox"
|
||||
load "nat.quox"
|
||||
load "maybe.quox"
|
||||
load "bool.quox"
|
||||
load "qty.quox"
|
||||
|
||||
namespace vec {
|
||||
|
||||
def0 Vec : ℕ → ★ → ★ =
|
||||
λ n A ⇒
|
||||
caseω n return ★ of {
|
||||
zero ⇒ {nil};
|
||||
succ _, 0.Tail ⇒ A × Tail
|
||||
}
|
||||
|
||||
def drop-nil-dep : 0.(A : ★) → 0.(P : Vec 0 A → ★) →
|
||||
(xs : Vec 0 A) → P 'nil → P xs =
|
||||
λ A P xs p ⇒ case xs return xs' ⇒ P xs' of { 'nil ⇒ p }
|
||||
|
||||
def drop-nil : 0.(A B : ★) → Vec 0 A → B → B =
|
||||
λ A B ⇒ drop-nil-dep A (λ _ ⇒ B)
|
||||
|
||||
def match-dep :
|
||||
0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
|
||||
ω.(P 0 'nil) →
|
||||
ω.((n : ℕ) → (x : A) → (xs : Vec n A) → P (succ n) (x, xs)) →
|
||||
(n : ℕ) → (xs : Vec n A) → P n xs =
|
||||
λ A P pn pc n ⇒
|
||||
case n return n' ⇒ (xs : Vec n' A) → P n' xs of {
|
||||
0 ⇒ λ nil ⇒ drop-nil-dep A (P 0) nil pn;
|
||||
succ len ⇒ λ cons ⇒
|
||||
case cons return cons' ⇒ P (succ len) cons' of {
|
||||
(first, rest) ⇒ pc len first rest
|
||||
}
|
||||
}
|
||||
|
||||
def match-depω :
|
||||
0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
|
||||
ω.(P 0 'nil) →
|
||||
ω.(ω.(n : ℕ) → ω.(x : A) → ω.(xs : Vec n A) → P (succ n) (x, xs)) →
|
||||
ω.(n : ℕ) → ω.(xs : Vec n A) → P n xs =
|
||||
λ A P pn pc n ⇒
|
||||
caseω n return n' ⇒ ω.(xs : Vec n' A) → P n' xs of {
|
||||
0 ⇒ λ nil ⇒ drop-nil-dep A (P 0) nil pn;
|
||||
succ len ⇒ λ cons ⇒
|
||||
caseω cons return cons' ⇒ P (succ len) cons' of {
|
||||
(first, rest) ⇒ pc len first rest
|
||||
}
|
||||
}
|
||||
def match-dep# = match-depω
|
||||
|
||||
def elim : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
|
||||
P 0 'nil →
|
||||
ω.((x : A) → 0.(n : ℕ) → 0.(xs : Vec n A) →
|
||||
P n xs → P (succ n) (x, xs)) →
|
||||
(n : ℕ) → (xs : Vec n A) → P n xs =
|
||||
λ A P pn pc n ⇒
|
||||
case n return n' ⇒ (xs' : Vec n' A) → P n' xs' of {
|
||||
zero ⇒ λ nil ⇒
|
||||
case nil return nil' ⇒ P 0 nil' of { 'nil ⇒ pn };
|
||||
succ n, IH ⇒ λ cons ⇒
|
||||
case cons return cons' ⇒ P (succ n) cons' of {
|
||||
(first, rest) ⇒ pc first n rest (IH rest)
|
||||
}
|
||||
}
|
||||
|
||||
def elim2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★) →
|
||||
P 0 'nil 'nil →
|
||||
ω.((x : A) → (y : B) → 0.(n : ℕ) →
|
||||
0.(xs : Vec n A) → 0.(ys : Vec n B) →
|
||||
P n xs ys → P (succ n) (x, xs) (y, ys)) →
|
||||
(n : ℕ) → (xs : Vec n A) → (ys : Vec n B) → P n xs ys =
|
||||
λ A B P pn pc n ⇒
|
||||
case n return n' ⇒ (xs : Vec n' A) → (ys : Vec n' B) → P n' xs ys of {
|
||||
zero ⇒ λ nila nilb ⇒
|
||||
drop-nil-dep A (λ n ⇒ P 0 n nilb) nila
|
||||
(drop-nil-dep B (λ n ⇒ P 0 'nil n) nilb pn);
|
||||
succ n, IH ⇒ λ consa consb ⇒
|
||||
case consa return consa' ⇒ P (succ n) consa' consb of { (a, as) ⇒
|
||||
case consb return consb' ⇒ P (succ n) (a, as) consb' of { (b, bs) ⇒
|
||||
pc a b n as bs (IH as bs)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
def elim2-uneven :
|
||||
0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →
|
||||
-- both nil
|
||||
ω.(P 0 0 'nil 'nil) →
|
||||
-- first nil
|
||||
ω.((y : B) → 0.(n : ℕ) → 0.(ys : Vec n B) →
|
||||
P 0 n 'nil ys → P 0 (succ n) 'nil (y, ys)) →
|
||||
-- second nil
|
||||
ω.((x : A) → 0.(m : ℕ) → 0.(xs : Vec m A) →
|
||||
P m 0 xs 'nil → P (succ m) 0 (x, xs) 'nil) →
|
||||
-- both cons
|
||||
ω.((x : A) → (y : B) → 0.(m n : ℕ) →
|
||||
0.(xs : Vec m A) → 0.(ys : Vec n B) →
|
||||
P m n xs ys → P (succ m) (succ n) (x, xs) (y, ys)) →
|
||||
(m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) → P m n xs ys =
|
||||
λ A B P pnn pnc pcn pcc ⇒
|
||||
nat.elim-pair (λ m n ⇒ (xs : Vec m A) → (ys : Vec n B) → P m n xs ys)
|
||||
(λ xnil ynil ⇒
|
||||
let0 Ret = P 0 0 'nil 'nil in
|
||||
drop-nil A Ret xnil (drop-nil B Ret ynil pnn))
|
||||
(λ n IH xnil yys ⇒
|
||||
case yys return yys' ⇒ P 0 (succ n) 'nil yys' of { (y, ys) ⇒
|
||||
pnc y n ys (IH xnil ys)
|
||||
})
|
||||
(λ m IH xxs ynil ⇒
|
||||
case xxs return xxs' ⇒ P (succ m) 0 xxs' 'nil of { (x, xs) ⇒
|
||||
pcn x m xs (IH xs ynil)
|
||||
})
|
||||
(λ m n IH xxs yys ⇒
|
||||
case xxs return xxs' ⇒ P (succ m) (succ n) xxs' yys of { (x, xs) ⇒
|
||||
case yys return yys' ⇒ P (succ m) (succ n) (x, xs) yys' of { (y, ys) ⇒
|
||||
pcc x y m n xs ys (IH xs ys)
|
||||
}})
|
||||
|
||||
-- haha gross
|
||||
def elimω : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
|
||||
ω.(P 0 'nil) →
|
||||
ω.(ω.(x : A) → ω.(n : ℕ) → ω.(xs : Vec n A) →
|
||||
ω.(P n xs) → P (succ n) (x, xs)) →
|
||||
ω.(n : ℕ) → ω.(xs : Vec n A) → P n xs =
|
||||
λ A P pn pc n ⇒
|
||||
caseω n return n' ⇒ ω.(xs' : Vec n' A) → P n' xs' of {
|
||||
zero ⇒ λ _ ⇒ pn;
|
||||
succ n, ω.IH ⇒ λ xxs ⇒
|
||||
letω x = fst xxs; xs = snd xxs in pc x n xs (IH xs)
|
||||
}
|
||||
|
||||
def elimω2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★) →
|
||||
ω.(P 0 'nil 'nil) →
|
||||
ω.(ω.(x : A) → ω.(y : B) → ω.(n : ℕ) →
|
||||
ω.(xs : Vec n A) → ω.(ys : Vec n B) →
|
||||
ω.(P n xs ys) → P (succ n) (x, xs) (y, ys)) →
|
||||
ω.(n : ℕ) → ω.(xs : Vec n A) → ω.(ys : Vec n B) → P n xs ys =
|
||||
λ A B P pn pc n ⇒
|
||||
caseω n return n' ⇒ ω.(xs : Vec n' A) → ω.(ys : Vec n' B) → P n' xs ys of {
|
||||
zero ⇒ λ _ _ ⇒ pn;
|
||||
succ n, ω.IH ⇒ λ xxs yys ⇒
|
||||
letω x = fst xxs; xs = snd xxs; y = fst yys; ys = snd yys in
|
||||
pc x y n xs ys (IH xs ys)
|
||||
}
|
||||
|
||||
postulate elimP :
|
||||
ω.(π : NzQty) → ω.(ρₙ ρₗ : Qty) →
|
||||
0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
|
||||
FunNz π (P 0 'nil)
|
||||
(Fun 'any
|
||||
(FUN-NZ π A (λ x ⇒ FUN ρₙ ℕ (λ n ⇒ FUN ρₗ (Vec n A) (λ xs ⇒
|
||||
FunNz π (P n xs) (P (succ n) (x, xs))))))
|
||||
(FUN-NZ π ℕ (λ n ⇒ FUN-NZ π (Vec n A) (λ xs ⇒ P n xs))))
|
||||
{-
|
||||
=
|
||||
λ π ρₙ ρₗ A P ⇒ uhhhhhhhhhhhhhhhhhhh
|
||||
-}
|
||||
|
||||
def elimω2-uneven :
|
||||
0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →
|
||||
-- both nil
|
||||
ω.(P 0 0 'nil 'nil) →
|
||||
-- first nil
|
||||
ω.(ω.(y : B) → ω.(n : ℕ) → ω.(ys : Vec n B) →
|
||||
ω.(P 0 n 'nil ys) → P 0 (succ n) 'nil (y, ys)) →
|
||||
-- second nil
|
||||
ω.(ω.(x : A) → ω.(m : ℕ) → ω.(xs : Vec m A) →
|
||||
ω.(P m 0 xs 'nil) → P (succ m) 0 (x, xs) 'nil) →
|
||||
-- both cons
|
||||
ω.(ω.(x : A) → ω.(y : B) → ω.(m n : ℕ) →
|
||||
ω.(xs : Vec m A) → ω.(ys : Vec n B) →
|
||||
ω.(P m n xs ys) → P (succ m) (succ n) (x, xs) (y, ys)) →
|
||||
ω.(m n : ℕ) → ω.(xs : Vec m A) → ω.(ys : Vec n B) → P m n xs ys =
|
||||
λ A B P pnn pnc pcn pcc ⇒
|
||||
nat.elim-pairω (λ m n ⇒ ω.(xs : Vec m A) → ω.(ys : Vec n B) → P m n xs ys)
|
||||
(λ _ _ ⇒ pnn)
|
||||
(λ n IH xnil yys ⇒
|
||||
letω y = fst yys; ys = snd yys in pnc y n ys (IH xnil ys))
|
||||
(λ m IH xxs ynil ⇒
|
||||
letω x = fst xxs; xs = snd xxs in pcn x m xs (IH xs ynil))
|
||||
(λ m n IH xxs yys ⇒
|
||||
letω x = fst xxs; xs = snd xxs; y = fst yys; ys = snd yys in
|
||||
pcc x y m n xs ys (IH xs ys))
|
||||
|
||||
def zip-with : 0.(A B C : ★) → ω.(A → B → C) →
|
||||
(n : ℕ) → Vec n A → Vec n B → Vec n C =
|
||||
λ A B C f ⇒
|
||||
elim2 A B (λ n _ _ ⇒ Vec n C) 'nil (λ a b _ _ _ abs ⇒ (f a b, abs))
|
||||
|
||||
def zip-withω : 0.(A B C : ★) → ω.(ω.A → ω.B → C) →
|
||||
ω.(n : ℕ) → ω.(Vec n A) → ω.(Vec n B) → Vec n C =
|
||||
λ A B C f ⇒
|
||||
elimω2 A B (λ n _ _ ⇒ Vec n C) 'nil (λ a b _ _ _ abs ⇒ (f a b, abs))
|
||||
|
||||
|
||||
namespace zip-with {
|
||||
def0 Failure : (A B : ★) → (m n : ℕ) → Vec m A → Vec n B → ★ =
|
||||
λ A B m n xs ys ⇒
|
||||
Sing (Vec m A) xs × Sing (Vec n B) ys × [0. Not (m ≡ n : ℕ)]
|
||||
|
||||
def0 Success : (C : ★) → (m n : ℕ) → ★ =
|
||||
λ C m n ⇒ Vec n C × [0. m ≡ n : ℕ]
|
||||
|
||||
def0 Result : (A B C : ★) → (m n : ℕ) → Vec m A → Vec n B → ★ =
|
||||
λ A B C m n xs ys ⇒
|
||||
Either (Failure A B m n xs ys) (Success C m n)
|
||||
|
||||
def zip-with-hetω : 0.(A B C : ★) → ω.(A → B → C) →
|
||||
ω.(m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) →
|
||||
Result A B C m n xs ys =
|
||||
λ A B C f m n xs ys ⇒
|
||||
let0 TNo : Vec m A → Vec n B → ★ = Failure A B m n;
|
||||
TYes : ★ = Success C m n;
|
||||
TRes : Vec m A → Vec n B → ★ = λ xs ys ⇒ Either (TNo xs ys) TYes in
|
||||
dec.elim (m ≡ n : ℕ)
|
||||
(λ _ ⇒ (xs : Vec m A) → (ys : Vec n B) → TRes xs ys)
|
||||
(λ eq xs ys ⇒
|
||||
let zs : Vec n C =
|
||||
zip-with A B C f n (coe (𝑖 ⇒ Vec (eq @𝑖) A) xs) ys in
|
||||
Right (TNo xs ys) TYes (zs, [eq]))
|
||||
(λ neq xs ys ⇒ Left (TNo xs ys) TYes
|
||||
(sing (Vec m A) xs, sing (Vec n B) ys, [neq]))
|
||||
(nat.eq? m n) xs ys
|
||||
|
||||
def zip-with-het : 0.(A B C : ★) → ω.(A → B → C) →
|
||||
(m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) →
|
||||
Result A B C m n xs ys =
|
||||
λ A B C f m n ⇒
|
||||
let0 Ret : ℕ → ℕ → ★ =
|
||||
λ m n ⇒ (xs : Vec m A) → (ys : Vec n B) → Result A B C m n xs ys in
|
||||
dup.elim ℕ m (λ m' ⇒ Ret m' n)
|
||||
(λ m ⇒ dup.elim ℕ n (λ n' ⇒ Ret m n')
|
||||
(λ n ⇒ zip-with-hetω A B C f m n) (nat.dup! n))
|
||||
(nat.dup! m)
|
||||
}
|
||||
def0 ZipWith = zip-with.Result
|
||||
def zip-with-het = zip-with.zip-with-het
|
||||
def zip-with-hetω = zip-with.zip-with-hetω
|
||||
|
||||
#[compile-scheme "(lambda% (n xs) xs)"]
|
||||
def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A =
|
||||
λ A n ⇒
|
||||
case n return n' ⇒ Vec n' A → Vec¹ n' A of {
|
||||
zero ⇒ λ xs ⇒
|
||||
case xs return Vec¹ 0 A of { 'nil ⇒ 'nil };
|
||||
succ n', f' ⇒ λ xs ⇒
|
||||
case xs return Vec¹ (succ n') A of {
|
||||
(first, rest) ⇒ (first, f' rest)
|
||||
}
|
||||
}
|
||||
|
||||
def append : 0.(A : ★) → (m : ℕ) → 0.(n : ℕ) →
|
||||
Vec m A → Vec n A → Vec (nat.plus m n) A =
|
||||
λ A m n xs ys ⇒
|
||||
elim A (λ m _ ⇒ Vec (nat.plus m n) A) ys (λ x _ _ xsys ⇒ (x, xsys)) m xs
|
||||
|
||||
}
|
||||
|
||||
def0 Vec = vec.Vec
|
||||
|
||||
|
||||
namespace list {
|
||||
|
||||
def0 List : ★ → ★ =
|
||||
λ A ⇒ (len : ℕ) × Vec len A
|
||||
|
||||
def Nil : 0.(A : ★) → List A =
|
||||
λ A ⇒ (0, 'nil)
|
||||
|
||||
def Cons : 0.(A : ★) → A → List A → List A =
|
||||
λ A x xs ⇒ case xs return List A of { (len, elems) ⇒ (succ len, x, elems) }
|
||||
|
||||
def single : 0.(A : ★) → A → List A =
|
||||
λ A x ⇒ Cons A x (Nil A)
|
||||
|
||||
def elim : 0.(A : ★) → 0.(P : List A → ★) →
|
||||
P (Nil A) →
|
||||
ω.((x : A) → 0.(xs : List A) → P xs → P (Cons A x xs)) →
|
||||
(xs : List A) → P xs =
|
||||
λ A P pn pc xs ⇒
|
||||
case xs return xs' ⇒ P xs' of { (len, elems) ⇒
|
||||
vec.elim A (λ n xs ⇒ P (n, xs))
|
||||
pn (λ x n xs IH ⇒ pc x (n, xs) IH)
|
||||
len elems
|
||||
}
|
||||
|
||||
def elimω : 0.(A : ★) → 0.(P : List A → ★) →
|
||||
ω.(P (Nil A)) →
|
||||
ω.(ω.(x : A) → ω.(xs : List A) → ω.(P xs) → P (Cons A x xs)) →
|
||||
ω.(xs : List A) → P xs =
|
||||
λ A P pn pc xs ⇒
|
||||
caseω xs return xs' ⇒ P xs' of { (len, elems) ⇒
|
||||
vec.elimω A (λ n xs ⇒ P (n, xs))
|
||||
pn (λ x n xs IH ⇒ pc x (n, xs) IH)
|
||||
len elems
|
||||
}
|
||||
|
||||
def elim2 : 0.(A B : ★) → 0.(P : List A → List B → ★) →
|
||||
ω.(P (Nil A) (Nil B)) →
|
||||
ω.((y : B) → 0.(ys : List B) →
|
||||
P (Nil A) ys → P (Nil A) (Cons B y ys)) →
|
||||
ω.((x : A) → 0.(xs : List A) →
|
||||
P xs (Nil B) → P (Cons A x xs) (Nil B)) →
|
||||
ω.((x : A) → 0.(xs : List A) → (y : B) → 0.(ys : List B) →
|
||||
P xs ys → P (Cons A x xs) (Cons B y ys)) →
|
||||
(xs : List A) → (ys : List B) → P xs ys =
|
||||
λ A B P pnn pnc pcn pcc xs ys ⇒
|
||||
case xs return xs' ⇒ P xs' ys of { (m, xs) ⇒
|
||||
case ys return ys' ⇒ P (m, xs) ys' of { (n, ys) ⇒
|
||||
vec.elim2-uneven A B (λ m n xs ys ⇒ P (m, xs) (n, ys))
|
||||
pnn
|
||||
(λ y n ys IH ⇒ pnc y (n, ys) IH)
|
||||
(λ x m xs IH ⇒ pcn x (m, xs) IH)
|
||||
(λ x y m n xs ys IH ⇒ pcc x (m, xs) y (n, ys) IH)
|
||||
m n xs ys
|
||||
}}
|
||||
|
||||
def elimω2 : 0.(A B : ★) → 0.(P : List A → List B → ★) →
|
||||
ω.(P (Nil A) (Nil B)) →
|
||||
ω.(ω.(y : B) → ω.(ys : List B) →
|
||||
ω.(P (Nil A) ys) → P (Nil A) (Cons B y ys)) →
|
||||
ω.(ω.(x : A) → ω.(xs : List A) →
|
||||
ω.(P xs (Nil B)) → P (Cons A x xs) (Nil B)) →
|
||||
ω.(ω.(x : A) → ω.(xs : List A) → ω.(y : B) → ω.(ys : List B) →
|
||||
ω.(P xs ys) → P (Cons A x xs) (Cons B y ys)) →
|
||||
ω.(xs : List A) → ω.(ys : List B) → P xs ys =
|
||||
λ A B P pnn pnc pcn pcc xs ys ⇒
|
||||
caseω xs return xs' ⇒ P xs' ys of { (m, xs) ⇒
|
||||
caseω ys return ys' ⇒ P (m, xs) ys' of { (n, ys) ⇒
|
||||
vec.elimω2-uneven A B (λ m n xs ys ⇒ P (m, xs) (n, ys))
|
||||
pnn
|
||||
(λ y n ys IH ⇒ pnc y (n, ys) IH)
|
||||
(λ x m xs IH ⇒ pcn x (m, xs) IH)
|
||||
(λ x y m n xs ys IH ⇒ pcc x (m, xs) y (n, ys) IH)
|
||||
m n xs ys
|
||||
}}
|
||||
|
||||
def as-vec : 0.(A : ★) → 0.(P : List A → ★) → (xs : List A) →
|
||||
(ω.(n : ℕ) → (xs : Vec n A) → P (n, xs)) → P xs =
|
||||
λ A P xs f ⇒
|
||||
case xs return xs' ⇒ P xs' of { (n, xs) ⇒
|
||||
dup.elim ℕ n (λ n' ⇒ (xs : Vec n' A) → P (n', xs)) f (nat.dup! n) xs
|
||||
}
|
||||
|
||||
def match-dep :
|
||||
0.(A : ★) → 0.(P : List A → ★) →
|
||||
ω.(P (Nil A)) → ω.((x : A) → (xs : List A) → P (Cons A x xs)) →
|
||||
(xs : List A) → P xs =
|
||||
λ A P pn pc xs ⇒
|
||||
case xs return xs' ⇒ P xs' of {
|
||||
(len, elems) ⇒
|
||||
vec.match-dep A (λ n xs ⇒ P (n, xs)) pn (λ n x xs ⇒ pc x (n, xs))
|
||||
len elems
|
||||
}
|
||||
|
||||
def match-depω :
|
||||
0.(A : ★) → 0.(P : List A → ★) →
|
||||
ω.(P (Nil A)) →
|
||||
ω.(ω.(x : A) → ω.(xs : List A) → P (Cons A x xs)) →
|
||||
ω.(xs : List A) → P xs =
|
||||
λ A P pn pc xs ⇒
|
||||
vec.match-depω A (λ n xs ⇒ P (n, xs)) pn (λ n x xs ⇒ pc x (n, xs))
|
||||
(fst xs) (snd xs)
|
||||
def match-dep# = match-depω
|
||||
|
||||
def match : 0.(A B : ★) → ω.B → ω.(A → List A → B) → List A → B =
|
||||
λ A B ⇒ match-dep A (λ _ ⇒ B)
|
||||
|
||||
def matchω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.(List A) → B) → ω.(List A) → B =
|
||||
λ A B ⇒ match-depω A (λ _ ⇒ B)
|
||||
def match# = matchω
|
||||
|
||||
|
||||
def up : 0.(A : ★) → List A → List¹ A =
|
||||
λ A xs ⇒
|
||||
case xs return List¹ A of { (len, elems) ⇒
|
||||
dup.elim'¹ ℕ len (λ _ ⇒ List¹ A)
|
||||
(λ len eq ⇒ (len, vec.up A len (coe (𝑖 ⇒ Vec (eq @𝑖) A) @1 @0 elems)))
|
||||
(nat.dup! len)
|
||||
}
|
||||
|
||||
def foldr : 0.(A B : ★) → B → ω.(A → B → B) → List A → B =
|
||||
λ A B z f xs ⇒ elim A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs
|
||||
|
||||
def foldl : 0.(A B : ★) → B → ω.(B → A → B) → List A → B =
|
||||
λ A B z f xs ⇒
|
||||
foldr A (B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z
|
||||
|
||||
def map : 0.(A B : ★) → ω.(A → B) → List A → List B =
|
||||
λ A B f ⇒ foldr A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys)
|
||||
|
||||
|
||||
-- ugh
|
||||
def foldrω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.B → B) → ω.(List A) → B =
|
||||
λ A B z f xs ⇒ elimω A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs
|
||||
|
||||
def foldlω : 0.(A B : ★) → ω.B → ω.(ω.B → ω.A → B) → ω.(List A) → B =
|
||||
λ A B z f xs ⇒
|
||||
foldrω A (ω.B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z
|
||||
|
||||
def mapω : 0.(A B : ★) → ω.(ω.A → B) → ω.(List A) → List B =
|
||||
λ A B f ⇒ foldrω A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys)
|
||||
|
||||
|
||||
def0 All : (A : ★) → (P : A → ★) → List A → ★ =
|
||||
λ A P xs ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps) (up A xs)
|
||||
|
||||
def append : 0.(A : ★) → List A → List A → List A =
|
||||
λ A xs ys ⇒ foldr A (List A) ys (Cons A) xs
|
||||
|
||||
def reverse : 0.(A : ★) → List A → List A =
|
||||
λ A ⇒ foldl A (List A) (Nil A) (λ xs x ⇒ Cons A x xs)
|
||||
|
||||
|
||||
def find : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → Maybe A =
|
||||
λ A p ⇒
|
||||
foldlω A (Maybe A) (Nothing A) (λ m x ⇒ maybe.or A m (maybe.check A p x))
|
||||
|
||||
def cons-first : 0.(A : ★) → ω.A → List (List A) → List (List A) =
|
||||
λ A x ⇒
|
||||
match (List A) (List (List A))
|
||||
(single (List A) (single A x))
|
||||
(λ xs xss ⇒ Cons (List A) (Cons A x xs) xss)
|
||||
|
||||
def split : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List (List A) =
|
||||
λ A p ⇒
|
||||
foldrω A (List (List A))
|
||||
(Nil (List A))
|
||||
(λ x xss ⇒ bool.if (List (List A)) (p x)
|
||||
(Cons (List A) (Nil A) xss)
|
||||
(cons-first A x xss))
|
||||
|
||||
def break : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List A × List A =
|
||||
λ A p xs ⇒
|
||||
let0 Lst = List A; Lst2 = (Lst × Lst) ∷ ★; State = Either Lst Lst2 in
|
||||
letω LeftS = Left Lst Lst2; RightS = Right Lst Lst2 in
|
||||
letω res =
|
||||
foldlω A State
|
||||
(LeftS (Nil A))
|
||||
(λ acc x ⇒
|
||||
either.foldω Lst Lst2 State
|
||||
(λ xs ⇒ bool.if State (p x)
|
||||
(RightS (xs, list.single A x))
|
||||
(LeftS (Cons A x xs)))
|
||||
(λ xsys ⇒
|
||||
RightS (fst xsys, Cons A x (snd xsys))) acc)
|
||||
xs ∷ State in
|
||||
letω res =
|
||||
either.fold Lst Lst2 Lst2 (λ xs ⇒ (Nil A, xs)) (λ xsys ⇒ xsys) res in
|
||||
(reverse A (fst res), reverse A (snd res))
|
||||
|
||||
def uncons : 0.(A : ★) → List A → Maybe (A × List A) =
|
||||
λ A ⇒
|
||||
match A (Maybe (A × List A))
|
||||
(Nothing (A × List A))
|
||||
(λ x xs ⇒ Just (A × List A) (x, xs))
|
||||
|
||||
def head : 0.(A : ★) → ω.(List A) → Maybe A =
|
||||
λ A ⇒ matchω A (Maybe A) (Nothing A) (λ x _ ⇒ Just A x)
|
||||
|
||||
def tail : 0.(A : ★) → ω.(List A) → Maybe (List A) =
|
||||
λ A ⇒ matchω A (Maybe (List A)) (Nothing (List A)) (λ _ xs ⇒ Just (List A) xs)
|
||||
|
||||
def tail-or-nil : 0.(A : ★) → ω.(List A) → List A =
|
||||
λ A ⇒ matchω A (List A) (Nil A) (λ _ xs ⇒ xs)
|
||||
|
||||
-- slip (xs, []) = (xs, [])
|
||||
-- slip (xs, y :: ys) = (y :: xs, ys)
|
||||
def slip : 0.(A : ★) → List A × List A → List A × List A =
|
||||
λ A xsys ⇒
|
||||
case xsys return List A × List A of { (xs, ys) ⇒
|
||||
match A (List A → List A × List A)
|
||||
(λ xs ⇒ (xs, Nil A))
|
||||
(λ y ys xs ⇒ (Cons A y xs, ys))
|
||||
ys xs
|
||||
}
|
||||
|
||||
def split-at' : 0.(A : ★) → ℕ → List A → List A × List A =
|
||||
λ A n xs ⇒
|
||||
(case n return List A × List A → List A × List A of {
|
||||
0 ⇒ λ xsys ⇒ xsys;
|
||||
succ _, f ⇒ λ xsys ⇒ f (slip A xsys)
|
||||
}) (Nil A, xs)
|
||||
|
||||
def split-at : 0.(A : ★) → ℕ → List A → List A × List A =
|
||||
λ A n xs ⇒
|
||||
case split-at' A n xs return List A × List A of {
|
||||
(xs', ys) ⇒ (reverse A xs', ys)
|
||||
}
|
||||
|
||||
def filter : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List A =
|
||||
λ A p ⇒
|
||||
foldrω A (List A)
|
||||
(Nil A)
|
||||
(λ x xs ⇒ bool.if (List A) (p x) (Cons A x xs) xs)
|
||||
|
||||
def length : 0.(A : ★) → ω.(List A) → ℕ =
|
||||
λ A xs ⇒ fst xs
|
||||
|
||||
|
||||
namespace zip-with {
|
||||
def0 VFailure = vec.zip-with.Failure
|
||||
def0 VSuccess = vec.zip-with.Success
|
||||
|
||||
def0 Failure : (A B : ★) → List A → List B → ★ =
|
||||
λ A B xs ys ⇒ VFailure A B (fst xs) (fst ys) (snd xs) (snd ys)
|
||||
|
||||
def0 Result : (A B C : ★) → List A → List B → ★ =
|
||||
λ A B C xs ys ⇒ Either (Failure A B xs ys) (List C)
|
||||
|
||||
def zip-with : 0.(A B C : ★) → ω.(A → B → C) →
|
||||
(xs : List A) → (ys : List B) →
|
||||
Result A B C xs ys =
|
||||
λ A B C f xs ys ⇒
|
||||
let0 Ret = Result A B C in
|
||||
as-vec A (λ xs' ⇒ Ret xs' ys) xs (λ m xs ⇒
|
||||
as-vec B (λ ys' ⇒ Ret (m, xs) ys') ys (λ n ys ⇒
|
||||
let0 Err = Failure A B (m, xs) (n, ys) in
|
||||
either.fold Err (VSuccess C m n) (Ret (m, xs) (n, ys))
|
||||
(λ no ⇒ Left Err (List C) no)
|
||||
(λ yes ⇒ case yes return Ret (m, xs) (n, ys) of { (vec, prf) ⇒
|
||||
Right Err (List C) (drop0 (m ≡ n : ℕ) (List C) prf (n, vec))
|
||||
})
|
||||
(vec.zip-with-hetω A B C f m n xs ys)))
|
||||
}
|
||||
def0 ZipWith = zip-with.Result
|
||||
def zip-with = zip-with.zip-with
|
||||
|
||||
def zip-withω : 0.(A B C : ★) → ω.(ω.A → ω.B → C) →
|
||||
ω.(xs : List A) → ω.(ys : List B) →
|
||||
Either [0. Not (fst xs ≡ fst ys : ℕ)] (List C) =
|
||||
λ A B C f xs ys ⇒
|
||||
letω m = fst xs; xs = snd xs;
|
||||
n = fst ys; ys = snd ys in
|
||||
let0 Err : ★ = [0. Not (m ≡ n : ℕ)] in
|
||||
dec.elim (m ≡ n : ℕ) (λ _ ⇒ Either Err (List C))
|
||||
(λ mn ⇒
|
||||
letω xs = coe (𝑖 ⇒ Vec (mn @𝑖) A) xs in
|
||||
Right Err (List C) (n, vec.zip-withω A B C f n xs ys))
|
||||
(λ nmn ⇒ Left Err (List C) [nmn])
|
||||
(nat.eq? m n)
|
||||
def zip-with# = zip-withω
|
||||
|
||||
|
||||
def zip-with-uneven :
|
||||
0.(A B C : ★) → ω.(ω.A → ω.B → C) → ω.(List A) → ω.(List B) → List C =
|
||||
λ A B C f xs ys ⇒
|
||||
caseω nat.min (fst xs) (fst ys)
|
||||
return ω.(List A) → ω.(List B) → List C of {
|
||||
0 ⇒ λ _ _ ⇒ Nil C;
|
||||
succ _, ω.fih ⇒ λ xs ys ⇒
|
||||
maybe.foldω (A × List A) (List C) (Nil C)
|
||||
(λ xxs ⇒ maybe.foldω (B × List B) (List C) (Nil C)
|
||||
(λ yys ⇒ Cons C (f (fst xxs) (fst yys)) (fih (snd xxs) (snd yys)))
|
||||
(list.uncons B ys))
|
||||
(list.uncons A xs)
|
||||
} xs ys
|
||||
|
||||
|
||||
def sum : List ℕ → ℕ = foldl ℕ ℕ 0 nat.plus
|
||||
def product : List ℕ → ℕ = foldl ℕ ℕ 1 nat.times
|
||||
|
||||
|
||||
namespace mergesort {
|
||||
def deal : 0.(A : ★) → List A → List A × List A =
|
||||
λ A ⇒
|
||||
let0 One = List A; Pair : ★ = One × One in
|
||||
foldl A Pair (Nil A, Nil A)
|
||||
(pair.uncurry' One One (A → Pair) (λ ys zs x ⇒ (Cons A x zs, ys)))
|
||||
|
||||
}
|
||||
|
||||
|
||||
postulate0 SchemeList : ★ → ★
|
||||
|
||||
#[compile-scheme
|
||||
"(lambda (list) (cons (length list) (fold-right cons 'nil list)))"]
|
||||
postulate from-scheme : 0.(A : ★) → SchemeList A → List A
|
||||
|
||||
#[compile-scheme
|
||||
"(lambda (lst)
|
||||
(do [(lst (cdr lst) (cdr lst))
|
||||
(acc '() (cons (car lst) acc))]
|
||||
[(equal? lst 'nil) (reverse acc)]))"]
|
||||
postulate to-scheme : 0.(A : ★) → List A → SchemeList A
|
||||
|
||||
}
|
||||
|
||||
def0 List = list.List
|
||||
|
|
@ -0,0 +1,146 @@
|
|||
load "misc.quox"
|
||||
load "pair.quox"
|
||||
load "either.quox"
|
||||
|
||||
namespace maybe {
|
||||
|
||||
def0 Tag : ★ = {nothing, just}
|
||||
|
||||
def0 Payload : Tag → ★ → ★ =
|
||||
λ tag A ⇒ case tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
|
||||
|
||||
def0 Maybe : ★ → ★ =
|
||||
λ A ⇒ (t : Tag) × Payload t A
|
||||
|
||||
def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
|
||||
λ _ x ⇒ caseω x return Tag of { (tag, _) ⇒ tag }
|
||||
|
||||
def Nothing : 0.(A : ★) → Maybe A =
|
||||
λ _ ⇒ ('nothing, 'true)
|
||||
|
||||
def Just : 0.(A : ★) → A → Maybe A =
|
||||
λ _ x ⇒ ('just, x)
|
||||
|
||||
def0 IsJustTag : Tag → ★ =
|
||||
λ t ⇒ case t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
|
||||
|
||||
def0 IsJust : (A : ★) → Maybe A → ★ =
|
||||
λ A x ⇒ IsJustTag (tag A x)
|
||||
|
||||
def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
|
||||
λ A x ⇒
|
||||
caseω tag A x return t ⇒ Dec (IsJustTag t) of {
|
||||
'just ⇒ Yes True 'true;
|
||||
'nothing ⇒ No False (λ x ⇒ x)
|
||||
}
|
||||
|
||||
def0 nothing-unique :
|
||||
(A : ★) → (x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
|
||||
λ A x ⇒
|
||||
case x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
|
||||
'true ⇒ δ _ ⇒ ('nothing, 'true)
|
||||
}
|
||||
|
||||
def elim' :
|
||||
0.(A : ★) →
|
||||
0.(P : (t : Tag) → Payload t A → ★) →
|
||||
ω.(P 'nothing 'true) →
|
||||
ω.((x : A) → P 'just x) →
|
||||
(t : Tag) → (x : Payload t A) → P t x =
|
||||
λ A P nothing just tag ⇒
|
||||
case tag return t ⇒ (x : Payload t A) → P t x of {
|
||||
'nothing ⇒ λ x ⇒ case x return x' ⇒ P 'nothing x' of { 'true ⇒ nothing };
|
||||
'just ⇒ just
|
||||
}
|
||||
|
||||
def elim :
|
||||
0.(A : ★) →
|
||||
0.(P : Maybe A → ★) →
|
||||
ω.(P (Nothing A)) →
|
||||
ω.((x : A) → P (Just A x)) →
|
||||
(x : Maybe A) → P x =
|
||||
λ A P n j x ⇒
|
||||
case x return x' ⇒ P x' of {
|
||||
(tag, payload) ⇒ elim' A (λ x t ⇒ P (x, t)) n j tag payload
|
||||
}
|
||||
|
||||
def elimω' :
|
||||
0.(A : ★) →
|
||||
0.(P : (t : Tag) → Payload t A → ★) →
|
||||
ω.(P 'nothing 'true) →
|
||||
ω.(ω.(x : A) → P 'just x) →
|
||||
ω.(t : Tag) → ω.(x : Payload t A) → P t x =
|
||||
λ A P nothing just tag ⇒
|
||||
case tag return t ⇒ ω.(x : Payload t A) → P t x of {
|
||||
'nothing ⇒ λ x ⇒ case x return x' ⇒ P 'nothing x' of { 'true ⇒ nothing };
|
||||
'just ⇒ just
|
||||
}
|
||||
|
||||
def elimω :
|
||||
0.(A : ★) →
|
||||
0.(P : Maybe A → ★) →
|
||||
ω.(P (Nothing A)) →
|
||||
ω.(ω.(x : A) → P (Just A x)) →
|
||||
ω.(x : Maybe A) → P x =
|
||||
λ A P n j x ⇒
|
||||
caseω x return x' ⇒ P x' of {
|
||||
(tag, payload) ⇒ elimω' A (λ x t ⇒ P (x, t)) n j tag payload
|
||||
}
|
||||
|
||||
{-
|
||||
-- direct elim implementation
|
||||
def elim :
|
||||
0.(A : ★) →
|
||||
0.(P : Maybe A → ★) →
|
||||
ω.(P (Nothing A)) →
|
||||
ω.((x : A) → P (Just A x)) →
|
||||
(x : Maybe A) → P x =
|
||||
λ A P n j x ⇒
|
||||
case x return x' ⇒ P x' of { (tag, payload) ⇒
|
||||
(case tag
|
||||
return t ⇒
|
||||
0.(eq : tag ≡ t : Tag) → P (t, coe (𝑖 ⇒ Payload (eq @𝑖) A) payload)
|
||||
of {
|
||||
'nothing ⇒
|
||||
λ eq ⇒
|
||||
case coe (𝑖 ⇒ Payload (eq @𝑖) A) payload
|
||||
return p ⇒ P ('nothing, p)
|
||||
of { 'true ⇒ n };
|
||||
'just ⇒ λ eq ⇒ j (coe (𝑖 ⇒ Payload (eq @𝑖) A) payload)
|
||||
}) (δ 𝑖 ⇒ tag)
|
||||
}
|
||||
-}
|
||||
|
||||
def fold : 0.(A B : ★) → ω.B → ω.(A → B) → Maybe A → B =
|
||||
λ A B ⇒ elim A (λ _ ⇒ B)
|
||||
|
||||
def foldω : 0.(A B : ★) → ω.B → ω.(ω.A → B) → ω.(Maybe A) → B =
|
||||
λ A B ⇒ elimω A (λ _ ⇒ B)
|
||||
|
||||
def join : 0.(A : ★) → (Maybe (Maybe A)) → Maybe A =
|
||||
λ A ⇒ fold (Maybe A) (Maybe A) (Nothing A) (λ x ⇒ x)
|
||||
|
||||
def pair : 0.(A B : ★) → ω.(Maybe A) → ω.(Maybe B) → Maybe (A × B) =
|
||||
λ A B x y ⇒
|
||||
foldω A (Maybe (A × B)) (Nothing (A × B))
|
||||
(λ x' ⇒ fold B (Maybe (A × B)) (Nothing (A × B))
|
||||
(λ y' ⇒ Just (A × B) (x', y')) y) x
|
||||
|
||||
def map : 0.(A B : ★) → ω.(A → B) → Maybe A → Maybe B =
|
||||
λ A B f ⇒ fold A (Maybe B) (Nothing B) (λ x ⇒ Just B (f x))
|
||||
|
||||
def mapω : 0.(A B : ★) → ω.(ω.A → B) → ω.(Maybe A) → Maybe B =
|
||||
λ A B f ⇒ foldω A (Maybe B) (Nothing B) (λ x ⇒ Just B (f x))
|
||||
|
||||
|
||||
def check : 0.(A : ★) → (ω.A → Bool) → ω.A → Maybe A =
|
||||
λ A p x ⇒ bool.if (Maybe A) (p x) (Just A x) (Nothing A)
|
||||
|
||||
def or : 0.(A : ★) → Maybe A → ω.(Maybe A) → Maybe A =
|
||||
λ A l r ⇒ fold A (Maybe A) r (Just A) l
|
||||
|
||||
}
|
||||
|
||||
def0 Maybe = maybe.Maybe
|
||||
def Just = maybe.Just
|
||||
def Nothing = maybe.Nothing
|
||||
|
|
@ -0,0 +1,261 @@
|
|||
namespace true {
|
||||
def0 True : ★ = {true}
|
||||
|
||||
def drop : 0.(A : ★) → True → A → A =
|
||||
λ A t x ⇒ case t return A of { 'true ⇒ x }
|
||||
|
||||
def0 eta : (s : True) → s ≡ 'true : True =
|
||||
λ s ⇒ case s return s' ⇒ s' ≡ 'true : True of { 'true ⇒ δ 𝑖 ⇒ 'true }
|
||||
|
||||
def0 irr : (s t : True) → s ≡ t : True =
|
||||
λ s t ⇒
|
||||
coe (𝑖 ⇒ eta s @𝑖 ≡ t : True) @1 @0
|
||||
(coe (𝑖 ⇒ 'true ≡ eta t @𝑖 : True) @1 @0 (δ _ ⇒ 'true))
|
||||
|
||||
def revive : 0.True → True = λ _ ⇒ 'true
|
||||
}
|
||||
def0 True = true.True
|
||||
|
||||
namespace false {
|
||||
def0 False : ★ = {}
|
||||
|
||||
def void : 0.(A : ★) → 0.False → A =
|
||||
λ A v ⇒ case0 v return A of { }
|
||||
|
||||
def0 irr : (u v : False) → u ≡ v : False =
|
||||
λ u v ⇒ void (u ≡ v : False) u
|
||||
|
||||
def revive : 0.False → False = void False
|
||||
}
|
||||
def0 False = false.False
|
||||
def void = false.void
|
||||
|
||||
|
||||
def0 Not : ★ → ★ = λ A ⇒ ω.A → False
|
||||
|
||||
def0 Iff : ★ → ★ → ★ = λ A B ⇒ (A → B) × (B → A)
|
||||
|
||||
def0 All : (A : ★) → (A → ★) → ★ =
|
||||
λ A P ⇒ (x : A) → P x
|
||||
|
||||
def cong :
|
||||
0.(A : ★) → 0.(P : A → ★) → 1.(p : All A P) →
|
||||
0.(x y : A) → 1.(xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
|
||||
λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
|
||||
|
||||
def cong' :
|
||||
0.(A B : ★) → 1.(f : A → B) →
|
||||
0.(x y : A) → 1.(xy : x ≡ y : A) → f x ≡ f y : B =
|
||||
λ A B ⇒ cong A (λ _ ⇒ B)
|
||||
|
||||
def coherence :
|
||||
0.(A B : ★) → 0.(AB : A ≡ B : ★) → 1.(x : A) →
|
||||
Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) =
|
||||
λ A B AB x ⇒
|
||||
δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x
|
||||
|
||||
|
||||
def0 EqF : (A : ★) → (P : A → ★) → (p : All A P) → (q : All A P) → A → ★ =
|
||||
λ A P p q x ⇒ p x ≡ q x : P x
|
||||
|
||||
def funext :
|
||||
0.(A : ★) → 0.(P : A → ★) → 0.(p q : All A P) →
|
||||
1.(All A (EqF A P p q)) → p ≡ q : All A P =
|
||||
λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖
|
||||
|
||||
def refl : 0.(A : ★) → 1.(x : A) → x ≡ x : A = λ A x ⇒ δ _ ⇒ x
|
||||
|
||||
def sym : 0.(A : ★) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
|
||||
λ A x y eq ⇒ coe (𝑗 ⇒ eq @𝑗 ≡ x : A) (δ _ ⇒ eq @0)
|
||||
-- btw this uses eq @0 instead of just x because of the quantities
|
||||
|
||||
def sym-c : 0.(A : ★) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
|
||||
λ A x y eq ⇒ δ 𝑖 ⇒
|
||||
comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }
|
||||
|
||||
{-
|
||||
def sym-het : 0.(A B : ★) → 0.(AB : A ≡ B : ★) →
|
||||
0.(x : A) → 0.(y : B) →
|
||||
1.(Eq (𝑖 ⇒ AB @𝑖) x y) →
|
||||
Eq (𝑖 ⇒ sym¹ ★ A B AB @𝑖) y x =
|
||||
λ A B AB x y xy ⇒
|
||||
let0 BA = sym¹ ★ A B AB;
|
||||
y' : A = coe (𝑖 ⇒ BA @𝑖) y;
|
||||
yy' : Eq (𝑖 ⇒ BA @𝑖) y y' =
|
||||
δ 𝑗 ⇒ coe (𝑖 ⇒ BA @𝑖) @0 @𝑗 y;
|
||||
in
|
||||
0
|
||||
-}
|
||||
|
||||
{-
|
||||
δ 𝑖 ⇒
|
||||
comp (𝑗 ⇒ sym¹ ★ A B AB @𝑗) @0 @𝑖 y @𝑖 {
|
||||
0 𝑗 ⇒ xy @𝑗;
|
||||
1 𝑗 ⇒ xy @𝑗
|
||||
}
|
||||
-}
|
||||
|
||||
def trans10 : 0.(A : ★) → 0.(x y z : A) →
|
||||
1.(x ≡ y : A) → 0.(y ≡ z : A) → x ≡ z : A =
|
||||
λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ x ≡ eq2 @𝑗 : A) eq1
|
||||
|
||||
def trans01 : 0.(A : ★) → 0.(x y z : A) →
|
||||
0.(x ≡ y : A) → 1.(y ≡ z : A) → x ≡ z : A =
|
||||
λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ eq1 @𝑗 ≡ z : A) @1 @0 eq2
|
||||
|
||||
def trans : 0.(A : ★) → 0.(x y z : A) →
|
||||
ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
|
||||
λ A x y z eq1 eq2 ⇒ trans01 A x y z eq1 eq2
|
||||
|
||||
{-
|
||||
def trans-het : 0.(A B C : ★) → 0.(AB : A ≡ B : ★) → 0.(BC : B ≡ C : ★) →
|
||||
0.(x : A) → 0.(y : B) → 0.(z : C) →
|
||||
ω.(Eq (𝑖 ⇒ AB @𝑖) x y) →
|
||||
ω.(Eq (𝑖 ⇒ BC @𝑖) y z) →
|
||||
Eq (𝑖 ⇒ trans¹ ★ A B C AB BC @𝑖) x z
|
||||
=
|
||||
λ A B C AB BC x y z xy yz ⇒
|
||||
let 0.AC = trans¹ ★ A B C AB BC;
|
||||
0.y' : A = coe (𝑗 ⇒ AB @𝑗) @1 @0 y;
|
||||
in
|
||||
δ 𝑖 ⇒
|
||||
trans (AC @𝑖) (coe (𝑗 ⇒ AC @𝑗) @0 @𝑖 x)
|
||||
(coe (𝑗 ⇒ AC @𝑗) @0 @𝑖 y')
|
||||
(coe (𝑗 ⇒ AC @𝑗) @1 @𝑖 z)
|
||||
0
|
||||
0
|
||||
@𝑖
|
||||
|
||||
def0 trans-trans-het :
|
||||
(A : ★) → (x y z : A) →
|
||||
(xy : x ≡ y : A) → (yz : y ≡ z : A) →
|
||||
Eq (_ ⇒ x ≡ z : A)
|
||||
(trans A x y z xy yz)
|
||||
(trans-het A A A (δ _ ⇒ A) (δ _ ⇒ A) x y z xy yz) =
|
||||
λ A x y z xy yz ⇒ δ _ ⇒ trans A x y z xy yz
|
||||
-}
|
||||
|
||||
def appω : 0.(A B : ★) → ω.(f : ω.A → B) → [ω.A] → [ω.B] =
|
||||
λ A B f x ⇒ case x return [ω.B] of { [x'] ⇒ [f x'] }
|
||||
def app# = appω
|
||||
|
||||
def app2ω : 0.(A B C : ★) → ω.(f : ω.A → ω.B → C) → [ω.A] → [ω.B] → [ω.C] =
|
||||
λ A B C f x y ⇒
|
||||
case x return [ω.C] of { [x'] ⇒
|
||||
case y return [ω.C] of { [y'] ⇒ [f x' y'] }
|
||||
}
|
||||
def app2# = app2ω
|
||||
|
||||
def getω : 0.(A : ★) → [ω.A] → A =
|
||||
λ A x ⇒ case x return A of { [x] ⇒ x }
|
||||
def get# = getω
|
||||
|
||||
def0 get0 : (A : ★) → [0.A] → A =
|
||||
λ A x ⇒ case x return A of { [x] ⇒ x }
|
||||
|
||||
def0 get0-box : (A : ★) → (b : [0.A]) →
|
||||
[get0 A b] ≡ b : [0.A] =
|
||||
λ A b ⇒ case b return b' ⇒ [get0 A b'] ≡ b' : [0.A] of { [x] ⇒ δ _ ⇒ [x] }
|
||||
|
||||
def drop0 : 0.(A B : ★) → [0.A] → B → B =
|
||||
λ A B x y ⇒ case x return B of { [_] ⇒ y }
|
||||
|
||||
def0 drop0-eq : (A B : ★) → (x : [0.A]) → (y : B) → drop0 A B x y ≡ y : B =
|
||||
λ A B x y ⇒
|
||||
case x return x' ⇒ drop0 A B x' y ≡ y : B of { [_] ⇒ δ 𝑖 ⇒ y }
|
||||
|
||||
def0 HEq : (A B : ★) → A → B → ★¹ =
|
||||
λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y
|
||||
|
||||
def0 boxω-inj : (A : ★) → (x y : A) → [x] ≡ [y] : [ω.A] → x ≡ y : A =
|
||||
λ A x y xy ⇒ δ 𝑖 ⇒ getω A (xy @𝑖)
|
||||
-- [todo] change lexical syntax to allow "box#-inj"
|
||||
|
||||
def revive0 : 0.(A : ★) → 0.[0.A] → [0.A] =
|
||||
λ A s ⇒ [get0 A s]
|
||||
|
||||
|
||||
namespace sing {
|
||||
|
||||
def0 Sing : (A : ★) → A → ★ =
|
||||
λ A x ⇒ (val : A) × [0. val ≡ x : A]
|
||||
|
||||
def sing : 0.(A : ★) → (x : A) → Sing A x =
|
||||
λ A x ⇒ (x, [δ _ ⇒ x])
|
||||
|
||||
def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
|
||||
λ A x sg ⇒
|
||||
case sg return A of { (x', eq) ⇒ drop0 (x' ≡ x : A) A eq x' }
|
||||
|
||||
def0 val-fst : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ fst sg : A =
|
||||
λ A x sg ⇒ drop0-eq (fst sg ≡ x : A) A (snd sg) (fst sg)
|
||||
|
||||
def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
|
||||
λ A x sg ⇒
|
||||
trans A (val A x sg) (fst sg) x
|
||||
(val-fst A x sg) (get0 (fst sg ≡ x : A) (snd sg))
|
||||
|
||||
def app : 0.(A B : ★) → 0.(x : A) →
|
||||
(f : A → B) → Sing A x → Sing B (f x) =
|
||||
λ A B x f sg ⇒
|
||||
let 1.x' = val A x sg;
|
||||
0.xx = proof A x sg in
|
||||
(f x', [δ 𝑖 ⇒ f (xx @𝑖)])
|
||||
|
||||
}
|
||||
|
||||
def0 Sing = sing.Sing
|
||||
def sing = sing.sing
|
||||
|
||||
|
||||
namespace dup {
|
||||
|
||||
def0 Dup : (A : ★) → A → ★ =
|
||||
λ A x ⇒ Sing [ω.A] [x]
|
||||
|
||||
def from-parts :
|
||||
0.(A : ★) →
|
||||
(dup : A → [ω.A]) →
|
||||
0.(prf : (x : A) → dup x ≡ [x] : [ω.A]) →
|
||||
(x : A) → Dup A x =
|
||||
λ A dup prf x ⇒ (dup x, [prf x])
|
||||
|
||||
def to-drop : 0.(A : ★) → (A → [ω.A]) → 0.(B : ★) → A → B → B =
|
||||
λ A dup B x y ⇒ case dup x return B of { [_] ⇒ y }
|
||||
|
||||
def erased : 0.(A : ★) → (x : [0.A]) → Dup [0.A] x =
|
||||
λ A x ⇒ case x return x' ⇒ Dup [0.A] x' of { [x] ⇒ sing [ω.[0.A]] [[x]] }
|
||||
|
||||
def valω : 0.(A : ★) → 0.(x : A) → Dup A x → [ω.A] =
|
||||
λ A x ⇒ sing.val [ω.A] [x]
|
||||
def val# = valω
|
||||
|
||||
def val : 0.(A : ★) → 0.(x : A) → Dup A x → A =
|
||||
λ A x x! ⇒ getω A (valω A x x!)
|
||||
|
||||
def0 proofω : (A : ★) → (x : A) → (x! : Dup A x) → valω A x x! ≡ [x] : [ω.A] =
|
||||
λ A x x! ⇒ sing.proof [ω.A] [x] x!
|
||||
def0 proof# : (A : ★) → (x : A) → (x! : Dup A x) → val# A x x! ≡ [x] : [ω.A] =
|
||||
proofω
|
||||
|
||||
def0 proof : (A : ★) → (x : A) → (x! : Dup A x) → val A x x! ≡ x : A =
|
||||
λ A x x! ⇒ δ 𝑖 ⇒ getω A (proofω A x x! @𝑖)
|
||||
|
||||
def elim' : 0.(A : ★) → 0.(x : A) → 0.(P : A → ★) →
|
||||
(ω.(x' : A) → 0.(x' ≡ x : A) → P x) → Dup A x → P x =
|
||||
λ A x P f x! ⇒
|
||||
let xω : [ω.A] = sing.val [ω.A] [x] x! in
|
||||
case xω return xω' ⇒ 0.(xω' ≡ xω : [ω.A]) → P x of { [x'] ⇒ λ eq1 ⇒
|
||||
let0 eq2 = sing.proof [ω.A] [x] x!;
|
||||
eq = boxω-inj A x' x (trans [ω.A] [x'] xω [x] eq1 eq2) in
|
||||
f x' eq
|
||||
} (δ _ ⇒ xω)
|
||||
|
||||
def elim : 0.(A : ★) → 0.(x : A) → 0.(P : A → ★) →
|
||||
(ω.(x' : A) → P x') → Dup A x → P x =
|
||||
λ A x P f ⇒ elim' A x P (λ x' xx ⇒ coe (𝑖 ⇒ P (xx @𝑖)) (f x'))
|
||||
|
||||
|
||||
}
|
||||
|
||||
def0 Dup = dup.Dup
|
||||
|
|
@ -0,0 +1,297 @@
|
|||
load "misc.quox"
|
||||
load "bool.quox"
|
||||
load "either.quox"
|
||||
load "sub.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')
|
||||
}
|
||||
}
|
||||
|
||||
def elim-pairω :
|
||||
0.(P : ℕ → ℕ → ★) →
|
||||
ω.(P 0 0) →
|
||||
ω.(ω.(n : ℕ) → ω.(P 0 n) → P 0 (succ n)) →
|
||||
ω.(ω.(m : ℕ) → ω.(P m 0) → P (succ m) 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')
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
def succ-boxω : [ω.ℕ] → [ω.ℕ] =
|
||||
λ n ⇒ case n return [ω.ℕ] of { [n] ⇒ [succ n] }
|
||||
|
||||
#[compile-scheme "(lambda (n) n)"]
|
||||
def dup : ℕ → [ω.ℕ] =
|
||||
λ n ⇒ case n return [ω.ℕ] of {
|
||||
0 ⇒ [0];
|
||||
succ _, n! ⇒ succ-boxω n!
|
||||
}
|
||||
|
||||
def0 dup-ok : (n : ℕ) → dup n ≡ [n] : [ω.ℕ] =
|
||||
λ n ⇒
|
||||
case n return n' ⇒ dup n' ≡ [n'] : [ω.ℕ] of {
|
||||
0 ⇒ δ 𝑖 ⇒ [0];
|
||||
succ _, ih ⇒ δ 𝑖 ⇒ succ-boxω (ih @𝑖)
|
||||
}
|
||||
|
||||
def dup! : (n : ℕ) → Dup ℕ n =
|
||||
dup.from-parts ℕ dup dup-ok
|
||||
|
||||
|
||||
def drop : 0.(A : ★) → ℕ → A → A =
|
||||
dup.to-drop ℕ dup
|
||||
|
||||
|
||||
def natopω' : 0.(A : ★) → ω.(ω.ℕ → ω.ℕ → A) → ℕ → ℕ → A =
|
||||
λ A f m n ⇒
|
||||
getω A (app2ω ℕ ℕ A f (dup m) (dup n))
|
||||
|
||||
def natopω = natopω' ℕ
|
||||
|
||||
#[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 = natopω timesω
|
||||
|
||||
def pred : ℕ → ℕ = λ n ⇒ case n return ℕ of { zero ⇒ zero; succ n ⇒ n }
|
||||
|
||||
def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
|
||||
λ n ⇒ δ 𝑖 ⇒ n
|
||||
|
||||
def succ-inj : 0.(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
|
||||
|
||||
|
||||
def minω : ω.ℕ → ω.ℕ → ℕ =
|
||||
elim-pairω (λ _ _ ⇒ ℕ) 0 (λ _ _ ⇒ 0) (λ _ _ ⇒ 0) (λ _ _ x ⇒ succ x)
|
||||
|
||||
def min = natopω minω
|
||||
|
||||
|
||||
def0 IsSucc : ℕ → ★ =
|
||||
λ n ⇒ case n return ★ of { zero ⇒ False; succ _ ⇒ True }
|
||||
|
||||
def is-succ? : ω.(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)
|
||||
}
|
||||
|
||||
|
||||
def0 IsSuccOf : ℕ → ℕ → ★ =
|
||||
λ n p ⇒ n ≡ succ p : ℕ
|
||||
|
||||
def0 PredOf : ℕ → ★ =
|
||||
λ n ⇒ Sub ℕ (IsSuccOf n)
|
||||
|
||||
def0 no-pred0 : Not (PredOf 0) =
|
||||
λ p ⇒
|
||||
case p return False of { (p, lt) ⇒
|
||||
zero-not-succ p (get0 (0 ≡ succ p : ℕ) lt)
|
||||
}
|
||||
|
||||
def pred? : (n : ℕ) → DecT (PredOf n) =
|
||||
λ n ⇒
|
||||
case n return n' ⇒ DecT (PredOf n') of {
|
||||
zero ⇒ NoT (PredOf zero) no-pred0;
|
||||
succ n ⇒ YesT (PredOf (succ n)) (n, [δ _ ⇒ succ n])
|
||||
}
|
||||
|
||||
namespace pred-of {
|
||||
|
||||
def revive : (n : ℕ) → 0.(PredOf n) → PredOf n =
|
||||
λ n hs ⇒
|
||||
let0 p = fst hs in
|
||||
case n return n' ⇒ 0.(n' ≡ succ p : ℕ) → PredOf n' of {
|
||||
zero ⇒ λ eq ⇒ void (PredOf zero) (zero-not-succ p eq);
|
||||
succ p' ⇒ λ _ ⇒ (p', [δ _ ⇒ succ p'])
|
||||
} (get0 (n ≡ succ p : ℕ) (snd hs))
|
||||
|
||||
def val : 0.(n : ℕ) → PredOf n → ℕ =
|
||||
λ n ⇒ sub.val ℕ (IsSuccOf n)
|
||||
|
||||
def0 proof : (n : ℕ) → (p : PredOf n) → n ≡ succ (fst p) : ℕ =
|
||||
λ n ⇒ sub.proof ℕ (IsSuccOf n)
|
||||
|
||||
}
|
||||
|
||||
|
||||
def divmodω : ω.ℕ → ω.ℕ → ℕ × ℕ =
|
||||
-- https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Init.Nat.html#divmod
|
||||
letω divmod' : ℕ → ω.ℕ → ℕ → ℕ → ℕ × ℕ =
|
||||
λ x ⇒
|
||||
case x return ω.ℕ → ℕ → ℕ → ℕ × ℕ of {
|
||||
0 ⇒ λ y q u ⇒ (q, u);
|
||||
succ _, f' ⇒ λ y q u ⇒
|
||||
case u return ℕ × ℕ of {
|
||||
0 ⇒ f' y (succ q) y;
|
||||
succ u' ⇒ f' y q u'
|
||||
}
|
||||
} in
|
||||
λ x y ⇒
|
||||
caseω y return ℕ × ℕ of {
|
||||
0 ⇒ (0, 0);
|
||||
succ y' ⇒
|
||||
case divmod' x y' 0 y' return ℕ × ℕ of { (d, m) ⇒ (d, minus y' m) }
|
||||
}
|
||||
|
||||
def divmod = natopω' (ℕ × ℕ) divmodω
|
||||
|
||||
def divω : ω.ℕ → ω.ℕ → ℕ = λ x y ⇒ fst (divmodω x y)
|
||||
def div = natopω divω
|
||||
|
||||
def modω : ω.ℕ → ω.ℕ → ℕ = λ x y ⇒ snd (divmodω x y)
|
||||
def mod = natopω modω
|
||||
|
||||
|
||||
#[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"]
|
||||
def eq? : DecEq ℕ =
|
||||
λ m n ⇒
|
||||
elim-pair (λ m n ⇒ Dec (m ≡ n : ℕ))
|
||||
(Yes (0 ≡ 0 : ℕ) (δ 𝑖 ⇒ 0))
|
||||
(λ n p ⇒
|
||||
dec.drop (0 ≡ n : ℕ) (Dec (0 ≡ succ n : ℕ)) p
|
||||
(No (0 ≡ succ n : ℕ) (λ zs ⇒ zero-not-succ n zs)))
|
||||
(λ m p ⇒
|
||||
dec.drop (m ≡ 0 : ℕ) (Dec (succ m ≡ 0 : ℕ)) p
|
||||
(No (succ m ≡ 0 : ℕ) (λ sz ⇒ succ-not-zero m sz)))
|
||||
(λ m n ⇒
|
||||
dec.elim (m ≡ n : ℕ) (λ _ ⇒ Dec (succ m ≡ succ n : ℕ))
|
||||
(λ yy ⇒ Yes (succ m ≡ succ n : ℕ) (δ 𝑖 ⇒ succ (yy @𝑖)))
|
||||
(λ nn ⇒ No (succ m ≡ succ n : ℕ) (λ yy ⇒ nn (succ-inj m n yy))))
|
||||
m n
|
||||
|
||||
|
||||
def0 Ordering : ★ = {lt, eq, gt}
|
||||
|
||||
namespace ordering {
|
||||
def from : 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 : 0.(A : ★) → Ordering → A → A =
|
||||
λ A o x ⇒ case o return A of { 'lt ⇒ x; 'eq ⇒ x; 'gt ⇒ x }
|
||||
|
||||
def eq : Ordering → Ordering → Bool =
|
||||
λ x y ⇒
|
||||
case x return Bool of {
|
||||
'lt ⇒ case y return Bool of { 'lt ⇒ 'true; 'eq ⇒ 'false; 'gt ⇒ 'false };
|
||||
'eq ⇒ case y return Bool of { 'lt ⇒ 'false; 'eq ⇒ 'true; 'gt ⇒ 'false };
|
||||
'gt ⇒ case y return Bool of { 'lt ⇒ 'false; 'eq ⇒ 'false; 'gt ⇒ 'true };
|
||||
}
|
||||
}
|
||||
|
||||
def compare : ℕ → ℕ → Ordering =
|
||||
elim-pair (λ _ _ ⇒ Ordering)
|
||||
'eq
|
||||
(λ _ o ⇒ ordering.drop Ordering o 'lt)
|
||||
(λ _ o ⇒ ordering.drop Ordering o 'gt)
|
||||
(λ _ _ x ⇒ x)
|
||||
|
||||
def lt : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ ordering.eq (compare m n) 'lt
|
||||
def eq : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ ordering.eq (compare m n) 'eq
|
||||
def gt : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ ordering.eq (compare m n) 'gt
|
||||
def ne : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ bool.not (eq m n)
|
||||
def le : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ bool.not (gt m n)
|
||||
def ge : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ bool.not (lt 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
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -0,0 +1,67 @@
|
|||
namespace pair {
|
||||
|
||||
def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x
|
||||
|
||||
def uncurry :
|
||||
0.(A : ★) → 0.(B : A → ★) → 0.(C : (x : A) → (B x) → ★) →
|
||||
(f : (x : A) → (y : B x) → C x y) →
|
||||
(p : Σ A B) → C (fst p) (snd p) =
|
||||
λ A B C f p ⇒
|
||||
case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y }
|
||||
|
||||
def uncurry' :
|
||||
0.(A B C : ★) → (A → B → C) → (A × B) → C =
|
||||
λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C)
|
||||
|
||||
def curry :
|
||||
0.(A : ★) → 0.(B : A → ★) → 0.(C : (Σ A B) → ★) →
|
||||
(f : (p : Σ A B) → C p) → (x : A) → (y : B x) → C (x, y) =
|
||||
λ A B C f x y ⇒ f (x, y)
|
||||
|
||||
def curry' :
|
||||
0.(A B C : ★) → (A × B → C) → A → B → C =
|
||||
λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C)
|
||||
|
||||
def0 fst-snd :
|
||||
(A : ★) → (B : A → ★) →
|
||||
(p : Σ A B) → p ≡ (fst p, snd p) : Σ A B =
|
||||
λ A B p ⇒ δ 𝑖 ⇒ p -- η
|
||||
|
||||
def0 fst-eq :
|
||||
(A : ★) → (B : A → ★) →
|
||||
(p q : Σ A B) → p ≡ q : Σ A B → fst p ≡ fst q : A =
|
||||
λ A B p q eq ⇒ δ 𝑖 ⇒ fst (eq @𝑖)
|
||||
|
||||
def0 snd-eq :
|
||||
(A : ★) → (B : A → ★) →
|
||||
(p q : Σ A B) → (eq : p ≡ q : Σ A B) →
|
||||
Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd p) (snd q) =
|
||||
λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖)
|
||||
|
||||
def0 pair-eq :
|
||||
(A : ★) → (B : A → ★) →
|
||||
(x0 x1 : A) → (y0 : B x0) → (y1 : B x1) →
|
||||
(xx : x0 ≡ x1 : A) → (yy : Eq (𝑖 ⇒ B (xx @𝑖)) y0 y1) →
|
||||
(x0, y0) ≡ (x1, y1) : ((x : A) × B x) =
|
||||
λ A B x0 x1 y0 y1 xx yy ⇒ δ 𝑖 ⇒ (xx @𝑖, yy @𝑖)
|
||||
|
||||
def map :
|
||||
0.(A A' : ★) →
|
||||
0.(B : A → ★) → 0.(B' : A' → ★) →
|
||||
(f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
|
||||
Σ A B → Σ A' B' =
|
||||
λ A A' B B' f g p ⇒
|
||||
case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) }
|
||||
|
||||
def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' =
|
||||
λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g)
|
||||
|
||||
def map-fst : 0.(A A' B : ★) → (A → A') → A × B → A' × B =
|
||||
λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x)
|
||||
|
||||
def map-snd : 0.(A B B' : ★) → (B → B') → A × B → A × B' =
|
||||
λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f
|
||||
|
||||
}
|
||||
|
||||
def0 Σ = pair.Σ
|
||||
|
|
@ -0,0 +1,156 @@
|
|||
load "misc.quox"
|
||||
|
||||
def0 Qty : ★ = {"zero", one, any}
|
||||
|
||||
def0 NzQty : ★ = {one, any}
|
||||
|
||||
def nz : NzQty → Qty =
|
||||
λ π ⇒ case π return Qty of { 'one ⇒ 'one; 'any ⇒ 'any }
|
||||
|
||||
def dup! : (π : Qty) → Dup Qty π =
|
||||
λ π ⇒ case π return π' ⇒ Dup Qty π' of {
|
||||
'zero ⇒ (['zero], [δ _ ⇒ ['zero]]);
|
||||
'one ⇒ (['one], [δ _ ⇒ ['one]]);
|
||||
'any ⇒ (['any], [δ _ ⇒ ['any]]);
|
||||
}
|
||||
|
||||
def dup : (π : Qty) → [ω.Qty] =
|
||||
λ π ⇒ dup.valω Qty π (dup! π)
|
||||
|
||||
def drop : 0.(A : ★) → Qty → A → A =
|
||||
λ A π x ⇒ case π return A of {
|
||||
'zero ⇒ x;
|
||||
'one ⇒ x;
|
||||
'any ⇒ x;
|
||||
}
|
||||
|
||||
def if-zero : 0.(A : ★) → Qty → ω.A → ω.A → A =
|
||||
λ A π z nz ⇒
|
||||
case π return A of { 'zero ⇒ z; 'one ⇒ nz; 'any ⇒ nz }
|
||||
|
||||
def plus : Qty → ω.Qty → Qty =
|
||||
λ π ρ ⇒
|
||||
case π return Qty of {
|
||||
'zero ⇒ ρ;
|
||||
'one ⇒ if-zero Qty ρ 'one 'any;
|
||||
'any ⇒ 'any;
|
||||
}
|
||||
|
||||
def times : Qty → ω.Qty → Qty =
|
||||
λ π ρ ⇒
|
||||
case π return Qty of {
|
||||
'zero ⇒ 'zero;
|
||||
'one ⇒ ρ;
|
||||
'any ⇒ if-zero Qty ρ 'zero 'any;
|
||||
}
|
||||
|
||||
def0 FUN : Qty → (A : ★) → (A → ★) → ★ =
|
||||
λ π A B ⇒
|
||||
case π return ★ of {
|
||||
'zero ⇒ 0.(x : A) → B x;
|
||||
'one ⇒ 1.(x : A) → B x;
|
||||
'any ⇒ ω.(x : A) → B x;
|
||||
}
|
||||
|
||||
def0 FUN-NZ : NzQty → (A : ★) → (A → ★) → ★ =
|
||||
λ π A B ⇒
|
||||
case π return ★ of {
|
||||
'one ⇒ 1.(x : A) → B x;
|
||||
'any ⇒ ω.(x : A) → B x;
|
||||
}
|
||||
|
||||
def0 Fun : Qty → ★ → ★ → ★ =
|
||||
λ π A B ⇒ FUN π A (λ _ ⇒ B)
|
||||
|
||||
def0 FunNz : NzQty → ★ → ★ → ★ =
|
||||
λ π A B ⇒ FUN-NZ π A (λ _ ⇒ B)
|
||||
|
||||
def0 Box : Qty → ★ → ★ =
|
||||
λ π A ⇒
|
||||
case π return ★ of {
|
||||
'zero ⇒ [0.A];
|
||||
'one ⇒ [1.A];
|
||||
'any ⇒ [ω.A];
|
||||
}
|
||||
|
||||
def0 BoxNz : NzQty → ★ → ★ =
|
||||
λ π A ⇒
|
||||
case π return ★ of {
|
||||
'one ⇒ [1.A];
|
||||
'any ⇒ [ω.A];
|
||||
}
|
||||
|
||||
def0 unbox : (π : Qty) → (A : ★) → Box π A → A =
|
||||
λ π A ⇒
|
||||
case π return π' ⇒ Box π' A → A of {
|
||||
'zero ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||||
'one ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||||
'any ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||||
}
|
||||
|
||||
def0 unbox0 = unbox 'zero
|
||||
def0 unbox1 = unbox 'one
|
||||
def0 unboxω = unbox 'any
|
||||
|
||||
def0 unbox-nz : (π : NzQty) → (A : ★) → BoxNz π A → A =
|
||||
λ π A ⇒
|
||||
case π return π' ⇒ BoxNz π' A → A of {
|
||||
'one ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||||
'any ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||||
}
|
||||
|
||||
def0 unbox-nz1 = unbox-nz 'one
|
||||
def0 unbox-nzω = unbox-nz 'any
|
||||
|
||||
def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
|
||||
FUN π A B → (x : Box π A) → B (unbox π A x) =
|
||||
λ π A B ⇒
|
||||
case π
|
||||
return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x)
|
||||
of {
|
||||
'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox0 A x') of { [x] ⇒ f x };
|
||||
'one ⇒ λ f x ⇒ case x return x' ⇒ B (unbox1 A x') of { [x] ⇒ f x };
|
||||
'any ⇒ λ f x ⇒ case x return x' ⇒ B (unboxω A x') of { [x] ⇒ f x };
|
||||
}
|
||||
|
||||
def apply' : (π : Qty) → 0.(A B : ★) → Fun π A B → (x : Box π A) → B =
|
||||
λ π A B ⇒ apply π A (λ _ ⇒ B)
|
||||
|
||||
def apply-nz : (π : NzQty) → 0.(A : ★) → 0.(B : A → ★) →
|
||||
FUN-NZ π A B → (x : BoxNz π A) → B (unbox-nz π A x) =
|
||||
λ π A B ⇒
|
||||
case π
|
||||
return π' ⇒ FUN-NZ π' A B → (x : BoxNz π' A) → B (unbox-nz π' A x)
|
||||
of {
|
||||
'one ⇒ λ f x ⇒ case x return x' ⇒ B (unbox-nz1 A x') of { [x] ⇒ f x };
|
||||
'any ⇒ λ f x ⇒ case x return x' ⇒ B (unbox-nzω A x') of { [x] ⇒ f x };
|
||||
}
|
||||
|
||||
def apply-nz' : (π : NzQty) → 0.(A B : ★) → FunNz π A B → (x : BoxNz π A) → B =
|
||||
λ π A B ⇒ apply-nz π A (λ _ ⇒ B)
|
||||
|
||||
def lam : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
|
||||
((x : Box π A) → B (unbox π A x)) → FUN π A B =
|
||||
λ π A B ⇒
|
||||
case π
|
||||
return π' ⇒ ((x : Box π' A) → B (unbox π' A x)) → FUN π' A B of {
|
||||
'zero ⇒ λ f x ⇒ f [x];
|
||||
'one ⇒ λ f x ⇒ f [x];
|
||||
'any ⇒ λ f x ⇒ f [x];
|
||||
}
|
||||
|
||||
def lam' : (π : Qty) → 0.(A B : ★) → (Box π A → B) → Fun π A B =
|
||||
λ π A B ⇒ lam π A (λ _ ⇒ B)
|
||||
|
||||
def lam-nz : (π : NzQty) → 0.(A : ★) → 0.(B : A → ★) →
|
||||
((x : BoxNz π A) → B (unbox-nz π A x)) → FUN-NZ π A B =
|
||||
λ π A B ⇒
|
||||
case π
|
||||
return π' ⇒ ((x : BoxNz π' A) → B (unbox-nz π' A x)) → FUN-NZ π' A B of {
|
||||
'one ⇒ λ f x ⇒ f [x];
|
||||
'any ⇒ λ f x ⇒ f [x];
|
||||
}
|
||||
|
||||
def lam-nz' : (π : NzQty) → 0.(A B : ★) → (BoxNz π A → B) → FunNz π A B =
|
||||
λ π A B ⇒ lam-nz π A (λ _ ⇒ B)
|
||||
|
||||
|
|
@ -0,0 +1,144 @@
|
|||
load "bool.quox"
|
||||
load "list.quox"
|
||||
load "maybe.quox"
|
||||
load "either.quox"
|
||||
|
||||
namespace char {
|
||||
|
||||
postulate0 Char : ★
|
||||
|
||||
#[compile-scheme "(lambda (c) c)"]
|
||||
postulate dup : Char → [ω.Char]
|
||||
|
||||
#[compile-scheme "char->integer"]
|
||||
postulate to-ℕ : Char → ℕ
|
||||
|
||||
#[compile-scheme "integer->char"]
|
||||
postulate from-ℕ : ℕ → Char
|
||||
|
||||
def space = from-ℕ 0x20
|
||||
def tab = from-ℕ 0x09
|
||||
def newline = from-ℕ 0x0a
|
||||
|
||||
def test-via-ℕ : (ω.ℕ → ω.ℕ → Bool) → (ω.Char → ω.Char → Bool) =
|
||||
λ p c d ⇒ p (to-ℕ c) (to-ℕ d)
|
||||
def lt = test-via-ℕ nat.lt
|
||||
def eq = test-via-ℕ nat.eq
|
||||
def gt = test-via-ℕ nat.gt
|
||||
def le = test-via-ℕ nat.le
|
||||
def ne = test-via-ℕ nat.ne
|
||||
def ge = test-via-ℕ nat.ge
|
||||
|
||||
postulate0 eq-iff-nat : (c d : Char) → Iff (c ≡ d : Char) (to-ℕ c ≡ to-ℕ d : ℕ)
|
||||
|
||||
def eq? : DecEq Char =
|
||||
λ c d ⇒
|
||||
let0 Ty = (c ≡ d : Char) ∷ ★ in
|
||||
dec.elim (to-ℕ c ≡ to-ℕ d : ℕ) (λ _ ⇒ Dec Ty)
|
||||
(λ y ⇒ Yes Ty ((snd (eq-iff-nat c d)) y))
|
||||
(λ n ⇒ No Ty (λ y ⇒ n ((fst (eq-iff-nat c d)) y)))
|
||||
(nat.eq? (to-ℕ c) (to-ℕ d))
|
||||
|
||||
def ws? : ω.Char → Bool =
|
||||
λ c ⇒ bool.or (bool.or (eq c space) (eq c tab)) (eq c newline)
|
||||
|
||||
def digit? : ω.Char → Bool =
|
||||
λ c ⇒ bool.and (ge c (from-ℕ 0x30)) (le c (from-ℕ 0x39))
|
||||
|
||||
def digit-val : Char → Maybe ℕ =
|
||||
λ c ⇒ case dup c return Maybe ℕ of { [c] ⇒
|
||||
bool.if (Maybe ℕ) (digit? c)
|
||||
(Just ℕ (nat.minus (to-ℕ c) 0x30))
|
||||
(Nothing ℕ)
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
def0 Char = char.Char
|
||||
|
||||
namespace string {
|
||||
|
||||
#[compile-scheme "string->list"]
|
||||
postulate to-scheme-list : String → list.SchemeList Char
|
||||
|
||||
def to-list : String → List Char =
|
||||
λ str ⇒ list.from-scheme Char (to-scheme-list str)
|
||||
|
||||
#[compile-scheme "list->string"]
|
||||
postulate from-scheme-list : list.SchemeList Char → String
|
||||
|
||||
def from-list : List Char → String =
|
||||
λ cs ⇒ from-scheme-list (list.to-scheme Char cs)
|
||||
|
||||
def foldl : 0.(A : ★) → A → ω.(A → Char → A) → String → A =
|
||||
λ A z f str ⇒ list.foldl Char A z f (to-list str)
|
||||
|
||||
def foldlω : 0.(A : ★) → ω.A → ω.(ω.A → ω.Char → A) → ω.String → A =
|
||||
λ A z f str ⇒ list.foldlω Char A z f (to-list str)
|
||||
|
||||
def split : ω.(ω.Char → Bool) → ω.String → List String =
|
||||
λ p str ⇒
|
||||
list.map (List Char) String from-list
|
||||
(list.split Char p (to-list str))
|
||||
|
||||
def break : ω.(ω.Char → Bool) → ω.String → String × String =
|
||||
λ p str ⇒
|
||||
letω pair = list.break Char p (to-list str) in
|
||||
(from-list (fst pair), from-list (snd pair))
|
||||
|
||||
def reverse : String → String =
|
||||
λ str ⇒ from-list (list.reverse Char (to-list str))
|
||||
|
||||
#[compile-scheme "(lambda% (y n a b) (if (string=? a b) y n))"]
|
||||
postulate eq' : 0.(A : ★) → A → A → ω.String → ω.String → A
|
||||
def eq : ω.String → ω.String → Bool = eq' Bool 'true 'false
|
||||
|
||||
def null : ω.String → Bool = eq ""
|
||||
def not-null : ω.String → Bool = λ s ⇒ bool.not (null s)
|
||||
|
||||
#[compile-scheme "(lambda (str) str)"]
|
||||
postulate dup : String → [ω.String]
|
||||
|
||||
postulate0 dup-ok : (str : String) → dup str ≡ [str] : [ω.String]
|
||||
|
||||
def dup! : (str : String) → Dup String str =
|
||||
dup-from-parts String dup dup-ok
|
||||
|
||||
|
||||
def to-ℕ : String → Maybe ℕ =
|
||||
letω add-digit : Maybe ℕ → ℕ → Maybe ℕ =
|
||||
maybe.fold ℕ (ℕ → Maybe ℕ) (λ d ⇒ Just ℕ d)
|
||||
(λ n d ⇒ Just ℕ (nat.plus (nat.times 10 n) d)) in
|
||||
letω drop : Maybe ℕ → Maybe ℕ =
|
||||
maybe.fold ℕ (Maybe ℕ) (Nothing ℕ)
|
||||
(λ n ⇒ nat.drop (Maybe ℕ) n (Nothing ℕ)) in
|
||||
letω add-digit-c : Maybe ℕ → Char → Maybe ℕ =
|
||||
λ acc c ⇒
|
||||
maybe.fold ℕ (Maybe ℕ → Maybe ℕ) drop (λ n acc ⇒ add-digit acc n)
|
||||
(char.digit-val c) acc in
|
||||
λ str ⇒
|
||||
case dup str return Maybe ℕ of { [str] ⇒
|
||||
bool.if (Maybe ℕ) (not-null str)
|
||||
(foldl (Maybe ℕ) (Just ℕ 0) add-digit-c str)
|
||||
(Nothing ℕ)
|
||||
}
|
||||
|
||||
def to-ℕ-or-0 : String → ℕ =
|
||||
λ str ⇒ maybe.fold ℕ ℕ 0 (λ x ⇒ x) (to-ℕ str)
|
||||
|
||||
|
||||
#[compile-scheme
|
||||
"(lambda% (yes no str)
|
||||
(let [(len (string-length str))]
|
||||
(if (= len 0)
|
||||
no
|
||||
(let [(first (string-ref str 0))
|
||||
(rest (substring str 1 len))]
|
||||
(% yes first rest)))))"]
|
||||
postulate uncons' : 0.(A : ★) → ω.A → ω.(Char → String → A) → String → A
|
||||
|
||||
def uncons : String → Maybe (Char × String) =
|
||||
let0 Pair : ★ = Char × String in
|
||||
uncons' (Maybe Pair) (Nothing Pair) (λ c s ⇒ Just Pair (c, s))
|
||||
|
||||
}
|
||||
|
|
@ -0,0 +1,159 @@
|
|||
load "misc.quox"
|
||||
load "either.quox"
|
||||
load "maybe.quox"
|
||||
|
||||
namespace sub {
|
||||
|
||||
def0 Irr : (A : ★) → ★ =
|
||||
λ A ⇒ (x y : A) → x ≡ y : A
|
||||
|
||||
def0 Irr1 : (A : ★) → (A → ★) → ★ =
|
||||
λ A P ⇒ (x : A) → Irr (P x)
|
||||
|
||||
def0 Irr2 : (A B : ★) → (A → B → ★) → ★ =
|
||||
λ A B P ⇒ (x : A) → (y : B) → Irr (P x y)
|
||||
|
||||
def0 Sub : (A : ★) → (P : A → ★) → ★ =
|
||||
λ A P ⇒ (x : A) × [0. P x]
|
||||
|
||||
|
||||
def sub : 0.(A : ★) → 0.(P : A → ★) → (x : A) → 0.(P x) → Sub A P =
|
||||
λ A P x p ⇒ (x, [p])
|
||||
|
||||
def sub? : 0.(A : ★) → 0.(P : A → ★) → (ω.(x : A) → Dec (P x)) →
|
||||
ω.A → Maybe (Sub A P) =
|
||||
λ A P p? x ⇒
|
||||
dec.elim (P x) (λ _ ⇒ Maybe (Sub A P))
|
||||
(λ y ⇒ Just (Sub A P) (x, [y]))
|
||||
(λ n ⇒ Nothing (Sub A P))
|
||||
(p? x)
|
||||
|
||||
|
||||
def val : 0.(A : ★) → 0.(P : A → ★) → Sub A P → A =
|
||||
λ A P s ⇒ case s return A of { (x, p) ⇒ drop0 (P x) A p x }
|
||||
|
||||
def0 proof : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (fst s) =
|
||||
λ A P s ⇒ get0 (P (fst s)) (snd s)
|
||||
|
||||
{-
|
||||
|
||||
def0 proof' : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (fst s) =
|
||||
λ A P s ⇒ get0 (P (fst s)) (snd s)
|
||||
|
||||
def0 val-fst : (A : ★) → (P : A → ★) →
|
||||
(s : Sub A P) → val A P s ≡ fst s : A =
|
||||
λ A P s ⇒
|
||||
case s return s' ⇒ val A P s' ≡ fst s' : A of {
|
||||
(x, p) ⇒ drop0-eq (P x) A p x
|
||||
}
|
||||
|
||||
def0 proof : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (val A P s) =
|
||||
λ A P s ⇒ coe (𝑖 ⇒ P (val-fst A P s @𝑖)) @1 @0 (proof' A P s)
|
||||
|
||||
postulate0 proof-snd' : (A : ★) → (P : A → ★) → (s : Sub A P) →
|
||||
Eq (𝑖 ⇒ P (val-fst A P s @𝑖)) (proof A P s) (proof' A P s)
|
||||
|
||||
postulate0 proof-snd : (A : ★) → (P : A → ★) → (s : Sub A P) →
|
||||
Eq (𝑖 ⇒ [0.P (val-fst A P s @𝑖)]) [proof A P s] (snd s)
|
||||
|
||||
#![log (all, 10) (equal, 100)]
|
||||
def0 val-proof-eq : (A : ★) → (P : A → ★) → (s : Sub A P) →
|
||||
sub A P (val A P s) (proof A P s) ≡ s : Sub A P =
|
||||
λ A P s ⇒
|
||||
case s return s' ⇒ sub A P (val A P s') (proof A P s') ≡ s' : Sub A P
|
||||
of { (xxxxx, p) ⇒
|
||||
case p
|
||||
return p' ⇒
|
||||
sub A P (val A P (xxxxx, p')) (proof A P (xxxxx, p')) ≡ (xxxxx, p') : Sub A P
|
||||
of { [p0] ⇒
|
||||
δ 𝑖 ⇒ (val-fst A P (xxxxx, [p0]) @𝑖, proof-snd A P (xxxxx, [p0]) @𝑖)
|
||||
}
|
||||
}
|
||||
#![log pop]
|
||||
|
||||
def elim' : 0.(A : ★) → 0.(P : A → ★) →
|
||||
0.(R : (x : A) → P x → ★) →
|
||||
(1.(x : A) → 0.(p : P x) → R x p) →
|
||||
(s : Sub A P) → R (val A P s) (proof A P s) =
|
||||
λ A P R p s ⇒ p (val A P s) (proof A P s)
|
||||
|
||||
{-
|
||||
def elim : 0.(A : ★) → 0.(P : A → ★) →
|
||||
0.(R : Sub A P → ★) →
|
||||
(1.(x : A) → 0.(p : P x) → R (x, [p])) →
|
||||
(s : Sub A P) → R s =
|
||||
λ A P R p s ⇒ p (val A P s) (proof A P s)
|
||||
-}
|
||||
|
||||
-}
|
||||
|
||||
|
||||
|
||||
def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ =
|
||||
λ A P s ⇒ Dup A (fst s)
|
||||
-- (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]]
|
||||
|
||||
def subdup-to-dup :
|
||||
0.(A : ★) → 0.(P : A → ★) →
|
||||
0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
|
||||
λ A P s sd ⇒
|
||||
case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
|
||||
case ss0 return Dup (Sub A P) s of { [ss0] ⇒
|
||||
case sω
|
||||
return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s
|
||||
of { [s!] ⇒ λ ss' ⇒
|
||||
let ω.p : [0.P (fst s)] = revive0 (P (fst s)) (snd s);
|
||||
0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss' in
|
||||
([(s!, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @0 p)],
|
||||
[δ 𝑗 ⇒ [(ss @𝑗, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @𝑗 p)]])
|
||||
} ss0
|
||||
}}
|
||||
|
||||
def subdup : 0.(A : ★) → 0.(P : A → ★) →
|
||||
((x : A) → Dup A x) →
|
||||
(s : Sub A P) → SubDup A P s =
|
||||
λ A P dup s ⇒
|
||||
case s return s' ⇒ SubDup A P s' of { (x, p) ⇒
|
||||
drop0 (P x) (Dup A x) p (dup x)
|
||||
}
|
||||
|
||||
def dup! : 0.(A : ★) → 0.(P : A → ★) → ((x : A) → Dup A x) →
|
||||
(s : Sub A P) → Dup (Sub A P) s =
|
||||
λ A P dupA s ⇒ subdup-to-dup A P s (subdup A P dupA s)
|
||||
|
||||
|
||||
def0 irr1-het : (A : ★) → (P : A → ★) → Irr1 A P →
|
||||
(x y : A) → (p : P x) → (q : P y) →
|
||||
(xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) p q =
|
||||
λ A P pirr x y p q xy ⇒ δ 𝑖 ⇒
|
||||
pirr (xy @𝑖) (coe (𝑗 ⇒ P (xy @𝑗)) @0 @𝑖 p) (coe (𝑗 ⇒ P (xy @𝑗)) @1 @𝑖 q) @𝑖
|
||||
|
||||
def0 irr2-het : (A B : ★) → (P : A → B → ★) → Irr2 A B P →
|
||||
(x₀ x₁ : A) → (y₀ y₁ : B) → (p : P x₀ y₀) → (q : P x₁ y₁) →
|
||||
(xx : x₀ ≡ x₁ : A) → (yy : y₀ ≡ y₁ : B) →
|
||||
Eq (𝑖 ⇒ P (xx @𝑖) (yy @𝑖)) p q =
|
||||
λ A B P pirr x₀ x₁ y₀ y₁ p q xx yy ⇒ δ 𝑖 ⇒
|
||||
pirr (xx @𝑖) (yy @𝑖)
|
||||
(coe (𝑗 ⇒ P (xx @𝑗) (yy @𝑗)) @0 @𝑖 p)
|
||||
(coe (𝑗 ⇒ P (xx @𝑗) (yy @𝑗)) @1 @𝑖 q) @𝑖
|
||||
|
||||
|
||||
def0 sub-eq : (A : ★) → (P : A → ★) → Irr1 A P →
|
||||
(x y : Sub A P) → fst x ≡ fst y : A → x ≡ y : Sub A P =
|
||||
λ A P pirr x y xy0 ⇒ δ 𝑖 ⇒
|
||||
let proof = proof A P in
|
||||
(xy0 @𝑖, [irr1-het A P pirr (fst x) (fst y) (proof x) (proof y) xy0 @𝑖])
|
||||
|
||||
|
||||
def eq? : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
|
||||
DecEq A → DecEq (Sub A P) =
|
||||
λ A P pirr aeq? s t ⇒
|
||||
let0 EQ : ★ = s ≡ t : Sub A P in
|
||||
dec.elim (fst s ≡ fst t : A) (λ _ ⇒ Dec EQ)
|
||||
(λ y ⇒ Yes EQ (sub-eq A P pirr s t y))
|
||||
(λ n ⇒ No EQ (λ eq ⇒ n (δ 𝑖 ⇒ fst (eq @𝑖))))
|
||||
(aeq? (fst s) (fst t))
|
||||
|
||||
}
|
||||
|
||||
def0 Sub = sub.Sub
|
||||
Loading…
Reference in New Issue