-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpropositions_and_proofs.html
702 lines (611 loc) · 47.6 KB
/
propositions_and_proofs.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
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
<!DOCTYPE HTML>
<html lang="zh" class="sidebar-visible no-js light">
<head>
<!-- Book generated using mdBook -->
<meta charset="UTF-8">
<title>命题和证明 - Lean定理证明</title>
<!-- Custom HTML head -->
<meta name="description" content="">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="theme-color" content="#ffffff" />
<link rel="icon" href="favicon.svg">
<link rel="shortcut icon" href="favicon.png">
<link rel="stylesheet" href="css/variables.css">
<link rel="stylesheet" href="css/general.css">
<link rel="stylesheet" href="css/chrome.css">
<link rel="stylesheet" href="css/print.css" media="print">
<!-- Fonts -->
<link rel="stylesheet" href="FontAwesome/css/font-awesome.css">
<link rel="stylesheet" href="fonts/fonts.css">
<!-- Highlight.js Stylesheets -->
<link rel="stylesheet" href="highlight.css">
<link rel="stylesheet" href="tomorrow-night.css">
<link rel="stylesheet" href="ayu-highlight.css">
<!-- Custom theme stylesheets -->
</head>
<body>
<div id="body-container">
<!-- Provide site root to javascript -->
<script>
var path_to_root = "";
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
</script>
<!-- Work around some values being stored in localStorage wrapped in quotes -->
<script>
try {
var theme = localStorage.getItem('mdbook-theme');
var sidebar = localStorage.getItem('mdbook-sidebar');
if (theme.startsWith('"') && theme.endsWith('"')) {
localStorage.setItem('mdbook-theme', theme.slice(1, theme.length - 1));
}
if (sidebar.startsWith('"') && sidebar.endsWith('"')) {
localStorage.setItem('mdbook-sidebar', sidebar.slice(1, sidebar.length - 1));
}
} catch (e) { }
</script>
<!-- Set the theme before any content is loaded, prevents flash -->
<script>
var theme;
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
if (theme === null || theme === undefined) { theme = default_theme; }
var html = document.querySelector('html');
html.classList.remove('no-js')
html.classList.remove('light')
html.classList.add(theme);
html.classList.add('js');
</script>
<!-- Hide / unhide sidebar before it is displayed -->
<script>
var html = document.querySelector('html');
var sidebar = null;
if (document.body.clientWidth >= 1080) {
try { sidebar = localStorage.getItem('mdbook-sidebar'); } catch(e) { }
sidebar = sidebar || 'visible';
} else {
sidebar = 'hidden';
}
html.classList.remove('sidebar-visible');
html.classList.add("sidebar-" + sidebar);
</script>
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded affix "><a href="title_page.html">Lean 4定理证明</a></li><li class="chapter-item expanded "><a href="introduction.html"><strong aria-hidden="true">1.</strong> 介绍</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="setup.html"><strong aria-hidden="true">1.1.</strong> 安装</a></li></ol></li><li class="chapter-item expanded "><a href="dependent_type_theory.html"><strong aria-hidden="true">2.</strong> 依值类型论</a></li><li class="chapter-item expanded "><a href="propositions_and_proofs.html" class="active"><strong aria-hidden="true">3.</strong> 命题和证明</a></li><li class="chapter-item expanded "><a href="quantifiers_and_equality.html"><strong aria-hidden="true">4.</strong> 量词与等价</a></li><li class="chapter-item expanded "><a href="tactics.html"><strong aria-hidden="true">5.</strong> 证明策略</a></li><li class="chapter-item expanded "><a href="interacting_with_lean.html"><strong aria-hidden="true">6.</strong> 使用Lean进行工作</a></li><li class="chapter-item expanded "><a href="inductive_types.html"><strong aria-hidden="true">7.</strong> 归纳类型</a></li><li class="chapter-item expanded "><a href="induction_and_recursion.html"><strong aria-hidden="true">8.</strong> Induction and Recursion</a></li><li class="chapter-item expanded "><a href="structures_and_records.html"><strong aria-hidden="true">9.</strong> 结构体和记录</a></li><li class="chapter-item expanded "><a href="type_classes.html"><strong aria-hidden="true">10.</strong> Type Classes</a></li><li class="chapter-item expanded "><a href="conv.html"><strong aria-hidden="true">11.</strong> 转换策略模式</a></li><li class="chapter-item expanded "><a href="axioms_and_computation.html"><strong aria-hidden="true">12.</strong> Axioms and Computation</a></li><li class="chapter-item expanded "><a href="glossary.html"><strong aria-hidden="true">13.</strong> 术语表</a></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle"></div>
</nav>
<!-- Track and set sidebar scroll position -->
<script>
var sidebarScrollbox = document.querySelector('#sidebar .sidebar-scrollbox');
sidebarScrollbox.addEventListener('click', function(e) {
if (e.target.tagName === 'A') {
sessionStorage.setItem('sidebar-scroll', sidebarScrollbox.scrollTop);
}
}, { passive: true });
var sidebarScrollTop = sessionStorage.getItem('sidebar-scroll');
sessionStorage.removeItem('sidebar-scroll');
if (sidebarScrollTop) {
// preserve sidebar scroll position when navigating via links within sidebar
sidebarScrollbox.scrollTop = sidebarScrollTop;
} else {
// scroll sidebar to current active section when navigating via "next/previous chapter" buttons
var activeSection = document.querySelector('#sidebar .active');
if (activeSection) {
activeSection.scrollIntoView({ block: 'center' });
}
}
</script>
<div id="page-wrapper" class="page-wrapper">
<div class="page">
<div id="menu-bar-hover-placeholder"></div>
<div id="menu-bar" class="menu-bar sticky">
<div class="left-buttons">
<button id="sidebar-toggle" class="icon-button" type="button" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
<i class="fa fa-bars"></i>
</button>
<button id="theme-toggle" class="icon-button" type="button" title="Change theme" aria-label="Change theme" aria-haspopup="true" aria-expanded="false" aria-controls="theme-list">
<i class="fa fa-paint-brush"></i>
</button>
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
<li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
</ul>
<button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
<i class="fa fa-search"></i>
</button>
</div>
<h1 class="menu-title">Lean定理证明</h1>
<div class="right-buttons">
<a href="print.html" title="Print this book" aria-label="Print this book">
<i id="print-button" class="fa fa-print"></i>
</a>
<a href="https://github.com/subfish-zhou/theorem_proving_in_lean4_zh_CN" title="Git repository" aria-label="Git repository">
<i id="git-repository-button" class="fa fa-github"></i>
</a>
</div>
</div>
<div id="search-wrapper" class="hidden">
<form id="searchbar-outer" class="searchbar-outer">
<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
</form>
<div id="searchresults-outer" class="searchresults-outer hidden">
<div id="searchresults-header" class="searchresults-header"></div>
<ul id="searchresults">
</ul>
</div>
</div>
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
<script>
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
link.setAttribute('tabIndex', sidebar === 'visible' ? 0 : -1);
});
</script>
<div id="content" class="content">
<main>
<h1 id="命题和证明"><a class="header" href="#命题和证明">命题和证明</a></h1>
<p>本项目已迁移到 <a href="https://github.com/Lean-zh/tp-lean-zh/"> https://github.com/Lean-zh/tp-lean-zh/ </a></p>
<p>网页地址 <a href="https://www.leanprover.cn/tp-lean-zh/"> https://www.leanprover.cn/tp-lean-zh/ </a></p>
<p>本仓库已弃用</p>
<p>前一章你已经看到了在Lean中定义对象和函数的一些方法。在本章中，我们还将开始解释如何用依值类型论的语言来编写数学命题和证明。</p>
<h2 id="命题即类型"><a class="header" href="#命题即类型">命题即类型</a></h2>
<p>证明在依值类型论语言中定义的对象的断言（assertion）的一种策略是在定义语言之上分层断言语言和证明语言。但是，没有理由以这种方式重复使用多种语言：依值类型论是灵活和富有表现力的，我们也没有理由不能在同一个总框架中表示断言和证明。</p>
<p>例如，我们可引入一种新类型<code>Prop</code>，来表示命题，然后引入用其他命题构造新命题的构造子。</p>
<pre><code class="language-lean">def Implies (p q : Prop) : Prop := p → q
#check And -- Prop → Prop → Prop
#check Or -- Prop → Prop → Prop
#check Not -- Prop → Prop
#check Implies -- Prop → Prop → Prop
variable (p q r : Prop)
#check And p q -- Prop
#check Or (And p q) r -- Prop
#check Implies (And p q) (And q p) -- Prop
</code></pre>
<p>对每个元素<code>p : Prop</code>，可以引入另一个类型<code>Proof p</code>，作为<code>p</code>的证明的类型。“公理”是这个类型中的常值。</p>
<pre><code class="language-lean">structure Proof (p : Prop) : Type where
proof : p
#check Proof -- Proof : Prop → Type
axiom and_comm (p q : Prop) : Proof (Implies (And p q) (And q p))
variable (p q : Prop)
#check and_comm p q -- Proof (Implies (And p q) (And q p))
</code></pre>
<p>然而，除了公理之外，我们还需要从旧证明中建立新证明的规则。例如，在许多命题逻辑的证明系统中，我们有肯定前件式（modus ponens）推理规则:</p>
<blockquote>
<p>如果能证明<code>Implies p q</code>和<code>p</code>，则能证明<code>q</code>。</p>
</blockquote>
<p>我们可以如下地表示它：</p>
<pre><code class="language-lean">axiom modus_ponens : (p q : Prop) → Proof (Implies p q) → Proof p → Proof q
</code></pre>
<p>命题逻辑的自然演绎系统通常也依赖于以下规则：</p>
<blockquote>
<p>当假设<code>p</code>成立时，如果我们能证明<code>q</code>. 则我们能证明<code>Implies p q</code>.</p>
</blockquote>
<p>我们可以如下地表示它：</p>
<pre><code class="language-lean">axiom implies_intro : (p q : Prop) → (Proof p → Proof q) → Proof (Implies p q)
</code></pre>
<p>这个功能让我们可以合理地搭建断言和证明。确定表达式<code>t</code>是<code>p</code>的证明，只需检查<code>t</code>具有类型<code>Proof p</code>。</p>
<p>可以做一些简化。首先，我们可以通过将<code>Proof p</code>和<code>p</code>本身合并来避免重复地写<code>Proof</code>这个词。换句话说，只要我们有<code>p : Prop</code>，我们就可以把<code>p</code>解释为一种类型，也就是它的证明类型。然后我们可以把<code>t : p</code>读作<code>t</code>是<code>p</code>的证明。</p>
<p>此外，我们可以在<code>Implies p q</code>和<code>p → q</code>之间来回切换。换句话说，命题<code>p</code>和<code>q</code>之间的含义对应于一个函数，它将<code>p</code>的任何元素接受为<code>q</code>的一个元素。因此，引入连接词<code>Implies</code>是完全多余的：我们可以使用依值类型论中常见的函数空间构造子<code>p → q</code>作为我们的蕴含概念。</p>
<p>这是在构造演算（Calculus of Constructions）中遵循的方法，因此在Lean中也是如此。自然演绎证明系统中的蕴含规则与控制函数抽象（abstraction）和应用（application）的规则完全一致，这是<em>Curry-Howard同构</em>的一个实例，有时也被称为<em>命题即类型</em>。事实上，类型<code>Prop</code>是上一章描述的类型层次结构的最底部<code>Sort 0</code>的语法糖。此外，<code>Type u</code>也只是<code>Sort (u+1)</code>的语法糖。<code>Prop</code>有一些特殊的特性，但像其他类型宇宙一样，它在箭头构造子下是封闭的:如果我们有<code>p q : Prop</code>，那么<code>p → q : Prop</code>。</p>
<p>至少有两种将命题作为类型来思考的方法。对于那些对逻辑和数学中的构造主义者来说，这是对命题含义的忠实诠释：命题<code>p</code>代表了一种数据类型，即构成证明的数据类型的说明。<code>p</code>的证明就是正确类型的对象<code>t : p</code>。</p>
<p>非构造主义者可以把它看作是一种简单的编码技巧。对于每个命题<code>p</code>，我们关联一个类型，如果<code>p</code>为假，则该类型为空，如果<code>p</code>为真，则有且只有一个元素，比如<code>*</code>。在后一种情况中，让我们说(与之相关的类型)<code>p</code>被<em>占据</em>（inhabited）。恰好，函数应用和抽象的规则可以方便地帮助我们跟踪<code>Prop</code>的哪些元素是被占据的。所以构造一个元素<code>t : p</code>告诉我们<code>p</code>确实是正确的。你可以把<code>p</code>的占据者想象成“<code>p</code>为真”的事实。对<code>p → q</code>的证明使用“<code>p</code>是真的”这个事实来得到“<code>q</code>是真的”这个事实。</p>
<p>事实上，如果<code>p : Prop</code>是任何命题，那么Lean的内核将任意两个元素<code>t1 t2 : p</code>看作定义相等，就像它把<code>(fun x => t) s</code>和<code>t[s/x]</code>看作定义等价。这就是所谓的“证明无关性”（proof irrelevance）。这意味着，即使我们可以把证明<code>t : p</code>当作依值类型论语言中的普通对象，它们除了<code>p</code>是真的这一事实之外，没有其他信息。</p>
<p>我们所建议的思考“命题即类型”范式的两种方式在一个根本性的方面有所不同。从构造的角度看，证明是抽象的数学对象，它被依值类型论中的合适表达式所<em>表示</em>。相反，如果我们从上述编码技巧的角度考虑，那么表达式本身并不表示任何有趣的东西。相反，是我们可以写下它们并检查它们是否有良好的类型这一事实确保了有关命题是真的。换句话说，表达式<em>本身</em>就是证明。</p>
<p>在下面的论述中，我们将在这两种说话方式之间来回切换，有时说一个表达式“构造”或“产生”或“返回”一个命题的证明，有时则简单地说它“是”这样一个证明。这类似于计算机科学家偶尔会模糊语法和语义之间的区别，有时说一个程序“计算”某个函数，有时又说该程序“是”该函数。</p>
<p>为了用依值类型论的语言正式表达一个数学断言，我们需要展示一个项<code>p : Prop</code>。为了<em>证明</em>该断言，我们需要展示一个项<code>t : p</code>。Lean的任务，作为一个证明助手，是帮助我们构造这样一个项<code>t</code>，并验证它的格式是否良好，类型是否正确。</p>
<h2 id="以命题即类型的方式工作"><a class="header" href="#以命题即类型的方式工作">以“命题即类型”的方式工作</a></h2>
<p>在“命题即类型”范式中，只涉及<code>→</code>的定理可以通过lambda抽象和应用来证明。在Lean中，<code>theorem</code>命令引入了一个新的定理：</p>
<pre><code class="language-lean">variable {p : Prop}
variable {q : Prop}
theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
</code></pre>
<p>这与上一章中常量函数的定义完全相同，唯一的区别是参数是<code>Prop</code>的元素，而不是<code>Type</code>的元素。直观地说，我们对<code>p → q → p</code>的证明假设<code>p</code>和<code>q</code>为真，并使用第一个假设(平凡地)建立结论<code>p</code>为真。</p>
<p>请注意，<code>theorem</code>命令实际上是<code>def</code>命令的一个翻版：在命题和类型对应下，证明定理<code>p → q → p</code>实际上与定义关联类型的元素是一样的。对于内核类型检查器，这两者之间没有区别。</p>
<p>然而，定义和定理之间有一些实用的区别。正常情况下，永远没有必要展开一个定理的“定义”；通过证明无关性，该定理的任何两个证明在定义上都是相等的。一旦一个定理的证明完成，通常我们只需要知道该证明的存在；证明是什么并不重要。鉴于这一事实，Lean将证明标记为<em>不可还原</em>（irreducible），作为对解析器（更确切地说，是<em>繁饰器</em>）的提示，在处理文件时一般不需要展开它。事实上，Lean通常能够并行地处理和检查证明，因为评估一个证明的正确性不需要知道另一个证明的细节。</p>
<p>和定义一样，<code>#print</code>命令可以展示一个定理的证明。</p>
<pre><code class="language-lean">theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
#print t1
</code></pre>
<p>注意，lambda抽象<code>hp : p</code>和<code>hq : q</code>可以被视为<code>t1</code>的证明中的临时假设。Lean还允许我们通过<code>show</code>语句明确指定最后一个项<code>hp</code>的类型。</p>
<pre><code class="language-lean">theorem t1 : p → q → p :=
fun hp : p =>
fun hq : q =>
show p from hp --试试改成 show q from hp 会怎样？
</code></pre>
<p>添加这些额外的信息可以提高证明的清晰度，并有助于在编写证明时发现错误。<code>show</code>命令只是注释类型，而且在内部，我们看到的所有关于<code>t1</code>的表示都产生了相同的项。</p>
<p>与普通定义一样，我们可以将lambda抽象的变量移到冒号的左边：</p>
<pre><code class="language-lean">theorem t1 (hp : p) (hq : q) : p := hp
#print t1 -- p → q → p
</code></pre>
<p>现在我们可以把定理<code>t1</code>作为一个函数应用。</p>
<pre><code class="language-lean">theorem t1 (hp : p) (hq : q) : p := hp
axiom hp : p
theorem t2 : q → p := t1 hp
</code></pre>
<p>这里，<code>axiom</code>声明假定存在给定类型的元素，因此可能会破坏逻辑一致性。例如，我们可以使用它来假设空类型<code>False</code>有一个元素：</p>
<pre><code class="language-lean">axiom unsound : False
-- false可导出一切
theorem ex : 1 = 0 :=
False.elim unsound
</code></pre>
<p>声明“公理”<code>hp : p</code>等同于声明<code>p</code>为真，正如<code>hp</code>所证明的那样。应用定理<code>t1 : p → q → p</code>到事实<code>hp : p</code>（也就是<code>p</code>为真）得到定理<code>t1 hp : q → p</code>。</p>
<p>回想一下，我们也可以这样写定理<code>t1</code>:</p>
<pre><code class="language-lean">theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp
#print t1
</code></pre>
<p><code>t1</code>的类型现在是<code>∀ {p q : Prop}, p → q → p</code>。我们可以把它理解为“对于每一对命题<code>p q</code>，我们都有<code>p → q → p</code>”。例如，我们可以将所有参数移到冒号的右边：</p>
<pre><code class="language-lean">theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q : Prop} (hp : p) (hq : q) => hp
</code></pre>
<p>如果<code>p</code>和<code>q</code>被声明为变量，Lean会自动为我们推广它们:</p>
<pre><code class="language-lean">variable {p q : Prop}
theorem t1 : p → q → p := fun (hp : p) (hq : q) => hp
</code></pre>
<p>事实上，通过命题即类型的对应关系，我们可以声明假设<code>hp</code>为<code>p</code>，作为另一个变量:</p>
<pre><code class="language-lean">variable {p q : Prop}
variable (hp : p)
theorem t1 : q → p := fun (hq : q) => hp
</code></pre>
<p>Lean检测到证明使用<code>hp</code>，并自动添加<code>hp : p</code>作为前提。在所有情况下，命令<code>#print t1</code>仍然会产生<code>∀ p q : Prop, p → q → p</code>。这个类型也可以写成<code>∀ (p q : Prop) (hp : p) (hq :q), p</code>，因为箭头仅仅表示一个箭头类型，其中目标不依赖于约束变量。</p>
<p>当我们以这种方式推广<code>t1</code>时，我们就可以将它应用于不同的命题对，从而得到一般定理的不同实例。</p>
<pre><code class="language-lean">theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp
variable (p q r s : Prop)
#check t1 p q -- p → q → p
#check t1 r s -- r → s → r
#check t1 (r → s) (s → r) -- (r → s) → (s → r) → r → s
variable (h : r → s)
#check t1 (r → s) (s → r) h -- (s → r) → r → s
</code></pre>
<p>同样，使用命题即类型对应，类型为<code>r → s</code>的变量<code>h</code>可以看作是<code>r → s</code>存在的假设或前提。</p>
<p>作为另一个例子，让我们考虑上一章讨论的组合函数，现在用命题代替类型。</p>
<pre><code class="language-lean">variable (p q r s : Prop)
theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=
fun h₃ : p =>
show r from h₁ (h₂ h₃)
</code></pre>
<p>作为一个命题逻辑定理，<code>t2</code>是什么意思？</p>
<p>注意，数字unicode下标输入方式为<code>\0</code>，<code>\1</code>，<code>\2</code>，...。</p>
<h2 id="命题逻辑"><a class="header" href="#命题逻辑">命题逻辑</a></h2>
<p>Lean定义了所有标准的逻辑连接词和符号。命题连接词有以下表示法:</p>
<div class="table-wrapper"><table><thead><tr><th>Ascii</th><th>Unicode</th><th>编辑器缩写</th><th>定义</th></tr></thead><tbody>
<tr><td>True</td><td></td><td></td><td>True</td></tr>
<tr><td>False</td><td></td><td></td><td>False</td></tr>
<tr><td>Not</td><td>¬</td><td><code>\not</code>, <code>\neg</code></td><td>Not</td></tr>
<tr><td>/\</td><td>∧</td><td><code>\and</code></td><td>And</td></tr>
<tr><td>\/</td><td>∨</td><td><code>\or</code></td><td>Or</td></tr>
<tr><td>-></td><td>→</td><td><code>\to</code>, <code>\r</code>, <code>\imp</code></td><td></td></tr>
<tr><td><-></td><td>↔</td><td><code>\iff</code>, <code>\lr</code></td><td>Iff</td></tr>
</tbody></table>
</div>
<p>它们都接收<code>Prop</code>值。</p>
<pre><code class="language-lean">variable (p q : Prop)
#check p → q → p ∧ q
#check ¬p → p ↔ False
#check p ∨ q → q ∨ p
</code></pre>
<p>操作符的优先级如下：<code>¬ > ∧ > ∨ > → > ↔</code>。举例：<code>a ∧ b → c ∨ d ∧ e</code>意为<code>(a ∧ b) → (c ∨ (d ∧ e))</code>。<code>→</code>等二元关系是右结合的。所以如果我们有<code>p q r : Prop</code>，表达式<code>p → q → r</code>读作“如果<code>p</code>，那么如果<code>q</code>，那么<code>r</code>”。这是<code>p ∧ q → r</code>的柯里化形式。</p>
<p>在上一章中，我们观察到lambda抽象可以被看作是<code>→</code>的“引入规则”，展示了如何“引入”或建立一个蕴含。应用可以看作是一个“消去规则”，展示了如何在证明中“消去”或使用一个蕴含。其他的命题连接词在Lean的库<code>Prelude.core</code>文件中定义。(参见<a href="./interacting_with_lean.html#_importing_files">导入文件</a>以获得关于库层次结构的更多信息)，并且每个连接都带有其规范引入和消去规则。</p>
<h3 id="合取"><a class="header" href="#合取">合取</a></h3>
<p>表达式<code>And.intro h1 h2</code>是<code>p ∧ q</code>的证明，它使用了<code>h1 : p</code>和<code>h2 : q</code>的证明。通常把<code>And.intro</code>称为<em>合取引入</em>规则。下面的例子我们使用<code>And.intro</code>来创建<code>p → q → p ∧ q</code>的证明。</p>
<pre><code class="language-lean">variable (p q : Prop)
example (hp : p) (hq : q) : p ∧ q := And.intro hp hq
#check fun (hp : p) (hq : q) => And.intro hp hq
</code></pre>
<p><code>example</code>命令声明了一个没有名字也不会永久保存的定理。本质上，它只是检查给定项是否具有指定的类型。它便于说明，我们将经常使用它。</p>
<p>表达式<code>And.left h</code>从<code>h : p ∧ q</code>建立了一个<code>p</code>的证明。类似地，<code>And.right h</code>是<code>q</code>的证明。它们常被称为左或右<em>合取消去</em>规则。</p>
<pre><code class="language-lean">variable (p q : Prop)
example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h
</code></pre>
<p>我们现在可以证明<code>p ∧ q → q ∧ p</code>：</p>
<pre><code class="language-lean">variable (p q : Prop)
example (h : p ∧ q) : q ∧ p :=
And.intro (And.right h) (And.left h)
</code></pre>
<p>请注意，引入和消去与笛卡尔积的配对和投影操作类似。区别在于，给定<code>hp : p</code>和<code>hq : q</code>，<code>And.intro hp hq</code>具有类型<code>p ∧ q : Prop</code>，而<code>Prod hp hq</code>具有类型<code>p × q : Type</code>。<code>∧</code>和<code>×</code>之间的相似性是Curry-Howard同构的另一个例子，但与蕴涵和函数空间构造子不同，在Lean中<code>∧</code>和<code>×</code>是分开处理的。然而，通过类比，我们刚刚构造的证明类似于交换一对中的元素的函数。</p>
<p>我们将在<a href="./structures_and_records.html">结构体和记录</a>一章中看到Lean中的某些类型是<em>Structures</em>，也就是说，该类型是用单个规范的<em>构造子</em>定义的，该构造子从一系列合适的参数构建该类型的一个元素。对于每一组<code>p q : Prop</code>， <code>p ∧ q</code>就是一个例子:构造一个元素的规范方法是将<code>And.intro</code>应用于合适的参数<code>hp : p</code>和<code>hq : q</code>。Lean允许我们使用<em>匿名构造子</em>表示法<code>⟨arg1, arg2, ...⟩</code>在此类情况下，当相关类型是归纳类型并可以从上下文推断时。特别地，我们经常可以写入<code>⟨hp, hq⟩</code>，而不是<code>And.intro hp hq</code>:</p>
<pre><code class="language-lean">variable (p q : Prop)
variable (hp : p) (hq : q)
#check (⟨hp, hq⟩ : p ∧ q)
</code></pre>
<p>尖括号可以用<code>\<</code>和<code>\></code>打出来。</p>
<p>Lean提供了另一个有用的语法小工具。给定一个归纳类型<code>Foo</code>的表达式<code>e</code>(可能应用于一些参数)，符号<code>e.bar</code>是<code>Foo.bar e</code>的缩写。这为访问函数提供了一种方便的方式，而无需打开名称空间。例如，下面两个表达的意思是相同的：</p>
<pre><code class="language-lean">variable (xs : List Nat)
#check List.length xs
#check xs.length
</code></pre>
<p>给定<code>h : p ∧ q</code>，我们可以写<code>h.left</code>来表示<code>And.left h</code>以及<code>h.right</code>来表示<code>And.right h</code>。因此我们可以简写上面的证明如下：</p>
<pre><code class="language-lean">variable (p q : Prop)
example (h : p ∧ q) : q ∧ p :=
⟨h.right, h.left⟩
</code></pre>
<p>在简洁和含混不清之间有一条微妙的界限，以这种方式省略信息有时会使证明更难阅读。但对于像上面这样简单的结构，当<code>h</code>的类型和结构的目标很突出时，符号是干净和有效的。</p>
<p>像<code>And.</code>这样的迭代结构是很常见的。Lean还允许你将嵌套的构造函数向右结合，这样这两个证明是等价的:</p>
<pre><code class="language-lean">variable (p q : Prop)
example (h : p ∧ q) : q ∧ p ∧ q:=
⟨h.right, ⟨h.left, h.right⟩⟩
example (h : p ∧ q) : q ∧ p ∧ q:=
⟨h.right, h.left, h.right⟩
</code></pre>
<p>这一点也很常用。</p>
<h3 id="析取"><a class="header" href="#析取">析取</a></h3>
<p>表达式<code>Or.intro_left q hp</code>从证明<code>hp : p</code>建立了<code>p ∨ q</code>的证明。类似地，<code>Or.intro_right p hq</code>从证明<code>hq : q</code>建立了<code>p ∨ q</code>的证明。这是左右析取引入规则。</p>
<pre><code class="language-lean">variable (p q : Prop)
example (hp : p) : p ∨ q := Or.intro_left q hp
example (hq : q) : p ∨ q := Or.intro_right p hq
</code></pre>
<p>析取消去规则稍微复杂一点。这个想法是，我们可以从<code>p ∨ q</code>证明<code>r</code>，通过从<code>p</code>证明<code>r</code>，且从<code>q</code>证明<code>r</code>。换句话说，它是一种逐情况证明。在表达式<code>Or.elim hpq hpr hqr</code>中，<code>Or.elim</code>接受三个论证，<code>hpq : p ∨ q</code>，<code>hpr : p → r</code>和<code>hqr : q → r</code>，生成<code>r</code>的证明。在下面的例子中，我们使用<code>Or.elim</code>证明<code>p ∨ q → q ∨ p</code>。</p>
<pre><code class="language-lean">variable (p q r : Prop)
example (h : p ∨ q) : q ∨ p :=
Or.elim h
(fun hp : p =>
show q ∨ p from Or.intro_right q hp)
(fun hq : q =>
show q ∨ p from Or.intro_left p hq)
</code></pre>
<p>在大多数情况下，<code>Or.intro_right</code>和<code>Or.intro_left</code>的第一个参数可以由Lean自动推断出来。因此，Lean提供了<code>Or.inr</code>和<code>Or.inl</code>作为<code>Or.intro_right _</code>和<code>Or.intro_left _</code>的缩写。因此，上面的证明项可以写得更简洁:</p>
<pre><code class="language-lean">variable (p q r : Prop)
example (h : p ∨ q) : q ∨ p :=
Or.elim h (fun hp => Or.inr hp) (fun hq => Or.inl hq)
</code></pre>
<p>Lean的完整表达式中有足够的信息来推断<code>hp</code>和<code>hq</code>的类型。但是在较长的版本中使用类型注释可以使证明更具可读性，并有助于捕获和调试错误。</p>
<p>因为<code>Or</code>有两个构造子，所以不能使用匿名构造子表示法。但我们仍然可以写<code>h.elim</code>而不是<code>Or.elim h</code>，不过你需要注意这些缩写是增强还是降低了可读性：</p>
<pre><code class="language-lean">variable (p q r : Prop)
example (h : p ∨ q) : q ∨ p :=
h.elim (fun hp => Or.inr hp) (fun hq => Or.inl hq)
</code></pre>
<h3 id="否定和假言"><a class="header" href="#否定和假言">否定和假言</a></h3>
<p>否定<code>¬p</code>真正的定义是<code>p → False</code>，所以我们通过从<code>p</code>导出一个矛盾来获得<code>¬p</code>。类似地，表达式<code>hnp hp</code>从<code>hp : p</code>和<code>hnp : ¬p</code>产生一个<code>False</code>的证明。下一个例子用所有这些规则来证明<code>(p → q) → ¬q → ¬p</code>。（<code>¬</code>符号可以由<code>\not</code>或者<code>\neg</code>来写出。）</p>
<pre><code class="language-lean">variable (p q : Prop)
example (hpq : p → q) (hnq : ¬q) : ¬p :=
fun hp : p =>
show False from hnq (hpq hp)
</code></pre>
<p>连接词<code>False</code>只有一个消去规则<code>False.elim</code>，它表达了一个事实，即矛盾能导出一切。这个规则有时被称为<em>ex falso</em> 【<em>ex falso sequitur quodlibet</em>（无稽之谈）的缩写】，或<em>爆炸原理</em>。</p>
<pre><code class="language-lean">variable (tp q : Prop)
example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp)
</code></pre>
<p>假命题导出任意的事实<code>q</code>，是<code>False.elim</code>的一个隐参数，而且是自动推断出来的。这种从相互矛盾的假设中推导出任意事实的模式很常见，用<code>absurd</code>来表示。</p>
<pre><code class="language-lean">variable (p q : Prop)
example (hp : p) (hnp : ¬p) : q := absurd hp hnp
</code></pre>
<p>证明<code>¬p → q → (q → p) → r</code>：</p>
<pre><code class="language-lean">variable (p q r : Prop)
example (hnp : ¬p) (hq : q) (hqp : q → p) : r :=
absurd (hqp hq) hnp
</code></pre>
<p>顺便说一句，就像<code>False</code>只有一个消去规则，<code>True</code>只有一个引入规则<code>True.intro : true</code>。换句话说，<code>True</code>就是真，并且有一个标准证明<code>True.intro</code>。</p>
<h3 id="逻辑等价"><a class="header" href="#逻辑等价">逻辑等价</a></h3>
<p>表达式<code>Iff.intro h1 h2</code>从<code>h1 : p → q</code>和<code>h2 : q → p</code>生成了<code>p ↔ q</code>的证明。表达式<code>Iff.mp h</code>从<code>h : p ↔ q</code>生成了<code>p → q</code>的证明。表达式<code>Iff.mpr h</code>从<code>h : p ↔ q</code>生成了<code>q → p</code>的证明。下面是<code>p ∧ q ↔ q ∧ p</code>的证明：</p>
<pre><code class="language-lean">variable (p q : Prop)
theorem and_swap : p ∧ q ↔ q ∧ p :=
Iff.intro
(fun h : p ∧ q =>
show q ∧ p from And.intro (And.right h) (And.left h))
(fun h : q ∧ p =>
show p ∧ q from And.intro (And.right h) (And.left h))
#check and_swap p q -- p ∧ q ↔ q ∧ p
variable (h : p ∧ q)
example : q ∧ p := Iff.mp (and_swap p q) h
</code></pre>
<p>我们可以用匿名构造子表示法来，从正反两个方向的证明，来构建<code>p ↔ q</code>的证明。我们也可以使用<code>.</code>符号连接<code>mp</code>和<code>mpr</code>。因此，前面的例子可以简写如下：</p>
<pre><code class="language-lean">variable (p q : Prop)
theorem and_swap : p ∧ q ↔ q ∧ p :=
⟨ fun h => ⟨h.right, h.left⟩, fun h => ⟨h.right, h.left⟩ ⟩
example (h : p ∧ q) : q ∧ p := (and_swap p q).mp h
</code></pre>
<h2 id="引入辅助子目标"><a class="header" href="#引入辅助子目标">引入辅助子目标</a></h2>
<p>这里介绍Lean提供的另一种帮助构造长证明的方法，即<code>have</code>结构，它在证明中引入了一个辅助的子目标。下面是一个小例子，改编自上一节:</p>
<pre><code class="language-lean">variable (p q : Prop)
example (h : p ∧ q) : q ∧ p :=
have hp : p := h.left
have hq : q := h.right
show q ∧ p from And.intro hq hp
</code></pre>
<p>在内部，表达式<code>have h : p := s; t</code>产生项<code>(fun (h : p) => t) s</code>。换句话说，<code>s</code>是<code>p</code>的证明，<code>t</code>是假设<code>h : p</code>的期望结论的证明，并且这两个是由lambda抽象和应用组合在一起的。这个简单的方法在构建长证明时非常有用，因为我们可以使用中间的<code>have</code>作为通向最终目标的垫脚石。</p>
<p>Lean还支持从目标向后推理的结构化方法，它模仿了普通数学文献中“足以说明某某”（suffices to show）的构造。下一个例子简单地排列了前面证明中的最后两行。</p>
<pre><code class="language-lean">variable (p q : Prop)
example (h : p ∧ q) : q ∧ p :=
have hp : p := h.left
suffices hq : q from And.intro hq hp
show q from And.right h
</code></pre>
<p><code>suffices hq : q</code>给出了两条目标。第一，我们需要证明，通过利用附加假设<code>hq : q</code>证明原目标<code>q ∧ p</code>，这样足以证明<code>q</code>，第二，我们需要证明<code>q</code>。</p>
<h2 id="经典逻辑"><a class="header" href="#经典逻辑">经典逻辑</a></h2>
<p>到目前为止，我们看到的引入和消去规则都是构造主义的，也就是说，它们反映了基于命题即类型对应的逻辑连接词的计算理解。普通经典逻辑在此基础上加上了排中律<code>p ∨ ¬p</code>（excluded middle, em）。要使用这个原则，你必须打开经典逻辑命名空间。</p>
<pre><code class="language-lean">open Classical
variable (p : Prop)
#check em p
</code></pre>
<p>从直觉上看，构造主义的“或”非常强：断言<code>p ∨ q</code>等于知道哪个是真实情况。如果<code>RH</code>代表黎曼猜想，经典数学家愿意断言<code>RH ∨ ¬RH</code>，即使我们还不能断言析取式的任何一端。</p>
<p>排中律的一个结果是双重否定消去规则（double-negation elimination, dne）:</p>
<pre><code class="language-lean">open Classical
theorem dne {p : Prop} (h : ¬¬p) : p :=
Or.elim (em p)
(fun hp : p => hp)
(fun hnp : ¬p => absurd hnp h)
</code></pre>
<p>双重否定消去规则给出了一种证明任何命题<code>p</code>的方法：通过假设<code>¬p</code>来推导出<code>false</code>，相当于证明了<code>p</code>。换句话说，双重否定消除允许反证法，这在构造主义逻辑中通常是不可能的。作为练习，你可以试着证明相反的情况，也就是说，证明<code>em</code>可以由<code>dne</code>证明。</p>
<p>经典公理还可以通过使用<code>em</code>让你获得额外的证明模式。例如，我们可以逐情况进行证明:</p>
<pre><code class="language-lean">open Classical
variable (p : Prop)
example (h : ¬¬p) : p :=
byCases
(fun h1 : p => h1)
(fun h1 : ¬p => absurd h1 h)
</code></pre>
<p>或者你可以用反证法来证明：</p>
<pre><code class="language-lean">open Classical
variable (p : Prop)
example (h : ¬¬p) : p :=
byContradiction
(fun h1 : ¬p =>
show False from h h1)
</code></pre>
<p>如果你不习惯构造主义，你可能需要一些时间来了解经典推理在哪里使用。在下面的例子中，它是必要的，因为从一个构造主义的观点来看，知道<code>p</code>和<code>q</code>不同时真并不一定告诉你哪一个是假的：</p>
<pre><code class="language-lean">open Classical
variable (p q : Prop)
-- BEGIN
example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
Or.elim (em p)
(fun hp : p =>
Or.inr
(show ¬q from
fun hq : q =>
h ⟨hp, hq⟩))
(fun hp : ¬p =>
Or.inl hp)
</code></pre>
<p>稍后我们将看到，构造逻辑中<em>有</em>某些情况允许“排中律”和“双重否定消除律”等，而Lean支持在这种情况下使用经典推理，而不依赖于排中律。</p>
<p>Lean中使用的公理的完整列表见<a href="./axioms_and_computation.html">公理与计算</a>。</p>
<h2 id="逻辑命题的例子"><a class="header" href="#逻辑命题的例子">逻辑命题的例子</a></h2>
<hr />
<p>Lean的标准库包含了许多命题逻辑的有效语句的证明，你可以自由地在自己的证明中使用这些证明。下面的列表包括一些常见的逻辑等价式。</p>
<p>交换律：</p>
<ol>
<li><code>p ∧ q ↔ q ∧ p</code></li>
<li><code>p ∨ q ↔ q ∨ p</code></li>
</ol>
<p>结合律：</p>
<ol start="3">
<li><code>(p ∧ q) ∧ r ↔ p ∧ (q ∧ r)</code></li>
<li><code>(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)</code></li>
</ol>
<p>分配律：</p>
<ol start="5">
<li><code>p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)</code></li>
<li><code>p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)</code></li>
</ol>
<p>其他性质：</p>
<ol>
<li><code>(p → (q → r)) ↔ (p ∧ q → r)</code></li>
<li><code>((p ∨ q) → r) ↔ (p → r) ∧ (q → r)</code></li>
<li><code>¬(p ∨ q) ↔ ¬p ∧ ¬q</code></li>
<li><code>¬p ∨ ¬q → ¬(p ∧ q)</code></li>
<li><code>¬(p ∧ ¬p)</code></li>
<li><code>p ∧ ¬q → ¬(p → q)</code></li>
<li><code>¬p → (p → q)</code></li>
<li><code>(¬p ∨ q) → (p → q)</code></li>
<li><code>p ∨ False ↔ p</code></li>
<li><code>p ∧ False ↔ False</code></li>
<li><code>¬(p ↔ ¬p)</code></li>
<li><code>(p → q) → (¬q → ¬p)</code></li>
</ol>
<p>经典推理：</p>
<ol start="19">
<li><code>(p → r ∨ s) → ((p → r) ∨ (p → s))</code></li>
<li><code>¬(p ∧ q) → ¬p ∨ ¬q</code></li>
<li><code>¬(p → q) → p ∧ ¬q</code></li>
<li><code>(p → q) → (¬p ∨ q)</code></li>
<li><code>(¬q → ¬p) → (p → q)</code></li>
<li><code>p ∨ ¬p</code></li>
<li><code>(((p → q) → p) → p)</code></li>
</ol>
<p><code>sorry</code>标识符神奇地生成任何东西的证明，或者提供任何数据类型的对象。当然，作为一种证明方法，它是不可靠的——例如，你可以使用它来证明<code>False</code>——并且当文件使用或导入依赖于它的定理时，Lean会产生严重的警告。但它对于增量地构建长证明非常有用。从上到下写证明，用<code>sorry</code>来填子证明。确保Lean接受所有的<code>sorry</code>；如果不是，则有一些错误需要纠正。然后返回，用实际的证据替换每个<code>sorry</code>，直到做完。</p>
<p>有另一个有用的技巧。你可以使用下划线<code>_</code>作为占位符，而不是<code>sorry</code>。回想一下，这告诉Lean该参数是隐式的，应该自动填充。如果Lean尝试这样做并失败了，它将返回一条错误消息“不知道如何合成占位符”（Don't know how to synthesize placeholder），然后是它所期望的项的类型，以及上下文中可用的所有对象和假设。换句话说，对于每个未解决的占位符，Lean报告在那一点上需要填充的子目标。然后，你可以通过递增填充这些占位符来构造一个证明。</p>
<p>这里有两个简单的证明例子作为参考。</p>
<pre><code class="language-lean">open Classical
-- 分配律
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
Iff.intro
(fun h : p ∧ (q ∨ r) =>
have hp : p := h.left
Or.elim (h.right)
(fun hq : q =>
show (p ∧ q) ∨ (p ∧ r) from Or.inl ⟨hp, hq⟩)
(fun hr : r =>
show (p ∧ q) ∨ (p ∧ r) from Or.inr ⟨hp, hr⟩))
(fun h : (p ∧ q) ∨ (p ∧ r) =>
Or.elim h
(fun hpq : p ∧ q =>
have hp : p := hpq.left
have hq : q := hpq.right
show p ∧ (q ∨ r) from ⟨hp, Or.inl hq⟩)
(fun hpr : p ∧ r =>
have hp : p := hpr.left
have hr : r := hpr.right
show p ∧ (q ∨ r) from ⟨hp, Or.inr hr⟩))
-- 需要一点经典推理的例子
example (p q : Prop) : ¬(p ∧ ¬q) → (p → q) :=
fun h : ¬(p ∧ ¬q) =>
fun hp : p =>
show q from
Or.elim (em q)
(fun hq : q => hq)
(fun hnq : ¬q => absurd (And.intro hp hnq) h)
</code></pre>
<h2 id="练习"><a class="header" href="#练习">练习</a></h2>
<p>证明以下等式，用真实证明取代“sorry”占位符。</p>
<pre><code class="language-lean">variable (p q r : Prop)
-- ∧ 和 ∨ 的交换律
example : p ∧ q ↔ q ∧ p := sorry
example : p ∨ q ↔ q ∨ p := sorry
-- ∧ 和 ∨ 的结合律
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry
-- 分配律
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry
-- 其他性质
example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry
example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry
example : ¬(p ∧ ¬p) := sorry
example : p ∧ ¬q → ¬(p → q) := sorry
example : ¬p → (p → q) := sorry
example : (¬p ∨ q) → (p → q) := sorry
example : p ∨ False ↔ p := sorry
example : p ∧ False ↔ False := sorry
example : (p → q) → (¬q → ¬p) := sorry
</code></pre>
<p>证明以下等式，用真实证明取代“sorry”占位符。这里需要一点经典逻辑。</p>
<pre><code class="language-lean">open Classical
variable (p q r s : Prop)
example : (p → r ∨ s) → ((p → r) ∨ (p → s)) := sorry
example : ¬(p ∧ q) → ¬p ∨ ¬q := sorry
example : ¬(p → q) → p ∧ ¬q := sorry
example : (p → q) → (¬p ∨ q) := sorry
example : (¬q → ¬p) → (p → q) := sorry
example : p ∨ ¬p := sorry
example : (((p → q) → p) → p) := sorry
</code></pre>
<p>证明<code>¬(p ↔ ¬p)</code>且不使用经典逻辑。</p>
</main>
<nav class="nav-wrapper" aria-label="Page navigation">
<!-- Mobile navigation buttons -->
<a rel="prev" href="dependent_type_theory.html" class="mobile-nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
<a rel="next" href="quantifiers_and_equality.html" class="mobile-nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
<div style="clear: both"></div>
</nav>
</div>
</div>
<nav class="nav-wide-wrapper" aria-label="Page navigation">
<a rel="prev" href="dependent_type_theory.html" class="nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
<a rel="next" href="quantifiers_and_equality.html" class="nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
</nav>
</div>
<script>
window.playground_copyable = true;
</script>
<script src="elasticlunr.min.js"></script>
<script src="mark.min.js"></script>
<script src="searcher.js"></script>
<script src="clipboard.min.js"></script>
<script src="highlight.js"></script>
<script src="book.js"></script>
<!-- Custom JS scripts -->
</div>
</body>
</html>