-
Notifications
You must be signed in to change notification settings - Fork 28
/
stlc_lessimpl.lean
170 lines (133 loc) · 6.75 KB
/
stlc_lessimpl.lean
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
def Ty6 : Type 1
:= ∀ (Ty6 : Type)
(nat top bot : Ty6)
(arr prod sum : Ty6 → Ty6 → Ty6)
, Ty6
def nat6 : Ty6 := λ _ nat6 _ _ _ _ _ => nat6
def top6 : Ty6 := λ _ _ top6 _ _ _ _ => top6
def bot6 : Ty6 := λ _ _ _ bot6 _ _ _ => bot6
def arr6 : Ty6 → Ty6 → Ty6
:= λ A B Ty6 nat6 top6 bot6 arr6 prod sum =>
arr6 (A Ty6 nat6 top6 bot6 arr6 prod sum) (B Ty6 nat6 top6 bot6 arr6 prod sum)
def prod6 : Ty6 → Ty6 → Ty6
:= λ A B Ty6 nat6 top6 bot6 arr6 prod6 sum =>
prod6 (A Ty6 nat6 top6 bot6 arr6 prod6 sum) (B Ty6 nat6 top6 bot6 arr6 prod6 sum)
def sum6 : Ty6 → Ty6 → Ty6
:= λ A B Ty6 nat6 top6 bot6 arr6 prod6 sum6 =>
sum6 (A Ty6 nat6 top6 bot6 arr6 prod6 sum6) (B Ty6 nat6 top6 bot6 arr6 prod6 sum6)
def Con6 : Type 1
:= ∀ (Con6 : Type)
(nil : Con6)
(snoc : Con6 → Ty6 → Con6)
, Con6
def nil6 : Con6
:= λ Con6 nil6 snoc => nil6
def snoc6 : Con6 → Ty6 → Con6
:= λ Γ A Con6 nil6 snoc6 => snoc6 (Γ Con6 nil6 snoc6) A
def Var6 : Con6 → Ty6 → Type 1
:= λ Γ A =>
∀ (Var6 : Con6 → Ty6 → Type)
(vz : ∀ Γ A, Var6 (snoc6 Γ A) A)
(vs : ∀ Γ B A, Var6 Γ A → Var6 (snoc6 Γ B) A)
, Var6 Γ A
def vz6 : ∀ {Γ A}, Var6 (snoc6 Γ A) A
:= λ Var6 vz6 vs => vz6 _ _
def vs6 : ∀ {Γ B A}, Var6 Γ A → Var6 (snoc6 Γ B) A
:= λ x Var6 vz6 vs6 => vs6 _ _ _ (x Var6 vz6 vs6)
def Tm6 : Con6 → Ty6 → Type 1
:= λ Γ A =>
∀ (Tm6 : Con6 → Ty6 → Type)
(var : ∀ Γ A , Var6 Γ A → Tm6 Γ A)
(lam : ∀ Γ A B , Tm6 (snoc6 Γ A) B → Tm6 Γ (arr6 A B))
(app : ∀ Γ A B , Tm6 Γ (arr6 A B) → Tm6 Γ A → Tm6 Γ B)
(tt : ∀ Γ , Tm6 Γ top6)
(pair : ∀ Γ A B , Tm6 Γ A → Tm6 Γ B → Tm6 Γ (prod6 A B))
(fst : ∀ Γ A B , Tm6 Γ (prod6 A B) → Tm6 Γ A)
(snd : ∀ Γ A B , Tm6 Γ (prod6 A B) → Tm6 Γ B)
(left : ∀ Γ A B , Tm6 Γ A → Tm6 Γ (sum6 A B))
(right : ∀ Γ A B , Tm6 Γ B → Tm6 Γ (sum6 A B))
(case : ∀ Γ A B C , Tm6 Γ (sum6 A B) → Tm6 Γ (arr6 A C) → Tm6 Γ (arr6 B C) → Tm6 Γ C)
(zero : ∀ Γ , Tm6 Γ nat6)
(suc : ∀ Γ , Tm6 Γ nat6 → Tm6 Γ nat6)
(rec : ∀ Γ A , Tm6 Γ nat6 → Tm6 Γ (arr6 nat6 (arr6 A A)) → Tm6 Γ A → Tm6 Γ A)
, Tm6 Γ A
def var6 : ∀ {Γ A}, Var6 Γ A → Tm6 Γ A
:= λ x Tm6 var6 lam app tt pair fst snd left right case zero suc rec =>
var6 _ _ x
def lam6 : ∀ {Γ A B} , Tm6 (snoc6 Γ A) B → Tm6 Γ (arr6 A B)
:= λ t Tm6 var6 lam6 app tt pair fst snd left right case zero suc rec =>
lam6 _ _ _ (t Tm6 var6 lam6 app tt pair fst snd left right case zero suc rec)
def app6 : ∀ {Γ A B} , Tm6 Γ (arr6 A B) → Tm6 Γ A → Tm6 Γ B
:= λ t u Tm6 var6 lam6 app6 tt pair fst snd left right case zero suc rec =>
app6 _ _ _
(t Tm6 var6 lam6 app6 tt pair fst snd left right case zero suc rec)
(u Tm6 var6 lam6 app6 tt pair fst snd left right case zero suc rec)
def tt6 : ∀ {Γ} , Tm6 Γ top6
:= λ Tm6 var6 lam6 app6 tt6 pair fst snd left right case zero suc rec => tt6 _
def pair6 : ∀ {Γ A B} , Tm6 Γ A → Tm6 Γ B → Tm6 Γ (prod6 A B)
:= λ t u Tm6 var6 lam6 app6 tt6 pair6 fst snd left right case zero suc rec =>
pair6 _ _ _
(t Tm6 var6 lam6 app6 tt6 pair6 fst snd left right case zero suc rec)
(u Tm6 var6 lam6 app6 tt6 pair6 fst snd left right case zero suc rec)
def fst6 : ∀ {Γ A B} , Tm6 Γ (prod6 A B) → Tm6 Γ A
:= λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd left right case zero suc rec =>
fst6 _ _ _
(t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd left right case zero suc rec)
def snd6 : ∀ {Γ A B} , Tm6 Γ (prod6 A B) → Tm6 Γ B
:= λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left right case zero suc rec =>
snd6 _ _ _
(t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left right case zero suc rec)
def left6 : ∀ {Γ A B} , Tm6 Γ A → Tm6 Γ (sum6 A B)
:= λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right case zero suc rec =>
left6 _ _ _
(t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right case zero suc rec)
def right6 : ∀ {Γ A B} , Tm6 Γ B → Tm6 Γ (sum6 A B)
:= λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case zero suc rec =>
right6 _ _ _
(t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case zero suc rec)
def case6 : ∀ {Γ A B C} , Tm6 Γ (sum6 A B) → Tm6 Γ (arr6 A C) → Tm6 Γ (arr6 B C) → Tm6 Γ C
:= λ t u v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec =>
case6 _ _ _ _
(t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec)
(u Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec)
(v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero suc rec)
def zero6 : ∀ {Γ} , Tm6 Γ nat6
:= λ Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc rec => zero6 _
def suc6 : ∀ {Γ} , Tm6 Γ nat6 → Tm6 Γ nat6
:= λ t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec =>
suc6 _ (t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec)
def rec6 : ∀ {Γ A} , Tm6 Γ nat6 → Tm6 Γ (arr6 nat6 (arr6 A A)) → Tm6 Γ A → Tm6 Γ A
:= λ t u v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6 =>
rec6 _ _
(t Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6)
(u Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6)
(v Tm6 var6 lam6 app6 tt6 pair6 fst6 snd6 left6 right6 case6 zero6 suc6 rec6)
def v06 : ∀ {Γ A}, Tm6 (snoc6 Γ A) A
:= var6 vz6
def v16 : ∀ {Γ A B}, Tm6 (snoc6 (snoc6 Γ A) B) A
:= var6 (vs6 vz6)
def v26 : ∀ {Γ A B C}, Tm6 (snoc6 (snoc6 (snoc6 Γ A) B) C) A
:= var6 (vs6 (vs6 vz6))
def v36 : ∀ {Γ A B C D}, Tm6 (snoc6 (snoc6 (snoc6 (snoc6 Γ A) B) C) D) A
:= var6 (vs6 (vs6 (vs6 vz6)))
def tbool6 : Ty6
:= sum6 top6 top6
def ttrue6 : ∀ {Γ}, Tm6 Γ tbool6
:= left6 tt6
def tfalse6 : ∀ {Γ}, Tm6 Γ tbool6
:= right6 tt6
def ifthenelse6 : ∀ {Γ A}, Tm6 Γ (arr6 tbool6 (arr6 A (arr6 A A)))
:= lam6 (lam6 (lam6 (case6 v26 (lam6 v26) (lam6 v16))))
def times46 : ∀ {Γ A}, Tm6 Γ (arr6 (arr6 A A) (arr6 A A))
:= lam6 (lam6 (app6 v16 (app6 v16 (app6 v16 (app6 v16 v06)))))
def add6 : ∀ {Γ}, Tm6 Γ (arr6 nat6 (arr6 nat6 nat6))
:= lam6 (rec6 v06
(lam6 (lam6 (lam6 (suc6 (app6 v16 v06)))))
(lam6 v06))
def mul6 : ∀ {Γ}, Tm6 Γ (arr6 nat6 (arr6 nat6 nat6))
:= lam6 (rec6 v06
(lam6 (lam6 (lam6 (app6 (app6 add6 (app6 v16 v06)) v06))))
(lam6 zero6))
def fact6 : ∀ {Γ}, Tm6 Γ (arr6 nat6 nat6)
:= lam6 (rec6 v06 (lam6 (lam6 (app6 (app6 mul6 (suc6 v16)) v06)))
(suc6 zero6))