-
Notifications
You must be signed in to change notification settings - Fork 1
/
Imp.html
3091 lines (2503 loc) · 236 KB
/
Imp.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
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!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>Imp: Simple Imperative Programs</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">Imp<span class="subtitle">Simple Imperative Programs</span></h1>
<div class="code code-tight">
</div>
<div class="doc">
<div class="paragraph"> </div>
In this chapter, we begin a new direction that will continue for
the rest of the course. Up to now most of our attention has been
focused on various aspects of Coq itself, while from now on we'll
mostly be using Coq to formalize other things. (We'll continue to
pause from time to time to introduce a few additional aspects of
Coq.)
<div class="paragraph"> </div>
Our first case study is a <i>simple imperative programming language</i>
called Imp, embodying a tiny core fragment of conventional
mainstream languages such as C and Java. Here is a familiar
mathematical function written in Imp.
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">Z</span> ::= <span class="id" type="var">X</span>;;<br/>
<span class="id" type="var">Y</span> ::= 1;;<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">not</span> (<span class="id" type="var">Z</span> = 0) <span class="id" type="var">DO</span><br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> × <span class="id" type="var">Z</span>;;<br/>
<span class="id" type="var">Z</span> ::= <span class="id" type="var">Z</span> - 1<br/>
<span class="id" type="var">END</span>
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
This chapter looks at how to define the <i>syntax</i> and <i>semantics</i>
of Imp; the chapters that follow develop a theory of <i>program
equivalence</i> and introduce <i>Hoare Logic</i>, a widely used logic for
reasoning about imperative programs.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab374"></a><h3 class="section">Sflib</h3>
<div class="paragraph"> </div>
A minor technical point: Instead of asking Coq to import our
earlier definitions from chapter <span class="inlinecode"><span class="id" type="var">Logic</span></span>, we import a small library
called <span class="inlinecode"><span class="id" type="var">Sflib.v</span></span>, containing just a few definitions and theorems
from earlier chapters that we'll actually use in the rest of the
course. This change should be nearly invisible, since most of what's
missing from Sflib has identical definitions in the Coq standard
library. The main reason for doing it is to tidy the global Coq
environment so that, for example, it is easier to search for
relevant theorems.
</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">SfLib</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab375"></a><h1 class="section">Arithmetic and Boolean Expressions</h1>
<div class="paragraph"> </div>
We'll present Imp in three parts: first a core language of
<i>arithmetic and boolean expressions</i>, then an extension of these
expressions with <i>variables</i>, and finally a language of <i>commands</i>
including assignment, conditions, sequencing, and loops.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab376"></a><h2 class="section">Syntax</h2>
</div>
<div class="code code-space">
<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">AExp</span>.<br/>
<br/>
</div>
<div class="doc">
These two definitions specify the <i>abstract syntax</i> of
arithmetic and boolean expressions.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
| <span class="id" type="var">ANum</span> : <span class="id" type="var">nat</span> <span style="font-family: arial;">→</span> <span class="id" type="var">aexp</span><br/>
| <span class="id" type="var">APlus</span> : <span class="id" type="var">aexp</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">aexp</span><br/>
| <span class="id" type="var">AMinus</span> : <span class="id" type="var">aexp</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">aexp</span><br/>
| <span class="id" type="var">AMult</span> : <span class="id" type="var">aexp</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">aexp</span>.<br/>
<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">bexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
| <span class="id" type="var">BTrue</span> : <span class="id" type="var">bexp</span><br/>
| <span class="id" type="var">BFalse</span> : <span class="id" type="var">bexp</span><br/>
| <span class="id" type="var">BEq</span> : <span class="id" type="var">aexp</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">bexp</span><br/>
| <span class="id" type="var">BLe</span> : <span class="id" type="var">aexp</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">bexp</span><br/>
| <span class="id" type="var">BNot</span> : <span class="id" type="var">bexp</span> <span style="font-family: arial;">→</span> <span class="id" type="var">bexp</span><br/>
| <span class="id" type="var">BAnd</span> : <span class="id" type="var">bexp</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">bexp</span>.<br/>
<br/>
</div>
<div class="doc">
In this chapter, we'll elide the translation from the
concrete syntax that a programmer would actually write to these
abstract syntax trees — the process that, for example, would
translate the string <span class="inlinecode">"1+2×3"</span> to the AST <span class="inlinecode"><span class="id" type="var">APlus</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span>
<span class="inlinecode">1)</span> <span class="inlinecode">(<span class="id" type="var">AMult</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">2)</span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">3))</span>. The optional chapter <span class="inlinecode"><span class="id" type="var">ImpParser</span></span>
develops a simple implementation of a lexical analyzer and parser
that can perform this translation. You do <i>not</i> need to
understand that file to understand this one, but if you haven't
taken a course where these techniques are covered (e.g., a
compilers course) you may want to skim it.
<div class="paragraph"> </div>
<a name="lab377"></a><h3 class="section"> </h3>
For comparison, here's a conventional BNF (Backus-Naur Form)
grammar defining the same abstract syntax:
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">a</span> ::= <span class="id" type="var">nat</span><br/>
| <span class="id" type="var">a</span> + <span class="id" type="var">a</span><br/>
| <span class="id" type="var">a</span> - <span class="id" type="var">a</span><br/>
| <span class="id" type="var">a</span> × <span class="id" type="var">a</span><br/>
<br/>
<span class="id" type="var">b</span> ::= <span class="id" type="var">true</span><br/>
| <span class="id" type="var">false</span><br/>
| <span class="id" type="var">a</span> = <span class="id" type="var">a</span><br/>
| <span class="id" type="var">a</span> ≤ <span class="id" type="var">a</span><br/>
| <span class="id" type="var">not</span> <span class="id" type="var">b</span><br/>
| <span class="id" type="var">b</span> <span class="id" type="var">and</span> <span class="id" type="var">b</span>
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
Compared to the Coq version above...
<div class="paragraph"> </div>
<ul class="doclist">
<li> The BNF is more informal — for example, it gives some
suggestions about the surface syntax of expressions (like the
fact that the addition operation is written <span class="inlinecode">+</span> and is an
infix symbol) while leaving other aspects of lexical analysis
and parsing (like the relative precedence of <span class="inlinecode">+</span>, <span class="inlinecode">-</span>, and
<span class="inlinecode">×</span>) unspecified. Some additional information — and human
intelligence — would be required to turn this description
into a formal definition (when implementing a compiler, for
example).
<div class="paragraph"> </div>
The Coq version consistently omits all this information and
concentrates on the abstract syntax only.
<div class="paragraph"> </div>
</li>
<li> On the other hand, the BNF version is lighter and
easier to read. Its informality makes it flexible, which is
a huge advantage in situations like discussions at the
blackboard, where conveying general ideas is more important
than getting every detail nailed down precisely.
<div class="paragraph"> </div>
Indeed, there are dozens of BNF-like notations and people
switch freely among them, usually without bothering to say which
form of BNF they're using because there is no need to: a
rough-and-ready informal understanding is all that's
needed.
</li>
</ul>
<div class="paragraph"> </div>
It's good to be comfortable with both sorts of notations:
informal ones for communicating between humans and formal ones for
carrying out implementations and proofs.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab378"></a><h2 class="section">Evaluation</h2>
<div class="paragraph"> </div>
<i>Evaluating</i> an arithmetic expression produces a number.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">aeval</span> (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">nat</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span> ⇒ <span class="id" type="var">n</span><br/>
| <span class="id" type="var">APlus</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a1</span>) + (<span class="id" type="var">aeval</span> <span class="id" type="var">a2</span>)<br/>
| <span class="id" type="var">AMinus</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a1</span>) - (<span class="id" type="var">aeval</span> <span class="id" type="var">a2</span>)<br/>
| <span class="id" type="var">AMult</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a1</span>) × (<span class="id" type="var">aeval</span> <span class="id" type="var">a2</span>)<br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_aeval1</span>:<br/>
<span class="id" type="var">aeval</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 2) (<span class="id" type="var">ANum</span> 2)) = 4.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab379"></a><h3 class="section"> </h3>
Similarly, evaluating a boolean expression yields a boolean.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">beval</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bool</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">BTrue</span> ⇒ <span class="id" type="var">true</span><br/>
| <span class="id" type="var">BFalse</span> ⇒ <span class="id" type="var">false</span><br/>
| <span class="id" type="var">BEq</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> ⇒ <span class="id" type="var">beq_nat</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">a1</span>) (<span class="id" type="var">aeval</span> <span class="id" type="var">a2</span>)<br/>
| <span class="id" type="var">BLe</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> ⇒ <span class="id" type="var">ble_nat</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">a1</span>) (<span class="id" type="var">aeval</span> <span class="id" type="var">a2</span>)<br/>
| <span class="id" type="var">BNot</span> <span class="id" type="var">b1</span> ⇒ <span class="id" type="var">negb</span> (<span class="id" type="var">beval</span> <span class="id" type="var">b1</span>)<br/>
| <span class="id" type="var">BAnd</span> <span class="id" type="var">b1</span> <span class="id" type="var">b2</span> ⇒ <span class="id" type="var">andb</span> (<span class="id" type="var">beval</span> <span class="id" type="var">b1</span>) (<span class="id" type="var">beval</span> <span class="id" type="var">b2</span>)<br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab380"></a><h2 class="section">Optimization</h2>
<div class="paragraph"> </div>
We haven't defined very much yet, but we can already get
some mileage out of the definitions. Suppose we define a function
that takes an arithmetic expression and slightly simplifies it,
changing every occurrence of <span class="inlinecode">0+<span class="id" type="var">e</span></span> (i.e., <span class="inlinecode">(<span class="id" type="var">APlus</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">0)</span> <span class="inlinecode"><span class="id" type="var">e</span></span>)
into just <span class="inlinecode"><span class="id" type="var">e</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">optimize_0plus</span> (<span class="id" type="var">a</span>:<span class="id" type="var">aexp</span>) : <span class="id" type="var">aexp</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span> ⇒<br/>
<span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
| <span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 0) <span class="id" type="var">e2</span> ⇒<br/>
<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e2</span><br/>
| <span class="id" type="var">APlus</span> <span class="id" type="var">e1</span> <span class="id" type="var">e2</span> ⇒<br/>
<span class="id" type="var">APlus</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e1</span>) (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e2</span>)<br/>
| <span class="id" type="var">AMinus</span> <span class="id" type="var">e1</span> <span class="id" type="var">e2</span> ⇒<br/>
<span class="id" type="var">AMinus</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e1</span>) (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e2</span>)<br/>
| <span class="id" type="var">AMult</span> <span class="id" type="var">e1</span> <span class="id" type="var">e2</span> ⇒<br/>
<span class="id" type="var">AMult</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e1</span>) (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e2</span>)<br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
To make sure our optimization is doing the right thing we
can test it on some examples and see if the output looks OK.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_optimize_0plus</span>:<br/>
<span class="id" type="var">optimize_0plus</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 2)<br/>
(<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 0)<br/>
(<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 0) (<span class="id" type="var">ANum</span> 1))))<br/>
= <span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 2) (<span class="id" type="var">ANum</span> 1).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
But if we want to be sure the optimization is correct —
i.e., that evaluating an optimized expression gives the same
result as the original — we should prove it.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_sound</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">a</span>,<br/>
<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="var">Case</span> "ANum". <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "APlus". <span class="id" type="tactic">destruct</span> <span class="id" type="var">a1</span>.<br/>
<span class="id" type="var">SCase</span> "a1 = ANum n". <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="var">SSCase</span> "n = 0". <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHa2</span>.<br/>
<span class="id" type="var">SSCase</span> "n ≠ 0". <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">SCase</span> "a1 = APlus a1_1 a1_2".<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">SCase</span> "a1 = AMinus a1_1 a1_2".<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">SCase</span> "a1 = AMult a1_1 a1_2".<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "AMinus".<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "AMult".<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab381"></a><h1 class="section">Coq Automation</h1>
<div class="paragraph"> </div>
The repetition in this last proof is starting to be a little
annoying. If either the language of arithmetic expressions or the
optimization being proved sound were significantly more complex,
it would begin to be a real problem.
<div class="paragraph"> </div>
So far, we've been doing all our proofs using just a small handful
of Coq's tactics and completely ignoring its powerful facilities
for constructing parts of proofs automatically. This section
introduces some of these facilities, and we will see more over the
next several chapters. Getting used to them will take some
energy — Coq's automation is a power tool — but it will allow us
to scale up our efforts to more complex definitions and more
interesting properties without becoming overwhelmed by boring,
repetitive, low-level details.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab382"></a><h2 class="section">Tacticals</h2>
<div class="paragraph"> </div>
<i>Tacticals</i> is Coq's term for tactics that take other tactics as
arguments — "higher-order tactics," if you will.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab383"></a><h3 class="section">The <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> Tactical</h3>
<div class="paragraph"> </div>
The <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> tactical takes another tactic and keeps applying
this tactic until the tactic fails. Here is an example showing
that <span class="inlinecode">100</span> is even using repeat.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev100</span> : <span class="id" type="var">ev</span> 100.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">repeat</span> (<span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>). <span class="comment">(* applies ev_SS 50 times,<br/>
until <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> fails *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">ev_0</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<span class="comment">(* Print ev100. *)</span><br/>
<br/>
</div>
<div class="doc">
The <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> tactic never fails; if the tactic <span class="inlinecode"><span class="id" type="var">T</span></span> doesn't apply
to the original goal, then repeat still succeeds without changing
the original goal (it repeats zero times).
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev100'</span> : <span class="id" type="var">ev</span> 100.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">repeat</span> (<span class="id" type="tactic">apply</span> <span class="id" type="var">ev_0</span>). <span class="comment">(* doesn't fail, applies ev_0 zero times *)</span><br/>
<span class="id" type="tactic">repeat</span> (<span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_0</span>. <span class="comment">(* we can continue the proof *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
The <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> tactic does not have any bound on the number of
times it applies <span class="inlinecode"><span class="id" type="var">T</span></span>. If <span class="inlinecode"><span class="id" type="var">T</span></span> is a tactic that always succeeds then
repeat <span class="inlinecode"><span class="id" type="var">T</span></span> will loop forever (e.g. <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> loops forever
since <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> always succeeds). While Coq's term language is
guaranteed to terminate, Coq's tactic language is not!
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab384"></a><h3 class="section">The <span class="inlinecode"><span class="id" type="tactic">try</span></span> Tactical</h3>
<div class="paragraph"> </div>
If <span class="inlinecode"><span class="id" type="var">T</span></span> is a tactic, then <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> is a tactic that is just like <span class="inlinecode"><span class="id" type="var">T</span></span>
except that, if <span class="inlinecode"><span class="id" type="var">T</span></span> fails, <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> <i>successfully</i> does nothing at
all (instead of failing).
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly1</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">ae</span>, <span class="id" type="var">aeval</span> <span class="id" type="var">ae</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">ae</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>. <span class="comment">(* this just does <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> *)</span> <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly2</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">P</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">P</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">HP</span>.<br/>
<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>. <span class="comment">(* just <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> would have failed *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">HP</span>. <span class="comment">(* we can still finish the proof in some other way *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Using <span class="inlinecode"><span class="id" type="tactic">try</span></span> in a completely manual proof is a bit silly, but
we'll see below that <span class="inlinecode"><span class="id" type="tactic">try</span></span> is very useful for doing automated
proofs in conjunction with the <span class="inlinecode">;</span> tactical.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab385"></a><h3 class="section">The <span class="inlinecode">;</span> Tactical (Simple Form)</h3>
<div class="paragraph"> </div>
In its most commonly used form, the <span class="inlinecode">;</span> tactical takes two tactics
as argument: <span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span> first performs the tactic <span class="inlinecode"><span class="id" type="var">T</span></span> and then
performs the tactic <span class="inlinecode"><span class="id" type="var">T'</span></span> on <i>each subgoal</i> generated by <span class="inlinecode"><span class="id" type="var">T</span></span>.
<div class="paragraph"> </div>
For example, consider the following trivial lemma:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">foo</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">n</span>, <span class="id" type="var">ble_nat</span> 0 <span class="id" type="var">n</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>.<br/>
<span class="comment">(* Leaves two subgoals, which are discharged identically... *)</span><br/>
<span class="id" type="var">Case</span> "n=0". <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "n=Sn'". <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
We can simplify this proof using the <span class="inlinecode">;</span> tactical:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">foo'</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">n</span>, <span class="id" type="var">ble_nat</span> 0 <span class="id" type="var">n</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>; <span class="comment">(* <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> the current goal *)</span><br/>
<span class="id" type="tactic">simpl</span>; <span class="comment">(* then <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> each resulting subgoal *)</span><br/>
<span class="id" type="tactic">reflexivity</span>. <span class="comment">(* and do <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> on each resulting subgoal *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Using <span class="inlinecode"><span class="id" type="tactic">try</span></span> and <span class="inlinecode">;</span> together, we can get rid of the repetition in
the proof that was bothering us a little while ago.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_sound'</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">a</span>,<br/>
<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>;<br/>
<span class="comment">(* Most cases follow directly by the IH *)</span><br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
<span class="comment">(* The remaining cases -- ANum and APlus -- are different *)</span><br/>
<span class="id" type="var">Case</span> "ANum". <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "APlus".<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">a1</span>;<br/>
<span class="comment">(* Again, most cases follow directly by the IH *)</span><br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>;<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
<span class="comment">(* The interesting case, on which the <span class="inlinecode"><span class="id" type="tactic">try</span>...</span> does nothing,<br/>
is when <span class="inlinecode"><span class="id" type="var">e1</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>. In this case, we have to destruct<br/>
<span class="inlinecode"><span class="id" type="var">n</span></span> (to see whether the optimization applies) and rewrite<br/>
with the induction hypothesis. *)</span><br/>
<span class="id" type="var">SCase</span> "a1 = ANum n". <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>;<br/>
<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Coq experts often use this "<span class="inlinecode">...;</span> <span class="inlinecode"><span class="id" type="tactic">try</span>...</span> <span class="inlinecode"></span>" idiom after a tactic
like <span class="inlinecode"><span class="id" type="tactic">induction</span></span> to take care of many similar cases all at once.
Naturally, this practice has an analog in informal proofs.
<div class="paragraph"> </div>
Here is an informal proof of this theorem that matches the
structure of the formal one:
<div class="paragraph"> </div>
<i>Theorem</i>: For all arithmetic expressions <span class="inlinecode"><span class="id" type="var">a</span></span>,
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.
<div class="paragraph"> </div>
</div>
<i>Proof</i>: By induction on <span class="inlinecode"><span class="id" type="var">a</span></span>. The <span class="inlinecode"><span class="id" type="var">AMinus</span></span> and <span class="inlinecode"><span class="id" type="var">AMult</span></span> cases
follow directly from the IH. The remaining cases are as follows:
<div class="paragraph"> </div>
<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> for some <span class="inlinecode"><span class="id" type="var">n</span></span>. We must show
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> (<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>)) = <span class="id" type="var">aeval</span> (<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>).
<div class="paragraph"> </div>
</div>
This is immediate from the definition of <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span>.
<div class="paragraph"> </div>
</li>
<li> Suppose <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">APlus</span></span> <span class="inlinecode"><span class="id" type="var">a1</span></span> <span class="inlinecode"><span class="id" type="var">a2</span></span> for some <span class="inlinecode"><span class="id" type="var">a1</span></span> and <span class="inlinecode"><span class="id" type="var">a2</span></span>. We
must show
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> (<span class="id" type="var">APlus</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span>))<br/>
= <span class="id" type="var">aeval</span> (<span class="id" type="var">APlus</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span>).
<div class="paragraph"> </div>
</div>
Consider the possible forms of <span class="inlinecode"><span class="id" type="var">a1</span></span>. For most of them,
<span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> simply calls itself recursively for the
subexpressions and rebuilds a new expression of the same form
as <span class="inlinecode"><span class="id" type="var">a1</span></span>; in these cases, the result follows directly from the
IH.
<div class="paragraph"> </div>
The interesting case is when <span class="inlinecode"><span class="id" type="var">a1</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> for some <span class="inlinecode"><span class="id" type="var">n</span></span>.
If <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode">0</span>, then
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">optimize_0plus</span> (<span class="id" type="var">APlus</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span>) = <span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a2</span>
<div class="paragraph"> </div>
</div>
and the IH for <span class="inlinecode"><span class="id" type="var">a2</span></span> is exactly what we need. On the other
hand, if <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> for some <span class="inlinecode"><span class="id" type="var">n'</span></span>, then again <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span>
simply calls itself recursively, and the result follows from
the IH. <font size=-2>☐</font>
</li>
</ul>
<div class="paragraph"> </div>
This proof can still be improved: the first case (for <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span>
<span class="inlinecode"><span class="id" type="var">n</span></span>) is very trivial — even more trivial than the cases that we
said simply followed from the IH — yet we have chosen to write it
out in full. It would be better and clearer to drop it and just
say, at the top, "Most cases are either immediate or direct from
the IH. The only interesting case is the one for <span class="inlinecode"><span class="id" type="var">APlus</span></span>..." We
can make the same improvement in our formal proof too. Here's how
it looks:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_sound''</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">a</span>,<br/>
<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>;<br/>
<span class="comment">(* Most cases follow directly by the IH *)</span><br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>);<br/>
<span class="comment">(* ... or are immediate by definition *)</span><br/>
<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="comment">(* The interesting case is when a = APlus a1 a2. *)</span><br/>
<span class="id" type="var">Case</span> "APlus".<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">a1</span>; <span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>;<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
<span class="id" type="var">SCase</span> "a1 = ANum n". <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>;<br/>
<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab386"></a><h3 class="section">The <span class="inlinecode">;</span> Tactical (General Form)</h3>
<div class="paragraph"> </div>
The <span class="inlinecode">;</span> tactical has a more general than the simple <span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span> we've
seen above, which is sometimes also useful. If <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">Tn</span></span> are tactics, then
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">T</span>; [<span class="id" type="var">T<sub>1</sub></span> | <span class="id" type="var">T<sub>2</sub></span> | ... | <span class="id" type="var">Tn</span>]
<div class="paragraph"> </div>
</div>
is a tactic that first performs <span class="inlinecode"><span class="id" type="var">T</span></span> and then performs <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> on the
first subgoal generated by <span class="inlinecode"><span class="id" type="var">T</span></span>, performs <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> on the second
subgoal, etc.
<div class="paragraph"> </div>
So <span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span> is just special notation for the case when all of the
<span class="inlinecode"><span class="id" type="var">Ti</span></span>'s are the same tactic; i.e. <span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span> is just a shorthand for:
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">T</span>; [<span class="id" type="var">T'</span> | <span class="id" type="var">T'</span> | ... | <span class="id" type="var">T'</span>]
<div class="paragraph"> </div>
</div>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab387"></a><h2 class="section">Defining New Tactic Notations</h2>
<div class="paragraph"> </div>
Coq also provides several ways of "programming" tactic scripts.
<div class="paragraph"> </div>
<ul class="doclist">
<li> The <span class="inlinecode"><span class="id" type="keyword">Tactic</span></span> <span class="inlinecode"><span class="id" type="keyword">Notation</span></span> idiom illustrated below gives a handy
way to define "shorthand tactics" that bundle several tactics
into a single command.
<div class="paragraph"> </div>
</li>
<li> For more sophisticated programming, Coq offers a small
built-in programming language called <span class="inlinecode"><span class="id" type="keyword">Ltac</span></span> with primitives
that can examine and modify the proof state. The details are
a bit too complicated to get into here (and it is generally
agreed that <span class="inlinecode"><span class="id" type="keyword">Ltac</span></span> is not the most beautiful part of Coq's
design!), but they can be found in the reference manual, and
there are many examples of <span class="inlinecode"><span class="id" type="keyword">Ltac</span></span> definitions in the Coq
standard library that you can use as examples.
<div class="paragraph"> </div>
</li>
<li> There is also an OCaml API, which can be used to build tactics
that access Coq's internal structures at a lower level, but
this is seldom worth the trouble for ordinary Coq users.
</li>
</ul>
<div class="paragraph"> </div>
The <span class="inlinecode"><span class="id" type="keyword">Tactic</span></span> <span class="inlinecode"><span class="id" type="keyword">Notation</span></span> mechanism is the easiest to come to grips with,
and it offers plenty of power for many purposes. Here's an example.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Tactic Notation</span> "simpl_and_try" <span class="id" type="var">tactic</span>(<span class="id" type="var">c</span>) :=<br/>
<span class="id" type="tactic">simpl</span>;<br/>
<span class="id" type="tactic">try</span> <span class="id" type="var">c</span>.<br/>
<br/>
</div>
<div class="doc">
This defines a new tactical called <span class="inlinecode"><span class="id" type="var">simpl_and_try</span></span> which
takes one tactic <span class="inlinecode"><span class="id" type="var">c</span></span> as an argument, and is defined to be
equivalent to the tactic <span class="inlinecode"><span class="id" type="tactic">simpl</span>;</span> <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span>. For example, writing
"<span class="inlinecode"><span class="id" type="var">simpl_and_try</span></span> <span class="inlinecode"><span class="id" type="tactic">reflexivity</span>.</span>" in a proof would be the same as
writing "<span class="inlinecode"><span class="id" type="tactic">simpl</span>;</span> <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="tactic">reflexivity</span>.</span>"
<div class="paragraph"> </div>
The next subsection gives a more sophisticated use of this
feature...
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab388"></a><h3 class="section">Bulletproofing Case Analyses</h3>
<div class="paragraph"> </div>
Being able to deal with most of the cases of an <span class="inlinecode"><span class="id" type="tactic">induction</span></span>
or <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> all at the same time is very convenient, but it can
also be a little confusing. One problem that often comes up is
that <i>maintaining</i> proofs written in this style can be difficult.
For example, suppose that, later, we extended the definition of
<span class="inlinecode"><span class="id" type="var">aexp</span></span> with another constructor that also required a special
argument. The above proof might break because Coq generated the
subgoals for this constructor before the one for <span class="inlinecode"><span class="id" type="var">APlus</span></span>, so that,
at the point when we start working on the <span class="inlinecode"><span class="id" type="var">APlus</span></span> case, Coq is
actually expecting the argument for a completely different
constructor. What we'd like is to get a sensible error message
saying "I was expecting the <span class="inlinecode"><span class="id" type="var">AFoo</span></span> case at this point, but the
proof script is talking about <span class="inlinecode"><span class="id" type="var">APlus</span></span>." Here's a nice trick (due
to Aaron Bohannon) that smoothly achieves this.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Tactic Notation</span> "aexp_cases" <span class="id" type="var">tactic</span>(<span class="id" type="var">first</span>) <span class="id" type="var">ident</span>(<span class="id" type="var">c</span>) :=<br/>
<span class="id" type="var">first</span>;<br/>
[ <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "ANum" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "APlus"<br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "AMinus" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "AMult" ].<br/>
<br/>
</div>
<div class="doc">
(<span class="inlinecode"><span class="id" type="var">Case_aux</span></span> implements the common functionality of <span class="inlinecode"><span class="id" type="var">Case</span></span>,
<span class="inlinecode"><span class="id" type="var">SCase</span></span>, <span class="inlinecode"><span class="id" type="var">SSCase</span></span>, etc. For example, <span class="inlinecode"><span class="id" type="var">Case</span></span> <span class="inlinecode">"<span class="id" type="var">foo</span>"</span> is defined as
<span class="inlinecode"><span class="id" type="var">Case_aux</span></span> <span class="inlinecode"><span class="id" type="var">Case</span></span> <span class="inlinecode">"<span class="id" type="var">foo</span>".)</span> <span class="inlinecode"></span>
<div class="paragraph"> </div>
For example, if <span class="inlinecode"><span class="id" type="var">a</span></span> is a variable of type <span class="inlinecode"><span class="id" type="var">aexp</span></span>, then doing
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">aexp_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>) <span class="id" type="var">Case</span>
<div class="paragraph"> </div>
</div>
will perform an induction on <span class="inlinecode"><span class="id" type="var">a</span></span> (the same as if we had just typed
<span class="inlinecode"><span class="id" type="tactic">induction</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span>) and <i>also</i> add a <span class="inlinecode"><span class="id" type="var">Case</span></span> tag to each subgoal
generated by the <span class="inlinecode"><span class="id" type="tactic">induction</span></span>, labeling which constructor it comes
from. For example, here is yet another proof of
<span class="inlinecode"><span class="id" type="var">optimize_0plus_sound</span></span>, using <span class="inlinecode"><span class="id" type="var">aexp_cases</span></span>:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_sound'''</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">a</span>,<br/>
<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="var">aexp_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>) <span class="id" type="var">Case</span>;<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>);<br/>
<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="comment">(* At this point, there is already an <span class="inlinecode">"<span class="id" type="var">APlus</span>"</span> case name<br/>
in the context. The <span class="inlinecode"><span class="id" type="var">Case</span></span> <span class="inlinecode">"<span class="id" type="var">APlus</span>"</span> here in the proof<br/>
text has the effect of a sanity check: if the "Case"<br/>
string in the context is anything _other_ than <span class="inlinecode">"<span class="id" type="var">APlus</span>"</span><br/>
(for example, because we added a clause to the definition<br/>
of <span class="inlinecode"><span class="id" type="var">aexp</span></span> and forgot to change the proof) we'll get a<br/>
helpful error at this point telling us that this is now<br/>
the wrong case. *)</span><br/>
<span class="id" type="var">Case</span> "APlus".<br/>
<span class="id" type="var">aexp_cases</span> (<span class="id" type="tactic">destruct</span> <span class="id" type="var">a1</span>) <span class="id" type="var">SCase</span>;<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>;<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
<span class="id" type="var">SCase</span> "ANum". <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>;<br/>
<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab389"></a><h4 class="section">Exercise: 3 stars (optimize_0plus_b)</h4>
Since the <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> tranformation doesn't change the value
of <span class="inlinecode"><span class="id" type="var">aexp</span></span>s, we should be able to apply it to all the <span class="inlinecode"><span class="id" type="var">aexp</span></span>s that
appear in a <span class="inlinecode"><span class="id" type="var">bexp</span></span> without changing the <span class="inlinecode"><span class="id" type="var">bexp</span></span>'s value. Write a
function which performs that transformation on <span class="inlinecode"><span class="id" type="var">bexp</span></span>s, and prove
it is sound. Use the tacticals we've just seen to make the proof
as elegant as possible.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">optimize_0plus_b</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bexp</span> :=<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">admit</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_b_sound</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">b</span>,<br/>
<span class="id" type="var">beval</span> (<span class="id" type="var">optimize_0plus_b</span> <span class="id" type="var">b</span>) = <span class="id" type="var">beval</span> <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
<font size=-2>☐</font>
<div class="paragraph"> </div>
<a name="lab390"></a><h4 class="section">Exercise: 4 stars, optional (optimizer)</h4>
<i>Design exercise</i>: The optimization implemented by our
<span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> function is only one of many imaginable
optimizations on arithmetic and boolean expressions. Write a more
sophisticated optimizer and prove it correct.
<div class="paragraph"> </div>
<span class="comment">(* FILL IN HERE *)</span><br/>
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab391"></a><h2 class="section">The <span class="inlinecode"><span class="id" type="tactic">omega</span></span> Tactic</h2>
<div class="paragraph"> </div>
The <span class="inlinecode"><span class="id" type="tactic">omega</span></span> tactic implements a decision procedure for a subset of
first-order logic called <i>Presburger arithmetic</i>. It is based on
the Omega algorithm invented in 1992 by William Pugh.
<div class="paragraph"> </div>
If the goal is a universally quantified formula made out of
<div class="paragraph"> </div>
<ul class="doclist">
<li> numeric constants, addition (<span class="inlinecode">+</span> and <span class="inlinecode"><span class="id" type="var">S</span></span>), subtraction (<span class="inlinecode">-</span>
and <span class="inlinecode"><span class="id" type="var">pred</span></span>), and multiplication by constants (this is what
makes it Presburger arithmetic),
<div class="paragraph"> </div>
</li>
<li> equality (<span class="inlinecode">=</span> and <span class="inlinecode">≠</span>) and inequality (<span class="inlinecode">≤</span>), and
<div class="paragraph"> </div>
</li>
<li> the logical connectives <span class="inlinecode"><span style="font-family: arial;">∧</span></span>, <span class="inlinecode"><span style="font-family: arial;">∨</span></span>, <span class="inlinecode">¬</span>, and <span class="inlinecode"><span style="font-family: arial;">→</span></span>,
</li>
</ul>
<div class="paragraph"> </div>
then invoking <span class="inlinecode"><span class="id" type="tactic">omega</span></span> will either solve the goal or tell you that
it is actually false.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">silly_presburger_example</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> <span class="id" type="var">p</span>,<br/>
<span class="id" type="var">m</span> + <span class="id" type="var">n</span> ≤ <span class="id" type="var">n</span> + <span class="id" type="var">o</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">o</span> + 3 = <span class="id" type="var">p</span> + 3 <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">m</span> ≤ <span class="id" type="var">p</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Liebniz wrote, "It is unworthy of excellent men to lose
hours like slaves in the labor of calculation which could be
relegated to anyone else if machines were used." We recommend
using the omega tactic whenever possible.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab392"></a><h2 class="section">A Few More Handy Tactics</h2>
<div class="paragraph"> </div>
Finally, here are some miscellaneous tactics that you may find
convenient.
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="tactic">clear</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>: Delete hypothesis <span class="inlinecode"><span class="id" type="var">H</span></span> from the context.
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode"><span class="id" type="tactic">subst</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>: Find an assumption <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span> or <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span> in the
context, replace <span class="inlinecode"><span class="id" type="var">x</span></span> with <span class="inlinecode"><span class="id" type="var">e</span></span> throughout the context and
current goal, and clear the assumption.
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode"><span class="id" type="tactic">subst</span></span>: Substitute away <i>all</i> assumptions of the form <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span>
or <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span>.
<div class="paragraph"> </div>
</li>