-
Notifications
You must be signed in to change notification settings - Fork 0
/
drinker.html
597 lines (560 loc) · 87.6 KB
/
drinker.html
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
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
<!doctype html>
<html>
<head>
<meta charset='UTF-8'><meta name='viewport' content='width=device-width initial-scale=1'>
<title>drinker</title><link href='https://fonts.loli.net/css?family=Ubuntu:400,700,400italic,700italic' rel='stylesheet' type='text/css' /><link href='https://fonts.loli.net/css?family=Raleway:600,400&subset=latin,latin-ext' rel='stylesheet' type='text/css' /><style type='text/css'>html {overflow-x: initial !important;}:root { --bg-color: #ffffff; --text-color: #333333; --select-text-bg-color: #B5D6FC; --select-text-font-color: auto; --monospace: "Lucida Console",Consolas,"Courier",monospace; }
html { font-size: 14px; background-color: var(--bg-color); color: var(--text-color); font-family: "Helvetica Neue", Helvetica, Arial, sans-serif; -webkit-font-smoothing: antialiased; }
body { margin: 0px; padding: 0px; height: auto; bottom: 0px; top: 0px; left: 0px; right: 0px; font-size: 1rem; line-height: 1.42857143; overflow-x: hidden; background-image: inherit; background-size: inherit; background-attachment: inherit; background-origin: inherit; background-clip: inherit; background-color: inherit; background-position: inherit inherit; background-repeat: inherit inherit; }
iframe { margin: auto; }
a.url { word-break: break-all; }
a:active, a:hover { outline: 0px; }
.in-text-selection, ::selection { text-shadow: none; background: var(--select-text-bg-color); color: var(--select-text-font-color); }
#write { margin: 0px auto; height: auto; width: inherit; word-break: normal; word-wrap: break-word; position: relative; white-space: normal; overflow-x: visible; padding-top: 40px; }
#write.first-line-indent p { text-indent: 2em; }
#write.first-line-indent li p, #write.first-line-indent p * { text-indent: 0px; }
#write.first-line-indent li { margin-left: 2em; }
.for-image #write { padding-left: 8px; padding-right: 8px; }
body.typora-export { padding-left: 30px; padding-right: 30px; }
.typora-export .footnote-line, .typora-export li, .typora-export p { white-space: pre-wrap; }
@media screen and (max-width: 500px) {
body.typora-export { padding-left: 0px; padding-right: 0px; }
.CodeMirror-sizer { margin-left: 0px !important; }
.CodeMirror-gutters { display: none !important; }
}
#write li > figure:first-child { margin-top: -20px; }
#write ol, #write ul { position: relative; }
img { max-width: 100%; vertical-align: middle; }
button, input, select, textarea { color: inherit; font-family: inherit; font-size: inherit; font-style: inherit; font-variant-caps: inherit; font-weight: inherit; font-stretch: inherit; line-height: inherit; }
input[type="checkbox"], input[type="radio"] { line-height: normal; padding: 0px; }
*, ::after, ::before { box-sizing: border-box; }
#write h1, #write h2, #write h3, #write h4, #write h5, #write h6, #write p, #write pre { width: inherit; }
#write h1, #write h2, #write h3, #write h4, #write h5, #write h6, #write p { position: relative; }
h1, h2, h3, h4, h5, h6 { break-after: avoid-page; break-inside: avoid; orphans: 2; }
p { orphans: 4; }
h1 { font-size: 2rem; }
h2 { font-size: 1.8rem; }
h3 { font-size: 1.6rem; }
h4 { font-size: 1.4rem; }
h5 { font-size: 1.2rem; }
h6 { font-size: 1rem; }
.md-math-block, .md-rawblock, h1, h2, h3, h4, h5, h6, p { margin-top: 1rem; margin-bottom: 1rem; }
.hidden { display: none; }
.md-blockmeta { color: rgb(204, 204, 204); font-weight: 700; font-style: italic; }
a { cursor: pointer; }
sup.md-footnote { padding: 2px 4px; background-color: rgba(238, 238, 238, 0.701961); color: rgb(85, 85, 85); border-top-left-radius: 4px; border-top-right-radius: 4px; border-bottom-right-radius: 4px; border-bottom-left-radius: 4px; cursor: pointer; }
sup.md-footnote a, sup.md-footnote a:hover { color: inherit; text-transform: inherit; text-decoration: inherit; }
#write input[type="checkbox"] { cursor: pointer; width: inherit; height: inherit; }
figure { overflow-x: auto; margin: 1.2em 0px; max-width: calc(100% + 16px); padding: 0px; }
figure > table { margin: 0px !important; }
tr { break-inside: avoid; break-after: auto; }
thead { display: table-header-group; }
table { border-collapse: collapse; border-spacing: 0px; width: 100%; overflow: auto; break-inside: auto; text-align: left; }
table.md-table td { min-width: 32px; }
.CodeMirror-gutters { border-right-width: 0px; background-color: inherit; }
.CodeMirror { text-align: left; }
.CodeMirror-placeholder { opacity: 0.3; }
.CodeMirror pre { padding: 0px 4px; }
.CodeMirror-lines { padding: 0px; }
div.hr:focus { cursor: none; }
#write pre { white-space: pre-wrap; }
#write.fences-no-line-wrapping pre { white-space: pre; }
#write pre.ty-contain-cm { white-space: normal; }
.CodeMirror-gutters { margin-right: 4px; }
.md-fences { font-size: 0.9rem; display: block; break-inside: avoid; text-align: left; overflow: visible; white-space: pre; background-image: inherit; background-size: inherit; background-attachment: inherit; background-origin: inherit; background-clip: inherit; background-color: inherit; position: relative !important; background-position: inherit inherit; background-repeat: inherit inherit; }
.md-diagram-panel { width: 100%; margin-top: 10px; text-align: center; padding-top: 0px; padding-bottom: 8px; overflow-x: auto; }
#write .md-fences.mock-cm { white-space: pre-wrap; }
.md-fences.md-fences-with-lineno { padding-left: 0px; }
#write.fences-no-line-wrapping .md-fences.mock-cm { white-space: pre; overflow-x: auto; }
.md-fences.mock-cm.md-fences-with-lineno { padding-left: 8px; }
.CodeMirror-line, twitterwidget { break-inside: avoid; }
.footnotes { opacity: 0.8; font-size: 0.9rem; margin-top: 1em; margin-bottom: 1em; }
.footnotes + .footnotes { margin-top: 0px; }
.md-reset { margin: 0px; padding: 0px; border: 0px; outline: 0px; vertical-align: top; text-decoration: none; text-shadow: none; float: none; position: static; width: auto; height: auto; white-space: nowrap; cursor: inherit; line-height: normal; font-weight: 400; text-align: left; box-sizing: content-box; direction: ltr; background-position: 0px 0px; background-repeat: initial initial; }
li div { padding-top: 0px; }
blockquote { margin: 1rem 0px; }
li .mathjax-block, li p { margin: 0.5rem 0px; }
li { margin: 0px; position: relative; }
blockquote > :last-child { margin-bottom: 0px; }
blockquote > :first-child, li > :first-child { margin-top: 0px; }
.footnotes-area { color: rgb(136, 136, 136); margin-top: 0.714rem; padding-bottom: 0.143rem; white-space: normal; }
#write .footnote-line { white-space: pre-wrap; }
@media print {
body, html { border: 1px solid transparent; height: 99%; break-after: avoid-page; break-before: avoid-page; }
#write { margin-top: 0px; padding-top: 0px; border-color: transparent !important; }
.typora-export * { -webkit-print-color-adjust: exact; }
html.blink-to-pdf { font-size: 13px; }
.typora-export #write { padding-left: 32px; padding-right: 32px; padding-bottom: 0px; break-after: avoid-page; }
.typora-export #write::after { height: 0px; }
@page { margin: 20mm 0px; }
}
.footnote-line { margin-top: 0.714em; font-size: 0.7em; }
a img, img a { cursor: pointer; }
pre.md-meta-block { font-size: 0.8rem; min-height: 0.8rem; white-space: pre-wrap; background-color: rgb(204, 204, 204); display: block; overflow-x: hidden; background-position: initial initial; background-repeat: initial initial; }
p > .md-image:only-child:not(.md-img-error) img, p > img:only-child { display: block; margin: auto; }
p > .md-image:only-child { display: inline-block; width: 100%; }
#write .MathJax_Display { margin: 0.8em 0px 0px; }
.md-math-block { width: 100%; }
.md-math-block:not(:empty)::after { display: none; }
[contenteditable="true"]:active, [contenteditable="true"]:focus { outline: 0px; box-shadow: none; }
.md-task-list-item { position: relative; list-style-type: none; }
.task-list-item.md-task-list-item { padding-left: 0px; }
.md-task-list-item > input { position: absolute; top: 0px; left: 0px; margin-left: -1.2em; margin-top: calc(1em - 10px); }
.math { font-size: 1rem; }
.md-toc { min-height: 3.58rem; position: relative; font-size: 0.9rem; border-top-left-radius: 10px; border-top-right-radius: 10px; border-bottom-right-radius: 10px; border-bottom-left-radius: 10px; }
.md-toc-content { position: relative; margin-left: 0px; }
.md-toc-content::after, .md-toc::after { display: none; }
.md-toc-item { display: block; color: rgb(65, 131, 196); }
.md-toc-item a { text-decoration: none; }
.md-toc-inner:hover { text-decoration: underline; }
.md-toc-inner { display: inline-block; cursor: pointer; }
.md-toc-h1 .md-toc-inner { margin-left: 0px; font-weight: 700; }
.md-toc-h2 .md-toc-inner { margin-left: 2em; }
.md-toc-h3 .md-toc-inner { margin-left: 4em; }
.md-toc-h4 .md-toc-inner { margin-left: 6em; }
.md-toc-h5 .md-toc-inner { margin-left: 8em; }
.md-toc-h6 .md-toc-inner { margin-left: 10em; }
@media screen and (max-width: 48em) {
.md-toc-h3 .md-toc-inner { margin-left: 3.5em; }
.md-toc-h4 .md-toc-inner { margin-left: 5em; }
.md-toc-h5 .md-toc-inner { margin-left: 6.5em; }
.md-toc-h6 .md-toc-inner { margin-left: 8em; }
}
a.md-toc-inner { font-size: inherit; font-style: inherit; font-weight: inherit; line-height: inherit; }
.footnote-line a:not(.reversefootnote) { color: inherit; }
.md-attr { display: none; }
.md-fn-count::after { content: "."; }
code, pre, samp, tt { font-family: var(--monospace); }
kbd { margin: 0px 0.1em; padding: 0.1em 0.6em; font-size: 0.8em; color: rgb(36, 39, 41); background-color: rgb(255, 255, 255); border: 1px solid rgb(173, 179, 185); border-top-left-radius: 3px; border-top-right-radius: 3px; border-bottom-right-radius: 3px; border-bottom-left-radius: 3px; box-shadow: rgba(12, 13, 14, 0.2) 0px 1px 0px, rgb(255, 255, 255) 0px 0px 0px 2px inset; white-space: nowrap; vertical-align: middle; background-position: initial initial; background-repeat: initial initial; }
.md-comment { color: rgb(162, 127, 3); opacity: 0.8; font-family: var(--monospace); }
code { text-align: left; }
a.md-print-anchor { white-space: pre !important; border: none !important; display: inline-block !important; position: absolute !important; width: 1px !important; right: 0px !important; outline: 0px !important; text-shadow: initial !important; background-position: 0px 0px !important; background-repeat: initial initial !important; }
.md-inline-math .MathJax_SVG .noError { display: none !important; }
.html-for-mac .inline-math-svg .MathJax_SVG { vertical-align: 0.2px; }
.md-math-block .MathJax_SVG_Display { text-align: center; margin: 0px; position: relative; text-indent: 0px; max-width: none; max-height: none; min-height: 0px; min-width: 100%; width: auto; overflow-y: hidden; display: block !important; }
.MathJax_SVG_Display, .md-inline-math .MathJax_SVG_Display { width: auto; margin: inherit; display: inline-block !important; }
.MathJax_SVG .MJX-monospace { font-family: var(--monospace); }
.MathJax_SVG .MJX-sans-serif { font-family: sans-serif; }
.MathJax_SVG { display: inline; font-style: normal; font-weight: 400; line-height: normal; zoom: 90%; text-indent: 0px; text-align: left; text-transform: none; letter-spacing: normal; word-spacing: normal; word-wrap: normal; white-space: nowrap; float: none; direction: ltr; max-width: none; max-height: none; min-width: 0px; min-height: 0px; border: 0px; padding: 0px; margin: 0px; }
.MathJax_SVG * { transition: none; }
.MathJax_SVG_Display svg { vertical-align: middle !important; margin-bottom: 0px !important; }
.os-windows.monocolor-emoji .md-emoji { font-family: "Segoe UI Symbol", sans-serif; }
.md-diagram-panel > svg { max-width: 100%; }
[lang="mermaid"] svg, [lang="flow"] svg { max-width: 100%; }
[lang="mermaid"] .node text { font-size: 1rem; }
table tr th { border-bottom-width: 0px; }
video { max-width: 100%; display: block; margin: 0px auto; }
iframe { max-width: 100%; width: 100%; border: none; }
.highlight td, .highlight tr { border: 0px; }
.CodeMirror { height: auto; }
.CodeMirror.cm-s-inner { background-image: inherit; background-size: inherit; background-attachment: inherit; background-origin: inherit; background-clip: inherit; background-color: inherit; background-position: inherit inherit; background-repeat: inherit inherit; }
.CodeMirror-scroll { overflow-y: hidden; overflow-x: auto; z-index: 3; }
.CodeMirror-gutter-filler, .CodeMirror-scrollbar-filler { background-color: rgb(255, 255, 255); }
.CodeMirror-gutters { border-right-width: 1px; border-right-style: solid; border-right-color: rgb(221, 221, 221); background-image: inherit; background-size: inherit; background-attachment: inherit; background-origin: inherit; background-clip: inherit; background-color: inherit; white-space: nowrap; background-position: inherit inherit; background-repeat: inherit inherit; }
.CodeMirror-linenumber { padding: 0px 3px 0px 5px; text-align: right; color: rgb(153, 153, 153); }
.cm-s-inner .cm-keyword { color: rgb(119, 0, 136); }
.cm-s-inner .cm-atom, .cm-s-inner.cm-atom { color: rgb(34, 17, 153); }
.cm-s-inner .cm-number { color: rgb(17, 102, 68); }
.cm-s-inner .cm-def { color: rgb(0, 0, 255); }
.cm-s-inner .cm-variable { color: rgb(0, 0, 0); }
.cm-s-inner .cm-variable-2 { color: rgb(0, 85, 170); }
.cm-s-inner .cm-variable-3 { color: rgb(0, 136, 85); }
.cm-s-inner .cm-string { color: rgb(170, 17, 17); }
.cm-s-inner .cm-property { color: rgb(0, 0, 0); }
.cm-s-inner .cm-operator { color: rgb(152, 26, 26); }
.cm-s-inner .cm-comment, .cm-s-inner.cm-comment { color: rgb(170, 85, 0); }
.cm-s-inner .cm-string-2 { color: rgb(255, 85, 0); }
.cm-s-inner .cm-meta { color: rgb(85, 85, 85); }
.cm-s-inner .cm-qualifier { color: rgb(85, 85, 85); }
.cm-s-inner .cm-builtin { color: rgb(51, 0, 170); }
.cm-s-inner .cm-bracket { color: rgb(153, 153, 119); }
.cm-s-inner .cm-tag { color: rgb(17, 119, 0); }
.cm-s-inner .cm-attribute { color: rgb(0, 0, 204); }
.cm-s-inner .cm-header, .cm-s-inner.cm-header { color: rgb(0, 0, 255); }
.cm-s-inner .cm-quote, .cm-s-inner.cm-quote { color: rgb(0, 153, 0); }
.cm-s-inner .cm-hr, .cm-s-inner.cm-hr { color: rgb(153, 153, 153); }
.cm-s-inner .cm-link, .cm-s-inner.cm-link { color: rgb(0, 0, 204); }
.cm-negative { color: rgb(221, 68, 68); }
.cm-positive { color: rgb(34, 153, 34); }
.cm-header, .cm-strong { font-weight: 700; }
.cm-del { text-decoration: line-through; }
.cm-em { font-style: italic; }
.cm-link { text-decoration: underline; }
.cm-error { color: red; }
.cm-invalidchar { color: red; }
.cm-constant { color: rgb(38, 139, 210); }
.cm-defined { color: rgb(181, 137, 0); }
div.CodeMirror span.CodeMirror-matchingbracket { color: rgb(0, 255, 0); }
div.CodeMirror span.CodeMirror-nonmatchingbracket { color: rgb(255, 34, 34); }
.cm-s-inner .CodeMirror-activeline-background { background-image: inherit; background-size: inherit; background-attachment: inherit; background-origin: inherit; background-clip: inherit; background-color: inherit; background-position: inherit inherit; background-repeat: inherit inherit; }
.CodeMirror { position: relative; overflow: hidden; }
.CodeMirror-scroll { height: 100%; outline: 0px; position: relative; box-sizing: content-box; background-image: inherit; background-size: inherit; background-attachment: inherit; background-origin: inherit; background-clip: inherit; background-color: inherit; background-position: inherit inherit; background-repeat: inherit inherit; }
.CodeMirror-sizer { position: relative; }
.CodeMirror-gutter-filler, .CodeMirror-hscrollbar, .CodeMirror-scrollbar-filler, .CodeMirror-vscrollbar { position: absolute; z-index: 6; display: none; }
.CodeMirror-vscrollbar { right: 0px; top: 0px; overflow: hidden; }
.CodeMirror-hscrollbar { bottom: 0px; left: 0px; overflow: hidden; }
.CodeMirror-scrollbar-filler { right: 0px; bottom: 0px; }
.CodeMirror-gutter-filler { left: 0px; bottom: 0px; }
.CodeMirror-gutters { position: absolute; left: 0px; top: 0px; padding-bottom: 30px; z-index: 3; }
.CodeMirror-gutter { white-space: normal; height: 100%; box-sizing: content-box; padding-bottom: 30px; margin-bottom: -32px; display: inline-block; }
.CodeMirror-gutter-wrapper { position: absolute; z-index: 4; border: none !important; background-position: 0px 0px !important; background-repeat: initial initial !important; }
.CodeMirror-gutter-background { position: absolute; top: 0px; bottom: 0px; z-index: 4; }
.CodeMirror-gutter-elt { position: absolute; cursor: default; z-index: 4; }
.CodeMirror-lines { cursor: text; }
.CodeMirror pre { border-top-left-radius: 0px; border-top-right-radius: 0px; border-bottom-right-radius: 0px; border-bottom-left-radius: 0px; border-width: 0px; font-family: inherit; font-size: inherit; margin: 0px; white-space: pre; word-wrap: normal; color: inherit; z-index: 2; position: relative; overflow: visible; background-position: 0px 0px; background-repeat: initial initial; }
.CodeMirror-wrap pre { word-wrap: break-word; white-space: pre-wrap; word-break: normal; }
.CodeMirror-code pre { border-right-width: 30px; border-right-style: solid; border-right-color: transparent; width: fit-content; }
.CodeMirror-wrap .CodeMirror-code pre { border-right-style: none; width: auto; }
.CodeMirror-linebackground { position: absolute; left: 0px; right: 0px; top: 0px; bottom: 0px; z-index: 0; }
.CodeMirror-linewidget { position: relative; z-index: 2; overflow: auto; }
.CodeMirror-wrap .CodeMirror-scroll { overflow-x: hidden; }
.CodeMirror-measure { position: absolute; width: 100%; height: 0px; overflow: hidden; visibility: hidden; }
.CodeMirror-measure pre { position: static; }
.CodeMirror div.CodeMirror-cursor { position: absolute; visibility: hidden; border-right-style: none; width: 0px; }
.CodeMirror div.CodeMirror-cursor { visibility: hidden; }
.CodeMirror-focused div.CodeMirror-cursor { visibility: inherit; }
.cm-searching { background-color: rgba(255, 255, 0, 0.4); background-position: initial initial; background-repeat: initial initial; }
@media print {
.CodeMirror div.CodeMirror-cursor { visibility: hidden; }
}
@include-when-export url(https://fonts.loli.net/css?family=Ubuntu:400,700,400italic,700italic);
@include-when-export url(https://fonts.loli.net/css?family=Raleway:600,400&subset=latin,latin-ext);
:root {
--window-border: none;
--typora-center-window-title: true;
--active-file-bg-color: #f3f3f3;
--bg-color: #fcfcfc;
--control-text-color: #777;
}
.mac-seamless-mode #typora-sidebar {
top: 20px;
padding-top: 0;
height: auto;
}
html,
body,
#write{
background: #fcfcfc;
background: var(--bg-color);
font-family: 'TeXGyreAdventor', "Century Gothic", 'Yu Gothic', 'Raleway', sans-serif;
font-weight: 300;
}
h1,
h2,
h3,
h4,
h5,
h6 {
color: #111;
font-family: 'TeXGyreAdventor', "Century Gothic", 'Yu Gothic', 'Ubuntu', sans-serif;
}
html {
font-size:16px;
}
#write {
max-width: 914px;
text-align: justify;
}
#write>h1:first-child {
margin-top: 2.75rem;
}
#write>h2:first-child {
margin-top: 1.75rem;
}
#write>h3:first-child {
margin-top: 1rem;
}
#write>h4:first-child {
margin-top: 0.5rem;
}
h1 {
font-weight: normal;
line-height: 4rem;
margin: 0 0 1.75rem;
padding: 20px 30px;
text-align: center;
text-transform: uppercase;
margin-top: 4rem;
}
h2 {
font-weight: normal;
line-height: 3rem;
margin: 0 0 1.9375rem;
padding: 0 30px;
text-align: center;
text-transform: uppercase;
margin-top: 3rem
}
h3 {
font-weight: normal;
}
h4 {
font-weight: normal;
}
h5 {
font-size: 1.125rem;
font-weight: normal;
}
h6 {
font-size: 1rem;
font-weight: bold;
}
p {
color: #111;
font-size: 1rem;
line-height: 1.75rem;
margin: 0 0 1.25rem;
}
#write>h3.md-focus:before {
left: -1.875rem;
top: 0.5rem;
padding: 2px;
}
#write>h4.md-focus:before {
left: -1.875rem;
top: 0.3125rem;
padding: 2px;
}
#write>h5.md-focus:before {
left: -1.875rem;
top: 0.25rem;
padding: 2px;
}
#write>h6.md-focus:before {
left: -1.875rem;
top: .125rem;
padding: 2px;
}
@media screen and (max-width: 48em) {
blockquote {
margin-left: 1rem;
margin-right: 0;
padding: 0.5em;
}
.h1,
h1 {
font-size: 2.827rem;
}
.h2,
h2 {
font-size: 1.999rem;
}
.h3,
h3 {
font-size: 1.413rem;
}
.h4,
h4 {
font-size: 1.250rem;
}
.h5,
h5 {
font-size: 1.150rem;
}
.h6,
h6 {
font-size: 1rem;
}
}
a,
.md-def-url {
color: #990000;
text-decoration: none;
}
a:hover {
text-decoration: underline;
}
table {
margin-bottom: 20px
}
table th,
table td {
padding: 8px;
line-height: 1.25rem;
vertical-align: top;
border-top: 1px solid #ddd
}
table th {
font-weight: bold
}
table thead th {
vertical-align: bottom
}
table caption+thead tr:first-child th,
table caption+thead tr:first-child td,
table colgroup+thead tr:first-child th,
table colgroup+thead tr:first-child td,
table thead:first-child tr:first-child th,
table thead:first-child tr:first-child td {
border-top: 0
}
table tbody+tbody {
border-top: 2px solid #ddd
}
code, .md-fences {
padding: .5em;
/*background: #f0f0f0;*/
border: 1px solid #ccc;
padding: .1em;
font-size: 0.9em;
margin-left: 0.2em;
margin-right: 0.2em;
}
.md-fences {
margin: 0 0 20px;
font-size: 1em;
padding: 0.3em 1em;
padding-top: 0.4em;
}
.task-list{
padding-left: 0;
}
.task-list-item {
padding-left:2.125rem;
}
input {
border-style: ridge;
}
.task-list-item input {
top: 3px;
}
.md-task-list-item input {
margin-left: -1.5em;
}
.task-list-item input:before {
content: "";
display: inline-block;
width: 1rem;
height: 1rem;
vertical-align: middle;
text-align: center;
border: 1px solid gray;
background-color: #fdfdfd;
margin-left: 0;
-webkit-appearance: none;
margin-top: -1rem;
}
.typora-node .task-list-item input:before {
top: 0.3ex;
position: absolute;
}
.task-list-item input:checked:before,
.task-list-item input[checked]:before{
content: '\25FC';
/*◘*/
font-size: 0.8125rem;
line-height: 0.9375rem;
}
/* Chrome 29+ */
@media screen and (-webkit-min-device-pixel-ratio:0)
and (min-resolution:.001dpcm) {
.task-list-item input:before {
margin-top: -0.2rem;
}
.task-list-item input:checked:before,
.task-list-item input[checked]:before {
margin-top: -0.2rem;
}
}
blockquote {
margin: 0 0 1.11111rem;
padding: 0.5rem 1.11111rem 0 1.05556rem;
border-left: 1px solid gray;
}
blockquote,
blockquote p {
line-height: 1.6;
color: #6f6f6f;
}
#write pre.md-meta-block {
min-height: 30px;
background: #f8f8f8;
padding: 1.5em;
font-weight: 300;
font-size: 1em;
padding-bottom: 1.5em;
padding-top: 3em;
margin-top: -1.5em;
color: #999;
width: 100vw;
max-width: calc(100% + 60px);
margin-left: -30px;
border-left: 30px #f8f8f8 solid;
border-right: 30px #f8f8f8 solid;
}
.MathJax_Display {
font-size: 0.9em;
margin-top: 0.5em;
margin-bottom: 0;
}
p.mathjax-block,
.mathjax-block {
padding-bottom: 0;
}
.mathjax-block>.code-tooltip {
bottom: 5px;
box-shadow: none;
}
.md-image>.md-meta {
padding-left: 0.5em;
padding-right: 0.5em;
}
.md-image>img {
margin-top: 2px;
}
.md-image>.md-meta:first-of-type:before {
padding-left: 4px;
}
#typora-source {
color: #555;
}
/** ui for windows **/
#md-searchpanel {
border-bottom: 1px solid #ccc;
}
#md-searchpanel .btn {
border: 1px solid #ccc;
}
#md-notification:before {
top: 14px;
}
#md-notification {
background: #eee;
}
.megamenu-menu-panel .btn {
border: 1px solid #ccc;
}
#typora-sidebar {
box-shadow: none;
}
.file-list-item ,
.show-folder-name .file-list-item {
padding-top: 20px;
padding-bottom: 20px;
line-height: 20px;
}
.file-list-item-summary {
height: 40px;
line-height: 20px;
}
.ty-table-edit {
background: #ededed;
}
.dropdown-menu .divider {
border-color: #e5e5e5;
}
body.typora-export {
padding-left: 20px !important;
padding-right: 20px !important;
}
.typora-export li, .typora-export p, .typora-export, .footnote-line {white-space: normal;}
</style>
</head>
<body class='typora-export' >
<div id='write' class = 'is-mac'><h1><a name='header-n0' class='md-header-anchor '></a>Struggling With My Drinker's Problem</h1><p>I've recently stumbled upon the <a href='https://en.wikipedia.org/wiki/Drinker_paradox'>Drinker's Problem</a>:</p><blockquote><p>The <strong>drinker paradox</strong> (also known as the <strong>drinker's theorem</strong>, the <strong>drinker's principle</strong>, or the <strong>drinking principle</strong>) is a <a href='https://en.wikipedia.org/wiki/Theorem'>theorem</a> of <a href='https://en.wikipedia.org/wiki/Classical_logic'>classical</a> <a href='https://en.wikipedia.org/wiki/Predicate_logic'>predicate logic</a> which can be stated as "There is someone in the pub such that, if he is drinking, then everyone in the pub is drinking." It was popularised by the <a href='https://en.wikipedia.org/wiki/Mathematical_logician'>mathematical logician</a> <a href='https://en.wikipedia.org/wiki/Raymond_Smullyan'>Raymond Smullyan</a>, who called it the "drinking principle" in his 1978 book <em>What Is the Name of this Book?</em></p></blockquote><p>Lovely book name. For people who love Greek letters, here's the formal problem definition:</p><div contenteditable="false" spellcheck="false" class="mathjax-block md-end-block md-math-block md-rawblock" id="mathjax-n6" cid="n6" mdtype="math_block">
<div class="md-rawblock-container md-math-container" tabindex="-1"><div class="MathJax_SVG_Display" style="text-align: center;"><span class="MathJax_SVG" id="MathJax-Element-2-Frame" tabindex="-1" style="font-size: 100%; display: inline-block;"><svg xmlns:xlink="http://www.w3.org/1999/xlink" width="222.23959350585938px" height="23.40277862548828px" viewBox="0 -838.5 11246.1 1184.9" role="img" focusable="false" style="vertical-align: -0.805ex; max-width: 100%;"><defs><path stroke-width="0" id="E2-MJMAIN-2203" d="M56 661T56 674T70 694H487Q497 686 500 679V15Q497 10 487 1L279 0H70Q56 7 56 20T70 40H460V327H84Q70 334 70 347T84 367H460V654H70Q56 661 56 674Z"></path><path stroke-width="0" id="E2-MJMATHI-78" d="M52 289Q59 331 106 386T222 442Q257 442 286 424T329 379Q371 442 430 442Q467 442 494 420T522 361Q522 332 508 314T481 292T458 288Q439 288 427 299T415 328Q415 374 465 391Q454 404 425 404Q412 404 406 402Q368 386 350 336Q290 115 290 78Q290 50 306 38T341 26Q378 26 414 59T463 140Q466 150 469 151T485 153H489Q504 153 504 145Q504 144 502 134Q486 77 440 33T333 -11Q263 -11 227 52Q186 -10 133 -10H127Q78 -10 57 16T35 71Q35 103 54 123T99 143Q142 143 142 101Q142 81 130 66T107 46T94 41L91 40Q91 39 97 36T113 29T132 26Q168 26 194 71Q203 87 217 139T245 247T261 313Q266 340 266 352Q266 380 251 392T217 404Q177 404 142 372T93 290Q91 281 88 280T72 278H58Q52 284 52 289Z"></path><path stroke-width="0" id="E2-MJMAIN-2208" d="M84 250Q84 372 166 450T360 539Q361 539 377 539T419 540T469 540H568Q583 532 583 520Q583 511 570 501L466 500Q355 499 329 494Q280 482 242 458T183 409T147 354T129 306T124 272V270H568Q583 262 583 250T568 230H124V228Q124 207 134 177T167 112T231 48T328 7Q355 1 466 0H570Q583 -10 583 -20Q583 -32 568 -40H471Q464 -40 446 -40T417 -41Q262 -41 172 45Q84 127 84 250Z"></path><path stroke-width="0" id="E2-MJMATHI-50" d="M287 628Q287 635 230 637Q206 637 199 638T192 648Q192 649 194 659Q200 679 203 681T397 683Q587 682 600 680Q664 669 707 631T751 530Q751 453 685 389Q616 321 507 303Q500 302 402 301H307L277 182Q247 66 247 59Q247 55 248 54T255 50T272 48T305 46H336Q342 37 342 35Q342 19 335 5Q330 0 319 0Q316 0 282 1T182 2Q120 2 87 2T51 1Q33 1 33 11Q33 13 36 25Q40 41 44 43T67 46Q94 46 127 49Q141 52 146 61Q149 65 218 339T287 628ZM645 554Q645 567 643 575T634 597T609 619T560 635Q553 636 480 637Q463 637 445 637T416 636T404 636Q391 635 386 627Q384 621 367 550T332 412T314 344Q314 342 395 342H407H430Q542 342 590 392Q617 419 631 471T645 554Z"></path><path stroke-width="0" id="E2-MJMAIN-2E" d="M78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path><path stroke-width="0" id="E2-MJMAIN-5B" d="M118 -250V750H255V710H158V-210H255V-250H118Z"></path><path stroke-width="0" id="E2-MJMATHI-44" d="M287 628Q287 635 230 637Q207 637 200 638T193 647Q193 655 197 667T204 682Q206 683 403 683Q570 682 590 682T630 676Q702 659 752 597T803 431Q803 275 696 151T444 3L430 1L236 0H125H72Q48 0 41 2T33 11Q33 13 36 25Q40 41 44 43T67 46Q94 46 127 49Q141 52 146 61Q149 65 218 339T287 628ZM703 469Q703 507 692 537T666 584T629 613T590 629T555 636Q553 636 541 636T512 636T479 637H436Q392 637 386 627Q384 623 313 339T242 52Q242 48 253 48T330 47Q335 47 349 47T373 46Q499 46 581 128Q617 164 640 212T683 339T703 469Z"></path><path stroke-width="0" id="E2-MJMAIN-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path stroke-width="0" id="E2-MJMAIN-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path stroke-width="0" id="E2-MJMATHI-79" d="M21 287Q21 301 36 335T84 406T158 442Q199 442 224 419T250 355Q248 336 247 334Q247 331 231 288T198 191T182 105Q182 62 196 45T238 27Q261 27 281 38T312 61T339 94Q339 95 344 114T358 173T377 247Q415 397 419 404Q432 431 462 431Q475 431 483 424T494 412T496 403Q496 390 447 193T391 -23Q363 -106 294 -155T156 -205Q111 -205 77 -183T43 -117Q43 -95 50 -80T69 -58T89 -48T106 -45Q150 -45 150 -87Q150 -107 138 -122T115 -142T102 -147L99 -148Q101 -153 118 -160T152 -167H160Q177 -167 186 -165Q219 -156 247 -127T290 -65T313 -9T321 21L315 17Q309 13 296 6T270 -6Q250 -11 231 -11Q185 -11 150 11T104 82Q103 89 103 113Q103 170 138 262T173 379Q173 380 173 381Q173 390 173 393T169 400T158 404H154Q131 404 112 385T82 344T65 302T57 280Q55 278 41 278H27Q21 284 21 287Z"></path><path stroke-width="0" id="E2-MJMAIN-5D" d="M22 710V750H159V-250H22V-210H119V710H22Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="matrix(1 0 0 -1 0 0)"><use xlink:href="#E2-MJMAIN-2203" x="0" y="0"></use><g transform="translate(556,0)"><use xlink:href="#E2-MJMATHI-78" x="0" y="0"></use><use xlink:href="#E2-MJMAIN-2208" x="849" y="0"></use><use xlink:href="#E2-MJMATHI-50" x="1794" y="0"></use></g><use xlink:href="#E2-MJMAIN-2E" x="3101" y="0"></use><g transform="translate(3546,0)"><use xlink:href="#E2-MJMAIN-5B" x="0" y="0"></use><use xlink:href="#E2-MJMATHI-44" x="278" y="0"></use><use xlink:href="#E2-MJMAIN-28" x="1106" y="0"></use><use xlink:href="#E2-MJMATHI-78" x="1495" y="0"></use><use xlink:href="#E2-MJMAIN-29" x="2067" y="0"></use><use xlink:href="#E2-MJMAIN-2208" x="2733" y="0"></use><use xlink:href="#E2-MJMATHI-50" x="3678" y="0"></use><use xlink:href="#E2-MJMAIN-2E" x="4429" y="0"></use><use xlink:href="#E2-MJMATHI-44" x="4874" y="0"></use><use xlink:href="#E2-MJMAIN-28" x="5702" y="0"></use><use xlink:href="#E2-MJMATHI-79" x="6091" y="0"></use><use xlink:href="#E2-MJMAIN-29" x="6588" y="0"></use><use xlink:href="#E2-MJMAIN-5D" x="6977" y="0"></use></g><use xlink:href="#E2-MJMAIN-2E" x="10968" y="0"></use></g></svg></span></div><script type="math/tex; mode=display" id="MathJax-Element-2">\exists{x \in P}. \left[D(x) \in P. D(y)\right].</script></div></div><p>The non-formal verbal proof is remarkably simple to understand. Here's the quote from Wikipedia:</p><blockquote><p>The proof begins by recognizing it is true that either everyone in the pub is drinking, or at least one person in the pub is not drinking. Consequently, there are two cases to consider:[<a href='https://en.wikipedia.org/wiki/Drinker_paradox#cite_note-Smullyan-1'>1]</a>[<a href='https://en.wikipedia.org/wiki/Drinker_paradox#cite_note-Images_of_SMC_Research_1996-2'>2]</a></p><ol start='' ><li>Suppose everyone is drinking. For any particular person, it cannot be wrong to say that <em>if that particular person is drinking, then everyone in the pub is drinking</em> — because everyone is drinking. Because everyone is drinking, then that one person must drink because when <em>that person</em> drinks <em>everybody</em> drinks, everybody includes that person.</li><li>Otherwise at least one person is not drinking. For any nondrinking person, the statement <em>if that particular person is drinking, then everyone in the pub is drinking</em> is formally true: its <a href='https://en.wikipedia.org/wiki/Antecedent_(logic)'>antecedent</a> ("that particular person is drinking") is false, therefore the statement is true due to the nature of <a href='https://en.wikipedia.org/wiki/Material_conditional#Definition'>material implication</a> in formal logic, which states that "If P, then Q" is always true if P is false.[<a href='https://en.wikipedia.org/wiki/Drinker_paradox#cite_note-Smullyan-1'>1]</a>[<a href='https://en.wikipedia.org/wiki/Drinker_paradox#cite_note-Images_of_SMC_Research_1996-2'>2]</a> (These kinds of statements are said to be <a href='https://en.wikipedia.org/wiki/Vacuous_truth'>vacuously true</a>.)</li></ol></blockquote><p>In this post, I will:</p><ul><li>articulate a bit on the "paradoxical" part of the problem</li><li>describe my way of proving it with Curry–Howard correspondence (or <a href='https://ncatlab.org/nlab/show/Brouwer-Heyting-Kolmogorov+interpretation'>Brouwer-Heyting-Kolmogorov interpretation</a>, if you like) in <a href='https://github.com/mortberg/cubicaltt'>cubicaltt</a></li><li>mention few things which were discovered as a pleasant surprise as I went along</li></ul><h2><a name='header-n23' class='md-header-anchor '></a>Paradoxiness</h2><p>There are few peculiar things about this paradox. First, it isn't really a paradox, there's only a paradox-ish part about it. The part is that linguistically, it seems like the person is causing everyone else to drink somehow, whereas in reality, what is stated is that you can always find a person, such that it just so happens that everyone else is drinking along. To make a similar statement not involving conscious agents: "every day, I can find a person, such that, if that person is up, then the sun is up". This doesn't mean that the sun follows some person's actions. What we see is a principle named <a href='https://en.wikipedia.org/wiki/Correlation_does_not_imply_causation'>Correlation does not imply causation</a>.</p><h2><a name='header-n25' class='md-header-anchor '></a>Stating it via Propositions-as-Types</h2><p>Let's start with the hardest part, getting the theorem statement precisely and correctly:</p><pre spellcheck="false" class="md-fences md-end-block ty-contain-cm modeLoaded" lang="haskell"><div class="CodeMirror cm-s-inner CodeMirror-wrap" lang="haskell"><div style="overflow: hidden; position: relative; width: 3px; height: 0px; top: 0px; left: 4px;"><textarea autocorrect="off" autocapitalize="off" spellcheck="false" tabindex="0" style="position: absolute; bottom: -1em; padding: 0px; width: 1000px; height: 1em; outline: none;"></textarea></div><div class="CodeMirror-scrollbar-filler" cm-not-content="true"></div><div class="CodeMirror-gutter-filler" cm-not-content="true"></div><div class="CodeMirror-scroll" tabindex="-1"><div class="CodeMirror-sizer" style="margin-left: 0px; margin-bottom: 0px; border-right-width: 0px; padding-right: 0px; padding-bottom: 0px;"><div style="position: relative; top: 0px;"><div class="CodeMirror-lines" role="presentation"><div role="presentation" style="position: relative; outline: none;"><div class="CodeMirror-measure"></div><div class="CodeMirror-measure"></div><div style="position: relative; z-index: 1;"></div><div class="CodeMirror-code" role="presentation" style=""><div class="CodeMirror-activeline" style="position: relative;"><div class="CodeMirror-activeline-background CodeMirror-linebackground"></div><div class="CodeMirror-gutter-background CodeMirror-activeline-gutter" style="left: 0px; width: 0px;"></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">drinker</span></span></pre></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>) <span class="cm-comment">-- [1]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">D</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span> <span class="cm-keyword">-></span> <span class="cm-variable-2">U</span>) <span class="cm-comment">-- [2]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-comment">-- [3]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">:</span> ( (<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-comment">-- [4]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-builtin">*</span> ((<span class="cm-variable">y</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>) <span class="cm-comment">-- [5]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">-></span> (<span class="cm-variable">z</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-comment">-- [6]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">z</span> <span class="cm-comment">-- [7]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> )</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> )</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-builtin">undefined</span></span></pre></div></div></div></div></div><div style="position: absolute; height: 0px; width: 1px; border-bottom-width: 0px; border-bottom-style: solid; border-bottom-color: transparent; top: 242px;"></div><div class="CodeMirror-gutters" style="display: none; height: 242px;"></div></div></div></pre><ul><li><strong>[1]</strong>: <code>A</code> is the type of all drinkers</li><li><strong>[2]</strong>: <code>D</code> is the property meaning "is drinking"</li><li><strong>[3]</strong>: I didn't have the <code>x : A</code> present at first, it was needed later as I went along, but it makes total sense, since we need the bar to have at least one person, otherwise the theorem wouldn't make sense. In other words, our type must be <strong>inhabited</strong></li><li><strong>[4]</strong>: I will return you a specific person</li><li><strong>[5]</strong>: and a function, which states, that given a fact that person is drinking</li><li><strong>[6]</strong>: for any person in the bar</li><li><strong>[7]</strong>: I will prove that that person is drinking</li></ul><h2><a name='header-n43' class='md-header-anchor '></a>Proving it: All or Counter-example</h2><p>Not knowing what else can I do, I decided to follow the verbal proof, stated in the beginning. So, we need to begin by stating "either everyone is drinking, or there's someone who is not":</p><pre spellcheck="false" class="md-fences md-end-block ty-contain-cm modeLoaded" lang="haskell" style="page-break-inside: unset;"><div class="CodeMirror cm-s-inner CodeMirror-wrap" lang="haskell"><div style="overflow: hidden; position: relative; width: 3px; height: 0px; top: 0px; left: 4px;"><textarea autocorrect="off" autocapitalize="off" spellcheck="false" tabindex="0" style="position: absolute; bottom: -1em; padding: 0px; width: 1000px; height: 1em; outline: none;"></textarea></div><div class="CodeMirror-scrollbar-filler" cm-not-content="true"></div><div class="CodeMirror-gutter-filler" cm-not-content="true"></div><div class="CodeMirror-scroll" tabindex="-1"><div class="CodeMirror-sizer" style="margin-left: 0px; margin-bottom: 0px; border-right-width: 0px; padding-right: 0px; padding-bottom: 0px;"><div style="position: relative; top: 0px;"><div class="CodeMirror-lines" role="presentation"><div role="presentation" style="position: relative; outline: none;"><div class="CodeMirror-measure"><span><span></span>x</span></div><div class="CodeMirror-measure"></div><div style="position: relative; z-index: 1;"></div><div class="CodeMirror-code" role="presentation" style=""><div class="CodeMirror-activeline" style="position: relative;"><div class="CodeMirror-activeline-background CodeMirror-linebackground"></div><div class="CodeMirror-gutter-background CodeMirror-activeline-gutter" style="left: 0px; width: 0px;"></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-keyword">data</span> <span class="cm-variable-2">N0</span> <span class="cm-keyword">=</span> <span class="cm-comment">-- [1]</span></span></pre></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span cm-text=""></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-comment">-- [2]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">neg</span> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>) <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span> <span class="cm-keyword">=</span> <span class="cm-variable-2">A</span> <span class="cm-keyword">-></span> <span class="cm-variable-2">N0</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span cm-text=""></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-comment">-- [3]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-keyword">data</span> <span class="cm-builtin">or</span> (<span class="cm-variable-2">A</span> <span class="cm-variable-2">B</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-variable">inl</span> (<span class="cm-variable">a</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-variable">|</span> <span class="cm-variable">inr</span> (<span class="cm-variable">b</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">B</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span cm-text=""></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-comment">-- [4]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">allOrCounterex</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">D</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span> <span class="cm-keyword">-></span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">:</span> (<span class="cm-builtin">or</span> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>) <span class="cm-comment">-- [5]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-builtin">*</span> (<span class="cm-variable">neg</span> (<span class="cm-variable-2">D</span> <span class="cm-variable">x</span>))) <span class="cm-comment">-- [6]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> )</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-builtin">undefined</span></span></pre></div></div></div></div></div><div style="position: absolute; height: 0px; width: 1px; border-bottom-width: 0px; border-bottom-style: solid; border-bottom-color: transparent; top: 396px;"></div><div class="CodeMirror-gutters" style="display: none; height: 396px;"></div></div></div></pre><ul><li><strong>[1]</strong>: the "impossible", or "absurd" type, we cannot construct its value. Copied from prelude.ctt</li><li><strong>[2]</strong>: negation in "propositions-as-types" mathematics is done via giving a function that returns absurd given that value. Copied from prelude.ctt</li><li><strong>[3]</strong>: good old <code>Either</code> type. Copied from prelude.ctt</li><li><strong>[4]</strong>: notice how all this function needs is the type and the property, no "real values" (it should work for non-inhabited types)</li><li><strong>[5]</strong> you either get <code>inl</code> with "for all <code>x:A</code>, I'll prove they're drinking"</li><li><strong>[6]</strong>: or you get <code>inr</code> with specific person <code>x:A</code>, and a proof they aren't (<code>neg (D x)</code>)</li></ul><p>We'll get back to the actual implementation later, let us first see if we can actually use this for the full proof.</p><h2><a name='header-n60' class='md-header-anchor '></a>Finishing the drinker</h2><p>We need to case-split on the <code>allOrCounterex</code> result, let's create a continuation doing that:</p><pre spellcheck="false" class="md-fences md-end-block ty-contain-cm modeLoaded" lang="haskell" style="page-break-inside: unset;"><div class="CodeMirror cm-s-inner CodeMirror-wrap" lang="haskell"><div style="overflow: hidden; position: relative; width: 3px; height: 0px; top: 0px; left: 4px;"><textarea autocorrect="off" autocapitalize="off" spellcheck="false" tabindex="0" style="position: absolute; bottom: -1em; padding: 0px; width: 1000px; height: 1em; outline: none;"></textarea></div><div class="CodeMirror-scrollbar-filler" cm-not-content="true"></div><div class="CodeMirror-gutter-filler" cm-not-content="true"></div><div class="CodeMirror-scroll" tabindex="-1"><div class="CodeMirror-sizer" style="margin-left: 0px; margin-bottom: 0px; border-right-width: 0px; padding-right: 0px; padding-bottom: 0px;"><div style="position: relative; top: 0px;"><div class="CodeMirror-lines" role="presentation"><div role="presentation" style="position: relative; outline: none;"><div class="CodeMirror-measure"><pre><span>xxxxxxxxxx</span></pre></div><div class="CodeMirror-measure"></div><div style="position: relative; z-index: 1;"></div><div class="CodeMirror-code" role="presentation" style=""><div class="CodeMirror-activeline" style="position: relative;"><div class="CodeMirror-activeline-background CodeMirror-linebackground"></div><div class="CodeMirror-gutter-background CodeMirror-activeline-gutter" style="left: 0px; width: 0px;"></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-comment">-- [1]</span></span></pre></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">efq</span> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>) <span class="cm-keyword">:</span> <span class="cm-variable-2">N0</span> <span class="cm-keyword">-></span> <span class="cm-variable-2">A</span> <span class="cm-keyword">=</span> <span class="cm-variable">split</span> {}</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span cm-text=""></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-comment">-- [2]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">drinkerC1</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">D</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span> <span class="cm-keyword">-></span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">:</span> (<span class="cm-builtin">or</span> ((<span class="cm-variable">q</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">q</span>) <span class="cm-comment">-- [3]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> ((<span class="cm-variable">q</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-builtin">*</span> (<span class="cm-variable">neg</span> (<span class="cm-variable-2">D</span> <span class="cm-variable">q</span>))))</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">-></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> ( (<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-builtin">*</span> ((<span class="cm-variable">y</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">-></span> (<span class="cm-variable">z</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">z</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> )</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> )</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-variable">split</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-variable">inl</span> <span class="cm-variable">allD</span> <span class="cm-keyword">-></span> <span class="cm-comment">-- [4]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> ( <span class="cm-variable">x</span> <span class="cm-comment">-- [5]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> , (<span class="cm-keyword">\</span>(<span class="cm-keyword">_</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>) <span class="cm-keyword">-></span> <span class="cm-comment">-- [6]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">\</span>(<span class="cm-variable">z</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-comment">-- [7]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-variable">allD</span> <span class="cm-variable">z</span>))</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-variable">inr</span> <span class="cm-variable">pair</span> <span class="cm-keyword">-></span> <span class="cm-comment">-- [8]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> ( <span class="cm-variable">pair</span><span class="cm-builtin">.</span><span class="cm-number">1</span> <span class="cm-comment">-- [9]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> , <span class="cm-keyword">\</span>(<span class="cm-variable">y</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">D</span> <span class="cm-variable">pair</span><span class="cm-builtin">.</span><span class="cm-number">1</span>) <span class="cm-keyword">-></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">\</span>(<span class="cm-variable">z</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-variable">efq</span> (<span class="cm-variable-2">D</span> <span class="cm-variable">z</span>) (<span class="cm-variable">pair</span><span class="cm-builtin">.</span><span class="cm-number">2</span> <span class="cm-variable">y</span>)) <span class="cm-comment">-- [10]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span cm-text=""></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">drinker</span> <span class="cm-keyword">..</span><span class="cm-builtin">.</span> <span class="cm-keyword">=</span> <span class="cm-variable">drinkerC1</span> <span class="cm-variable-2">A</span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span> (<span class="cm-variable">allOrCounterex</span> <span class="cm-variable-2">A</span> <span class="cm-variable-2">D</span>)</span></pre></div></div></div></div></div><div style="position: absolute; height: 0px; width: 1px; border-bottom-width: 0px; border-bottom-style: solid; border-bottom-color: transparent; top: 660px;"></div><div class="CodeMirror-gutters" style="display: none; height: 660px;"></div></div></div></pre><ul><li><strong>[1]</strong>: We'll need this in our proof. Given an absurd value (which can never be constructed!), I can prove anything. This is akin to saying "which is impossible because earlier we've shown the opposite xyz, leading to contradiction" in your verbal proof. Copied from prelude.ctt</li><li><strong>[2]</strong>: function's signature is copied from <code>drinker</code>, and we only add the first parameter in its return type</li><li><strong>[3]</strong>: here's that parameter, which is an alpha-renamed result from <code>allOrConterex</code></li><li><strong>[4]</strong>: branch when everybody's drinking</li><li><strong>[5]</strong>: then any person can suite as a proof, so let's take the inhabitant</li><li><strong>[6]</strong>: we're not interested in the fact he is drinking (we know that)</li><li><strong>[7]</strong>: we're just passing the <code>allD</code> to prove that everyone's drinking</li><li><strong>[8]</strong>: in "not everyone's drinking" case, where we get a specific person and a proof they're not drinking</li><li><strong>[9]</strong>: we return that person as "the answer"</li><li><strong>[10]</strong>: the most interesting part. We need to prove "if that person's drinking, everybody else does", but we've got our "they are not drinking" value, so we pass "that person is drinking" (<code>y</code>) to the "that person is <strong>not</strong> drinking" function (<code>pair.2</code>), and get an absurd, from which we can prove anything (via <code>efq</code>)</li></ul><h2><a name='header-n84' class='md-header-anchor '></a>De Morgan</h2><p>This was satisfying already, but now there is another problem that's bugging: the whole "either everyone is drinking, or somebody is not" sounds terrifically obvious to the listener, but is this a fundamental claim? Doesn't sound like an axiom or a law to me, it feels like we can break this down a bit more.</p><p>I started searching for the drinker's solution on the internet and came up to the post called <a href='http://math.andrej.com/2014/05/08/seemingly-impossible-proofs/'>Seemingly impossible constructive proofs</a>, which had another one, called <a href='http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/'>Seemingly impossible functional programs</a> before it. It seemed unrelated at first, but I decided to give the "functional programs" one a go before I switch to the main thing. It turned out rewarding, indeed.</p><p>In that post, something that caught my eye was this:</p><pre spellcheck="false" class="md-fences md-end-block ty-contain-cm modeLoaded" lang="haskell"><div class="CodeMirror cm-s-inner CodeMirror-wrap" lang="haskell"><div style="overflow: hidden; position: relative; width: 3px; height: 0px; top: 0px; left: 4px;"><textarea autocorrect="off" autocapitalize="off" spellcheck="false" tabindex="0" style="position: absolute; bottom: -1em; padding: 0px; width: 1000px; height: 1em; outline: none;"></textarea></div><div class="CodeMirror-scrollbar-filler" cm-not-content="true"></div><div class="CodeMirror-gutter-filler" cm-not-content="true"></div><div class="CodeMirror-scroll" tabindex="-1"><div class="CodeMirror-sizer" style="margin-left: 0px; margin-bottom: 0px; border-right-width: 0px; padding-right: 0px; padding-bottom: 0px;"><div style="position: relative; top: 0px;"><div class="CodeMirror-lines" role="presentation"><div role="presentation" style="position: relative; outline: none;"><div class="CodeMirror-measure"><pre><span>xxxxxxxxxx</span></pre></div><div class="CodeMirror-measure"></div><div style="position: relative; z-index: 1;"></div><div class="CodeMirror-code" role="presentation"><div class="CodeMirror-activeline" style="position: relative;"><div class="CodeMirror-activeline-background CodeMirror-linebackground"></div><div class="CodeMirror-gutter-background CodeMirror-activeline-gutter" style="left: 0px; width: 0px;"></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-builtin">></span> <span class="cm-variable">forevery</span> <span class="cm-variable">p</span> <span class="cm-keyword">=</span> <span class="cm-builtin">not</span>(<span class="cm-variable">forsome</span>(<span class="cm-keyword">\</span><span class="cm-variable">a</span> <span class="cm-keyword">-></span> <span class="cm-builtin">not</span>(<span class="cm-variable">p</span> <span class="cm-variable">a</span>)))</span></pre></div></div></div></div></div></div><div style="position: absolute; height: 0px; width: 1px; border-bottom-width: 0px; border-bottom-style: solid; border-bottom-color: transparent; top: 22px;"></div><div class="CodeMirror-gutters" style="display: none; height: 22px;"></div></div></div></pre><p>An implementation of "for every", using "for some". It also explicitly links the <a href='https://en.wikipedia.org/wiki/De_Morgan%27s_laws'>De Morgan's Laws</a> page.</p><p>Now, I was aware of the whole De Morgan thing related to conjunctions, disjunctions, and negations, but completely forgot (or did I not know?) about its use for the quantifiers! Here are the laws for conjunction and disjunction:</p><div contenteditable="false" spellcheck="false" class="mathjax-block md-end-block md-math-block md-rawblock" id="mathjax-n91" cid="n91" mdtype="math_block">
<div class="md-rawblock-container md-math-container" tabindex="-1"><div class="MathJax_SVG_Display"><span class="MathJax_SVG" id="MathJax-Element-3-Frame" tabindex="-1" style="font-size: 100%; display: inline-block;"><svg xmlns:xlink="http://www.w3.org/1999/xlink" width="828.5069580078125px" height="51.614585876464844px" viewBox="0 -838.5 41923.7 2611.9" role="img" focusable="false" style="vertical-align: -4.119ex; max-width: 100%;"><defs><path stroke-width="0" id="E3-MJMAIN-AC" d="M56 323T56 336T70 356H596Q603 353 611 343V102Q598 89 591 89Q587 89 584 90T579 94T575 98T572 102L571 209V316H70Q56 323 56 336Z"></path><path stroke-width="0" id="E3-MJMAIN-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path stroke-width="0" id="E3-MJMATHI-50" d="M287 628Q287 635 230 637Q206 637 199 638T192 648Q192 649 194 659Q200 679 203 681T397 683Q587 682 600 680Q664 669 707 631T751 530Q751 453 685 389Q616 321 507 303Q500 302 402 301H307L277 182Q247 66 247 59Q247 55 248 54T255 50T272 48T305 46H336Q342 37 342 35Q342 19 335 5Q330 0 319 0Q316 0 282 1T182 2Q120 2 87 2T51 1Q33 1 33 11Q33 13 36 25Q40 41 44 43T67 46Q94 46 127 49Q141 52 146 61Q149 65 218 339T287 628ZM645 554Q645 567 643 575T634 597T609 619T560 635Q553 636 480 637Q463 637 445 637T416 636T404 636Q391 635 386 627Q384 621 367 550T332 412T314 344Q314 342 395 342H407H430Q542 342 590 392Q617 419 631 471T645 554Z"></path><path stroke-width="0" id="E3-MJMAIN-2227" d="M318 591Q325 598 333 598Q344 598 348 591Q349 590 414 445T545 151T611 -4Q609 -22 591 -22Q588 -22 586 -21T581 -20T577 -17T575 -13T572 -9T570 -4L333 528L96 -4Q87 -20 80 -21Q78 -22 75 -22Q57 -22 55 -4Q55 2 120 150T251 444T318 591Z"></path><path stroke-width="0" id="E3-MJMATHI-51" d="M399 -80Q399 -47 400 -30T402 -11V-7L387 -11Q341 -22 303 -22Q208 -22 138 35T51 201Q50 209 50 244Q50 346 98 438T227 601Q351 704 476 704Q514 704 524 703Q621 689 680 617T740 435Q740 255 592 107Q529 47 461 16L444 8V3Q444 2 449 -24T470 -66T516 -82Q551 -82 583 -60T625 -3Q631 11 638 11Q647 11 649 2Q649 -6 639 -34T611 -100T557 -165T481 -194Q399 -194 399 -87V-80ZM636 468Q636 523 621 564T580 625T530 655T477 665Q429 665 379 640Q277 591 215 464T153 216Q153 110 207 59Q231 38 236 38V46Q236 86 269 120T347 155Q372 155 390 144T417 114T429 82T435 55L448 64Q512 108 557 185T619 334T636 468ZM314 18Q362 18 404 39L403 49Q399 104 366 115Q354 117 347 117Q344 117 341 117T337 118Q317 118 296 98T274 52Q274 18 314 18Z"></path><path stroke-width="0" id="E3-MJMAIN-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path stroke-width="0" id="E3-MJMAIN-22A2" d="M55 678Q55 679 56 681T58 684T61 688T65 691T70 693T77 694Q88 692 95 679V367H540Q555 359 555 347Q555 334 540 327H95V15Q88 2 77 0Q73 0 70 1T65 3T61 6T59 9T57 13T55 16V678Z"></path><path stroke-width="0" id="E3-MJMAIN-2228" d="M55 580Q56 587 61 592T75 598Q86 598 96 580L333 48L570 580Q579 596 586 597Q588 598 591 598Q609 598 611 580Q611 574 546 426T415 132T348 -15Q343 -22 333 -22T318 -15Q317 -14 252 131T121 425T55 580Z"></path><path stroke-width="0" id="E3-MJMAIN-2E" d="M78 60Q78 84 95 102T138 120Q162 120 180 104T199 61Q199 36 182 18T139 0T96 17T78 60Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="matrix(1 0 0 -1 0 0)"><g transform="translate(15807,0)"><use xlink:href="#E3-MJMAIN-AC" x="0" y="0"></use><use xlink:href="#E3-MJMAIN-28" x="667" y="0"></use><use xlink:href="#E3-MJMATHI-50" x="1056" y="0"></use><use xlink:href="#E3-MJMAIN-2227" x="2029" y="0"></use><use xlink:href="#E3-MJMATHI-51" x="2918" y="0"></use><use xlink:href="#E3-MJMAIN-29" x="3709" y="0"></use><use xlink:href="#E3-MJMAIN-22A2" x="4376" y="0"></use><use xlink:href="#E3-MJMAIN-28" x="5264" y="0"></use><use xlink:href="#E3-MJMAIN-AC" x="5653" y="0"></use><use xlink:href="#E3-MJMATHI-50" x="6320" y="0"></use><use xlink:href="#E3-MJMAIN-2228" x="7294" y="0"></use><use xlink:href="#E3-MJMAIN-AC" x="8183" y="0"></use><use xlink:href="#E3-MJMATHI-51" x="8850" y="0"></use><use xlink:href="#E3-MJMAIN-29" x="9641" y="0"></use><use xlink:href="#E3-MJMAIN-2E" x="10030" y="0"></use></g><g transform="translate(15807,-1431)"><use xlink:href="#E3-MJMAIN-AC" x="0" y="0"></use><use xlink:href="#E3-MJMAIN-28" x="667" y="0"></use><use xlink:href="#E3-MJMATHI-50" x="1056" y="0"></use><use xlink:href="#E3-MJMAIN-2228" x="2029" y="0"></use><use xlink:href="#E3-MJMATHI-51" x="2918" y="0"></use><use xlink:href="#E3-MJMAIN-29" x="3709" y="0"></use><use xlink:href="#E3-MJMAIN-22A2" x="4376" y="0"></use><use xlink:href="#E3-MJMAIN-28" x="5264" y="0"></use><use xlink:href="#E3-MJMAIN-AC" x="5653" y="0"></use><use xlink:href="#E3-MJMATHI-50" x="6320" y="0"></use><use xlink:href="#E3-MJMAIN-2227" x="7294" y="0"></use><use xlink:href="#E3-MJMAIN-AC" x="8183" y="0"></use><use xlink:href="#E3-MJMATHI-51" x="8850" y="0"></use><use xlink:href="#E3-MJMAIN-29" x="9641" y="0"></use><use xlink:href="#E3-MJMAIN-2E" x="10030" y="0"></use></g></g></svg></span></div><script type="math/tex; mode=display" id="MathJax-Element-3">\neg(P \land Q) \vdash (\neg P \lor \neg Q).\\
\neg(P \lor Q) \vdash (\neg P \land \neg Q).</script></div></div><p>And here they are for quantifiers:</p><div contenteditable="false" spellcheck="false" class="mathjax-block md-end-block md-math-block md-rawblock" id="mathjax-n93" cid="n93" mdtype="math_block">
<div class="md-rawblock-container md-math-container" tabindex="-1"><div class="MathJax_SVG_Display"><span class="MathJax_SVG" id="MathJax-Element-4-Frame" tabindex="-1" style="font-size: 100%; display: inline-block;"><svg xmlns:xlink="http://www.w3.org/1999/xlink" width="828.5069580078125px" height="51.614585876464844px" viewBox="0 -838.5 41923.7 2611.9" role="img" focusable="false" style="vertical-align: -4.119ex; max-width: 100%;"><defs><path stroke-width="0" id="E4-MJMAIN-2200" d="M0 673Q0 684 7 689T20 694Q32 694 38 680T82 567L126 451H430L473 566Q483 593 494 622T512 668T519 685Q524 694 538 694Q556 692 556 674Q556 670 426 329T293 -15Q288 -22 278 -22T263 -15Q260 -11 131 328T0 673ZM414 410Q414 411 278 411T142 410L278 55L414 410Z"></path><path stroke-width="0" id="E4-MJMATHI-78" d="M52 289Q59 331 106 386T222 442Q257 442 286 424T329 379Q371 442 430 442Q467 442 494 420T522 361Q522 332 508 314T481 292T458 288Q439 288 427 299T415 328Q415 374 465 391Q454 404 425 404Q412 404 406 402Q368 386 350 336Q290 115 290 78Q290 50 306 38T341 26Q378 26 414 59T463 140Q466 150 469 151T485 153H489Q504 153 504 145Q504 144 502 134Q486 77 440 33T333 -11Q263 -11 227 52Q186 -10 133 -10H127Q78 -10 57 16T35 71Q35 103 54 123T99 143Q142 143 142 101Q142 81 130 66T107 46T94 41L91 40Q91 39 97 36T113 29T132 26Q168 26 194 71Q203 87 217 139T245 247T261 313Q266 340 266 352Q266 380 251 392T217 404Q177 404 142 372T93 290Q91 281 88 280T72 278H58Q52 284 52 289Z"></path><path stroke-width="0" id="E4-MJMATHI-50" d="M287 628Q287 635 230 637Q206 637 199 638T192 648Q192 649 194 659Q200 679 203 681T397 683Q587 682 600 680Q664 669 707 631T751 530Q751 453 685 389Q616 321 507 303Q500 302 402 301H307L277 182Q247 66 247 59Q247 55 248 54T255 50T272 48T305 46H336Q342 37 342 35Q342 19 335 5Q330 0 319 0Q316 0 282 1T182 2Q120 2 87 2T51 1Q33 1 33 11Q33 13 36 25Q40 41 44 43T67 46Q94 46 127 49Q141 52 146 61Q149 65 218 339T287 628ZM645 554Q645 567 643 575T634 597T609 619T560 635Q553 636 480 637Q463 637 445 637T416 636T404 636Q391 635 386 627Q384 621 367 550T332 412T314 344Q314 342 395 342H407H430Q542 342 590 392Q617 419 631 471T645 554Z"></path><path stroke-width="0" id="E4-MJMAIN-28" d="M94 250Q94 319 104 381T127 488T164 576T202 643T244 695T277 729T302 750H315H319Q333 750 333 741Q333 738 316 720T275 667T226 581T184 443T167 250T184 58T225 -81T274 -167T316 -220T333 -241Q333 -250 318 -250H315H302L274 -226Q180 -141 137 -14T94 250Z"></path><path stroke-width="0" id="E4-MJMAIN-29" d="M60 749L64 750Q69 750 74 750H86L114 726Q208 641 251 514T294 250Q294 182 284 119T261 12T224 -76T186 -143T145 -194T113 -227T90 -246Q87 -249 86 -250H74Q66 -250 63 -250T58 -247T55 -238Q56 -237 66 -225Q221 -64 221 250T66 725Q56 737 55 738Q55 746 60 749Z"></path><path stroke-width="0" id="E4-MJMAIN-2261" d="M56 444Q56 457 70 464H707Q722 456 722 444Q722 430 706 424H72Q56 429 56 444ZM56 237T56 250T70 270H707Q722 262 722 250T707 230H70Q56 237 56 250ZM56 56Q56 71 72 76H706Q722 70 722 56Q722 44 707 36H70Q56 43 56 56Z"></path><path stroke-width="0" id="E4-MJMAIN-AC" d="M56 323T56 336T70 356H596Q603 353 611 343V102Q598 89 591 89Q587 89 584 90T579 94T575 98T572 102L571 209V316H70Q56 323 56 336Z"></path><path stroke-width="0" id="E4-MJMAIN-5B" d="M118 -250V750H255V710H158V-210H255V-250H118Z"></path><path stroke-width="0" id="E4-MJMAIN-2203" d="M56 661T56 674T70 694H487Q497 686 500 679V15Q497 10 487 1L279 0H70Q56 7 56 20T70 40H460V327H84Q70 334 70 347T84 367H460V654H70Q56 661 56 674Z"></path><path stroke-width="0" id="E4-MJMAIN-5D" d="M22 710V750H159V-250H22V-210H119V710H22Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="matrix(1 0 0 -1 0 0)"><g transform="translate(15954,0)"><use xlink:href="#E4-MJMAIN-2200" x="0" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="556" y="0"></use><use xlink:href="#E4-MJMATHI-50" x="1294" y="0"></use><use xlink:href="#E4-MJMAIN-28" x="2045" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="2434" y="0"></use><use xlink:href="#E4-MJMAIN-29" x="3006" y="0"></use><use xlink:href="#E4-MJMAIN-2261" x="3673" y="0"></use><use xlink:href="#E4-MJMAIN-AC" x="4729" y="0"></use><use xlink:href="#E4-MJMAIN-5B" x="5396" y="0"></use><use xlink:href="#E4-MJMAIN-2203" x="5674" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="6230" y="0"></use><use xlink:href="#E4-MJMAIN-AC" x="6968" y="0"></use><use xlink:href="#E4-MJMATHI-50" x="7635" y="0"></use><use xlink:href="#E4-MJMAIN-28" x="8386" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="8775" y="0"></use><use xlink:href="#E4-MJMAIN-29" x="9347" y="0"></use><use xlink:href="#E4-MJMAIN-5D" x="9736" y="0"></use></g><g transform="translate(15954,-1431)"><use xlink:href="#E4-MJMAIN-2203" x="0" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="556" y="0"></use><use xlink:href="#E4-MJMATHI-50" x="1294" y="0"></use><use xlink:href="#E4-MJMAIN-28" x="2045" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="2434" y="0"></use><use xlink:href="#E4-MJMAIN-29" x="3006" y="0"></use><use xlink:href="#E4-MJMAIN-2261" x="3673" y="0"></use><use xlink:href="#E4-MJMAIN-AC" x="4729" y="0"></use><use xlink:href="#E4-MJMAIN-5B" x="5396" y="0"></use><use xlink:href="#E4-MJMAIN-2200" x="5674" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="6230" y="0"></use><use xlink:href="#E4-MJMAIN-AC" x="6968" y="0"></use><use xlink:href="#E4-MJMATHI-50" x="7635" y="0"></use><use xlink:href="#E4-MJMAIN-28" x="8386" y="0"></use><use xlink:href="#E4-MJMATHI-78" x="8775" y="0"></use><use xlink:href="#E4-MJMAIN-29" x="9347" y="0"></use><use xlink:href="#E4-MJMAIN-5D" x="9736" y="0"></use></g></g></svg></span></div><script type="math/tex; mode=display" id="MathJax-Element-4">\forall x \, P(x) \equiv \neg [ \exists x \, \neg P(x)]\\
\exists x \, P(x) \equiv \neg [ \forall x \, \neg P(x)]</script></div></div><p>And it makes total sense when you think about it. "All things hold" is the same as "not (some thing doesn't)". "Something holds" is the same as "not (all thing do)".</p><pre spellcheck="false" class="md-fences md-end-block ty-contain-cm modeLoaded" lang="haskell"><div class="CodeMirror cm-s-inner CodeMirror-wrap" lang="haskell"><div style="overflow: hidden; position: relative; width: 3px; height: 0px; top: 0px; left: 4px;"><textarea autocorrect="off" autocapitalize="off" spellcheck="false" tabindex="0" style="position: absolute; bottom: -1em; padding: 0px; width: 1000px; height: 1em; outline: none;"></textarea></div><div class="CodeMirror-scrollbar-filler" cm-not-content="true"></div><div class="CodeMirror-gutter-filler" cm-not-content="true"></div><div class="CodeMirror-scroll" tabindex="-1"><div class="CodeMirror-sizer" style="margin-left: 0px; margin-bottom: 0px; border-right-width: 0px; padding-right: 0px; padding-bottom: 0px;"><div style="position: relative; top: 0px;"><div class="CodeMirror-lines" role="presentation"><div role="presentation" style="position: relative; outline: none;"><div class="CodeMirror-measure"><pre><span>xxxxxxxxxx</span></pre></div><div class="CodeMirror-measure"></div><div style="position: relative; z-index: 1;"></div><div class="CodeMirror-code" role="presentation" style=""><div class="CodeMirror-activeline" style="position: relative;"><div class="CodeMirror-activeline-background CodeMirror-linebackground"></div><div class="CodeMirror-gutter-background CodeMirror-activeline-gutter" style="left: 0px; width: 0px;"></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">deMorgan</span></span></pre></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">D</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span> <span class="cm-keyword">-></span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">:</span> (<span class="cm-variable">neg</span> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>)) <span class="cm-comment">-- [1]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">-></span> ( (<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-comment">-- [2]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-builtin">*</span> (<span class="cm-variable">neg</span> (<span class="cm-variable-2">D</span> <span class="cm-variable">x</span>)))</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-builtin">undefined</span></span></pre></div></div></div></div></div><div style="position: absolute; height: 0px; width: 1px; border-bottom-width: 0px; border-bottom-style: solid; border-bottom-color: transparent; top: 154px;"></div><div class="CodeMirror-gutters" style="display: none; height: 154px;"></div></div></div></pre><ul><li><strong>[1]</strong>: if we were to have a "not everyone's drinking" statement</li><li><strong>[2]</strong>: then we could turn it into a "there exists a person, for whom we'd give a proof they're not drinking"</li></ul><p>This gives us a hint on how to get from "not everyone's drinking" branch to a useful dependent pair, but not a complete solution yet. What's missing?</p><h2><a name='header-n102' class='md-header-anchor '></a>Law of Excluded Middle</h2><p>What's missing is a way to get something out of thin air. The notorious law of excluded middle, a constructivist's nightmare:</p><pre spellcheck="false" class="md-fences md-end-block ty-contain-cm modeLoaded" lang="haskell"><div class="CodeMirror cm-s-inner CodeMirror-wrap" lang="haskell"><div style="overflow: hidden; position: relative; width: 3px; height: 0px; top: 0px; left: 4px;"><textarea autocorrect="off" autocapitalize="off" spellcheck="false" tabindex="0" style="position: absolute; bottom: -1em; padding: 0px; width: 1000px; height: 1em; outline: none;"></textarea></div><div class="CodeMirror-scrollbar-filler" cm-not-content="true"></div><div class="CodeMirror-gutter-filler" cm-not-content="true"></div><div class="CodeMirror-scroll" tabindex="-1"><div class="CodeMirror-sizer" style="margin-left: 0px; margin-bottom: 0px; border-right-width: 0px; padding-right: 0px; padding-bottom: 0px;"><div style="position: relative; top: 0px;"><div class="CodeMirror-lines" role="presentation"><div role="presentation" style="position: relative; outline: none;"><div class="CodeMirror-measure"><pre><span>xxxxxxxxxx</span></pre></div><div class="CodeMirror-measure"></div><div style="position: relative; z-index: 1;"></div><div class="CodeMirror-code" role="presentation"><div class="CodeMirror-activeline" style="position: relative;"><div class="CodeMirror-activeline-background CodeMirror-linebackground"></div><div class="CodeMirror-gutter-background CodeMirror-activeline-gutter" style="left: 0px; width: 0px;"></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">lem</span> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>)</span></pre></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">:</span> <span class="cm-builtin">or</span> <span class="cm-variable-2">A</span> (<span class="cm-variable">neg</span> <span class="cm-variable-2">A</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-builtin">undefined</span></span></pre></div></div></div></div></div><div style="position: absolute; height: 0px; width: 1px; border-bottom-width: 0px; border-bottom-style: solid; border-bottom-color: transparent; top: 66px;"></div><div class="CodeMirror-gutters" style="display: none; height: 66px;"></div></div></div></pre><p>Using <code>lem</code>, we can make our first case-splitting continuation on <code>allOrCounterex</code> and finish the proof:</p><pre spellcheck="false" class="md-fences md-end-block ty-contain-cm modeLoaded" lang="haskell" style="page-break-inside: unset;"><div class="CodeMirror cm-s-inner CodeMirror-wrap" lang="haskell"><div style="overflow: hidden; position: relative; width: 3px; height: 0px; top: 0px; left: 4px;"><textarea autocorrect="off" autocapitalize="off" spellcheck="false" tabindex="0" style="position: absolute; bottom: -1em; padding: 0px; width: 1000px; height: 1em; outline: none;"></textarea></div><div class="CodeMirror-scrollbar-filler" cm-not-content="true"></div><div class="CodeMirror-gutter-filler" cm-not-content="true"></div><div class="CodeMirror-scroll" tabindex="-1"><div class="CodeMirror-sizer" style="margin-left: 0px; margin-bottom: 0px; border-right-width: 0px; padding-right: 0px; padding-bottom: 0px;"><div style="position: relative; top: 0px;"><div class="CodeMirror-lines" role="presentation"><div role="presentation" style="position: relative; outline: none;"><div class="CodeMirror-measure"><pre><span>xxxxxxxxxx</span></pre></div><div class="CodeMirror-measure"></div><div style="position: relative; z-index: 1;"></div><div class="CodeMirror-code" role="presentation" style=""><div class="CodeMirror-activeline" style="position: relative;"><div class="CodeMirror-activeline-background CodeMirror-linebackground"></div><div class="CodeMirror-gutter-background CodeMirror-activeline-gutter" style="left: 0px; width: 0px;"></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">allOrCounterexC1</span></span></pre></div><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">A</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable-2">D</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span> <span class="cm-keyword">-></span> <span class="cm-variable-2">U</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">:</span> (<span class="cm-variable">lem</span> <span class="cm-keyword">:</span> <span class="cm-builtin">or</span> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable">neg</span> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>)))</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">-></span> (<span class="cm-builtin">or</span> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>)</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-builtin">*</span> (<span class="cm-variable">neg</span> (<span class="cm-variable-2">D</span> <span class="cm-variable">x</span>))))</span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-variable">split</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-variable">inl</span> <span class="cm-variable">f</span> <span class="cm-keyword">-></span> <span class="cm-variable">inl</span> <span class="cm-variable">f</span> <span class="cm-comment">-- [1]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-variable">inr</span> <span class="cm-variable">f</span> <span class="cm-keyword">-></span> <span class="cm-variable">inr</span> (<span class="cm-variable">deMorgan</span> <span class="cm-variable-2">A</span> <span class="cm-variable-2">D</span> <span class="cm-variable">f</span>) <span class="cm-comment">-- [2]</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span cm-text=""></span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"><span class="cm-variable">allOrCounterex</span> <span class="cm-keyword">..</span><span class="cm-builtin">.</span></span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> <span class="cm-keyword">=</span> <span class="cm-variable">allOrCounterexC1</span> <span class="cm-variable-2">A</span> <span class="cm-variable-2">D</span> </span></pre><pre class=" CodeMirror-line " role="presentation"><span role="presentation" style="padding-right: 0.1px;"> (<span class="cm-variable">lem</span> ((<span class="cm-variable">x</span> <span class="cm-keyword">:</span> <span class="cm-variable-2">A</span>) <span class="cm-keyword">-></span> <span class="cm-variable-2">D</span> <span class="cm-variable">x</span>)) <span class="cm-comment">-- [3]</span></span></pre></div></div></div></div></div><div style="position: absolute; height: 0px; width: 1px; border-bottom-width: 0px; border-bottom-style: solid; border-bottom-color: transparent; top: 308px;"></div><div class="CodeMirror-gutters" style="display: none; height: 308px;"></div></div></div></pre><ul><li><strong>[1]</strong>: "everyone's drinking" branch fits ideally as is</li><li><strong>[2]</strong>: "not (everyone's drinking)" is translated via <code>deMorgan</code> introduced earlier, precisely matching what we need</li><li><strong>[3]</strong>: we use <code>lem</code>, passing a type meaning "everyone's drinking", which constructs the <code>or</code> we split upon</li></ul><p>Voila!</p><h2><a name='header-n115' class='md-header-anchor '></a>Summary</h2><p>In this post:</p><ul><li>we've seen the usage of absurd type <code>N0</code>, the notion of negation (<code>neg</code>), "prove by absurdity" (<code>efq</code>), good old <code>or</code> type</li><li>introduced an explicit use of LEM only when we needed it</li><li>introduced De Morgan's law for quantifiers, jumping from "forall" statement to "there exists" one</li><li>had an exercise in proving things via "propositions as types" concept, formally</li></ul><p>Well, that's one drinking problem less in my life. Pass that scotch&beer, let's celebrate! 🥃🍺</p><p>Full source code can be found in <a href='./drinker/drinker.ctt'>drinker.ctt</a>.</p><p>Please send your feedback in Issues or PRs in <a href='https://github.com/k-bx/k-bx.github.io'>this blog's repo</a>.</p></div>
</body>
</html>