-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathInduction.glob
347 lines (347 loc) · 13.8 KB
/
Induction.glob
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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
DIGEST 1baac9acdee18f2dd9b134588bc64170
FInduction
R159:164 Basics <> <> lib
prf 2362:2378 <> plus_n_O_firsttry
R2391:2393 Coq.Init.Datatypes <> nat ind
R2399:2401 Coq.Init.Logic <> :type_scope:x_'='_x not
R2398:2398 Induction <> n var
R2403:2405 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2402:2402 Induction <> n var
prf 2945:2962 <> plus_n_O_secondtry
R2975:2977 Coq.Init.Datatypes <> nat ind
R2983:2985 Coq.Init.Logic <> :type_scope:x_'='_x not
R2982:2982 Induction <> n var
R2987:2989 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2986:2986 Induction <> n var
prf 4262:4269 <> plus_n_O
R4282:4284 Coq.Init.Datatypes <> nat ind
R4288:4290 Coq.Init.Logic <> :type_scope:x_'='_x not
R4287:4287 Induction <> n var
R4292:4294 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4291:4291 Induction <> n var
prf 5475:5484 <> minus_diag
R5509:5511 Coq.Init.Logic <> :type_scope:x_'='_x not
R5500:5504 Coq.Init.Peano <> minus syndef
R5508:5508 Induction <> n var
R5506:5506 Induction <> n var
prf 6050:6057 <> mult_0_r
R6070:6072 Coq.Init.Datatypes <> nat ind
R6082:6084 Coq.Init.Logic <> :type_scope:x_'='_x not
R6078:6080 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6077:6077 Induction <> n var
prf 6246:6254 <> plus_n_Sm
R6271:6273 Coq.Init.Datatypes <> nat ind
R6287:6289 Coq.Init.Logic <> :type_scope:x_'='_x not
R6278:6278 Coq.Init.Datatypes <> S constr
R6282:6284 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6281:6281 Induction <> n var
R6285:6285 Induction <> m var
R6291:6294 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6298:6298 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6290:6290 Induction <> n var
R6295:6295 Coq.Init.Datatypes <> S constr
R6297:6297 Induction <> m var
prf 6469:6477 <> plus_comm
R6494:6496 Coq.Init.Datatypes <> nat ind
R6506:6508 Coq.Init.Logic <> :type_scope:x_'='_x not
R6502:6504 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6501:6501 Induction <> n var
R6505:6505 Induction <> m var
R6510:6512 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6509:6509 Induction <> m var
R6513:6513 Induction <> n var
R6589:6596 Induction <> plus_n_O thm
R6589:6596 Induction <> plus_n_O thm
R6589:6596 Induction <> plus_n_O thm
R6653:6661 Induction <> plus_n_Sm thm
R6653:6661 Induction <> plus_n_Sm thm
R6653:6661 Induction <> plus_n_Sm thm
prf 6726:6735 <> plus_assoc
R6754:6756 Coq.Init.Datatypes <> nat ind
R6772:6774 Coq.Init.Logic <> :type_scope:x_'='_x not
R6762:6765 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6771:6771 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6761:6761 Induction <> n var
R6767:6769 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6766:6766 Induction <> m var
R6770:6770 Induction <> p var
R6775:6775 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6781:6784 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6777:6779 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6776:6776 Induction <> n var
R6780:6780 Induction <> m var
R6785:6785 Induction <> p var
def 7084:7089 <> double
R7094:7096 Coq.Init.Datatypes <> nat ind
R7110:7110 Induction <> n var
R7121:7121 Coq.Init.Datatypes <> O constr
R7126:7126 Coq.Init.Datatypes <> O constr
R7132:7132 Coq.Init.Datatypes <> S constr
R7140:7140 Coq.Init.Datatypes <> S constr
R7143:7143 Coq.Init.Datatypes <> S constr
R7146:7151 Induction <> double def
prf 7236:7246 <> double_plus
R7268:7270 Coq.Init.Logic <> :type_scope:x_'='_x not
R7260:7265 Induction <> double def
R7267:7267 Induction <> n var
R7272:7274 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7271:7271 Induction <> n var
R7275:7275 Induction <> n var
R7393:7401 Induction <> plus_n_Sm thm
R7393:7401 Induction <> plus_n_Sm thm
R7393:7401 Induction <> plus_n_Sm thm
prf 7849:7855 <> evenb_S
R7870:7872 Coq.Init.Datatypes <> nat ind
R7888:7890 Coq.Init.Logic <> :type_scope:x_'='_x not
R7877:7881 Basics <> evenb def
R7884:7884 Coq.Init.Datatypes <> S constr
R7886:7886 Induction <> n var
R7891:7894 Basics <> negb def
R7897:7901 Basics <> evenb def
R7903:7903 Induction <> n var
R8020:8034 Basics <> negb_involutive thm
R8020:8034 Basics <> negb_involutive thm
R8020:8034 Basics <> negb_involutive thm
prf 9061:9072 <> mult_0_plus'
R9089:9091 Coq.Init.Datatypes <> nat ind
R9107:9109 Coq.Init.Logic <> :type_scope:x_'='_x not
R9096:9096 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R9102:9105 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R9098:9100 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9101:9101 Induction <> n var
R9106:9106 Induction <> m var
R9111:9113 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R9110:9110 Induction <> n var
R9114:9114 Induction <> m var
R9156:9158 Coq.Init.Logic <> :type_scope:x_'='_x not
R9152:9154 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9156:9158 Coq.Init.Logic <> :type_scope:x_'='_x not
R9152:9154 Coq.Init.Peano <> :nat_scope:x_'+'_x not
prf 10728:10750 <> plus_rearrange_firsttry
R10771:10773 Coq.Init.Datatypes <> nat ind
R10795:10797 Coq.Init.Logic <> :type_scope:x_'='_x not
R10778:10778 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10784:10788 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10794:10794 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10780:10782 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10779:10779 Induction <> n var
R10783:10783 Induction <> m var
R10790:10792 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10789:10789 Induction <> p var
R10793:10793 Induction <> q var
R10798:10798 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10804:10808 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10814:10814 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10800:10802 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10799:10799 Induction <> m var
R10803:10803 Induction <> n var
R10810:10812 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10809:10809 Induction <> p var
R10813:10813 Induction <> q var
R10954:10962 Induction <> plus_comm thm
R10954:10962 Induction <> plus_comm thm
R10954:10962 Induction <> plus_comm thm
prf 11306:11319 <> plus_rearrange
R11340:11342 Coq.Init.Datatypes <> nat ind
R11364:11366 Coq.Init.Logic <> :type_scope:x_'='_x not
R11347:11347 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11353:11357 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11363:11363 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11349:11351 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11348:11348 Induction <> n var
R11352:11352 Induction <> m var
R11359:11361 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11358:11358 Induction <> p var
R11362:11362 Induction <> q var
R11367:11367 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11373:11377 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11383:11383 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11369:11371 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11368:11368 Induction <> m var
R11372:11372 Induction <> n var
R11379:11381 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11378:11378 Induction <> p var
R11382:11382 Induction <> q var
R11429:11431 Coq.Init.Logic <> :type_scope:x_'='_x not
R11425:11427 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11433:11435 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11429:11431 Coq.Init.Logic <> :type_scope:x_'='_x not
R11425:11427 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11433:11435 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11455:11463 Induction <> plus_comm thm
R11455:11463 Induction <> plus_comm thm
R11455:11463 Induction <> plus_comm thm
prf 14378:14388 <> plus_assoc'
R14407:14409 Coq.Init.Datatypes <> nat ind
R14425:14427 Coq.Init.Logic <> :type_scope:x_'='_x not
R14415:14418 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14424:14424 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14414:14414 Induction <> n var
R14420:14422 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14419:14419 Induction <> m var
R14423:14423 Induction <> p var
R14428:14428 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14434:14437 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14430:14432 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14429:14429 Induction <> n var
R14433:14433 Induction <> m var
R14438:14438 Induction <> p var
prf 14752:14763 <> plus_assoc''
R14782:14784 Coq.Init.Datatypes <> nat ind
R14800:14802 Coq.Init.Logic <> :type_scope:x_'='_x not
R14790:14793 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14799:14799 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14789:14789 Induction <> n var
R14795:14797 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14794:14794 Induction <> m var
R14798:14798 Induction <> p var
R14803:14803 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14809:14812 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14805:14807 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14804:14804 Induction <> n var
R14808:14808 Induction <> m var
R14813:14813 Induction <> p var
prf 17346:17354 <> plus_swap
R17373:17375 Coq.Init.Datatypes <> nat ind
R17391:17393 Coq.Init.Logic <> :type_scope:x_'='_x not
R17381:17384 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R17390:17390 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R17380:17380 Induction <> n var
R17386:17388 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R17385:17385 Induction <> m var
R17389:17389 Induction <> p var
R17395:17398 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R17404:17404 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R17394:17394 Induction <> m var
R17400:17402 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R17399:17399 Induction <> n var
R17403:17403 Induction <> p var
prf 17677:17685 <> mult_comm
R17702:17704 Coq.Init.Datatypes <> nat ind
R17714:17716 Coq.Init.Logic <> :type_scope:x_'='_x not
R17710:17712 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R17709:17709 Induction <> m var
R17713:17713 Induction <> n var
R17718:17720 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R17717:17717 Induction <> n var
R17721:17721 Induction <> m var
R18267:18269 Basics <> leb def
prf 18281:18288 <> leb_refl
R18301:18303 Coq.Init.Datatypes <> nat ind
R18312:18314 Coq.Init.Logic <> :type_scope:x_'='_x not
R18308:18311 Basics <> true constr
R18315:18317 Basics <> leb def
R18321:18321 Induction <> n var
R18319:18319 Induction <> n var
prf 18371:18381 <> zero_nbeq_S
R18394:18396 Coq.Init.Datatypes <> nat ind
R18416:18418 Coq.Init.Logic <> :type_scope:x_'='_x not
R18401:18407 Basics <> beq_nat def
R18412:18412 Coq.Init.Datatypes <> S constr
R18414:18414 Induction <> n var
R18419:18423 Basics <> false constr
prf 18473:18484 <> andb_false_r
R18499:18502 Basics <> bool ind
R18519:18521 Coq.Init.Logic <> :type_scope:x_'='_x not
R18507:18510 Basics <> andb def
R18514:18518 Basics <> false constr
R18512:18512 Induction <> b var
R18522:18526 Basics <> false constr
prf 18576:18592 <> plus_ble_compat_l
R18611:18613 Coq.Init.Datatypes <> nat ind
R18632:18635 Coq.Init.Logic <> :type_scope:x_'->'_x not
R18655:18657 Coq.Init.Logic <> :type_scope:x_'='_x not
R18636:18638 Basics <> leb def
R18650:18652 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R18649:18649 Induction <> p var
R18653:18653 Induction <> m var
R18642:18644 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R18641:18641 Induction <> p var
R18645:18645 Induction <> n var
R18658:18661 Basics <> true constr
R18625:18627 Coq.Init.Logic <> :type_scope:x_'='_x not
R18618:18620 Basics <> leb def
R18624:18624 Induction <> m var
R18622:18622 Induction <> n var
R18628:18631 Basics <> true constr
prf 18711:18718 <> S_nbeq_0
R18731:18733 Coq.Init.Datatypes <> nat ind
R18753:18755 Coq.Init.Logic <> :type_scope:x_'='_x not
R18738:18744 Basics <> beq_nat def
R18747:18747 Coq.Init.Datatypes <> S constr
R18749:18749 Induction <> n var
R18756:18760 Basics <> false constr
prf 18810:18817 <> mult_1_l
R18830:18832 Coq.Init.Datatypes <> nat ind
R18840:18842 Coq.Init.Logic <> :type_scope:x_'='_x not
R18836:18838 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R18839:18839 Induction <> n var
R18843:18843 Induction <> n var
prf 18893:18901 <> all3_spec
R18918:18921 Basics <> bool ind
R18993:18997 Coq.Init.Logic <> :type_scope:x_'='_x not
R18928:18930 Basics <> orb def
R18956:18958 Basics <> orb def
R18985:18988 Basics <> negb def
R18990:18990 Induction <> c var
R18961:18964 Basics <> negb def
R18966:18966 Induction <> b var
R18939:18942 Basics <> andb def
R18946:18946 Induction <> c var
R18944:18944 Induction <> b var
R18998:19001 Basics <> true constr
prf 19051:19067 <> mult_plus_distr_r
R19086:19088 Coq.Init.Datatypes <> nat ind
R19104:19106 Coq.Init.Logic <> :type_scope:x_'='_x not
R19093:19093 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19099:19102 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19095:19097 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R19094:19094 Induction <> n var
R19098:19098 Induction <> m var
R19103:19103 Induction <> p var
R19107:19107 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R19113:19117 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R19123:19123 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R19109:19111 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19108:19108 Induction <> n var
R19112:19112 Induction <> p var
R19119:19121 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19118:19118 Induction <> m var
R19122:19122 Induction <> p var
prf 19173:19182 <> mult_assoc
R19201:19203 Coq.Init.Datatypes <> nat ind
R19219:19221 Coq.Init.Logic <> :type_scope:x_'='_x not
R19209:19212 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19218:19218 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19208:19208 Induction <> n var
R19214:19216 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19213:19213 Induction <> m var
R19217:19217 Induction <> p var
R19222:19222 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19228:19231 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19224:19226 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R19223:19223 Induction <> n var
R19227:19227 Induction <> m var
R19232:19232 Induction <> p var
prf 19690:19701 <> beq_nat_refl
R19716:19718 Coq.Init.Datatypes <> nat ind
R19727:19729 Coq.Init.Logic <> :type_scope:x_'='_x not
R19723:19726 Basics <> true constr
R19730:19736 Basics <> beq_nat def
R19740:19740 Induction <> n var
R19738:19738 Induction <> n var
prf 20337:20346 <> plus_swap'
R20365:20367 Coq.Init.Datatypes <> nat ind
R20383:20385 Coq.Init.Logic <> :type_scope:x_'='_x not
R20373:20376 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R20382:20382 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R20372:20372 Induction <> n var
R20378:20380 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R20377:20377 Induction <> m var
R20381:20381 Induction <> p var
R20387:20390 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R20396:20396 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R20386:20386 Induction <> m var
R20392:20394 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R20391:20391 Induction <> n var
R20395:20395 Induction <> p var