-
Notifications
You must be signed in to change notification settings - Fork 0
/
conv.html
378 lines (337 loc) · 18.6 KB
/
conv.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
<!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"><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" class="active"><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>在策略块中,可以使用关键字<code>conv</code>进入转换模式(conversion mode)。这种模式允许在假设和目标内部,甚至在函数抽象和依赖箭头内部移动,以应用重写或简化步骤。</p>
<h2 id="基本导航和重写"><a class="header" href="#基本导航和重写">基本导航和重写</a></h2>
<p>作为第一个例子,让我们证明<code>(a b c : Nat) : a * (b * c) = a * (c * b)</code>(本段中的例子有些刻意设计,因为其他策略可以立即完成它们)。首次简单的尝试是尝试<code>rw [Nat.mul_comm]</code>,但这将目标转化为<code>b * c * a = a * (c * b)</code>,因为它作用于项中出现的第一个乘法。有几种方法可以解决这个问题,其中一个方法是</p>
<pre><code class="language-lean">example (a b c : Nat) : a * (b * c) = a * (c * b) := by
rw [Nat.mul_comm b c]
</code></pre>
<p>不过本节介绍一个更精确的工具:转换模式。下面的代码块显示了每行之后的当前目标。</p>
<pre><code class="language-lean">example (a b c : Nat) : a * (b * c) = a * (c * b) := by
conv =>
-- |- a * (b * c) = a * (c * b)
lhs
-- |- a * (b * c)
congr
-- 2 goals : |- a and |- b * c
skip
-- |- b * c
rw [Nat.mul_comm]
</code></pre>
<p>上面这段涉及三个导航指令:</p>
<ul>
<li><code>lhs</code>(left hand side)导航到关系(此处是等式)左边。同理<code>rhs</code>导航到右边。</li>
<li><code>congr</code>创建与当前头函数的(非依赖的和显式的)参数数量一样多的目标(此处的头函数是乘法)。</li>
<li><code>skip</code>走到下一个目标。</li>
</ul>
<p>一旦到达相关目标,我们就可以像在普通策略模式中一样使用<code>rw</code>。</p>
<p>使用转换模式的第二个主要原因是在约束器下重写。假设我们想证明<code>(fun x : Nat => 0 + x) = (fun x => x)</code>。首次简单的尝试<code>rw [zero_add]</code>是失败的。报错:</p>
<pre><code>error: tactic 'rewrite' failed, did not find instance of the pattern
in the target expression
0 + ?n
⊢ (fun x => 0 + x) = fun x => x
</code></pre>
<p>(错误:'rewrite'策略失败了,没有找到目标表达式中的模式0 + ?n)</p>
<p>正确的结果为:</p>
<pre><code class="language-lean">example : (fun x : Nat => 0 + x) = (fun x => x) := by
conv =>
lhs
intro x
rw [Nat.zero_add]
</code></pre>
<p>其中<code>intro x</code>是导航命令,它进入了<code>fun</code>约束器。这个例子有点刻意,你也可以这样做:</p>
<pre><code class="language-lean">example : (fun x : Nat => 0 + x) = (fun x => x) := by
funext x; rw [Nat.zero_add]
</code></pre>
<p>或者这样:</p>
<pre><code class="language-lean">example : (fun x : Nat => 0 + x) = (fun x => x) := by
simp
</code></pre>
<p>所有这些也可以用<code>conv at h</code>从局部上下文重写一个假设<code>h</code>。</p>
<h2 id="模式匹配"><a class="header" href="#模式匹配">模式匹配</a></h2>
<p>使用上面的命令进行导航可能很无聊。使用下面的模式匹配来简化它:</p>
<pre><code class="language-lean">example (a b c : Nat) : a * (b * c) = a * (c * b) := by
conv in b * c => rw [Nat.mul_comm]
</code></pre>
<p>这是下面代码的语法糖:</p>
<pre><code class="language-lean">example (a b c : Nat) : a * (b * c) = a * (c * b) := by
conv =>
pattern b * c
rw [Nat.mul_comm]
</code></pre>
<p>当然也可以用通配符:</p>
<pre><code class="language-lean">example (a b c : Nat) : a * (b * c) = a * (c * b) := by
conv in _ * c => rw [Nat.mul_comm]
</code></pre>
<h2 id="结构化转换策略"><a class="header" href="#结构化转换策略">结构化转换策略</a></h2>
<p>大括号和<code>.</code>也可以在<code>conv</code>模式下用于结构化策略。</p>
<pre><code class="language-lean">example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by
conv =>
lhs
congr
. rw [Nat.zero_add]
. rw [Nat.mul_comm]
</code></pre>
<h2 id="转换模式中的其他策略"><a class="header" href="#转换模式中的其他策略">转换模式中的其他策略</a></h2>
<ul>
<li><code>arg i</code>进入一个应用的第<code>i</code>个非独立显式参数。</li>
</ul>
<pre><code class="language-lean">example (a b c : Nat) : a * (b * c) = a * (c * b) := by
conv =>
-- |- a * (b * c) = a * (c * b)
lhs
-- |- a * (b * c)
arg 2
-- |- b * c
rw [Nat.mul_comm]
</code></pre>
<ul>
<li>
<p><code>args</code>是<code>congr</code>的替代品。</p>
</li>
<li>
<p><code>simp</code>将简化器应用于当前目标。它支持常规策略模式中的相同选项。</p>
</li>
</ul>
<pre><code class="language-lean">def f (x : Nat) :=
if x > 0 then x + 1 else x + 2
example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := by
conv =>
rhs
simp [f, h₂]
exact h₁
</code></pre>
<ul>
<li><code>enter [1, x, 2, y]</code>是<code>arg</code>和<code>intro</code>使用给定参数的宏。</li>
</ul>
<pre><code>syntax enterArg := ident <|> num
syntax "enter " "[" (colGt enterArg),+ "]": conv
macro_rules
| `(conv| enter [$i:numLit]) => `(conv| arg $i)
| `(conv| enter [$id:ident]) => `(conv| ext $id)
| `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
</code></pre>
<ul>
<li>
<p><code>done</code>会失败如果有未解决的目标。</p>
</li>
<li>
<p><code>traceState</code>显示当前策略状态。</p>
</li>
<li>
<p><code>whnf</code> put term in weak head normal form.</p>
</li>
<li>
<p><code>tactic => <tactic sequence></code>回到常规策略模式。这对于退出<code>conv</code>模式不支持的目标,以及应用自定义的一致性和扩展性引理很有用。</p>
</li>
</ul>
<pre><code class="language-lean">example (g : Nat → Nat → Nat)
(h₁ : ∀ x, x ≠ 0 → g x x = 1)
(h₂ : x ≠ 0)
: g x x + x = 1 + x := by
conv =>
lhs
-- |- g x x + x
arg 1
-- |- g x x
rw [h₁]
-- 2 goals: |- 1, |- x ≠ 0
. skip
. tactic => exact h₂
</code></pre>
<ul>
<li><code>apply <term></code>是<code>tactic => apply <term></code>的语法糖。</li>
</ul>
<pre><code class="language-lean">example (g : Nat → Nat → Nat)
(h₁ : ∀ x, x ≠ 0 → g x x = 1)
(h₂ : x ≠ 0)
: g x x + x = 1 + x := by
conv =>
lhs
arg 1
rw [h₁]
. skip
. apply h₂
</code></pre>
</main>
<nav class="nav-wrapper" aria-label="Page navigation">
<!-- Mobile navigation buttons -->
<a rel="prev" href="type_classes.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="axioms_and_computation.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="type_classes.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="axioms_and_computation.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>