-
Notifications
You must be signed in to change notification settings - Fork 1
/
List.ced
98 lines (72 loc) · 3.06 KB
/
List.ced
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
import Nat.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ListC ◂ ★ ➔ ★ = λ A : ★ . ∀ X : ★ . X ➔ (A ➔ X ➔ X) ➔ X.
nilCL ◂ ∀ A : ★ . ListC · A =
Λ A . Λ X . λ cN . λ cC . cN .
consCL ◂ ∀ A : ★ . A ➔ ListC · A ➔ ListC · A =
Λ A . λ x . λ xs . Λ X . λ cN . λ cC . cC x (xs · X cN cC) .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ListP ◂ Π A : ★ . ListC · A ➔ ★ =
λ A : ★ . λ xsC : ListC · A .
∀ X : ★ . ∀ P : X ➔ ★ .
∀ cN : X . ∀ cC : A ➔ X ➔ X .
P cN ➔
(∀ xs : X . Π x : A . P xs ➔ P (cC x xs)) ➔
P (xsC · X cN cC) .
nilPL ◂ ∀ A : ★ . ListP · A (nilCL · A) = Λ A .
Λ X . Λ P . Λ cN . Λ cC . λ pN . λ pC .
pN .
consPL ◂ ∀ A : ★ . ∀ xsC : ListC · A .
Π x : A . ListP · A xsC ➔ ListP · A (consCL · A x xsC) =
Λ A . Λ xsC . λ x . λ xsP .
Λ X . Λ P . Λ cN . Λ cC . λ pN . λ pC .
pC -(xsC · X cN cC) x (xsP · X · P -cN -cC pN pC) .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ListR ◂ Π A : ★ . ListC · A ➔ ★ =
λ A : ★ . λ xsC : ListC · A .
xsC · (ListC · A) nilCL consCL ≃ xsC .
nilRL ◂ ∀ A : ★ . ListR · A (nilCL · A) =
Λ A . β .
consRL ◂ ∀ A : ★ .
∀ x : A . ∀ xsC : ListC · A .
∀ q : ListR · A xsC .
ListR · A (consCL · A x xsC)
= Λ A . Λ x . Λ xsC . Λ q .
ρ+ q - β .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
List ◂ ★ ➔ ★ = λ A : ★ .
ι xs : (ι xsC : ListC · A . ListP · A xsC) . ListR · A xs.1 .
mkList ◂ ∀ A : ★ .
Π xs : (ι xsC : ListC · A . ListP · A xsC) .
ListR · A xs.1 ➾ List · A =
Λ A . λ xs . Λ q . [ xs , ρ q - β{xs} ] .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nilL ◂ ∀ A : ★ . List · A = Λ A .
mkList · A [ nilCL · A , nilPL · A ] -(nilRL · A) .
consL ◂ ∀ A : ★ . A ➔ List · A ➔ List · A =
Λ A . λ x . λ xs . mkList · A
[ consCL · A x xs.1.1
, consPL · A -xs.1.1 x xs.1.2 ]
-(consRL · A -x -xs.1.1 -xs.2) .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
elimList ◂ ∀ A : ★ . Π xs : List · A .
∀ P : List · A ➔ ★ .
P (nilL · A) ➔
(∀ xs : List · A . Π x : A . P xs ➔ P (consL · A x xs)) ➔
P xs
= Λ A . λ xs . Λ P .
ρ ς xs.2 -
(xs.1.2 · (List · A) · P -(nilL · A) -(consL · A)) .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
elimList' ◂ ∀ A : ★ . ∀ P : List · A ➔ ★ .
P (nilL · A) ➔
(∀ xs : List · A . Π x : A . P xs ➔ P (consL · A x xs)) ➔
Π xs : List · A . P xs
= Λ A . Λ P . λ pN . λ pC . λ xs .
elimList · A xs · P pN pC .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
length ◂ ∀ A : ★ . List · A ➔ Nat
= Λ A . elimList' · A · (λ xs : List · A . Nat)
zero
(Λ xs . λ x . suc) .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%