forked from 0x00-pl/SFCT
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathAuto.html
806 lines (653 loc) · 83.4 KB
/
Auto.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
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Auto: More Automation</title>
<script type="text/javascript" src="jquery-1.8.3.js"></script>
<script type="text/javascript" src="main.js"></script>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
<div class="code code-tight">
</div>
<div class="doc">
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Imp</span>.<br/>
<br/>
</div>
<div class="doc">
到现在，我们一直用的是 Coq 的策略系统中的非常有限的一部分。在这章中，
我们会学习 Coq 的策略语言的两个强大的功能：使用 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>
进行证明搜索，和使用 <span class="inlinecode"><span class="id" type="keyword">Ltac</span></span> 的前提搜索功能进行自动化正向推理。
这些功能和 Ltac 的脚本功能可以使我们能把证明搞的很短。
适当使用这些功能，我们也可以把我们的证明可维护性更好，在以后增量修改
底层的定义后也可以更健壮。
<div class="paragraph"> </div>
还有第三种主要自动化的的方式，我们还没有完全了解，这就是自带的
对某些特定种类问题决策算法：<span class="inlinecode"><span class="id" type="tactic">omega</span></span> 是这样的一个例子，不过还有其他的。
我们将稍微多推迟一下这个话题。
<div class="paragraph"> </div>
我们的动机例子将是这个证明，加上几个在 <span class="inlinecode"><span class="id" type="var">Imp</span></span> 里的小的改动。
我们将分几个阶段将它简化。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Ltac</span> <span class="id" type="var">inv</span> <span class="id" type="var">H</span> := <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">H</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>.<br/>
- <span class="comment">(* E_Skip *)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
- <span class="comment">(* E_Ass *)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
- <span class="comment">(* E_Seq *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span>.<br/>
{ <span class="comment">(* 断言的证明 *)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_1</span>; <span class="id" type="tactic">assumption</span>. }<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_2</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="comment">(* E_IfTrue *)</span><br/>
- <span class="comment">(* b 求值为真 *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1</span>. <span class="id" type="tactic">assumption</span>.<br/>
- <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H5</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
<span class="comment">(* E_IfFalse *)</span><br/>
- <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H5</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* b 求值为假 *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="comment">(* E_WhileEnd *)</span><br/>
- <span class="comment">(* b 求值为假 *)</span><br/>
<span class="id" type="tactic">reflexivity</span>.<br/>
- <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H2</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H2</span>.<br/>
<span class="comment">(* E_WhileLoop *)</span><br/>
- <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H4</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H4</span>.<br/>
- <span class="comment">(* b 求值为真 *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span>.<br/>
{ <span class="comment">(* 断言的证明 *)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_1</span>; <span class="id" type="tactic">assumption</span>. }<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_2</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab624"></a><h1 class="section">证明策略 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">eauto</span></span></h1>
<div class="paragraph"> </div>
话说这么久以来，我们（几乎）总是在写证明脚本时通过名字来使用有关的前提和
引理。特别的，当我们需要一系列的前提的应用时，我们将它们显式地把它们列出。
（目前讲过的仅有的例外是使用 <span class="inlinecode"><span class="id" type="tactic">assumption</span></span> 来搜索一个与目标匹配的没有量词的
前提和使用 <span class="inlinecode">(<span class="id" type="var">e</span>)<span class="id" type="var">constructor</span></span> 来搜索一个匹配的构造子）
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_1</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span>: <span class="id" type="keyword">Prop</span>), (<span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">Q</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">Q</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>) <span style="font-family: arial;">→</span> <span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span> <span class="id" type="var">H1</span> <span class="id" type="var">H2</span> <span class="id" type="var">H3</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H2</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H1</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
证明策略 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 可以使我们免于这些苦役，办法是 <i>搜索_ 一个可以
解决证明目标的一系列应用。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_1'</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span>: <span class="id" type="keyword">Prop</span>), (<span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">Q</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">Q</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>) <span style="font-family: arial;">→</span> <span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span> <span class="id" type="var">H1</span> <span class="id" type="var">H2</span> <span class="id" type="var">H3</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">auto</span></span> 策略可以解决任何可由如下策略的组合解决的证明目标：
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="tactic">intros</span></span>
</li>
<li> <span class="inlinecode"><span class="id" type="tactic">apply</span></span>（默认使用一个当前的前提）
</li>
</ul>
<span class="inlinecode"><span class="id" type="tactic">eauto</span></span> 策略与 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 的效果非常相似，除了它使用的是 <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>
而不是 <span class="inlinecode"><span class="id" type="tactic">apply</span></span>。
<div class="paragraph"> </div>
<div class="paragraph"> </div>
使用 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 一定是“安全”的，意思是说，它不会失败，也不会改变
当前证明状态：<span class="inlinecode"><span class="id" type="tactic">auto</span></span> 要么完全解决它，要么什么也不做。
<div class="paragraph"> </div>
一个更复杂的例子
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_2</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span> : <span class="id" type="keyword">Prop</span>,<br/>
(<span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">Q</span>) <span style="font-family: arial;">→</span><br/>
(<span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>) <span style="font-family: arial;">→</span><br/>
(<span class="id" type="var">T</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>) <span style="font-family: arial;">→</span><br/>
(<span class="id" type="var">S</span> <span style="font-family: arial;">→</span> <span class="id" type="var">T</span> <span style="font-family: arial;">→</span> <span class="id" type="var">U</span>) <span style="font-family: arial;">→</span><br/>
((<span class="id" type="var">P</span><span style="font-family: arial;">→</span><span class="id" type="var">Q</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">P</span><span style="font-family: arial;">→</span><span class="id" type="var">S</span>)) <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">T</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">P</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">U</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
搜索可能需要任意长的时间，所以有限制参数来控制 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 的搜索深度。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_3</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span>: <span class="id" type="keyword">Prop</span>), <br/>
(<span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">Q</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">Q</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">R</span> <span style="font-family: arial;">→</span> <span class="id" type="var">S</span>) <span style="font-family: arial;">→</span> <br/>
(<span class="id" type="var">S</span> <span style="font-family: arial;">→</span> <span class="id" type="var">T</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">T</span> <span style="font-family: arial;">→</span> <span class="id" type="var">U</span>) <span style="font-family: arial;">→</span> <span class="id" type="var">P</span> <span style="font-family: arial;">→</span> <span class="id" type="var">U</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="comment">(* 不能解决目标的话，什么也不会发生 *)</span><br/>
<span class="id" type="tactic">auto</span> 6. <span class="comment">(* 可选参数控制它的搜索深度（默认是 5） *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
当搜索当前目标可能的证明时，<span class="inlinecode"><span class="id" type="tactic">auto</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> 会同时考虑当前上下文中的前提
和一个包含了其他引理和构造子的 <i>提示库_ 。有些我们已经见到引理和构造子已经
在默认的提示库里装好了，如 <span class="inlinecode"><span class="id" type="var">eq_refl</span></span> 、<span class="inlinecode"><span class="id" type="var">conj</span></span> 、 <span class="inlinecode"><span class="id" type="var">or_introl</span></span> 、 <span class="inlinecode"><span class="id" type="var">or_intror</span></span>
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_4</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span> : <span class="id" type="keyword">Prop</span>,<br/>
<span class="id" type="var">Q</span> <span style="font-family: arial;">→</span><br/>
(<span class="id" type="var">Q</span> <span style="font-family: arial;">→</span> <span class="id" type="var">R</span>) <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">P</span> <span style="font-family: arial;">∨</span> (<span class="id" type="var">Q</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">R</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
如果我们想看 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 用到了什么，我们可以使用 <span class="inlinecode"><span class="id" type="var">info_auto</span></span>
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_5</span>: 2 = 2.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="var">info_auto</span>. <span class="comment">(* 可以代替 reflexivity，因为提示库里有 eq_refl *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
我们可以为某一次 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 或 <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> 的调用扩展提示库，方法是使用 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="keyword">using</span></span> <span class="inlinecode">...</span>
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">le_antisym</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>: <span class="id" type="var">nat</span>, (<span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">m</span> ≤ <span class="id" type="var">n</span>) <span style="font-family: arial;">→</span> <span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">omega</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_6</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">p</span> : <span class="id" type="var">nat</span>,<br/>
(<span class="id" type="var">n</span>≤ <span class="id" type="var">p</span> <span style="font-family: arial;">→</span> (<span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">m</span> ≤ <span class="id" type="var">n</span>)) <span style="font-family: arial;">→</span> <br/>
<span class="id" type="var">n</span> ≤ <span class="id" type="var">p</span> <span style="font-family: arial;">→</span> <br/>
<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="comment">(* 什么都没发生： auto 不会销毁一个前提 *)</span><br/>
<span class="id" type="tactic">auto</span> <span class="id" type="keyword">using</span> <span class="id" type="var">le_antisym</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
当然, 在任何开发过程中我们都会有自己特有的一套构造子和引理会
在证明中经常用到。我们可以将这些加入全局提示库里，方法是在顶层使用：
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">T</span>.
<div class="paragraph"> </div>
</div>
其中 <span class="inlinecode"><span class="id" type="var">T</span></span> 是一个顶层的定理或一个归纳定义的命题（也就是说，任何类型是一个
“蕴含”的命题）。我们也可以使用一个简写：
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">c</span>.
<div class="paragraph"> </div>
</div>
告诉 Coq 对归纳定义<span class="inlinecode"><span class="id" type="var">c</span></span> 的 <i>每一个_ 构造子进行一个 <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="keyword">Resolve</span></span>。
<div class="paragraph"> </div>
有时我们可能需要
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Unfold</span> <span class="id" type="var">d</span>.
<div class="paragraph"> </div>
</div>
其中，<span class="inlinecode"><span class="id" type="var">d</span></span> 是一个定义的标识符。这样，<span class="inlinecode"><span class="id" type="tactic">auto</span></span> 就知道展开用到的 <span class="inlinecode"><span class="id" type="var">d</span></span>
来获得更多的使用已知的引理的机会。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">le_antisym</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_6'</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">p</span> : <span class="id" type="var">nat</span>,<br/>
(<span class="id" type="var">n</span>≤ <span class="id" type="var">p</span> <span style="font-family: arial;">→</span> (<span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">m</span> ≤ <span class="id" type="var">n</span>)) <span style="font-family: arial;">→</span> <br/>
<span class="id" type="var">n</span> ≤ <span class="id" type="var">p</span> <span style="font-family: arial;">→</span> <br/>
<span class="id" type="var">n</span> = <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="comment">(* 从提示库里得到了引理 *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">is_fortytwo</span> <span class="id" type="var">x</span> := <span class="id" type="var">x</span> = 42.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_7</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">x</span>, (<span class="id" type="var">x</span> ≤ 42 <span style="font-family: arial;">∧</span> 42 ≤ <span class="id" type="var">x</span>) <span style="font-family: arial;">→</span> <span class="id" type="var">is_fortytwo</span> <span class="id" type="var">x</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="comment">(* 什么都没发生 *)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Unfold</span> <span class="id" type="var">is_fortytwo</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_7'</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">x</span>, (<span class="id" type="var">x</span> ≤ 42 <span style="font-family: arial;">∧</span> 42 ≤ <span class="id" type="var">x</span>) <span style="font-family: arial;">→</span> <span class="id" type="var">is_fortytwo</span> <span class="id" type="var">x</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="var">info_auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">ceval</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">st12</span> := <span class="id" type="var">update</span> (<span class="id" type="var">update</span> <span class="id" type="var">empty_state</span> <span class="id" type="var">X</span> 1) <span class="id" type="var">Y</span> 2.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">st21</span> := <span class="id" type="var">update</span> (<span class="id" type="var">update</span> <span class="id" type="var">empty_state</span> <span class="id" type="var">X</span> 2) <span class="id" type="var">Y</span> 1.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_8</span> : <span style="font-family: arial;">∃</span><span class="id" type="var">s'</span>,<br/>
(<span class="id" type="var">IFB</span> (<span class="id" type="var">BLe</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>))<br/>
<span class="id" type="var">THEN</span> (<span class="id" type="var">Z</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>))<br/>
<span class="id" type="var">ELSE</span> (<span class="id" type="var">Y</span> ::= <span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Z</span>))<br/>
<span class="id" type="var">FI</span>) / <span class="id" type="var">st21</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">s'</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="var">eexists</span>. <span class="id" type="var">info_auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">auto_example_8'</span> : <span style="font-family: arial;">∃</span><span class="id" type="var">s'</span>,<br/>
(<span class="id" type="var">IFB</span> (<span class="id" type="var">BLe</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>))<br/>
<span class="id" type="var">THEN</span> (<span class="id" type="var">Z</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>))<br/>
<span class="id" type="var">ELSE</span> (<span class="id" type="var">Y</span> ::= <span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Z</span>))<br/>
<span class="id" type="var">FI</span>) / <span class="id" type="var">st12</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">s'</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="var">eexists</span>. <span class="id" type="var">info_auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
现在我们来看看 <span class="inlinecode"><span class="id" type="var">ceval_deterministic</span></span>，并用 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 来简化证明脚本。
我们发现所有简单的前提的应用和 <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> 都可以用 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 代替，
因此我们把它加到每个情况默认执行的策略里。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>; <span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_Seq *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span> <span class="id" type="tactic">by</span> <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_IfTrue *)</span><br/>
+ <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H5</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* E_IfFalse *)</span><br/>
+ <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H5</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* E_WhileEnd *)</span><br/>
+ <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H2</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H2</span>.<br/>
<span class="comment">(* E_WhileLoop *)</span><br/>
- <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H4</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H4</span>.<br/>
- <span class="comment">(* b 求值为真 *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span> <span class="id" type="tactic">by</span> <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
如果我们在证明里反复用到某一个策略，我们可以使用一个 <span class="inlinecode"><span class="id" type="keyword">Proof</span></span> 命令的变体
来使这个策略称为默认策略。
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" type="keyword">Proof</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span>（其中 <span class="inlinecode"><span class="id" type="var">t</span></span> 是任意一个策略）使我们在证明中可以使用 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span>...</span>
作为 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span>;<span class="id" type="var">t</span></span> 的简写。作为一个示范，这是一个上一个证明的另一种写法，用到了
<span class="inlinecode"><span class="id" type="keyword">Proof</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> <span class="inlinecode"><span class="id" type="tactic">auto</span></span>。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'_alt</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>...<br/>
- <span class="comment">(* E_Seq *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span>...<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>...<br/>
- <span class="comment">(* E_IfTrue *)</span><br/>
+ <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H5</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* E_IfFalse *)</span><br/>
+ <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H5</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* E_WhileEnd *)</span><br/>
+ <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H2</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H2</span>.<br/>
<span class="comment">(* E_WhileLoop *)</span><br/>
- <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H4</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H4</span>.<br/>
- <span class="comment">(* b 求值为真 *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span>...<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
</div>
<div class="doc">
<a name="lab625"></a><h1 class="section">搜索前提</h1>
<div class="paragraph"> </div>
证明变得简单了，但是还是有一定的恼人的重复。我们先从矛盾的情况开始。这些
矛盾都是因为我们同时有这两个前提：
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" type="var">H1</span>:</span> <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>
<div class="paragraph"> </div>
和
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" type="var">H2</span>:</span> <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>
<div class="paragraph"> </div>
矛盾是显然的，但是证明有点麻烦：我们必须找到这两个假设 <span class="inlinecode"><span class="id" type="var">H1</span></span> 和 <span class="inlinecode"><span class="id" type="var">H2</span></span>，然后
用一个 <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> 和一个 <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>。我们希望自动化这个过程。
<div class="paragraph"> </div>
注：事实上，Coq 有一个自带的策略 <span class="inlinecode"><span class="id" type="tactic">congruence</span></span>，可以实现这个目的。但是
我们暂时忽略掉它的存在，而示范如何自己动手构建正向推理的策略。
<div class="paragraph"> </div>
<div class="paragraph"> </div>
第一步，我们抽象出这个证明脚本中的一部分作为一个参数化的 Ltac
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Ltac</span> <span class="id" type="var">rwinv</span> <span class="id" type="var">H1</span> <span class="id" type="var">H2</span> := <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H1</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">H2</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic''</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>; <span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_Seq *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span> <span class="id" type="tactic">by</span> <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_IfTrue *)</span><br/>
+ <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="var">rwinv</span> <span class="id" type="var">H</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* E_IfFalse *)</span><br/>
+ <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="var">rwinv</span> <span class="id" type="var">H</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* E_WhileEnd *)</span><br/>
+ <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="var">rwinv</span> <span class="id" type="var">H</span> <span class="id" type="var">H2</span>.<br/>
<span class="comment">(* E_WhileLoop *)</span><br/>
- <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="var">rwinv</span> <span class="id" type="var">H</span> <span class="id" type="var">H4</span>.<br/>
- <span class="comment">(* b 求值为真 *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span> <span class="id" type="tactic">by</span> <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
但是这并没有改进多少。我们真正希望的是 Coq 能自动发现有关的前提。
我们可以使用 Ltac 的 <span class="inlinecode"><span class="id" type="keyword">match</span></span> <span class="inlinecode"><span class="id" type="var">goal</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="keyword">end</span></span> 功能达到这个目标。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Ltac</span> <span class="id" type="var">find_rwinv</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">goal</span> <span class="id" type="keyword">with</span><br/>
<span class="id" type="var">H1</span>: ?<span class="id" type="var">E</span> = <span class="id" type="var">true</span>, <span class="id" type="var">H2</span>: ?<span class="id" type="var">E</span> = <span class="id" type="var">false</span> <span style="font-family: arial;">⊢</span> <span class="id" type="var">_</span> ⇒ <span class="id" type="var">rwinv</span> <span class="id" type="var">H1</span> <span class="id" type="var">H2</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
用中文表示，这个 <span class="inlinecode"><span class="id" type="keyword">match</span></span> <span class="inlinecode"><span class="id" type="var">goal</span></span> 搜索两个（不同）的前提，使得它们是左边是任意相同的
表达式 <span class="inlinecode"><span class="id" type="var">E</span></span>，右边是两个冲突的布尔值。如果找到了这样的前提，就把它们命名为 <span class="inlinecode"><span class="id" type="var">H1</span></span> 和 <span class="inlinecode"><span class="id" type="var">H2</span></span>，
并执行 <span class="inlinecode">⇒</span> 后面的策略。
<div class="paragraph"> </div>
将这个策略加入我们默认执行的策略序列中，就把所有矛盾情况解决了。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'''</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">find_rwinv</span>; <span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_Seq *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span> <span class="id" type="tactic">by</span> <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_WhileLoop *)</span><br/>
+ <span class="comment">(* b 求值为真 *)</span><br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ1</span> <span class="id" type="tactic">by</span> <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
最后我们来看看剩余的情况。每一个都用到了一个有条件的前提以得到一个等式。
目前我们把这些等式列为了断言，所以我们必须猜出需要的等式是什么（虽然
我们可以用 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 证明它们）。另一个方式是找出用到的有关的前提，然后
用他们重写，像这样：
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic''''</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">find_rwinv</span>; <span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_Seq *)</span><br/>
<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">IHE1_1</span> <span class="id" type="var">st'0</span> <span class="id" type="var">H1</span>) <span class="id" type="keyword">in</span> ×. <span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_WhileLoop *)</span><br/>
+ <span class="comment">(* b 求值为真 *)</span><br/>
<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">IHE1_1</span> <span class="id" type="var">st'0</span> <span class="id" type="var">H3</span>) <span class="id" type="keyword">in</span> ×. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
现在我们就可以自动化找有关的用来重写的前提的这个过程了。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Ltac</span> <span class="id" type="var">find_eqn</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">goal</span> <span class="id" type="keyword">with</span><br/>
<span class="id" type="var">H1</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">x</span>, ?<span class="id" type="var">P</span> <span class="id" type="var">x</span> <span style="font-family: arial;">→</span> ?<span class="id" type="var">L</span> = ?<span class="id" type="var">R</span>, <span class="id" type="var">H2</span>: ?<span class="id" type="var">P</span> ?<span class="id" type="var">X</span> <span style="font-family: arial;">⊢</span> <span class="id" type="var">_</span> ⇒ <br/>
<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H1</span> <span class="id" type="var">X</span> <span class="id" type="var">H2</span>) <span class="id" type="keyword">in</span> × <br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
但是有许多对前提都具有这种一般形式，而挑出我们真正需要的好像比较复杂。
一个关键在于认识到我们可以 <i>全试一遍<i>！
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> 在得到一个平凡的形如 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">X</span></span> 的等式时会失败。
</li>
<li> 每一个 <span class="inlinecode"><span class="id" type="keyword">match</span></span> <span class="inlinecode"><span class="id" type="var">goal</span></span> 在运行时都会不停的找可行的一对前提，直到
右面的策略成功。如果没有这样的一对前提就会失败。
</li>
<li> 我们可以把整个策略包在一个 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 中，这样就可以一直进行有用
的重写，直到只剩下平凡的了。
</li>
</ul>
</div>
<div class="code code-tight">
<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'''''</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">find_rwinv</span>; <span class="id" type="tactic">repeat</span> <span class="id" type="var">find_eqn</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
这样做的一个重要的成果是，我们的证明脚本在一些对语言的不太大的改变
后仍能正常使用。比如，我们可以给这个语言增加一个 <span class="inlinecode"><span class="id" type="var">REPEAT</span></span> 命令。
（这是 <span class="inlinecode"><span class="id" type="var">Hoare.v</span></span>）里的一个练习）
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Repeat</span>.<br/>
<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">com</span> : <span class="id" type="keyword">Type</span> :=<br/>
| <span class="id" type="var">CSkip</span> : <span class="id" type="var">com</span><br/>
| <span class="id" type="var">CAsgn</span> : <span class="id" type="var">id</span> <span style="font-family: arial;">→</span> <span class="id" type="var">aexp</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span><br/>
| <span class="id" type="var">CSeq</span> : <span class="id" type="var">com</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span><br/>
| <span class="id" type="var">CIf</span> : <span class="id" type="var">bexp</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span><br/>
| <span class="id" type="var">CWhile</span> : <span class="id" type="var">bexp</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span><br/>
| <span class="id" type="var">CRepeat</span> : <span class="id" type="var">com</span> <span style="font-family: arial;">→</span> <span class="id" type="var">bexp</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span>.<br/>
<br/>
</div>
<div class="doc">
<span class="inlinecode"><span class="id" type="var">REPEAT</span></span> 行为和 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 类似, 只是循环条件在每次循环主体执行 <i>之后_
执行，当条件为 <i>假_ 时重复执行。因此，循环主体至少会执行一次。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Notation</span> "'SKIP'" := <br/>
<span class="id" type="var">CSkip</span>.<br/>
<span class="id" type="keyword">Notation</span> "c1 ; c2" := <br/>
(<span class="id" type="var">CSeq</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
<span class="id" type="keyword">Notation</span> "X '::=' a" := <br/>
(<span class="id" type="var">CAsgn</span> <span class="id" type="var">X</span> <span class="id" type="var">a</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60).<br/>
<span class="id" type="keyword">Notation</span> "'WHILE' b 'DO' c 'END'" := <br/>
(<span class="id" type="var">CWhile</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
<span class="id" type="keyword">Notation</span> "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" := <br/>
(<span class="id" type="var">CIf</span> <span class="id" type="var">e1</span> <span class="id" type="var">e2</span> <span class="id" type="var">e3</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
<span class="id" type="keyword">Notation</span> "'REPEAT' e1 'UNTIL' b2 'END'" := <br/>
(<span class="id" type="var">CRepeat</span> <span class="id" type="var">e1</span> <span class="id" type="var">b2</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ceval</span> : <span class="id" type="var">state</span> <span style="font-family: arial;">→</span> <span class="id" type="var">com</span> <span style="font-family: arial;">→</span> <span class="id" type="var">state</span> <span style="font-family: arial;">→</span> <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">E_Skip</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">st</span>,<br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">st</span><br/>
| <span class="id" type="var">E_Ass</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">a1</span> <span class="id" type="var">n</span> <span class="id" type="var">X</span>,<br/>
<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a1</span> = <span class="id" type="var">n</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">X</span> ::= <span class="id" type="var">a1</span>) (<span class="id" type="var">update</span> <span class="id" type="var">st</span> <span class="id" type="var">X</span> <span class="id" type="var">n</span>)<br/>
| <span class="id" type="var">E_Seq</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span>,<br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">c1</span> <span class="id" type="var">st'</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st'</span> <span class="id" type="var">c2</span> <span class="id" type="var">st''</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">c1</span> ; <span class="id" type="var">c2</span>) <span class="id" type="var">st''</span><br/>
| <span class="id" type="var">E_IfTrue</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b1</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span>,<br/>
<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b1</span> = <span class="id" type="var">true</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">c1</span> <span class="id" type="var">st'</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">IFB</span> <span class="id" type="var">b1</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c1</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c2</span> <span class="id" type="var">FI</span>) <span class="id" type="var">st'</span><br/>
| <span class="id" type="var">E_IfFalse</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b1</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span>,<br/>
<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b1</span> = <span class="id" type="var">false</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">c2</span> <span class="id" type="var">st'</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">IFB</span> <span class="id" type="var">b1</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c1</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c2</span> <span class="id" type="var">FI</span>) <span class="id" type="var">st'</span><br/>
| <span class="id" type="var">E_WhileEnd</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">b1</span> <span class="id" type="var">st</span> <span class="id" type="var">c1</span>,<br/>
<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b1</span> = <span class="id" type="var">false</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b1</span> <span class="id" type="var">DO</span> <span class="id" type="var">c1</span> <span class="id" type="var">END</span>) <span class="id" type="var">st</span><br/>
| <span class="id" type="var">E_WhileLoop</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span> <span class="id" type="var">b1</span> <span class="id" type="var">c1</span>,<br/>
<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b1</span> = <span class="id" type="var">true</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">c1</span> <span class="id" type="var">st'</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st'</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b1</span> <span class="id" type="var">DO</span> <span class="id" type="var">c1</span> <span class="id" type="var">END</span>) <span class="id" type="var">st''</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b1</span> <span class="id" type="var">DO</span> <span class="id" type="var">c1</span> <span class="id" type="var">END</span>) <span class="id" type="var">st''</span><br/>
| <span class="id" type="var">E_RepeatEnd</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b1</span> <span class="id" type="var">c1</span>,<br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">c1</span> <span class="id" type="var">st'</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">beval</span> <span class="id" type="var">st'</span> <span class="id" type="var">b1</span> = <span class="id" type="var">true</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">CRepeat</span> <span class="id" type="var">c1</span> <span class="id" type="var">b1</span>) <span class="id" type="var">st'</span><br/>
| <span class="id" type="var">E_RepeatLoop</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span> <span class="id" type="var">b1</span> <span class="id" type="var">c1</span>,<br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">c1</span> <span class="id" type="var">st'</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">beval</span> <span class="id" type="var">st'</span> <span class="id" type="var">b1</span> = <span class="id" type="var">false</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st'</span> (<span class="id" type="var">CRepeat</span> <span class="id" type="var">c1</span> <span class="id" type="var">b1</span>) <span class="id" type="var">st''</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> (<span class="id" type="var">CRepeat</span> <span class="id" type="var">c1</span> <span class="id" type="var">b1</span>) <span class="id" type="var">st''</span><br/>
.<br/>
<br/>
<span class="id" type="keyword">Notation</span> "c1 '/' st '<span style="font-family: arial;">⇓</span>' st'" := (<span class="id" type="var">ceval</span> <span class="id" type="var">st</span> <span class="id" type="var">c1</span> <span class="id" type="var">st'</span>) <br/>
(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40, <span class="id" type="var">st</span> <span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 39).<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">find_rwinv</span>; <span class="id" type="tactic">repeat</span> <span class="id" type="var">find_eqn</span>; <span class="id" type="tactic">auto</span>.<br/>
- <span class="comment">(* E_RepeatEnd *)</span><br/>
+ <span class="comment">(* b 求值为假（矛盾） *)</span><br/>
<span class="id" type="var">find_rwinv</span>.<br/>
<span class="comment">(* 啊呀，为什么刚才 find_rwinv 没有为我们解决这个呢？<br/>
因为我们把顺序搞错了*)</span><br/>
- <span class="comment">(* E_RepeatLoop *)</span><br/>
+ <span class="comment">(* b 求值为真（矛盾） *)</span><br/>
<span class="id" type="var">find_rwinv</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span>,<br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st1</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">c</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st2</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">st1</span> = <span class="id" type="var">st2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st1</span> <span class="id" type="var">st2</span> <span class="id" type="var">E1</span> <span class="id" type="var">E2</span>;<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st2</span>;<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">E1</span>;<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st2</span> <span class="id" type="var">E2</span>; <span class="id" type="var">inv</span> <span class="id" type="var">E2</span>; <span class="id" type="tactic">repeat</span> <span class="id" type="var">find_eqn</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">find_rwinv</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Repeat</span>.<br/>
<br/>
</div>
<div class="doc">
这些例子只是给大家看看“高级自动化”可以做到什么。
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" type="keyword">match</span></span> <span class="inlinecode"><span class="id" type="var">goal</span></span> 在使用时的细节十分复杂，调试也很不方便。但是我们非常值得
在证明时至少加入简单的自动化，来避免繁琐的工作，并为未来的修改做好准备。
<div class="paragraph"> </div>
</div>
<div class="code code-tight">
</div>
</div>
<div id="footer">
<hr/><a href="coqindex.html">Index</a></div>
</div>
</body>
</html>