-
Notifications
You must be signed in to change notification settings - Fork 0
/
q10.html
198 lines (181 loc) · 35.6 KB
/
q10.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
<!DOCTYPE html>
<html>
<head>
<title>归纳法则</title>
<meta charset="utf-8"><link rel = "icon" href = "pic\coq.ico" type="image/gif">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<style>
body{
background:url("background3.png") no-repeat center center fixed;
//-webkit-background-size: cover;
//-o-background-size: cover;
//background-size: cover;
color : white;
}
.markdown-preview{width:100%;height:100%;box-sizing:border-box}.markdown-preview .pagebreak,.markdown-preview .newpage{page-break-before:always}.markdown-preview pre.line-numbers{position:relative;padding-left:3.8em;counter-reset:linenumber}.markdown-preview pre.line-numbers>code{position:relative}.markdown-preview pre.line-numbers .line-numbers-rows{position:absolute;pointer-events:none;top:1em;font-size:100%;left:0;width:3em;letter-spacing:-1px;border-right:1px solid #999;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none}.markdown-preview pre.line-numbers .line-numbers-rows>span{pointer-events:none;display:block;counter-increment:linenumber}.markdown-preview pre.line-numbers .line-numbers-rows>span:before{content:counter(linenumber);color:#999;display:block;padding-right:.8em;text-align:right}.markdown-preview .mathjax-exps .MathJax_Display{text-align:center !important}.markdown-preview:not([for="preview"]) .code-chunk .btn-group{display:none}.markdown-preview:not([for="preview"]) .code-chunk .status{display:none}.markdown-preview:not([for="preview"]) .code-chunk .output-div{margin-bottom:16px}.scrollbar-style::-webkit-scrollbar{width:8px}.scrollbar-style::-webkit-scrollbar-track{border-radius:10px;background-color:transparent}.scrollbar-style::-webkit-scrollbar-thumb{border-radius:5px;background-color:rgba(150,150,150,0.66);border:4px solid rgba(150,150,150,0.66);background-clip:content-box}html body[for="html-export"]:not([data-presentation-mode]){position:relative;width:100%;height:100%;top:0;left:0;margin:0;padding:0;overflow:auto}html body[for="html-export"]:not([data-presentation-mode]) .markdown-preview{position:relative;top:0}@media screen and (min-width:914px){html body[for="html-export"]:not([data-presentation-mode]) .markdown-preview{padding:2em calc(50% - 457px + 2em)}}@media screen and (max-width:914px){html body[for="html-export"]:not([data-presentation-mode]) .markdown-preview{padding:2em}}@media screen and (max-width:450px){html body[for="html-export"]:not([data-presentation-mode]) .markdown-preview{font-size:14px !important;padding:1em}}@media print{html body[for="html-export"]:not([data-presentation-mode]) #sidebar-toc-btn{display:none}}html body[for="html-export"]:not([data-presentation-mode]) #sidebar-toc-btn{position:fixed;bottom:8px;left:8px;font-size:28px;cursor:pointer;color:inherit;z-index:99;width:32px;text-align:center;opacity:.4}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] #sidebar-toc-btn{opacity:1}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc{position:fixed;top:0;left:0;width:300px;height:100%;padding:32px 0 48px 0;font-size:14px;box-shadow:0 0 4px rgba(150,150,150,0.33);box-sizing:border-box;overflow:auto;background-color:inherit}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc::-webkit-scrollbar{width:8px}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc::-webkit-scrollbar-track{border-radius:10px;background-color:transparent}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc::-webkit-scrollbar-thumb{border-radius:5px;background-color:rgba(150,150,150,0.66);border:4px solid rgba(150,150,150,0.66);background-clip:content-box}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc a{text-decoration:none}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc ul{padding:0 1.6em;margin-top:.8em}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc li{margin-bottom:.8em}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .md-sidebar-toc ul{list-style-type:none}html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .markdown-preview{left:300px;width:calc(100% - 300px);padding:2em calc(50% - 457px - 150px);margin:0;box-sizing:border-box}@media screen and (max-width:1274px){html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .markdown-preview{padding:2em}}@media screen and (max-width:450px){html body[for="html-export"]:not([data-presentation-mode])[html-show-sidebar-toc] .markdown-preview{width:100%}}html body[for="html-export"]:not([data-presentation-mode]):not([html-show-sidebar-toc]) .markdown-preview{left:50%;transform:translateX(-50%)}html body[for="html-export"]:not([data-presentation-mode]):not([html-show-sidebar-toc]) .md-sidebar-toc{display:none}pre{font-family:Menlo,Monaco,Consolas,'Courier New',monospace;direction:ltr;text-align:left;white-space:pre;word-spacing:normal;word-break:normal;padding:1em;margin:.5em 0;overflow:auto;line-height:1.5;tab-size:4;hyphens:none;color:#c5c8c6;background-color:#27292c !important;border:#43484c;border-radius:3px}pre[class*="language-"]{padding:1em}code[class*="language-"] .token.comment,pre[class*="language-"] .token.comment,code[class*="language-"] .token.prolog,pre[class*="language-"] .token.prolog,code[class*="language-"] .token.doctype,pre[class*="language-"] .token.doctype,code[class*="language-"] .token.cdata,pre[class*="language-"] .token.cdata{color:#7C7C7C}code[class*="language-"] .token.punctuation,pre[class*="language-"] .token.punctuation{color:#96CBFE}code[class*="language-"] .namespace,pre[class*="language-"] .namespace{opacity:.7}code[class*="language-"] .token.constant,pre[class*="language-"] .token.constant{color:#99CC99}code[class*="language-"] .token.boolean,pre[class*="language-"] .token.boolean,code[class*="language-"] .token.number,pre[class*="language-"] .token.number,code[class*="language-"] .token.function-name,pre[class*="language-"] .token.function-name{color:#FF73FD}code[class*="language-"] .token.tag,pre[class*="language-"] .token.tag{color:#96CBFE}code[class*="language-"] .token.selector,pre[class*="language-"] .token.selector{color:#96CBFE}code[class*="language-"] .token.attr-name,pre[class*="language-"] .token.attr-name{color:#C6C5FE}code[class*="language-"] .token.string,pre[class*="language-"] .token.string{color:#A8FF60}code[class*="language-"] .token.char,pre[class*="language-"] .token.char{color:#FF8000}code[class*="language-"] .token.entity,pre[class*="language-"] .token.entity{color:#FFD2A7}code[class*="language-"] .token.url,pre[class*="language-"] .token.url{color:#7C7C7C}code[class*="language-"] .token.operator,pre[class*="language-"] .token.operator{color:#EDEDED}code[class*="language-"] .token.atrule,pre[class*="language-"] .token.atrule,code[class*="language-"] .token.attr-value,pre[class*="language-"] .token.attr-value,code[class*="language-"] .token.keyword,pre[class*="language-"] .token.keyword{color:#CFCB90}code[class*="language-"] .token.function,pre[class*="language-"] .token.function{color:#FFD2A7}code[class*="language-"] .token.class-name,pre[class*="language-"] .token.class-name{color:#FFD2A7}code[class*="language-"] .token.variable,pre[class*="language-"] .token.variable{color:#C6C5FE}code[class*="language-"] .token.regex,pre[class*="language-"] .token.regex,code[class*="language-"] .token.important,pre[class*="language-"] .token.important{color:#E9C062}code[class*="language-"] .token.important,pre[class*="language-"] .token.important,code[class*="language-"] .token.bold,pre[class*="language-"] .token.bold{font-weight:bold}code[class*="language-"] .token.italic,pre[class*="language-"] .token.italic{font-style:italic}code[class*="language-"] .token.entity,pre[class*="language-"] .token.entity{cursor:help}pre[data-line]{position:relative;padding:1em 0 1em 3em}pre[data-line] .line-highlight-wrapper{position:absolute;top:0;left:0;background-color:transparent;display:block;width:100%}pre[data-line] .line-highlight{position:absolute;left:0;right:0;padding:inherit 0;margin-top:1em;background:rgba(153,122,102,0.08);background:linear-gradient(to right, rgba(153,122,102,0.1) 70%, rgba(153,122,102,0));pointer-events:none;line-height:inherit;white-space:pre}pre[data-line] .line-highlight:before,pre[data-line] .line-highlight[data-end]:after{content:attr(data-start);position:absolute;top:.4em;left:.6em;min-width:1em;padding:0 .5em;background-color:rgba(153,122,102,0.4);color:#f5f2f0;font:bold 65%/1.5 sans-serif;text-align:center;vertical-align:.3em;border-radius:999px;text-shadow:none;box-shadow:0 1px white}pre[data-line] .line-highlight[data-end]:after{content:attr(data-end);top:auto;bottom:.4em}.emoji {
height: 0.8em;
}html body{font-family:"Helvetica Neue",Helvetica,"Segoe UI",Arial,freesans,sans-serif;font-size:16px;line-height:1.6;color:#ccc;background-color:#141414;overflow:initial;box-sizing:border-box;word-wrap:break-word}html body>:first-child{margin-top:0}html body h1,html body h2,html body h3,html body h4,html body h5,html body h6{line-height:1.2;margin-top:1em;margin-bottom:16px;color:#fff}html body h1{font-size:2.25em;font-weight:300;padding-bottom:.3em}html body h2{font-size:1.75em;font-weight:400;padding-bottom:.3em}html body h3{font-size:1.5em;font-weight:500}html body h4{font-size:1.25em;font-weight:600}html body h5{font-size:1.1em;font-weight:600}html body h6{font-size:1em;font-weight:600}html body h1,html body h2,html body h3,html body h4,html body h5{font-weight:600}html body h5{font-size:1em}html body h6{color:#a3a3a3}html body strong{color:#fff}html body del{color:#a3a3a3}html body a:not([href]){color:inherit;text-decoration:none}html body a{color:#08c;text-decoration:none}html body a:hover{color:#00a3f5;text-decoration:none}html body img{max-width:100%}html body>p{margin-top:0;margin-bottom:16px;word-wrap:break-word}html body>ul,html body>ol{margin-bottom:16px}html body ul,html body ol{padding-left:2em}html body ul.no-list,html body ol.no-list{padding:0;list-style-type:none}html body ul ul,html body ul ol,html body ol ol,html body ol ul{margin-top:0;margin-bottom:0}html body li{margin-bottom:0}html body li.task-list-item{list-style:none}html body li>p{margin-top:0;margin-bottom:0}html body .task-list-item-checkbox{margin:0 .2em .25em -1.8em;vertical-align:middle}html body .task-list-item-checkbox:hover{cursor:pointer}html body blockquote{margin:16px 0;font-size:inherit;padding:0 15px;color:#a3a3a3;background-color:#282828;border-left:4px solid #3d3d3d}html body blockquote>:first-child{margin-top:0}html body blockquote>:last-child{margin-bottom:0}html body hr{height:4px;margin:32px 0;background-color:#3d3d3d;border:0 none}html body table{margin:10px 0 15px 0;border-collapse:collapse;border-spacing:0;display:block;width:100%;overflow:auto;word-break:normal;word-break:keep-all}html body table th{font-weight:bold;color:#fff}html body table td,html body table th{border:1px solid #3d3d3d;padding:6px 13px}html body dl{padding:0}html body dl dt{padding:0;margin-top:16px;font-size:1em;font-style:italic;font-weight:bold}html body dl dd{padding:0 16px;margin-bottom:16px}html body code{font-family:Menlo,Monaco,Consolas,'Courier New',monospace;font-size:.85em !important;color:#fff;background-color:#282828;border-radius:3px;padding:.2em 0}html body code::before,html body code::after{letter-spacing:-0.2em;content:"\00a0"}html body pre>code{padding:0;margin:0;font-size:.85em !important;word-break:normal;white-space:pre;background:transparent;border:0}html body .highlight{margin-bottom:16px}html body .highlight pre,html body pre{padding:1em;overflow:auto;font-size:.85em !important;line-height:1.45;border:#3d3d3d;border-radius:3px}html body .highlight pre{margin-bottom:0;word-break:normal}html body pre code,html body pre tt{display:inline;max-width:initial;padding:0;margin:0;overflow:initial;line-height:inherit;word-wrap:normal;background-color:transparent;border:0}html body pre code:before,html body pre tt:before,html body pre code:after,html body pre tt:after{content:normal}html body p,html body blockquote,html body ul,html body ol,html body dl,html body pre{margin-top:0;margin-bottom:16px}html body kbd{color:#fff;border:1px solid #3d3d3d;border-bottom:2px solid #2e2e2e;padding:2px 4px;background-color:#282828;border-radius:3px}@media print{html body{background-color:#141414}html body h1,html body h2,html body h3,html body h4,html body h5,html body h6{color:#fff;page-break-after:avoid}html body blockquote{color:#a3a3a3}html body pre{page-break-inside:avoid}html body table{display:table}html body img{display:block;max-width:100%;max-height:100%}html body pre,html body code{word-wrap:break-word;white-space:pre}}
/* Please visit the URL below for more information: */
/* https://shd101wyy.github.io/markdown-preview-enhanced/#/customize-css */
</style>
</head>
<body for="html-export">
<div class="mume markdown-preview">
<html><head></head><body><div><h1 class="mume-header" id="centercoq%E7%AC%94%E8%AE%B0-%E5%BD%92%E7%BA%B3%E6%B3%95%E5%88%99-center" ebook-toc-level-1 heading="<center>Coq&#x7B14;&#x8BB0; &lt;&#x5F52;&#x7EB3;&#x6CD5;&#x5219;&gt; </center>"><center>归纳法则 </center></h1>
<h2 class="mume-header" id="%E5%9F%BA%E7%A1%80" ebook-toc-level-2 heading="&#x57FA;&#x7840;">基础</h2>
<p>每次使用 Indutive 来声明数据类型时,Coq会自动为该类型生成'归纳法则'。这些法则名称是'数据类型_ind',例如nat_ind,list_ind等。</p>
<p>通常,为归纳类型t生成的归纳法则形式如下:</p>
<ul>
<li>对每个构造子c生成归纳法则中的一种情况</li>
<li>如果c不接受参数,该情况为<br>
"P 对 c 成立"</li>
<li>如果c接受参数 x1:a1 ... xn:an,该情况为:<br>
"对所有的x1:a1 ... xn:an,如果P对每个类型为t的参数都成立,则P对c x1 ... xn 成立"</li>
</ul>
<p><strong>示例:</strong></p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Inductive">Inductive</span> list <span class="token punctuation">(</span>X<span class="token punctuation">:</span><span class="token keyword keyword-Type">Type</span><span class="token punctuation">)</span> <span class="token punctuation">:</span> <span class="token keyword keyword-Type">Type</span> <span class="token operator">:=</span>
<span class="token operator">|</span> nil
<span class="token operator">|</span> cons <span class="token punctuation">(</span>n <span class="token punctuation">:</span> X<span class="token punctuation">)</span> <span class="token punctuation">(</span>l <span class="token punctuation">:</span> natlist<span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Check">Check</span> list_ind<span class="token punctuation">.</span>
<span class="token comment">(*list_ind
: forall (X : Type)
(P : list X -> Prop),
P (nil X) ->
(forall (n : X) (l : list X),
P l -> P (cons X n l)) ->
forall l : list X, P l*)</span>
<span class="token keyword keyword-Inductive">Inductive</span> season <span class="token punctuation">:</span> <span class="token keyword keyword-Type">Type</span> <span class="token operator">:=</span>
<span class="token operator">|</span> spring
<span class="token operator">|</span> summer
<span class="token operator">|</span> autumn
<span class="token operator">|</span> winter<span class="token punctuation">.</span>
<span class="token keyword keyword-Check">Check</span> season_ind<span class="token punctuation">.</span>
<span class="token comment">(*season_ind
: forall P : season -> Prop,
P spring ->
P summer ->
P autumn ->
P winter ->
forall s : season, P s*)</span>
</pre><p>可以看到,无论是否为递归的,Coq都会生成对应的归纳法则,归纳原理仍然可用来证明其性质。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Theorem">Theorem</span> n_plus_one_is_S_n <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n <span class="token punctuation">:</span> nat<span class="token punctuation">,</span>
n <span class="token operator">+</span> <span class="token number">1</span> <span class="token operator">=</span> S n<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> nat_ind<span class="token punctuation">.</span>
<span class="token operator">-</span>reflexivity<span class="token punctuation">.</span>
<span class="token operator">-</span>intros n IHn<span class="token punctuation">.</span>
simpl<span class="token punctuation">.</span> rewrite IHn<span class="token punctuation">.</span>reflexivity<span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Theorem">Theorem</span> n_plus_one_is_S_n1 <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n <span class="token punctuation">:</span> nat<span class="token punctuation">,</span>
n <span class="token operator">+</span> <span class="token number">1</span> <span class="token operator">=</span> S n<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n<span class="token punctuation">.</span>
induction n<span class="token punctuation">.</span>
<span class="token operator">-</span> reflexivity<span class="token punctuation">.</span>
<span class="token operator">-</span> simpl<span class="token punctuation">.</span> rewrite IHn<span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
</pre><p>induction的工作就是应用归纳类型对应的归纳法则,只不过增加了变量名的管理工作,在实践中使用induction更加方便。</p>
<h2 class="mume-header" id="%E6%B7%B1%E5%85%A5induction-%E7%AD%96%E7%95%A5" ebook-toc-level-2 heading="&#x6DF1;&#x5165;induction &#x7B56;&#x7565;">深入induction 策略</h2>
<p>考虑自然数的数学归纳法(非形式化陈述):<br>
如果P n是某个涉及数字n的命题,我们想要证明P对于所有数字n都成立,使用如下方式推理:</p>
<ul>
<li>证明P 0 成立</li>
<li>证明P n'成立,那么P (S n')成立</li>
<li>得出结论P n对所有n成立</li>
</ul>
<p>当我们使用intros n 和 induction n 证明时,Coq 实际上先考虑了一个特殊的n(引入上下文),然后通过归纳告诉它证明一些关于全体数字的性质。此时,Coq再次一般化了进行归纳的变量。</p>
<p>当然也可以不对n进行特殊化——对于目标中含有量词的变量应用induction也可以工作。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Theorem">Theorem</span> plus_assoc<span class="token operator">'</span> <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n m p <span class="token punctuation">:</span> nat<span class="token punctuation">,</span> n <span class="token operator">+</span> <span class="token punctuation">(</span>m <span class="token operator">+</span> p<span class="token punctuation">)</span> <span class="token operator">=</span> <span class="token punctuation">(</span>n <span class="token operator">+</span> m<span class="token punctuation">)</span> <span class="token operator">+</span> p<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n m p<span class="token punctuation">.</span>
induction n <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span>n<span class="token operator">'</span> IHn<span class="token operator">'</span><span class="token punctuation">]</span><span class="token punctuation">.</span>
<span class="token comment">(*重新一般化*)</span>
<span class="token operator">-</span> reflexivity<span class="token punctuation">.</span>
<span class="token operator">-</span> simpl<span class="token punctuation">.</span> rewrite <span class="token operator">-></span> IHn<span class="token operator">'</span><span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span> <span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Theorem">Theorem</span> plus_assoc<span class="token operator">'</span><span class="token operator">'</span> <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n m p <span class="token punctuation">:</span> nat<span class="token punctuation">,</span> n <span class="token operator">+</span> <span class="token punctuation">(</span>m <span class="token operator">+</span> p<span class="token punctuation">)</span> <span class="token operator">=</span> <span class="token punctuation">(</span>n <span class="token operator">+</span> m<span class="token punctuation">)</span> <span class="token operator">+</span> p<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
<span class="token comment">(*不进行特殊化*)</span>
induction n<span class="token punctuation">.</span>
<span class="token operator">-</span> simpl<span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span>
<span class="token operator">-</span>intros m p<span class="token punctuation">.</span>
simpl<span class="token punctuation">.</span> rewrite IHn<span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
Thorem plus_assoc<span class="token operator">'</span><span class="token operator">'</span><span class="token operator">'</span> <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n m p <span class="token punctuation">:</span> nat <span class="token punctuation">,</span> n <span class="token operator">+</span> <span class="token punctuation">(</span>m <span class="token operator">+</span> p<span class="token punctuation">)</span> <span class="token operator">=</span> <span class="token punctuation">(</span>n <span class="token operator">+</span> m<span class="token punctuation">)</span> <span class="token operator">+</span> p<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n m p<span class="token punctuation">.</span>
generalize n <span class="token keyword keyword-as">as</span> n0<span class="token punctuation">.</span>
<span class="token comment">(*将n取消特殊化*)</span>
induction n0<span class="token punctuation">.</span>
<span class="token operator">-</span> reflexivity<span class="token punctuation">.</span>
<span class="token operator">-</span> simpl<span class="token punctuation">.</span> rewrite IHn0<span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
</pre><h2 class="mume-header" id="prop-%E4%B8%AD%E7%9A%84%E5%BD%92%E7%BA%B3%E6%B3%95%E5%88%99" ebook-toc-level-2 heading="Prop &#x4E2D;&#x7684;&#x5F52;&#x7EB3;&#x6CD5;&#x5219;">Prop 中的归纳法则</h2>
<p>考虑之前学习的ev定义。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Inductive">Inductive</span> ev <span class="token punctuation">:</span> nat <span class="token operator">-></span> <span class="token keyword keyword-Prop">Prop</span> <span class="token operator">:=</span>
<span class="token operator">|</span> ev_0 <span class="token punctuation">:</span> ev <span class="token number">0</span>
<span class="token operator">|</span> ev_SS <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n <span class="token punctuation">:</span> nat <span class="token punctuation">,</span>ev n <span class="token operator">-></span> ev <span class="token punctuation">(</span>S <span class="token punctuation">(</span>S n<span class="token punctuation">)</span><span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Check">Check</span> ev_ind<span class="token punctuation">.</span>
<span class="token comment">(*ev_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat,
ev n -> P n -> P (S (S n))) ->
forall n : nat, ev n -> P n*)</span>
</pre><p>按照之前的归纳法则,ev_ind似乎应该是这样的:</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq">ev_ind<span class="token operator">'</span> <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> P <span class="token punctuation">:</span><span class="token punctuation">(</span> <span class="token keyword keyword-forall">forall</span> n <span class="token punctuation">:</span> nat <span class="token punctuation">,</span> ev n <span class="token operator">-></span> <span class="token keyword keyword-Prop">Prop</span><span class="token punctuation">)</span><span class="token punctuation">,</span>
P <span class="token number">0</span> ev_0 <span class="token operator">-></span>
<span class="token punctuation">(</span><span class="token keyword keyword-forall">forall</span> <span class="token punctuation">(</span>m <span class="token punctuation">:</span> nat<span class="token punctuation">)</span> <span class="token punctuation">(</span>E<span class="token punctuation">:</span>ev m<span class="token punctuation">)</span><span class="token punctuation">,</span>
P m E <span class="token operator">-></span> P <span class="token punctuation">(</span>S <span class="token punctuation">(</span>S m<span class="token punctuation">)</span><span class="token punctuation">)</span><span class="token punctuation">)</span> <span class="token punctuation">(</span>ev_SS m E<span class="token punctuation">)</span><span class="token punctuation">)</span> <span class="token operator">-></span>
<span class="token keyword keyword-forall">forall</span> <span class="token punctuation">(</span>n<span class="token punctuation">:</span>nat<span class="token punctuation">)</span> <span class="token punctuation">(</span>E<span class="token punctuation">:</span>ev n<span class="token punctuation">)</span><span class="token punctuation">,</span> P n E<span class="token punctuation">.</span>
</pre><p>然而我们真正想要的是证明某些自然数是偶数这样的性质,即关于自然数的断言而非证据,如果对于命题P的归纳法仅仅被n所参数化,且其结构是P对所有偶数n成立,那么会方便许多。因此Coq为ev生成了简化的归纳法则。</p>
<p>该归纳法则用自然语言表述:</p>
<p>假设P是关于自然数的一个性质,为证明当n是偶数时P n成立,需要证明:</p>
<ul>
<li>P 对 0 成立</li>
<li>对任意n,如果n是偶数且P对n成立,那么P对S (S n)成立。</li>
</ul>
<p>另外,Inductive定义的具体形式会影响到Coq生成的归纳法则。</p>
<p>例如</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Inductive">Inductive</span> le1 <span class="token punctuation">:</span> nat <span class="token operator">-></span> nat <span class="token operator">-></span> <span class="token keyword keyword-Prop">Prop</span> <span class="token operator">:=</span>
<span class="token operator">|</span> le1_n <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n <span class="token punctuation">,</span> le1 n n
<span class="token operator">|</span> le1_S <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n m <span class="token punctuation">,</span> <span class="token punctuation">(</span>le1 n m<span class="token punctuation">)</span> <span class="token operator">-></span> <span class="token punctuation">(</span>le1 n <span class="token punctuation">(</span>S m<span class="token punctuation">)</span><span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Inductive">Inductive</span> le2 <span class="token punctuation">(</span>n <span class="token punctuation">:</span> nat<span class="token punctuation">)</span> <span class="token punctuation">:</span> nat <span class="token operator">-></span> <span class="token keyword keyword-Prop">Prop</span> <span class="token operator">:=</span>
<span class="token operator">|</span> le2_n <span class="token punctuation">:</span> le2 n n
<span class="token operator">|</span> le2_S m <span class="token punctuation">(</span>H <span class="token punctuation">:</span> le2 n m<span class="token punctuation">)</span> <span class="token punctuation">:</span> le2 n <span class="token punctuation">(</span>S m<span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Check">Check</span> le1_ind<span class="token punctuation">.</span>
<span class="token comment">(*le1_ind
: forall P : nat -> nat -> Prop,
(forall n : nat, P n n) ->
(forall n m : nat,
le1 n m -> P n m -> P n (S m)) ->
forall n n0 : nat,
le1 n n0 -> P n n0*)</span>
<span class="token keyword keyword-Check">Check</span> le2_ind<span class="token punctuation">.</span>
<span class="token comment">(*le2_ind
: forall (n : nat)
(P : nat -> Prop),
P n ->
(forall m : nat,
le2 n m -> P m -> P (S m)) ->
forall n0 : nat,
le2 n n0 -> P n0*)</span>
</pre><p>第二个生成了更简单的归纳法则。</p>
<h2 class="mume-header" id="%E6%80%BB%E7%BB%93" ebook-toc-level-2 heading="&#x603B;&#x7ED3;">总结</h2>
<p>《软件基础》给出了两个关于归纳的模板,这对于学习归纳的底层原理是很有帮助的。</p>
<p><strong>对归纳定义的集合进行归纳</strong></p>
<p>有形如"forall n : S ,P (n)"的全称量化命题,其中S是某个归纳定义的集合。对n进行归纳。</p>
<p>对S中的每个构造子c的情形:</p>
<ul>
<li>假设n = c a1 ... ak , 为每个具有类型S的a陈述归纳假设IH,我们需要证明P(c a1 ... ak)成立。(继续证明至完成此情形)</li>
<li>其他情形以此类推</li>
</ul>
<p><strong>对归纳定义的命题进行归纳</strong></p>
<p>有形如"Q -> P"的命题,其中Q是某个个归纳定义的命题。证明对Q的导出式进行归纳。</p>
<p>对Q中的每个构造子c的情形:</p>
<ul>
<li>假设被用于证明Q的最终规则是c,在这里,我们陈述了所有a类型,以及构造子定义的所有等式,以及所有类型为Q的a的IH(如果有的话)</li>
</ul>
</div></body></html>
</div>
</body>
</html>