-
Notifications
You must be signed in to change notification settings - Fork 0
/
q8.html
179 lines (166 loc) · 38.5 KB
/
q8.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
<!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="center%E5%BD%92%E7%BA%B3%E5%AE%9A%E4%B9%89%E7%9A%84%E5%91%BD%E9%A2%98center" ebook-toc-level-1 heading="<center>&#x5F52;&#x7EB3;&#x5B9A;&#x4E49;&#x7684;&#x547D;&#x9898;</center>"><center>归纳定义的命题</center></h1>
<h2 class="mume-header" id="%E5%BD%92%E7%BA%B3%E5%AE%9A%E4%B9%89%E7%9A%84%E5%91%BD%E9%A2%98" ebook-toc-level-2 heading="&#x5F52;&#x7EB3;&#x5B9A;&#x4E49;&#x7684;&#x547D;&#x9898;">归纳定义的命题</h2>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Print">Print</span> even<span class="token punctuation">.</span>
<span class="token comment">(*查看偶数定义*)</span>
even <span class="token operator">=</span>
<span class="token keyword keyword-fun">fun</span> x <span class="token punctuation">:</span> nat <span class="token operator">=></span>
<span class="token keyword keyword-exists">exists</span> n <span class="token punctuation">:</span> nat<span class="token punctuation">,</span> x <span class="token operator">=</span> double n
<span class="token punctuation">:</span> nat <span class="token operator">-></span> <span class="token keyword keyword-Prop">Prop</span>
<span class="token keyword keyword-Arguments">Arguments</span> even x<span class="token operator">%</span>nat_scope
</pre><p>除了这种定义外，我们仍然可以使用归纳的方法对偶数进行定义。</p>
<ul>
<li>0 是偶数</li>
<li>如果n是偶数，那么S (S n)也是偶数</li>
</ul>
<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>n<span class="token punctuation">:</span>nat<span class="token punctuation">)</span> <span class="token punctuation">(</span>H <span class="token punctuation">:</span> ev n<span class="token punctuation">)</span> <span class="token punctuation">:</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>
</pre><p>Inductive 定义了一个从nat到Prop的映射，ev内含两个证据构造子(evidence constructors) ev_0 以及 ev_SS.</p>
<p>将定义中涉及到的类型均展示出来:</p>
<div align="center">
<img src="file:///D:\coq\笔记\p1.png">
</div>
<p>关于ev_SS:</p>
<div align="center">
<img src="file:///D:\coq\笔记\p2.png">
</div>
<p>ev_SS 本身接收两个参数——n和H,类型分别为nat和ev n(注意不是参数可以接收nat 和 ev n,而是参数所属的类型). ev_SS 本身的类型相当于一个蕴含式，从程序上讲是一个函数，允许接收两个参数，接收参数后变成高阶函数，类型也从全称命题变成了一个针对特定值的结论。</p>
<blockquote>
<p>区分： 在Inductive 定义中，类型构造子冒号左侧的参数为形参(parameter)，右侧叫做索引(index)或注解(annotation)，如ev定义的时候就使用了索引，这使得ev 后面可以接收特定的nat类型的值。</p>
</blockquote>
<h2 class="mume-header" id="%E5%9C%A8%E8%AF%81%E6%98%8E%E4%B8%AD%E4%BD%BF%E7%94%A8%E8%AF%81%E6%8D%AE" ebook-toc-level-2 heading="&#x5728;&#x8BC1;&#x660E;&#x4E2D;&#x4F7F;&#x7528;&#x8BC1;&#x636E;">在证明中使用证据</h2>
<p>对于ev的定义，其不仅说明ev_0和ev_SS是构造偶数证明证据的方式，同时也说明是ev中构造的全部方式。</p>
<p>这样我们可以像分析归纳定义的数据结构一样分析形如ev n的假设。可以使用归纳(induction)和分类讨论(case analysis)来进行证明。</p>
<h3 class="mume-header" id="%E5%AF%B9%E8%AF%81%E6%98%8E%E8%BF%9B%E8%A1%8C%E5%8F%8D%E6%BC%94inversion" ebook-toc-level-3 heading="&#x5BF9;&#x8BC1;&#x660E;&#x8FDB;&#x884C;&#x53CD;&#x6F14;&#xFF08;inversion&#xFF09;">对证明进行反演（inversion）</h3>
<p>通过destruct 可以对证据进行解构。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Theorem">Theorem</span> ev_inversion <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 punctuation">(</span>n <span class="token operator">=</span> <span class="token number">0</span><span class="token punctuation">)</span> <span class="token operator">\/</span> <span class="token punctuation">(</span><span class="token keyword keyword-exists">exists</span> n<span class="token operator">'</span><span class="token punctuation">,</span> n <span class="token operator">=</span> S <span class="token punctuation">(</span>S n<span class="token operator">'</span><span class="token punctuation">)</span> <span class="token operator">/\</span> ev n<span class="token operator">'</span><span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n E<span class="token punctuation">.</span>
destruct E <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span> <span class="token operator">|</span> n<span class="token operator">'</span> E<span class="token operator">'</span><span class="token punctuation">]</span><span class="token punctuation">.</span>
<span class="token comment">(*E = ev_0 : ev 0*)</span>
<span class="token operator">-</span> left<span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span>
<span class="token comment">(*E = ev_SS n' E' : ev (S (S n'))*)</span>
<span class="token operator">-</span> right<span class="token punctuation">.</span> <span class="token keyword keyword-exists">exists</span> n<span class="token operator">'</span><span class="token punctuation">.</span> split<span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span> <span class="token keyword keyword-apply">apply</span> E<span class="token operator">'</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
</pre><p>这里面的destruct对前提E进行了解构，由于E本身含有类型ev n.而ev又定义了两个证据构造子，所以destruct自然地将E解构成ev_0 和 ev_SS n' E'.</p>
<p>考虑之前学习自然数时对变量n的解构，实际上原理是相同:n类型时nat,而nat定义了两个构造子，所以destruct n将n非为了0和S n'.</p>
<p>然而，destruct 不是非常智能，有时需要一些辅助，例如下面这个定理的证明:</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq">Thereom evSS_ev <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n<span class="token punctuation">,</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 operator">-></span> even n<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n E<span class="token punctuation">.</span>
destruct E <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span><span class="token operator">|</span> n<span class="token operator">'</span> E<span class="token operator">'</span><span class="token punctuation">]</span> eqn <span class="token punctuation">:</span> E1<span class="token punctuation">.</span>
<span class="token operator">-</span> <span class="token comment">(*E = ev_0 : ev 0*)</span>
<span class="token comment">(* 这显然是不可能的，但条件不足无法证明下去 *)</span>
<span class="token keyword keyword-Abort">Abort</span><span class="token punctuation">.</span>
<span class="token comment">(*使用remember 进行变量替换*)</span>
<span class="token keyword keyword-Theorem">Theorem</span> evSS_ev <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n<span class="token punctuation">,</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 operator">-></span> even n<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n E<span class="token punctuation">.</span>
remember <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 keyword keyword-as">as</span> k<span class="token punctuation">.</span>
<span class="token comment">(*设 k = (S (S n))*)</span>
destruct E <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span><span class="token operator">|</span> n<span class="token operator">'</span> E<span class="token operator">'</span><span class="token punctuation">]</span><span class="token punctuation">.</span>
<span class="token operator">-</span> <span class="token comment">(*E = ev_0 *)</span>
<span class="token comment">(*0 = k = S (S n) 这显然不可能，且可以证明矛盾*)</span>
discriminate Heqk<span class="token punctuation">.</span>
<span class="token operator">-</span> <span class="token comment">(*E = ev_S n' E'*)</span>
injection Heqk <span class="token keyword keyword-as">as</span> Heq<span class="token punctuation">.</span>
rewrite Heq <span class="token keyword keyword-in">in</span> E<span class="token operator">'</span><span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> E<span class="token operator">'</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
</pre><p>或者也可以应用<code>ev_inversion</code>将evSS_ev 中的(S (S n))与ev_inversion中的n匹配。这样也可以解构前提。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Theorem">Theorem</span> evSS_ev1 <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n <span class="token punctuation">,</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 operator">-></span> ev n<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n H<span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> ev_inversion <span class="token keyword keyword-in">in</span> H<span class="token punctuation">.</span>
destruct H<span class="token punctuation">.</span>
<span class="token operator">-</span> discriminate H<span class="token punctuation">.</span>
<span class="token operator">-</span> destruct H <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span>n<span class="token operator">'</span> <span class="token punctuation">[</span> Hnm Hev<span class="token punctuation">]</span><span class="token punctuation">]</span><span class="token punctuation">.</span>
injection Hnm <span class="token keyword keyword-as">as</span> Heq<span class="token punctuation">.</span>
rewrite Heq<span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> Hev<span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
</pre><p>Coq提供一个更为强大的策略<code>inversion</code>,对于前提是等式，该策略可以自动使用<code>discriminate</code>和<code>injection</code>,同时也会使用<code>intros</code>和<code>rewrite</code>对前提进行化简;对于具有归纳定义的前提，该策略也可以对其进行解构，生成的子目标中矛盾的情况将被忽略，并保留其余子命题，我们只需要对其余的命题进行证明即可得证原命题。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Theorem">Theorem</span> evSS_ev2 <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n<span class="token punctuation">,</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 operator">-></span> ev n<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n E<span class="token punctuation">.</span>
inversion E <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span><span class="token operator">|</span> n<span class="token operator">'</span> E<span class="token operator">'</span> EQ<span class="token punctuation">]</span><span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> E<span class="token operator">'</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
</pre><h3 class="mume-header" id="%E5%AF%B9%E8%AF%81%E6%8D%AE%E8%BF%9B%E8%A1%8C%E5%BD%92%E7%BA%B3" ebook-toc-level-3 heading="&#x5BF9;&#x8BC1;&#x636E;&#x8FDB;&#x884C;&#x5F52;&#x7EB3;">对证据进行归纳</h3>
<p>对证据使用induction与对数据使用具有相同的行为——引导Coq对每个证据构造子生成一个子目标，同时提供了归纳假设。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Lemma">Lemma</span> ev_even <span class="token punctuation">:</span> <span class="token keyword keyword-forall">forall</span> n<span class="token punctuation">,</span>
ev n <span class="token operator">-></span> even n<span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
intros n E<span class="token punctuation">.</span>
induction E <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span><span class="token operator">|</span> n<span class="token operator">'</span> E<span class="token operator">'</span> IH<span class="token punctuation">]</span><span class="token punctuation">.</span>
<span class="token operator">-</span> <span class="token comment">(* E = ev_0 *)</span>
<span class="token keyword keyword-exists">exists</span> <span class="token number">0</span><span class="token punctuation">.</span> reflexivity<span class="token punctuation">.</span>
<span class="token operator">-</span> <span class="token comment">(* E = ev_SS n' E'*)</span>
<span class="token comment">(*IH : even n'*)</span>
destruct IH <span class="token keyword keyword-as">as</span> <span class="token punctuation">[</span>k<span class="token operator">'</span> Hk<span class="token operator">'</span><span class="token punctuation">]</span><span class="token punctuation">.</span>
<span class="token comment">(* 对even的定义进行解构
exists k' : n' = double k'
*)</span>
rewrite Hk<span class="token operator">'</span><span class="token punctuation">.</span>
<span class="token keyword keyword-exists">exists</span> <span class="token punctuation">(</span>S k<span class="token operator">'</span><span class="token punctuation">)</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>
</pre><h2 class="mume-header" id="%E5%BD%92%E7%BA%B3%E5%85%B3%E7%B3%BB" ebook-toc-level-2 heading="&#x5F52;&#x7EB3;&#x5173;&#x7CFB;">归纳关系</h2>
<p>ev定义了nat的一个子集，可以视为是一个'性质'。而有两个参数的命题就可以视为一个'关系'，定义了一个序对集合。</p>
<p>例如，小于等于:</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Inductive">Inductive</span> le <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> le_n <span class="token punctuation">(</span>n <span class="token punctuation">:</span>nat<span class="token punctuation">)</span> <span class="token punctuation">:</span> le n n
<span class="token operator">|</span> le_S <span class="token punctuation">(</span>n m <span class="token punctuation">:</span> nat<span class="token punctuation">)</span> <span class="token punctuation">(</span>H <span class="token punctuation">:</span> le n m<span class="token punctuation">)</span> <span class="token punctuation">:</span> le n <span class="token punctuation">(</span>S m<span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Notation">Notation</span> <span class="token string">"m <= n"</span> <span class="token operator">:=</span> <span class="token punctuation">(</span>le m n<span class="token punctuation">)</span><span class="token punctuation">.</span>
</pre><p>使用le_n和le_S构造子，可以证明关于le的事实。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Theorem">Theorem</span> test<span class="token punctuation">:</span>
<span class="token number">2</span> <span class="token operator"><=</span> <span class="token number">4</span> <span class="token operator">/\</span> <span class="token operator">~</span><span class="token punctuation">(</span><span class="token number">2</span> <span class="token operator">>=</span> <span class="token number">4</span><span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Proof">Proof</span><span class="token punctuation">.</span>
split<span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> le_S<span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> le_S<span class="token punctuation">.</span>
<span class="token keyword keyword-apply">apply</span> le_n<span class="token punctuation">.</span>
unfold not<span class="token punctuation">.</span>
intros<span class="token punctuation">.</span>
inversion H<span class="token punctuation">.</span>
inversion H2<span class="token punctuation">.</span>
inversion H5<span class="token punctuation">.</span>
<span class="token keyword keyword-Qed">Qed</span><span class="token punctuation">.</span>
</pre><p>小于关系的定义，可以使用le定义，也可以单独进行归纳定义。</p>
<pre data-role="codeBlock" data-info="coq" class="language-coq"><span class="token keyword keyword-Definition">Definition</span> lt<span class="token punctuation">(</span>n m <span class="token punctuation">:</span> nat<span class="token punctuation">)</span> <span class="token operator">:=</span> le <span class="token punctuation">(</span>S n<span class="token punctuation">)</span> m<span class="token punctuation">.</span>
<span class="token keyword keyword-Definition">Definition</span> lt1 <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> lt_n <span class="token punctuation">(</span>n <span class="token punctuation">:</span> nat<span class="token punctuation">)</span> <span class="token punctuation">:</span> lt n <span class="token punctuation">(</span>S n<span class="token punctuation">)</span>
<span class="token operator">|</span> lt_S <span class="token punctuation">(</span>n m <span class="token punctuation">:</span> nat<span class="token punctuation">)</span> <span class="token punctuation">(</span>H <span class="token punctuation">:</span> lt n m<span class="token punctuation">)</span> <span class="token punctuation">:</span> lt n <span class="token punctuation">(</span>S m<span class="token punctuation">)</span><span class="token punctuation">.</span>
<span class="token keyword keyword-Notation">Notation</span> <span class="token string">"m < n"</span> <span class="token operator">:=</span> <span class="token punctuation">(</span>lt m n<span class="token punctuation">)</span><span class="token punctuation">.</span>
</pre></div></body></html>
</div>
</body>
</html>