207 lines
6.8 KiB
Text
207 lines
6.8 KiB
Text
load "nat.quox"
|
||
load "either.quox"
|
||
load "maybe.quox"
|
||
|
||
|
||
namespace fin {
|
||
|
||
def0 LT : ℕ → ℕ → ★ =
|
||
λ m n ⇒
|
||
nat.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
|
||
m n
|
||
|
||
|
||
def0 lt-irr : (m n : ℕ) → (p q : LT m n) → p ≡ q : LT m n =
|
||
λ m n ⇒
|
||
nat.elim-pairω (λ m n ⇒ (p q : LT m n) → p ≡ q : LT m n)
|
||
false.irr (λ _ _ ⇒ true.irr) (λ _ _ ⇒ false.irr) (λ _ _ p ⇒ p) m n
|
||
|
||
def0 lt-irr-het :
|
||
(m m' n n' : ℕ) → (mm : m ≡ m' : ℕ) → (nn : n ≡ n' : ℕ) →
|
||
(p : LT m n) → (q : LT m' n') →
|
||
Eq (𝑖 ⇒ LT (mm @𝑖) (nn @𝑖)) p q =
|
||
λ m m' n n' mm nn p q ⇒ δ 𝑖 ⇒
|
||
lt-irr (mm @𝑖) (nn @𝑖)
|
||
(coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @0 @𝑖 p)
|
||
(coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @1 @𝑖 q) @𝑖
|
||
|
||
def0 lt-irr-het-left :
|
||
(m m' n : ℕ) → (mm : m ≡ m' : ℕ) → (p : LT m n) → (q : LT m' n) →
|
||
Eq (𝑖 ⇒ LT (mm @𝑖) n) p q =
|
||
λ m m' n mm ⇒ lt-irr-het m m' n n mm (δ _ ⇒ n)
|
||
|
||
|
||
def0 lt-true : (m n : ℕ) → LT m n → LT m n ≡ True : ★ =
|
||
λ m n p ⇒
|
||
nat.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)
|
||
m n p
|
||
|
||
|
||
#[compile-scheme "(lambda% (m n) (if (< m n) dec.Yes dec.No))"]
|
||
def lt? : ω.(m n : ℕ) → Dec (LT m n) =
|
||
nat.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 Fin : ℕ → ★ =
|
||
λ n ⇒ (i : ℕ) × [0.LT i n]
|
||
|
||
|
||
def to-ℕ : 0.(n : ℕ) → Fin n → ℕ =
|
||
λ n i ⇒ case i return ℕ of { (i, p) ⇒ drop0 (LT i n) ℕ p i }
|
||
|
||
def0 to-ℕ-fst : (n : ℕ) → (i : Fin n) → to-ℕ n i ≡ fst i : ℕ =
|
||
λ n i ⇒ drop0-eq (LT (fst i) n) ℕ (snd i) (fst i)
|
||
|
||
def0 to-ℕ-eq : (n : ℕ) → (i j : Fin n) →
|
||
to-ℕ n i ≡ to-ℕ n j : ℕ → i ≡ j : Fin n =
|
||
λ n i' j' ij' ⇒
|
||
let i = fst i'; ilt = get0 (LT i n) (snd i');
|
||
j = fst j'; jlt = get0 (LT j n) (snd j');
|
||
ij : (i ≡ j : ℕ) =
|
||
coe (𝑘 ⇒ to-ℕ-fst n i' @𝑘 ≡ j : ℕ)
|
||
(coe (𝑘 ⇒ to-ℕ n i' ≡ to-ℕ-fst n j' @𝑘 : ℕ) ij');
|
||
ltt : Eq (𝑘 ⇒ LT (ij @𝑘) n) ilt jlt =
|
||
lt-irr-het-left i j n ij ilt jlt in
|
||
δ 𝑘 ⇒ (ij @𝑘, [ltt @𝑘])
|
||
|
||
|
||
def fin? : ω.(n i : ℕ) → Maybe (Fin n) =
|
||
λ n i ⇒
|
||
dec.elim (LT i n) (λ _ ⇒ Maybe (Fin n))
|
||
(λ yes ⇒ Just (Fin n) (i, [yes]))
|
||
(λ no ⇒ Nothing (Fin n))
|
||
(lt? i n)
|
||
|
||
|
||
def F0 : 0.(n : ℕ) → Fin (succ n) = λ _ ⇒ (0, ['true])
|
||
def FS : 0.(n : ℕ) → Fin n → Fin (succ n) =
|
||
λ n i ⇒ case i return Fin (succ n) of { (i, p) ⇒ (succ i, p) }
|
||
|
||
def dup! : 0.(n : ℕ) → (i : Fin n) → Dup (Fin n) i =
|
||
λ n ilt ⇒
|
||
case ilt return ilt' ⇒ Dup (Fin n) ilt' of { (i, lt0) ⇒
|
||
case lt0 return ilt' ⇒ Dup (Fin n) (i, lt0) of { [lt] ⇒
|
||
case nat.dup! i return Dup (Fin n) (i, lt0) of { (iω, ii0) ⇒
|
||
case iω
|
||
return iω' ⇒ 0.(iω' ≡ iω : [ω.ℕ]) → Dup (Fin n) (i, lt0)
|
||
of { [i!] ⇒ λ iiω ⇒
|
||
let 0.iωi : iω ≡ [i] : [ω.ℕ] = get0 (iω ≡ [i] : [ω.ℕ]) ii0;
|
||
in
|
||
0
|
||
} (δ _ ⇒ iω)
|
||
}}}
|
||
|
||
{-
|
||
case ilt return ilt' ⇒ Dup (Fin n) ilt' of { (i, lt0) ⇒
|
||
case lt0 return lt0' ⇒ Dup (Fin n) (i, lt0') of { [lt] ⇒
|
||
case nat.dup! i return Dup (Fin n) (i, [lt]) of { (iω, eq0) ⇒
|
||
let ω.i! = fst ieq!;
|
||
0.ii : i! ≡ i : ℕ = get0 (i! ≡ i : ℕ) (snd ieq!);
|
||
0.lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
|
||
0.ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
|
||
lt-irr-het-left i! i n ii lt! lt;
|
||
ω.ilt! : Fin n = (i!, [lt!]);
|
||
0.iltt : ilt! ≡ ilt : Fin n =
|
||
δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])];
|
||
in
|
||
([ilt!], [iltt])
|
||
-- [((i!, [lt!]), [δ 𝑘 ⇒ (ii @𝑘, [ltt @𝑘])])]
|
||
}}}
|
||
-}
|
||
|
||
{-
|
||
def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] =
|
||
λ n i ⇒ appω (Sing (Fin n) i) (Fin n) (λ p ⇒ fst p) (dup! n i)
|
||
-}
|
||
|
||
{-
|
||
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
|
||
λ n i ⇒
|
||
|
||
appω (Sing (Fin n) i) [0.dup n i ≡ [i] : [ω.Fin n]]
|
||
(λ p ⇒ snd p) (dup! n i)
|
||
-}
|
||
|
||
{-
|
||
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
|
||
λ n i ⇒
|
||
case dup! n i return i' ⇒ fst i' ≡ [i] :
|
||
-}
|
||
|
||
{-
|
||
def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] =
|
||
λ n ilt ⇒
|
||
case ilt return [ω.Fin n] of { (i, lt0) ⇒
|
||
case lt0 return [ω.Fin n] of { [lt] ⇒
|
||
case nat.dup i
|
||
return i' ⇒ 0.(i' ≡ [i] : [ω.ℕ]) → [ω.Fin n]
|
||
of { [i!] ⇒ λ iiω ⇒
|
||
let0 ii : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω;
|
||
lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt in
|
||
[(i!, [lt!])]
|
||
} (nat.dup-ok i)
|
||
}}
|
||
-}
|
||
|
||
{-
|
||
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
|
||
λ n ilt ⇒ δ 𝑘 ⇒
|
||
let i = fst ilt; lt = get0 (LT i n) (snd ilt);
|
||
in
|
||
-}
|
||
|
||
{-
|
||
def dup-ok : 0.(n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
|
||
λ n i ⇒
|
||
case i return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒
|
||
case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒
|
||
case nat.dup i
|
||
return i' ⇒ (i' ≡ [i] : [ω.ℕ]) →
|
||
dup n (i, [lt]) ≡ [(i, [lt])] : [ω.Fin n]
|
||
of { [i!] ⇒ λ iiω ⇒
|
||
let0 ii : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω;
|
||
lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
|
||
ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
|
||
lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt
|
||
in
|
||
δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])]
|
||
} (nat.dup-ok i)
|
||
}}
|
||
-}
|
||
|
||
|
||
{-
|
||
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
|
||
λ n ilt ⇒
|
||
case ilt return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒
|
||
case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒
|
||
let i! = getω ℕ (nat.dup i);
|
||
ii : i! ≡ i : ℕ = δ 𝑘 ⇒ getω ℕ (nat.dup-ok i @𝑘);
|
||
lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
|
||
ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
|
||
lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt
|
||
in
|
||
δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])]
|
||
}}
|
||
-}
|
||
|
||
}
|
||
|
||
def0 Fin = fin.Fin
|
||
def F0 = fin.F0
|
||
def FS = fin.FS
|