/
UseAuto.html
2490 lines (2099 loc) · 257 KB
/
UseAuto.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="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>UseAuto: Theory and Practice of Automation in Coq Proofs</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
<body>
<div id="page">
<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'> <span class='booktitleinheader'>Volume 2: Programming Language Foundations</span><br></br>
<ul id='menu'>
<a href='toc.html'><li class='section_name'>Table of Contents</li></a>
<a href='coqindex.html'><li class='section_name'>Index</li></a>
<a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>
<div id="main">
<h1 class="libtitle">UseAuto<span class="subtitle">Theory and Practice of Automation in Coq Proofs</span></h1>
<div class="code code-tight">
<span class="comment">(* Chapter written and maintained by Arthur Chargueraud *)</span><br/>
</div>
<div class="doc">
In a machine-checked proof, every single detail has to be
justified. This can result in huge proof scripts. Fortunately,
Coq comes with a proof-search mechanism and with several decision
procedures that enable the system to automatically synthesize
simple pieces of proof. Automation is very powerful when set up
appropriately. The purpose of this chapter is to explain the
basics of how automation works in Coq.
<div class="paragraph"> </div>
The chapter is organized in two parts. The first part focuses on a
general mechanism called "proof search." In short, proof search
consists in naively trying to apply lemmas and assumptions in all
possible ways. The second part describes "decision procedures",
which are tactics that are very good at solving proof obligations
that fall in some particular fragments of the logic of Coq.
<div class="paragraph"> </div>
Many of the examples used in this chapter consist of small lemmas
that have been made up to illustrate particular aspects of automation.
These examples are completely independent from the rest of the Software
Foundations course. This chapter also contains some bigger examples
which are used to explain how to use automation in realistic proofs.
These examples are taken from other chapters of the course (mostly
from STLC), and the proofs that we present make use of the tactics
from the library <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>, which is presented in the chapter
<span class="inlinecode"><span class="id" type="var">UseTactics</span></span>.
</div>
<div class="code code-tight">
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Smallstep</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Stlc</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">LibTactics</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="var">Imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Lists.List</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">ListNotations</span>.<br/>
</div>
<div class="doc">
<a name="lab545"></a><h1 class="section">Basic Features of Proof Search</h1>
<div class="paragraph"> </div>
The idea of proof search is to replace a sequence of tactics
applying lemmas and assumptions with a call to a single tactic,
for example <span class="inlinecode"><span class="id" type="tactic">auto</span></span>. This form of proof automation saves a lot of
effort. It typically leads to much shorter proof scripts, and to
scripts that are typically more robust to change. If one makes a
little change to a definition, a proof that exploits automation
probably won't need to be modified at all. Of course, using too
much automation is a bad idea. When a proof script no longer
records the main arguments of a proof, it becomes difficult to fix
it when it gets broken after a change in a definition. Overall, a
reasonable use of automation is generally a big win, as it saves a
lot of time both in building proof scripts and in subsequently
maintaining those proof scripts.
</div>
<div class="doc">
<a name="lab546"></a><h2 class="section">Strength of Proof Search</h2>
<div class="paragraph"> </div>
We are going to study four proof-search tactics: <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="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span>. The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> are builtin
in Coq. The tactic <span class="inlinecode"><span class="id" type="var">iauto</span></span> is a shorthand for the builtin tactic
<span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">solve</span></span> <span class="inlinecode">[<span class="id" type="tactic">intuition</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span>]</span>. The tactic <span class="inlinecode"><span class="id" type="var">jauto</span></span> is defined in
the library <span class="inlinecode"><span class="id" type="var">LibTactics</span></span>, and simply performs some preprocessing
of the goal before calling <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>. The goal of this chapter is
to explain the general principles of proof search and to give
rule of thumbs for guessing which of the four tactics mentioned
above is best suited for solving a given goal.
<div class="paragraph"> </div>
Proof search is a compromise between efficiency and
expressiveness, that is, a tradeoff between how complex goals the
tactic can solve and how much time the tactic requires for
terminating. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> builds proofs only by using the
basic tactics <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>, <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>, and <span class="inlinecode"><span class="id" type="tactic">apply</span></span>. The tactic
<span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can also exploit <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>. The tactic <span class="inlinecode"><span class="id" type="var">jauto</span></span> extends
<span class="inlinecode"><span class="id" type="tactic">eauto</span></span> by being able to open conjunctions and existentials that
occur in the context. The tactic <span class="inlinecode"><span class="id" type="var">iauto</span></span> is able to deal with
conjunctions, disjunctions, and negation in a quite clever way;
however it is not able to open existentials from the context.
Also, <span class="inlinecode"><span class="id" type="var">iauto</span></span> usually becomes very slow when the goal involves
several disjunctions.
<div class="paragraph"> </div>
Note that proof search tactics never perform any rewriting
step (tactics <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>, <span class="inlinecode"><span class="id" type="tactic">subst</span></span>), nor any case analysis on an
arbitrary data structure or property (tactics <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> and
<span class="inlinecode"><span class="id" type="tactic">inversion</span></span>), nor any proof by induction (tactic <span class="inlinecode"><span class="id" type="tactic">induction</span></span>). So,
proof search is really intended to automate the final steps from
the various branches of a proof. It is not able to discover the
overall structure of a proof.
</div>
<div class="doc">
<a name="lab547"></a><h2 class="section">Basics</h2>
<div class="paragraph"> </div>
The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is able to solve a goal that can be proved
using a sequence of <span class="inlinecode"><span class="id" type="tactic">intros</span></span>, <span class="inlinecode"><span class="id" type="tactic">apply</span></span>, <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>, and <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>.
Two examples follow. The first one shows the ability for
<span class="inlinecode"><span class="id" type="tactic">auto</span></span> to call <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> at any time. In fact, calling
<span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> is always the first thing that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tries to do.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_by_reflexivity</span> :<br/>
2 + 3 = 5.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
The second example illustrates a proof where a sequence of
two calls to <span class="inlinecode"><span class="id" type="tactic">apply</span></span> are needed. The goal is to prove that
if <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> implies <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> for any <span class="inlinecode"><span class="id" type="var">n</span></span> and if <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> holds for any <span class="inlinecode"><span class="id" type="var">n</span></span>,
then <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span> holds.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_by_apply</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span>, <span class="id" type="var">Q</span> <span class="id" type="var">n</span> → <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span>, <span class="id" type="var">Q</span> <span class="id" type="var">n</span>) →<br/>
<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
If we are interested to see which proof <span class="inlinecode"><span class="id" type="tactic">auto</span></span> came up with,
one possibility is to look at the generated proof-term,
using the command:
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" type="keyword">Print</span></span> <span class="inlinecode"><span class="id" type="var">solving_by_apply</span>.</span>
<div class="paragraph"> </div>
The proof term is:
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" type="keyword">fun</span></span> <span class="inlinecode">(<span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span>)</span> <span class="inlinecode">(<span class="id" type="var">H</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span style='font-size:120%;'>∀</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span>,</span> <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">(<span class="id" type="var">H<sub>0</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span style='font-size:120%;'>∀</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span>,</span> <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>
<span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode">2</span> <span class="inlinecode">(<span class="id" type="var">H<sub>0</sub></span></span> <span class="inlinecode">2)</span>
<div class="paragraph"> </div>
This essentially means that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> applied the hypothesis <span class="inlinecode"><span class="id" type="var">H</span></span>
(the first one), and then applied the hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>0</sub></span></span> (the
second one).
<div class="paragraph"> </div>
<div class="paragraph"> </div>
The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can invoke <span class="inlinecode"><span class="id" type="tactic">apply</span></span> but not <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>. So, <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
cannot exploit lemmas whose instantiation cannot be directly
deduced from the proof goal. To exploit such lemmas, one needs to
invoke the tactic <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>, which is able to call <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>.
<div class="paragraph"> </div>
In the following example, the first hypothesis asserts that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>
is true when <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> is true for some <span class="inlinecode"><span class="id" type="var">m</span></span>, and the goal is to prove
that <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode">1</span> implies <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span>. This implication follows directly from
the hypothesis by instantiating <span class="inlinecode"><span class="id" type="var">m</span></span> as the value <span class="inlinecode">1</span>. The
following proof script shows that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> successfully solves the
goal, whereas <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is not able to do so.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_by_eapply</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">Q</span> <span class="id" type="var">m</span> → <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
<span class="id" type="var">Q</span> 1 →<br/>
<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
<a name="lab548"></a><h2 class="section">Conjunctions</h2>
<div class="paragraph"> </div>
So far, we've seen that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> is stronger than <span class="inlinecode"><span class="id" type="tactic">auto</span></span> in the
sense that it can deal with <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>. In the same way, we are going
to see how <span class="inlinecode"><span class="id" type="var">jauto</span></span> and <span class="inlinecode"><span class="id" type="var">iauto</span></span> are stronger than <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>
in the sense that they provide better support for conjunctions.
<div class="paragraph"> </div>
The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can prove a goal of the form
<span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">F'</span></span>, where <span class="inlinecode"><span class="id" type="var">F</span></span> and <span class="inlinecode"><span class="id" type="var">F'</span></span> are two propositions, as soon as
both <span class="inlinecode"><span class="id" type="var">F</span></span> and <span class="inlinecode"><span class="id" type="var">F'</span></span> can be proved in the current context.
An example follows.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_goal</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>) (<span class="id" type="var">F</span> : <span class="id" type="keyword">Prop</span>),<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span>, <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
<span class="id" type="var">F</span> →<br/>
<span class="id" type="var">F</span> ∧ <span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
However, when an assumption is a conjunction, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>
are not able to exploit this conjunction. It can be quite
surprising at first that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can prove very complex goals but
that it fails to prove that <span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">F'</span></span> implies <span class="inlinecode"><span class="id" type="var">F</span></span>. The tactics
<span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span> are able to decompose conjunctions from the context.
Here is an example.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_hyp</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">F</span> ∧ <span class="id" type="var">F'</span> →<br/>
<span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">jauto</span>. <span class="comment">(* or <span class="inlinecode"><span class="id" type="var">iauto</span></span> *)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
The tactic <span class="inlinecode"><span class="id" type="var">jauto</span></span> is implemented by first calling a
pre-processing tactic called <span class="inlinecode"><span class="id" type="var">jauto_set</span></span>, and then calling
<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>. So, to understand how <span class="inlinecode"><span class="id" type="var">jauto</span></span> works, one can directly
call the tactic <span class="inlinecode"><span class="id" type="var">jauto_set</span></span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_hyp'</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">F</span> ∧ <span class="id" type="var">F'</span> →<br/>
<span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="var">jauto_set</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
Next is a more involved goal that can be solved by <span class="inlinecode"><span class="id" type="var">iauto</span></span> and
<span class="inlinecode"><span class="id" type="var">jauto</span></span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_more</span> : <span style='font-size:120%;'>∀</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">nat</span>→<span class="id" type="keyword">Prop</span>) (<span class="id" type="var">F</span> : <span class="id" type="keyword">Prop</span>),<br/>
(<span class="id" type="var">F</span> ∧ (<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, (<span class="id" type="var">Q</span> <span class="id" type="var">m</span> ∧ <span class="id" type="var">R</span> <span class="id" type="var">n</span>) → <span class="id" type="var">P</span> <span class="id" type="var">n</span>)) →<br/>
(<span class="id" type="var">F</span> → <span class="id" type="var">R</span> 2) →<br/>
<span class="id" type="var">Q</span> 1 →<br/>
<span class="id" type="var">P</span> 2 ∧ <span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">jauto</span>. <span class="comment">(* or <span class="inlinecode"><span class="id" type="var">iauto</span></span> *)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
The strategy of <span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span> is to run a global analysis of
the top-level conjunctions, and then call <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>. For this
reason, those tactics are not good at dealing with conjunctions
that occur as the conclusion of some universally quantified
hypothesis. The following example illustrates a general weakness
of Coq proof search mechanisms.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_hyp_forall</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span>, <span class="id" type="var">P</span> <span class="id" type="var">n</span> ∧ <span class="id" type="var">Q</span> <span class="id" type="var">n</span>) →<br/>
<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">iauto</span>. <span class="id" type="var">jauto</span>.<br/>
<span class="comment">(* Nothing works, so we have to do some of the work by hand *)</span><br/>
<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">H</span> 2). <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
This situation is slightly disappointing, since automation is
able to prove the following goal, which is very similar. The
only difference is that the universal quantification has been
distributed over the conjunction.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solved_by_jauto</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>) (<span class="id" type="var">F</span> : <span class="id" type="keyword">Prop</span>),<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span>, <span class="id" type="var">P</span> <span class="id" type="var">n</span>) ∧ (<span style='font-size:120%;'>∀</span><span class="id" type="var">n</span>, <span class="id" type="var">Q</span> <span class="id" type="var">n</span>) →<br/>
<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">jauto</span>. <span class="comment">(* or <span class="inlinecode"><span class="id" type="var">iauto</span></span> *)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
<a name="lab549"></a><h2 class="section">Disjunctions</h2>
<div class="paragraph"> </div>
The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can handle disjunctions that
occur in the goal.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_disj_goal</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">F</span> →<br/>
<span class="id" type="var">F</span> ∨ <span class="id" type="var">F'</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
However, only <span class="inlinecode"><span class="id" type="var">iauto</span></span> is able to automate reasoning on the
disjunctions that appear in the context. For example, <span class="inlinecode"><span class="id" type="var">iauto</span></span> can
prove that <span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" type="var">F'</span></span> entails <span class="inlinecode"><span class="id" type="var">F'</span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" type="var">F</span></span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_disj_hyp</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">F</span> ∨ <span class="id" type="var">F'</span> →<br/>
<span class="id" type="var">F'</span> ∨ <span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">jauto</span>. <span class="id" type="var">iauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
More generally, <span class="inlinecode"><span class="id" type="var">iauto</span></span> can deal with complex combinations of
conjunctions, disjunctions, and negations. Here is an example.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_tauto</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">F<sub>1</sub></span> <span class="id" type="var">F<sub>2</sub></span> <span class="id" type="var">F<sub>3</sub></span> : <span class="id" type="keyword">Prop</span>),<br/>
((¬<span class="id" type="var">F<sub>1</sub></span> ∧ <span class="id" type="var">F<sub>3</sub></span>) ∨ (<span class="id" type="var">F<sub>2</sub></span> ∧ ¬<span class="id" type="var">F<sub>3</sub></span>)) →<br/>
(<span class="id" type="var">F<sub>2</sub></span> → <span class="id" type="var">F<sub>1</sub></span>) →<br/>
(<span class="id" type="var">F<sub>2</sub></span> → <span class="id" type="var">F<sub>3</sub></span>) →<br/>
¬<span class="id" type="var">F<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">iauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
However, the ability of <span class="inlinecode"><span class="id" type="var">iauto</span></span> to automatically perform a case
analysis on disjunctions comes with a downside: <span class="inlinecode"><span class="id" type="var">iauto</span></span> may be
very slow. If the context involves several hypotheses with
disjunctions, <span class="inlinecode"><span class="id" type="var">iauto</span></span> typically generates an exponential number of
subgoals on which <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> is called. One major advantage of <span class="inlinecode"><span class="id" type="var">jauto</span></span>
compared with <span class="inlinecode"><span class="id" type="var">iauto</span></span> is that it never spends time performing this
kind of case analyses.
</div>
<div class="doc">
<a name="lab550"></a><h2 class="section">Existentials</h2>
<div class="paragraph"> </div>
The tactics <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>, <span class="inlinecode"><span class="id" type="var">iauto</span></span>, and <span class="inlinecode"><span class="id" type="var">jauto</span></span> can prove goals whose
conclusion is an existential. For example, if the goal is <span class="inlinecode"><span style='font-size:120%;'>∃</span></span>
<span class="inlinecode"><span class="id" type="var">x</span>,</span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>, the tactic <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> introduces an existential variable,
say <span class="inlinecode">?25</span>, in place of <span class="inlinecode"><span class="id" type="var">x</span></span>. The remaining goal is <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode">?25</span>, and
<span class="inlinecode"><span class="id" type="tactic">eauto</span></span> tries to solve this goal, allowing itself to instantiate
<span class="inlinecode">?25</span> with any appropriate value. For example, if an assumption
<span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode">2</span> is available, then the variable <span class="inlinecode">?25</span> gets instantiated with
<span class="inlinecode">2</span> and the goal is solved, as shown below.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_exists_goal</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">f</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">f</span> 2 →<br/>
<span style='font-size:120%;'>∃</span><span class="id" type="var">x</span>, <span class="id" type="var">f</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">(* observe that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> does not deal with existentials, *)</span><br/>
<span class="id" type="tactic">eauto</span>. <span class="comment">(* whereas <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>, <span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span> solve the goal *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
A major strength of <span class="inlinecode"><span class="id" type="var">jauto</span></span> over the other proof search tactics is
that it is able to exploit the existentially-quantified
hypotheses, i.e., those of the form <span class="inlinecode"><span style='font-size:120%;'>∃</span></span> <span class="inlinecode"><span class="id" type="var">x</span>,</span> <span class="inlinecode"><span class="id" type="var">P</span></span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_exists_hyp</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">f</span> <span class="id" type="var">g</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">x</span>, <span class="id" type="var">f</span> <span class="id" type="var">x</span> → <span class="id" type="var">g</span> <span class="id" type="var">x</span>) →<br/>
(<span style='font-size:120%;'>∃</span><span class="id" type="var">a</span>, <span class="id" type="var">f</span> <span class="id" type="var">a</span>) →<br/>
(<span style='font-size:120%;'>∃</span><span class="id" type="var">a</span>, <span class="id" type="var">g</span> <span class="id" type="var">a</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">iauto</span>. <span class="comment">(* All of these tactics fail, *)</span><br/>
<span class="id" type="var">jauto</span>. <span class="comment">(* whereas <span class="inlinecode"><span class="id" type="var">jauto</span></span> succeeds. *)</span><br/>
<span class="comment">(* For the details, run <span class="inlinecode"><span class="id" type="tactic">intros</span>.</span> <span class="inlinecode"><span class="id" type="var">jauto_set</span>.</span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
<a name="lab551"></a><h2 class="section">Negation</h2>
<div class="paragraph"> </div>
The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> suffer from some limitations with
respect to the manipulation of negations, mostly related to the
fact that negation, written <span class="inlinecode">¬</span> <span class="inlinecode"><span class="id" type="var">P</span></span>, is defined as <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">False</span></span> but
that the unfolding of this definition is not performed
automatically. Consider the following example.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">negation_study_1</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">P</span> 0 →<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">x</span>, ¬<span class="id" type="var">P</span> <span class="id" type="var">x</span>) →<br/>
<span class="id" type="var">False</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">H<sub>0</sub></span> <span class="id" type="var">HX</span>.<br/>
<span class="id" type="tactic">eauto</span>. <span class="comment">(* It fails to see that <span class="inlinecode"><span class="id" type="var">HX</span></span> applies *)</span><br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span> <span class="id" type="keyword">in</span> *. <span class="id" type="tactic">eauto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
For this reason, the tactics <span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span> systematically
invoke <span class="inlinecode"><span class="id" type="tactic">unfold</span></span> <span class="inlinecode"><span class="id" type="var">not</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode">*</span> as part of their pre-processing. So,
they are able to solve the previous goal right away.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">negation_study_2</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">P</span> 0 →<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">x</span>, ¬<span class="id" type="var">P</span> <span class="id" type="var">x</span>) →<br/>
<span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">jauto</span>. <span class="comment">(* or <span class="inlinecode"><span class="id" type="var">iauto</span></span> *)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
We will come back later on to the behavior of proof search with
respect to the unfolding of definitions.
</div>
<div class="doc">
<a name="lab552"></a><h2 class="section">Equalities</h2>
<div class="paragraph"> </div>
Coq's proof-search feature is not good at exploiting equalities.
It can do very basic operations, like exploiting reflexivity
and symmetry, but that's about it. Here is a simple example
that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can solve, by first calling <span class="inlinecode"><span class="id" type="tactic">symmetry</span></span> and then
applying the hypothesis.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">equality_by_auto</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">f</span> <span class="id" type="var">g</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
(<span style='font-size:120%;'>∀</span><span class="id" type="var">x</span>, <span class="id" type="var">f</span> <span class="id" type="var">x</span> = <span class="id" type="var">g</span> <span class="id" type="var">x</span>) →<br/>
<span class="id" type="var">g</span> 2 = <span class="id" type="var">f</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
To automate more advanced reasoning on equalities, one should
rather try to use the tactic <span class="inlinecode"><span class="id" type="tactic">congruence</span></span>, which is presented at
the end of this chapter in the "Decision Procedures" section.
</div>
<div class="doc">
<a name="lab553"></a><h1 class="section">How Proof Search Works</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab554"></a><h2 class="section">Search Depth</h2>
<div class="paragraph"> </div>
The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> works as follows. It first tries to call
<span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> and <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>. If one of these calls solves the
goal, the job is done. Otherwise <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tries to apply the most
recently introduced assumption that can be applied to the goal
without producing and error. This application produces
subgoals. There are two possible cases. If the sugboals produced
can be solved by a recursive call to <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, then the job is done.
Otherwise, if this application produces at least one subgoal that
<span class="inlinecode"><span class="id" type="tactic">auto</span></span> cannot solve, then <span class="inlinecode"><span class="id" type="tactic">auto</span></span> starts over by trying to apply
the second most recently introduced assumption. It continues in a
similar fashion until it finds a proof or until no assumption
remains to be tried.
<div class="paragraph"> </div>
It is very important to have a clear idea of the backtracking
process involved in the execution of the <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tactic; otherwise
its behavior can be quite puzzling. For example, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is not
able to solve the following triviality.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_0</span> :<br/>
<span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>
<div class="doc">
The reason <span class="inlinecode"><span class="id" type="tactic">auto</span></span> fails to solve the goal is because there are
too many conjunctions. If there had been only five of them, <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
would have successfully solved the proof, but six is too many.
The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> limits the number of lemmas and hypotheses
that can be applied in a proof, so as to ensure that the proof
search eventually terminates. By default, the maximal number
of steps is five. One can specify a different bound, writing
for example <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span> to search for a proof involving at most
six steps. For example, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span> would solve the previous lemma.
(Similarly, one can invoke <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">6</span> or <span class="inlinecode"><span class="id" type="tactic">intuition</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">6</span>.)
The argument <span class="inlinecode"><span class="id" type="var">n</span></span> of <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is called the "search depth."
The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is simply defined as a shorthand for <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">5</span>.
<div class="paragraph"> </div>
The behavior of <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> can be summarized as follows. It first
tries to solve the goal using <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> and <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>. If
this fails, it tries to apply a hypothesis (or a lemma that has
been registered in the hint database), and this application
produces a number of sugoals. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">(<span class="id" type="var">n</span>-1)</span> is then
called on each of those subgoals. If all the subgoals are solved,
the job is completed, otherwise <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> tries to apply a
different hypothesis.
<div class="paragraph"> </div>
During the process, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> calls <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">(<span class="id" type="var">n</span>-1)</span>, which in turn
might call <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">(<span class="id" type="var">n</span>-2)</span>, and so on. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">0</span> only
tries <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> and <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>, and does not try to apply
any lemma. Overall, this means that when the maximal number of
steps allowed has been exceeded, the <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tactic stops searching
and backtracks to try and investigate other paths.
<div class="paragraph"> </div>
The following lemma admits a unique proof that involves exactly
three steps. So, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> proves this goal iff <span class="inlinecode"><span class="id" type="var">n</span></span> is greater than
three.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_1</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="id" type="var">P</span> 0 →<br/>
(<span class="id" type="var">P</span> 0 → <span class="id" type="var">P</span> 1) →<br/>
(<span class="id" type="var">P</span> 1 → <span class="id" type="var">P</span> 2) →<br/>
(<span class="id" type="var">P</span> 2).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">auto</span> 0. <span class="comment">(* does not find the proof *)</span><br/>
<span class="id" type="tactic">auto</span> 1. <span class="comment">(* does not find the proof *)</span><br/>
<span class="id" type="tactic">auto</span> 2. <span class="comment">(* does not find the proof *)</span><br/>
<span class="id" type="tactic">auto</span> 3. <span class="comment">(* finds the proof *)</span><br/>
<span class="comment">(* more generally, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> solves the goal if <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≥</span> <span class="inlinecode">3</span> *)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
We can generalize the example by introducing an assumption
asserting that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span> is derivable from <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">k</span>-1)</span> for all <span class="inlinecode"><span class="id" type="var">k</span></span>,
and keep the assumption <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">0</span>. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, which is the
same as <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">5</span>, is able to derive <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span> for all values of <span class="inlinecode"><span class="id" type="var">k</span></span>
less than 5. For example, it can prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_3</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="comment">(* Hypothesis H<sub>1</sub>: *)</span> (<span class="id" type="var">P</span> 0) →<br/>
<span class="comment">(* Hypothesis H<sub>2</sub>: *)</span> (<span style='font-size:120%;'>∀</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
<span class="comment">(* Goal: *)</span> (<span class="id" type="var">P</span> 4).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
However, to prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">5</span>, one needs to call at least <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_4</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="comment">(* Hypothesis H<sub>1</sub>: *)</span> (<span class="id" type="var">P</span> 0) →<br/>
<span class="comment">(* Hypothesis H<sub>2</sub>: *)</span> (<span style='font-size:120%;'>∀</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
<span class="comment">(* Goal: *)</span> (<span class="id" type="var">P</span> 5).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">auto</span> 6. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
Because <span class="inlinecode"><span class="id" type="tactic">auto</span></span> looks for proofs at a limited depth, there are
cases where <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can prove a goal <span class="inlinecode"><span class="id" type="var">F</span></span> and can prove a goal
<span class="inlinecode"><span class="id" type="var">F'</span></span> but cannot prove <span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">F'</span></span>. In the following example,
<span class="inlinecode"><span class="id" type="tactic">auto</span></span> can prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span> but it is not able to prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span>,
because the splitting of the conjunction consumes one proof step.
To prove the conjunction, one needs to increase the search depth,
using at least <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_5</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="comment">(* Hypothesis H<sub>1</sub>: *)</span> (<span class="id" type="var">P</span> 0) →<br/>
<span class="comment">(* Hypothesis H<sub>2</sub>: *)</span> (<span style='font-size:120%;'>∀</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
<span class="comment">(* Goal: *)</span> (<span class="id" type="var">P</span> 4 ∧ <span class="id" type="var">P</span> 4).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">auto</span> 6. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
<a name="lab555"></a><h2 class="section">Backtracking</h2>
<div class="paragraph"> </div>
In the previous section, we have considered proofs where
at each step there was a unique assumption that <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
could apply. In general, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can have several choices
at every step. The strategy of <span class="inlinecode"><span class="id" type="tactic">auto</span></span> consists of trying all
of the possibilities (using a depth-first search exploration).
<div class="paragraph"> </div>
To illustrate how automation works, we are going to extend the
previous example with an additional assumption asserting that
<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span> is also derivable from <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">k</span>+1)</span>. Adding this hypothesis
offers a new possibility that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> could consider at every step.
<div class="paragraph"> </div>
There exists a special command that one can use for tracing
all the steps that proof-search considers. To view such a
trace, one should write <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>. (For some reason, the
command <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">auto</span></span> does not exist, so we have to use the
command <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> instead.)
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">working_of_auto_1</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="comment">(* Hypothesis H<sub>1</sub>: *)</span> (<span class="id" type="var">P</span> 0) →<br/>
<span class="comment">(* Hypothesis H<sub>2</sub>: *)</span> (<span style='font-size:120%;'>∀</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
<span class="comment">(* Hypothesis H<sub>3</sub>: *)</span> (<span style='font-size:120%;'>∀</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>+1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
<span class="comment">(* Goal: *)</span> (<span class="id" type="var">P</span> 2).<br/>
<span class="comment">(* Uncomment "debug" in the following line to see the debug trace: *)</span><br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">H<sub>1</sub></span> <span class="id" type="var">H<sub>2</sub></span> <span class="id" type="var">H<sub>3</sub></span>. <span class="comment">(* debug *)</span> <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
The output message produced by <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> is as follows.
<pre>
1 depth=5
1.1 depth=4 simple apply H<sub>2</sub>
1.1.1 depth=3 simple apply H<sub>2</sub>
1.1.1.1 depth=3 exact H<sub>1</sub>
</pre>
The depth indicates the value of <span class="inlinecode"><span class="id" type="var">n</span></span> with which <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is
called. The tactics shown in the message indicate that the first
thing that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> has tried to do is to apply <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span>. The effect of
applying <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> is to replace the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span> with the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span>.
Then, again, <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> has been applied, changing the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span> into
<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">0</span>. At that point, the goal was exactly the hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span>.
<div class="paragraph"> </div>
It seems that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> was quite lucky there, as it never even
tried to use the hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span> at any time. The reason is that
<span class="inlinecode"><span class="id" type="tactic">auto</span></span> always tried to use the <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> first. So, let's permute
the hypotheses <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span> and see what happens.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">working_of_auto_2</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
<span class="comment">(* Hypothesis H<sub>1</sub>: *)</span> (<span class="id" type="var">P</span> 0) →<br/>
<span class="comment">(* Hypothesis H<sub>3</sub>: *)</span> (<span style='font-size:120%;'>∀</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>+1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
<span class="comment">(* Hypothesis H<sub>2</sub>: *)</span> (<span style='font-size:120%;'>∀</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
<span class="comment">(* Goal: *)</span> (<span class="id" type="var">P</span> 2).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">H<sub>1</sub></span> <span class="id" type="var">H<sub>3</sub></span> <span class="id" type="var">H<sub>2</sub></span>. <span class="comment">(* debug *)</span> <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
This time, the output message suggests that the proof search
investigates many possibilities. If we print the proof term:
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" type="keyword">Print</span></span> <span class="inlinecode"><span class="id" type="var">working_of_auto_2</span>.</span>
<div class="paragraph"> </div>
we observe that the proof term refers to <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>. Thus the proof
is not the simplest one, since only <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> are needed.
<div class="paragraph"> </div>
In turns out that the proof goes through the proof obligation <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span>,
even though it is not required to do so. The following tree drawing
describes all the goals that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> has been going through.
<pre>
|5||4||3||2||1||0| -- below, tabulation indicates the depth
[P 2]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 4]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 5]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 6]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 7]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 5]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 4]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 5]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 4]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 5]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 2]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 1]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 2]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 4]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 5]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 2]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 1]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 1]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 2]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 3]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 1]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> [P 0]
<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span> !! Done !!
</pre>
The first few lines read as follows. To prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span>, <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">5</span>
has first tried to apply <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>, producing the subgoal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span>.
To solve it, <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">4</span> has tried again to apply <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>, producing
the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span>. Similarly, the search goes through <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">5</span>, <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">6</span>
and <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">7</span>. When reaching <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">7</span>, the tactic <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">0</span> is called
but as it is not allowed to try and apply any lemma, it fails.
So, we come back to the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">6</span>, and try this time to apply
hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span>, producing the subgoal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">5</span>. Here again,
<span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">0</span> fails to solve this goal.
<div class="paragraph"> </div>
The process goes on and on, until backtracking to <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span> and trying
to apply <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span> three times in a row, going through <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span> and <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span>
and <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">0</span>. This search tree explains why <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> came up with a
proof term starting with an application of <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>.
</div>
<div class="doc">
<a name="lab556"></a><h2 class="section">Adding Hints</h2>
<div class="paragraph"> </div>
By default, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> (and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>) only tries to apply the
hypotheses that appear in the proof context. There are two
possibilities for telling <span class="inlinecode"><span class="id" type="tactic">auto</span></span> to exploit a lemma that have
been proved previously: either adding the lemma as an assumption
just before calling <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, or adding the lemma as a hint, so
that it can be used by every calls to <span class="inlinecode"><span class="id" type="tactic">auto</span></span>.
<div class="paragraph"> </div>
The first possibility is useful to have <span class="inlinecode"><span class="id" type="tactic">auto</span></span> exploit a lemma
that only serves at this particular point. To add the lemma as
hypothesis, one can type <span class="inlinecode"><span class="id" type="tactic">generalize</span></span> <span class="inlinecode"><span class="id" type="var">mylemma</span>;</span> <span class="inlinecode"><span class="id" type="tactic">intros</span></span>, or simply
<span class="inlinecode"><span class="id" type="var">lets</span>:</span> <span class="inlinecode"><span class="id" type="var">mylemma</span></span> (the latter requires <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>).
<div class="paragraph"> </div>
The second possibility is useful for lemmas that need to be
exploited several times. The syntax for adding a lemma as a hint
is <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="keyword">Resolve</span></span> <span class="inlinecode"><span class="id" type="var">mylemma</span></span>. For example:
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">nat_le_refl</span> : <span style='font-size:120%;'>∀</span>(<span class="id" type="var">x</span>:<span class="id" type="var">nat</span>), <span class="id" type="var">x</span> ≤ <span class="id" type="var">x</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_n</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">nat_le_refl</span>.<br/>
</div>
<div class="doc">
A convenient shorthand for adding all the constructors of an
inductive datatype as hints is the command <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="var">Constructors</span></span>
<span class="inlinecode"><span class="id" type="var">mydatatype</span></span>.
<div class="paragraph"> </div>
Warning: some lemmas, such as transitivity results, should
not be added as hints as they would very badly affect the
performance of proof search. The description of this problem
and the presentation of a general work-around for transitivity
lemmas appear further on.
</div>
<div class="doc">
<a name="lab557"></a><h2 class="section">Integration of Automation in Tactics</h2>
<div class="paragraph"> </div>
The library "LibTactics" introduces a convenient feature for
invoking automation after calling a tactic. In short, it suffices
to add the symbol star (<span class="inlinecode">*</span>) to the name of a tactic. For example,
<span class="inlinecode"><span class="id" type="tactic">apply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> is equivalent to <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">H</span>;</span> <span class="inlinecode"><span class="id" type="var">auto_star</span></span>, where <span class="inlinecode"><span class="id" type="var">auto_star</span></span>
is a tactic that can be defined as needed.
<div class="paragraph"> </div>
The definition of <span class="inlinecode"><span class="id" type="var">auto_star</span></span>, which determines the meaning of the
star symbol, can be modified whenever needed. Simply write:
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="keyword">Ltac</span> <span class="id" type="var">auto_star</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a_new_definition</span>.
<div class="paragraph"> </div>
</div>
Observe the use of <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> instead of <span class="inlinecode">:=</span>, which indicates that the
tactic is being rebound to a new definition. So, the default
definition is as follows.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Ltac</span> <span class="id" type="var">auto_star</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [ <span class="id" type="var">jauto</span> ].<br/>
</div>
<div class="doc">
Nearly all standard Coq tactics and all the tactics from
"LibTactics" can be called with a star symbol. For example, one
can invoke <span class="inlinecode"><span class="id" type="tactic">subst</span>*</span>, <span class="inlinecode"><span class="id" type="tactic">destruct</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span>, <span class="inlinecode"><span class="id" type="var">inverts</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span>, <span class="inlinecode"><span class="id" type="var">lets</span>*</span> <span class="inlinecode"><span class="id" type="var">I</span>:</span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>,
<span class="inlinecode"><span class="id" type="var">specializes</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>, and so on... There are two notable exceptions.
The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span>*</span> is just another name for the tactic
<span class="inlinecode"><span class="id" type="var">auto_star</span></span>. And the tactic <span class="inlinecode"><span class="id" type="tactic">apply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> calls <span class="inlinecode"><span class="id" type="tactic">eapply</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> (or the
more powerful <span class="inlinecode"><span class="id" type="var">applys</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> if needed), and then calls <span class="inlinecode"><span class="id" type="var">auto_star</span></span>.
Note that there is no <span class="inlinecode"><span class="id" type="tactic">eapply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> tactic, use <span class="inlinecode"><span class="id" type="tactic">apply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span>
instead.
<div class="paragraph"> </div>
In large developments, it can be convenient to use two degrees of
automation. Typically, one would use a fast tactic, like <span class="inlinecode"><span class="id" type="tactic">auto</span></span>,
and a slower but more powerful tactic, like <span class="inlinecode"><span class="id" type="var">jauto</span></span>. To allow for
a smooth coexistence of the two form of automation, <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>
also defines a "tilde" version of tactics, like <span class="inlinecode"><span class="id" type="tactic">apply</span>¬</span> <span class="inlinecode"><span class="id" type="var">H</span></span>,
<span class="inlinecode"><span class="id" type="tactic">destruct</span>¬</span> <span class="inlinecode"><span class="id" type="var">H</span></span>, <span class="inlinecode"><span class="id" type="tactic">subst</span>¬</span>, <span class="inlinecode"><span class="id" type="tactic">auto</span>¬</span> and so on. The meaning of the
tilde symbol is described by the <span class="inlinecode"><span class="id" type="var">auto_tilde</span></span> tactic, whose
default implementation is <span class="inlinecode"><span class="id" type="tactic">auto</span></span>.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Ltac</span> <span class="id" type="var">auto_tilde</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="tactic">auto</span>.<br/>
</div>
<div class="doc">
In the examples that follow, only <span class="inlinecode"><span class="id" type="var">auto_star</span></span> is needed.
<div class="paragraph"> </div>
An alternative, possibly more efficient version of auto_star is the
following":
<div class="paragraph"> </div>
Ltac auto_star <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> try solve <span class="inlinecode"></span> <span class="inlinecode"><span class="id" type="var">eassumption</span></span> <span class="inlinecode">|</span> <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">|</span> <span class="inlinecode"><span class="id" type="var">jauto</span></span> <span class="inlinecode"></span>.
<div class="paragraph"> </div>
With the above definition, <span class="inlinecode"><span class="id" type="var">auto_star</span></span> first tries to solve the
goal using the assumptions; if it fails, it tries using <span class="inlinecode"><span class="id" type="tactic">auto</span></span>,
and if this still fails, then it calls <span class="inlinecode"><span class="id" type="var">jauto</span></span>. Even though
<span class="inlinecode"><span class="id" type="var">jauto</span></span> is strictly stronger than <span class="inlinecode"><span class="id" type="var">eassumption</span></span> and <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, it
makes sense to call these tactics first, because, when the
succeed, they save a lot of time, and when they fail to prove
the goal, they fail very quickly.".
<div class="paragraph"> </div>
</div>
<div class="doc">
<a name="lab558"></a><h1 class="section">Example Proofs using Automation</h1>
<div class="paragraph"> </div>
Let's see how to use proof search in practice on the main theorems
of the "Software Foundations" course, proving in particular
results such as determinism, preservation and progress.
</div>
<div class="doc">
<a name="lab559"></a><h2 class="section">Determinism</h2>
</div>
<div class="code code-space">
<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">DeterministicImp</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
</div>
<div class="doc">
Recall the original proof of the determinism lemma for the IMP
language, shown below.
</div>
<div class="code code-tight">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic</span>: <span style='font-size:120%;'>∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span> →<br/>
<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></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">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">E<sub>2</sub></span>.<br/>
<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
(<span class="id" type="tactic">induction</span> <span class="id" type="var">E<sub>1</sub></span>); <span class="id" type="tactic">intros</span> <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="tactic">subst</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">EQ<sub>1</sub></span>.<br/>
{ <span class="comment">(* Proof of assertion *)</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<sub>1</sub> reduces to true *)</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<sub>1</sub> reduces to false (contradiction) *)</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">H<sub>5</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
<span class="comment">(* E_IfFalse *)</span><br/>
- <span class="comment">(* b<sub>1</sub> reduces to true (contradiction) *)</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">H<sub>5</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
- <span class="comment">(* b<sub>1</sub> reduces to false *)</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_WhileFalse *)</span><br/>
- <span class="comment">(* b<sub>1</sub> reduces to true *)</span><br/>
<span class="id" type="tactic">reflexivity</span>.<br/>
- <span class="comment">(* b<sub>1</sub> reduces to false (contradiction) *)</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">H<sub>2</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
<span class="comment">(* E_WhileTrue *)</span><br/>
- <span class="comment">(* b<sub>1</sub> reduces to true (contradiction) *)</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">H<sub>4</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>4</sub></span>.<br/>
- <span class="comment">(* b<sub>1</sub> reduces to false *)</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">EQ<sub>1</sub></span>.<br/>
{ <span class="comment">(* Proof of assertion *)</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="id" type="keyword">Qed</span>.<br/>
</div>
<div class="doc">
Exercise: rewrite this proof using <span class="inlinecode"><span class="id" type="tactic">auto</span></span> whenever possible.
(The solution uses <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 9 times.)
</div>
<div class="code code-tight">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'</span>: <span style='font-size:120%;'>∀</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span> →<br/>
<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
In fact, using automation is not just a matter of calling <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
in place of one or two other tactics. Using automation is about
rethinking the organization of sequences of tactics so as to
minimize the effort involved in writing and maintaining the proof.
This process is eased by the use of the tactics from
<span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>. So, before trying to optimize the way automation
is used, let's first rewrite the proof of determinism:
<div class="paragraph"> </div>