-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathUseAuto_J.v
More file actions
2429 lines (2094 loc) · 116 KB
/
UseAuto_J.v
File metadata and controls
2429 lines (2094 loc) · 116 KB
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
(** * UseAuto_J: Coqの証明自動化の理論と実際 *)
(* * UseAuto: Theory and Practice of Automation in Coq Proofs *)
(* $Date: 2011-04-20 14:26:52 -0400 (Wed, 20 Apr 2011) $ *)
(* Chapter maintained by Arthur Chargueraud *)
(* 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 decision procedures
that enable the system to automatically synthetizes simple pieces
of proof. Automation is very powerful when set up
appropriately. The purpose of this chapter is to explain the
basics of working of automation.
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 until proving the goal. The second part describes
"decision procedures," which are tactics that are very good at
solving proof obligations that fall in some particular fragment of
the logic of Coq.
The examples from this chapter include small lemmas made up to
illustrate particular aspects of automation as well as larger
examples taken from the rest of the Software Foundations
development. For the larger examples, tactics from the library
[LibTactics.v] are used. Those tactics are described in the
chapter [UseTactics.v]. (You will need to read that chapter to
understand the later parts of this one, but the earlier parts can
be read on their own.) *)
(** 機械がチェックした証明においては、細部の一つ一つの正しさが確認されています。
これが巨大な証明記述にもなります。
幸い、Coqは証明探索メカニズムと決定手続きを持っていて、
それにより証明の小さな部分を自動合成することができます。
自動化は設定を適切に行えば非常に強力です。
この章の目的は自動化の扱い方の基本を説明することです。
この章は2つの部分から成ります。
第一部は証明探索("proof search")と呼ばれる一般的メカニズムに焦点を当てます。
簡単に言うと、証明探索は、証明が終わるまで、
単純に補題と仮定を可能なすべての方法で適用してみようとします。
第二部は決定手続き("decision procedures")について記述します。
それらは、Coqの論理の特定の断片についての証明課題を解くことを得意とするタクティックです。
この章の例には、自動化の特定の側面を示す小さな補題から、「ソフトウェアの基礎」(Software
Foundations)の他の部分から抽出した大きな例までを含みます。
大きな例においては、ライブラリ[LibTactics_J.v]のタクティックが使用されます。
それらのタクティックについては[UseTactics_J.v]章に記述されています。
(この章の後半を理解するには[UseTactics_J.v]章を読んでおくべきです。
しかし、前半は他の知識を必要としません。) *)
Require Import LibTactics_J.
(* ####################################################### *)
(* * Basic Features of Proof Search *)
(** * 証明探索の基本性質 *)
(* 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 [auto]. 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. *)
(** 証明探索のアイデアは、補題や仮定を適用するタクティックの列を、
例えば[auto]のような1つのタクティックで置き換えることです。
この形の証明自動化で、たくさんの作業を省くことができます。
典型的には証明記述ははるかに短くなり、またその記述は典型的にはより変更に強いものになります。
もし定義に何か小さな変更をした場合、自動化を使った証明はおそらく何の変更も必要ありません。
もちろん、自動化の使い過ぎはよいことではありません。
証明記述が証明の主要議論をもはや記録していないときには、
定義の変更で証明が成立しなくなったときに、直すことは難しくなります。
全体として、自動化の適度の利用は大きな勝利です。
証明の構築と、その後のメンテナンスの時間を、ともに大きく減らすことができます。*)
(* ####################################################### *)
(* ** Strength of Proof Search *)
(** ** 証明探索の強さ *)
(* We are going to study four proof-search tactics: [auto], [eauto],
[iauto] and [jauto]. The tactics [auto] and [eauto] are builtin
in Coq. The tactic [iauto] is a shorthand for the builtin tactic
[try solve [intuition eauto]]. The tactic [jauto] is defined in
the library [LibTactics], and simply performs some preprocessing
of the goal before calling [eauto]. 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.
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 [auto] builds proofs only by using the
basic tactics [reflexivity], [assumption], and [apply]. The tactic
[eauto] can also exploit [eapply]. The tactic [jauto] extends
[eauto] by being able to open conjunctions and existentials that
occur in the context. The tactic [iauto] 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, [iauto] usually gets very slow when the goal
involves several disjunctions.
Note that proof search tactics never perform any rewriting
step (tactics [rewrite], [subst]), nor any case analysis on an
arbitrary data structure or predicate (tactics [destruct] and
[inversion]), nor any proof by induction (tactic [induction]). 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. *)
(** これから4つの証明探索のタクティックを勉強します:[auto]、[eauto]、[iauto]、[jauto]です。
タクティック[auto]と[eauto]はCoqのビルトインです。
タクティック[iauto]はビルトインのタクティック [try solve [intuition eauto]]
の略記法です。
タクティック[jauto]はライブラリ[LibTactics_J]に定義されています。
このタクティックは単に[eauto]を呼ぶ前にゴールにある前処理を行います。
この章のゴールは証明探索の一般原理を説明し、
与えられたゴールを解くために上述の4つのタクティックのうちどれが一番適当かを推測する経験則を示すことです。
証明探索は効率と表現力の妥協案です。
つまり、どれだけ複雑なゴールを解くことができるか、と、
タクティックが停止するまでにどれだけの時間を必要とするかのトレードオフです。
タクティック[auto]は、基本タクティック[reflexivity]、[assumption]、
[apply]だけを使って証明を構築します。
タクティック[eauto]はこれに加えて[eapply]も使います。
タクティック[jauto]は[eauto]を拡張して、
コンテキストに現れる連言(and結合)と存在限量を展開することができるようにしています。
タクティック[iauto]は連言(and結合)、選言(or結合)、否定を非常に賢い方法で扱います。
しかしながら[iauto]はコンテキストから存在限量を展開することはできません。
さらに、[iauto]はゴールがいくつかの選言を含む場合にとても遅くなるのが普通です。
注意するべきは、証明探索は書き換えステップ(タクティック[rewrite]、[subst])、
任意のデータ構造や述語についての場合分け分析(タクティック[destruct]、[inversion])、
帰納法による証明(タクティック[induction])のいずれも実行しないことです。
そのため証明探索は、実際は証明のたくさんの枝の最後のステップを自動化することを意図したものです。
証明の全体構造を発見することはできません。*)
(* ####################################################### *)
(* ** Basics *)
(** ** 基本 *)
(* The tactic [auto] is able to solve a goal that can be proved
using a sequence of [intros], [apply], [assumption], and [reflexivity].
Two examples follow. The first one shows the ability for
[auto] to call [reflexivity] at any time. In fact, calling
[reflexivity] is always the first thing that [auto] tries to do. *)
(** タクティック[auto]は、[intros]、[apply]、[assumption]、[reflexivity]
の列で証明できるゴールを証明することができます。
以下で2つの例を示します。1つ目の例は[auto]が[reflexivity]をいつでも呼べることを示します。
実際、[auto]は常に最初に[reflexivity]を適用しようとします。*)
Lemma solving_by_reflexivity :
2 + 3 = 5.
Proof. auto. Qed.
(* The second example illustrates a proof where a sequence of
two calls to [apply] are needed. The goal is to prove that
if [Q n] implies [P n] for any [n] and if [Q n] holds for any [n],
then [P 2] holds. *)
(** 2つ目の例は[apply]を2回続けて呼ぶ必要がある証明です。
ゴールは、任意の[n]について [Q n] ならば [P n] であり、
かつ任意の[n]について [Q n] が成立するならば、[P 2]が成立する、というものです。*)
Lemma solving_by_apply : forall (P Q : nat->Prop),
(forall n, Q n -> P n) ->
(forall n, Q n) ->
P 2.
Proof. auto. Qed.
(* We can ask [auto] to tell us what proof it came up with,
by invoking [info auto] in place of [auto]. *)
(** [auto]に、どのような証明を見つけたのか教えてもらうことができます。
そのためには、[auto]の代わりに [info auto] として呼びます。*)
Lemma solving_by_apply' : forall (P Q : nat->Prop),
(forall n, Q n -> P n) ->
(forall n, Q n) ->
P 2.
Proof. info auto. Qed.
(* The output is: *)
(* [intro P; intro Q; intro H; intro H0; simple apply H; simple apply H0]. *)
(* which can be reformulated as [intros P Q H H0; apply H; apply H0]. *)
(* The tactic [auto] can invoke [apply] but not [eapply]. So, [auto]
cannot exploit lemmas whose instantiation cannot be directly
deduced from the proof goal. To exploit such lemmas, one needs to
invoke the tactic [eauto], which is able to call [eapply].
In the following example, the first hypothesis asserts that [P n]
is true when [Q m] is true for some [m], and the goal is to prove
that [Q 1] implies [P 2]. This implication follows direction from
the hypothesis by instantiating [m] as the value [1]. The
following proof script shows that [eauto] successfully solves the
goal, whereas [auto] is not able to do so. *)
(** タクティック[auto]は[apply]を呼ぶことがありますが、[eapply]は呼びません。
そのため[auto]は、証明のゴールから直接具体化できない補題は使うことができません。
そのような補題を使うためにはタクティック[eauto]を呼ぶ必要があります。
[eauto]は[eapply]を呼ぶことができます。
以下の例では、最初の仮定は、ある[m]について [Q m] が真のとき、
[P n] が真であると主張しています。
そして、ゴールは [Q 1] ならば [P 2] を証明することです。
この含意は、仮定の中の[m]を値[1]で具体化することから得られます。
次の証明記述は[eauto]が証明に成功し、一方[auto]はそうではないことを示します。*)
Lemma solving_by_eapply : forall (P Q : nat->Prop),
(forall n m, Q m -> P n) ->
Q 1 -> P 2.
Proof. auto. eauto. Qed.
(* Remark: Again, we can use [info eauto] to see what proof [eauto]
comes up with. *)
(** 注記: 同様に、[info eauto]を使うと[eauto]が何を見つけたかを知ることができます。*)
(* ####################################################### *)
(* ** Conjunctions *)
(** ** 連言 *)
(* So far, we've seen that [eauto] is stronger than [auto] in the
sense that it can deal with [eapply]. In the same way, we are going
to see how [jauto] and [iauto] are stronger than [auto] and [eauto]
in the sense that they provide better support for conjunctions. *)
(** ここまで、[eauto]が[eapply]を使えるという意味で[auto]より強いことを見てきました。
同様に、ここでは、[jauto]と[iauto]が連言に対してより優れたサポートをしているという点で、
[auto]や[eauto]より強いことを見ます。*)
(* The tactics [auto] and [eauto] can prove a goal of the form
[F /\ F'], where [F] and [F'] are two propositions, as soon as
both [F] and [F'] can be proved in the current context.
An example follows. *)
(** タクティック[auto]と[eauto]は [F /\ F'] という形のゴールを証明できます。
ここで[F]と[F']は2つの命題で、両者とも現在のコンテキストですぐに証明できるものです。
次はその例です。*)
Lemma solving_conj_goal : forall (P : nat->Prop) (F : Prop),
(forall n, P n) -> F -> F /\ P 2.
Proof. auto. Qed.
(* However, when an assumption is a conjunction, [auto] and [eauto]
are not able to exploit this conjunction. It can be quite
surprising at first that [eauto] can prove very complex goals but
that it fails to prove that [F /\ F'] implies [F]. The tactics
[iauto] and [jauto] are able to decompose conjunctions from the context.
Here is an example. *)
(** しかしながら、仮定が連言の場合、[auto]と[eauto]はこの連言を使うことができません。
[eauto]がとても複雑なゴールを証明できるのに、「[F /\ F'] ならば [F] 」
を証明できないことに、最初はとても驚きます。
タクティック[iauto]と[jauto]はコンテキストの連言を分解することができます。
次はその例です。*)
Lemma solving_conj_hyp : forall (F F' : Prop),
F /\ F' -> F.
Proof. auto. eauto. jauto. (* or [iauto] *) Qed.
(* The tactic [jauto] is implemented by first calling a
pre-processing tactic called [jauto_set], and then calling
[eauto]. So, to understand how [jauto] works, one can directly
call the tactic [jauto_set]. *)
(** タクティック[jauto]は、最初に[jauto_set]という前処理のタクティックを呼び、
その後[eauto]を呼ぶように作られています。
これから、[jauto]がどうはたらくかを理解するためには、タクティック[jauto_set]
を直接呼んでみるのが良いでしょう。*)
Lemma solving_conj_hyp' : forall (F F' : Prop),
F /\ F' -> F.
Proof. intros. jauto_set. eauto. Qed.
(* Next is a more involved goal that can be solved by [iauto] and
[jauto]. *)
(** 次は[iauto]と[jauto]で解けるより複雑なゴールです。 *)
Lemma solving_conj_more : forall (P Q R : nat->Prop) (F : Prop),
(F /\ (forall n m, (Q m /\ R n) -> P n)) ->
(F -> R 2) ->
Q 1 ->
P 2 /\ F.
Proof. jauto. (* or [iauto] *) Qed.
(* The strategy of [iauto] and [jauto] is to run a global analysis of
the top-level conjunctions, and then call [eauto]. 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. *)
(** [iauto]と[jauto]の戦略は、トップレベルの連言をグローバルに解析し、
その後[eauto]を呼ぶというものです。
このため、全称限量子を持つ仮定の、結論部の連言を扱うのが苦手です。
次の例は、Coqの証明探索メカニズムの一般的な弱点を示しています。*)
Lemma solving_conj_hyp_forall : forall (P Q : nat->Prop),
(forall n, P n /\ Q n) -> P 2.
Proof.
auto. eauto. iauto. jauto.
(* Nothing works, so we have to do some of the work by hand *)
intros. destruct (H 2). auto.
Qed.
(* 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. *)
(** この状況にはちょっとがっかりします。
というのは、ほとんど同じである次のゴールは自動証明できるのです。
唯一の違いは、全称限量子が連言のそれぞれに別々に付けられていることです。*)
Lemma solved_by_jauto : forall (P Q : nat->Prop) (F : Prop),
(forall n, P n) /\ (forall n, Q n) -> P 2.
Proof. jauto. (* or [iauto] *) Qed.
(* ####################################################### *)
(* ** Disjunctions *)
(** ** 選言 *)
(* The tactics [auto] and [eauto] can handle disjunctions that
occur in the goal. *)
(** タクティック[auto]と[eauto]はゴールに現れる選言を扱うことができます。*)
Lemma solving_disj_goal : forall (F F' : Prop),
F -> F \/ F'.
Proof. auto. Qed.
(* However, only [iauto] is able to automate reasoning on the
disjunctions that appear in the context. For example, [iauto] can
prove that [F \/ F'] entails [F' \/ F]. *)
(** しかし、コンテキストに現れる選言についての推論を自動化できるのは[iauto]だけです。
例えば、[iauto]は 「[F \/ F'] ならば [F' \/ F]」を証明できます。 *)
Lemma solving_disj_hyp : forall (F F' : Prop),
F \/ F' -> F' \/ F.
Proof. auto. eauto. jauto. iauto. Qed.
(* More generally, [iauto] can deal with complex combinations of
conjunctions, disjunctions, and negations. Here is an example. *)
(** より一般に、[iauto]は連言、選言、否定の複雑な組み合わせを扱うことができます。
次はその例です。*)
Lemma solving_tauto : forall (F1 F2 F3 : Prop),
((~F1 /\ F3) \/ (F2 /\ ~F3)) ->
(F2 -> F1) ->
(F2 -> F3) ->
~F2.
Proof. iauto. Qed.
(* However, the ability of [iauto] to automatically perform a case
analysis on disjunctions comes with a downside: [iauto] can get
very slow. If the context involves several hypotheses with
disjunctions, [iauto] typically generates an exponential number of
subgoals on which [eauto] is called. One advantage of [jauto]
compared with [iauto] is that it never spends time performing this
kind of case analyses. *)
(** しかしながら、[iauto]が選言の場合分けを自動実行する能力には、悪い面もあります。
[iauto]は非常に遅くなることがあるのです。
コンテキストが数個の選言を含む仮定を持つとき、[iauto]は通常、その指数の数のサブゴールを作り、
その1つ1つについて[eauto]を呼びます。
[iauto]と比べた[jauto]の長所は、このような場合分けをする時間を費さないことです。*)
(* ####################################################### *)
(* ** Existentials *)
(** ** 存在限量 *)
(* The tactics [eauto], [iauto], and [jauto] can prove goals whose
conclusion is an existential. For example, if the goal is [exists
x, f x], the tactic [eauto] introduces an existential variable,
say [?25], in place of [x]. The remaining goal is [f ?25], and
[eauto] tries to solve this goal, allowing itself to instantiate
[?25] with any appropriate value. For example, if an assumption [f
2] is available, then the variable [?25] gets instantiated with
[2] and the goal is solved, as shown below. *)
(** タクティック[eauto]、[iauto]、[jauto]は結論部が存在限量であるゴールを証明することができます。
例えばゴールが [exists x, f x] のとき、
タクティック[eauto]は[x]の場所に存在変数を導入します。
それを[?25]としましょう。残ったゴールは[f ?25]になります。
そして[eauto]は、[?25]を何らかの適当な値で具体化することで、これを解こうとします。
例えば、仮定 [f 2] があるならば、変数 [?25] を[2]で置換してゴールが解決されます。
以下の通りです。*)
Lemma solving_exists_goal : forall (f : nat->Prop),
f 2 -> exists x, f x.
Proof.
auto. (* [auto] does not deal with existentials *)
eauto. (* [eauto], [iauto] and [jauto] solve the goal *)
Qed.
(* A major strength of [jauto] over the other proof search tactics is
that it is able to exploit the existentially quantified
_hypotheses_, i.e., those of the form [exists x, P]. *)
(** 証明探索の他のタクティックと比べた[jauto]の主な長所は、
存在限量された、つまり [exists x, P] という形の 「仮定」を使える点です。*)
Lemma solving_exists_hyp : forall (f g : nat->Prop),
(forall x, f x -> g x) ->
(exists a, f a) ->
(exists a, g a).
Proof.
auto. eauto. iauto. (* All of these tactics fail, *)
jauto. (* whereas [jauto] succeeds. *)
(* For the details, run [intros. jauto_set. eauto] *)
Qed.
(* ####################################################### *)
(* ** Negation *)
(** ** 否定 *)
(* The tactics [auto] and [eauto] suffer from some limitations with
respect to the manipulation of negations, mostly related to the
fact that negation, written [~ P], is defined as [P -> False] but
that the unfolding of this definition is not performed
automatically. Consider the following example. *)
(** タクティック[auto]と[eauto]は、否定の扱いに関して制限があります。
これは主に、否定([~ P] と記述される)が [P -> False] と定義されているのに、
この定義の展開が自動では行われないことに関係しています。
次の例を見てください。*)
Lemma negation_study_1 : forall (P : nat->Prop),
P 0 -> (forall x, ~ P x) -> False.
Proof.
intros P H0 HX.
eauto. (* It fails to see that [HX] applies, *)
unfold not in *. eauto. (* unless the negation is unfolded *)
Qed.
(* For this reason, the tactics [iauto] and [jauto] systematically
invoke [unfold not in *] as part of their pre-processing. So,
they are able to solve the previous goal right away. *)
(** このため、タクティック[iauto]と[jauto]は前処理の中で [unfold not in *]
を組織的に呼びます。これにより、[iauto]、[jauto]は上記のゴールをすぐに解決できます。*)
Lemma negation_study_2 : forall (P : nat->Prop),
P 0 -> (forall x, ~ P x) -> False.
Proof. jauto. (* or [iauto] *) Qed.
(* (We will come back later to the behavior of proof search with
respect to the unfolding of definitions.) *)
(** (定義の展開に関する証明探索の振る舞いについては後でまた議論します。) *)
(* ####################################################### *)
(* ** Equalities *)
(** ** 等式 *)
(* 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 [auto] can solve, by first calling [symmetry] and then
applying the hypothesis. *)
(** Coq の証明探索機能は等式を扱うのが不得意です。
反射律、対称律といった基本的操作は行うことができますが、それぐらいです。
以下は[auto]が解くことができる簡単な例です。
最初に[symmetry]を呼び、その後仮定を適用します。*)
Lemma equality_by_auto : forall (f g : nat->Prop),
(forall x, f x = g x) -> g 2 = f 2.
Proof. auto. Qed.
(* To automate more advanced reasoning on equalities, one should
rather try to use the tactic [congruence], which is presented at
the end of this chapter in the "Decision Procedures" section. *)
(** 等式についてのより高度な推論を自動化するためには、
むしろタクティック[congruence]を使うべきです。
これについてはこの章の終わりの「決定手続き」節で説明します。*)
(* ####################################################### *)
(* * How Proof Search Works *)
(** * 証明探索はどのようにはたらくか *)
(* ####################################################### *)
(* ** Search Depth *)
(** ** 探索の深さ *)
(* The tactic [auto] works as follows. It first tries to call
[reflexivity] and [assumption]. If one of these calls solves the
goal, the job is done. Otherwise [auto] 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 [auto], then the job is done.
Otherwise, if this application produces at least one subgoal that
[auto] cannot solve, then [auto] 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.
It is very important to have a clear idea of the backtracking
process involved in the execution of the [auto] tactic; otherwise
its behavior can be quite puzzling. For example, [auto] is not
able to solve the following triviality. *)
(** タクティック[auto]は次のようにはたらきます。
最初に[reflexivity]と[assumption]を試してみます。
もしどちらかがゴールを解いたならば仕事は完了です。
そうでないとき[auto]は、エラーにならずにゴールに適用できる仮定のうち、
一番最後に導入されたものを適用することを試みます。
この適用によりサブゴールが生成されます。
このあと2つの場合があります。
もし生成されたサブゴールがすべて[auto]の再帰的呼び出しにより解かれた場合、
それで終了です。
そうではなく、生成されたサブゴール中に[auto]が解けないものが1つでもある場合、
やり直して、最後から2番目に導入された仮定を適用しようとします。
同様のやり方を、証明を発見するか、適用する仮定がなくなるかするまで続けます。
[auto]タクティックの実行の際のバックトラックプロセスを明確に理解しておくことはとても重要です。
そうしないと、[auto]の振る舞いにはかなり当惑します。
例えば、[auto]は次の自明なものを解くことができません。*)
Lemma search_depth_0 :
True /\ True /\ True /\ True /\ True /\ True.
Proof.
auto.
Admitted.
(* The reason [auto] fails to solve the goal is because there are
too many conjunctions. If there had been only five of them, [auto]
would have successfully solved the proof, but six is too many.
The tactic [auto] 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 [auto 6] to search for a proof involving at most
six steps. For example, [auto 6] would solve the previous lemma.
(Similarly, one can invoke [eauto 6] or [intuition eauto 6].)
The argument [n] of [auto n] is called the "search depth."
The tactic [auto] is simply defined as a shorthand for [auto 5].
The behavior of [auto n] can be summarized as follows. It first
tries to solve the goal using [reflexivity] and [assumption]. 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 [auto (n-1)] is then
called on each of those subgoals. If all the subgoals are solved,
the job is completed, otherwise [auto n] tries to apply a
different hypothesis.
During the process, [auto n] calls [auto (n-1)], which in turn
might call [auto (n-2)], and so on. The tactic [auto 0] only
tries [reflexivity] and [assumption], and does not try to apply
any lemma. Overall, this means that when the maximal number of
steps allowed has been exceeded, the [auto] tactic stops searching
and backtracks to try and investigate other paths. *)
(** このゴールに[auto]が失敗する理由は、連言の数が多すぎることです。
もしこれが5個だったら、[auto]は証明に成功したでしょう。しかし6個は多過ぎなのです。
タクティック[auto]は補題と仮定の数を制限することで、
証明探索がいつかは停止することを保証しています。
デフォルトではステップの最大数は5です。制限を別の値にするには、例えば [auto 6]
と書くと、証明探索は最大6ステップまでになります。
例えば [auto 6] は上記の補題を解くことができるでしょう。
(同様に、[eauto 6] や [intuition eauto 6] として呼ぶことができます。)
[auto n] の引数[n]は探索の深さ("search depth")と呼ばれます。
タクティック[auto]は単に[auto 5]の略記法として定義されています。
[auto n] の振る舞いは次のように要約されます。
最初にゴールを[reflexivity]と[assumption]を使って解こうとします。
もし失敗したときは、仮定(またはヒントデータベースに登録された補題)を適用しようとします。
これによりいくつものサブゴールが生成されます。
このそれぞれのサブゴールに対してタクティック [auto (n-1)] が呼ばれます。
もしすべてのサブゴールが解かれたならば処理は完了です。そうでなければ、
[auto n] は別の仮定を適用しようとします。
この過程は、[auto n] は [auto (n-1)] を呼び、次に [auto (n-1)] は
[auto (n-2)] を呼び... と続きます。
タクティック [auto 0] が適用を試みるのは[reflexivity]と[assumption]だけで、
補題を適用しようとすることはありません。
これは全体として、指定されたステップ数の上限値に逹したときには、
[auto]タクティックは探索を中止し、バックトラックして別のパスを調べることを意味します。*)
(* The following lemma admits a unique proof that involves exactly
three steps. So, [auto n] proves this goal iff [n] is greater than
three. *)
(** 次の補題には1つだけ証明があり、それは3ステップです。
このため、[auto n] は、[n]が3以上の時これを証明し、3未満のときは証明できません。*)
(* (訳注: 原文では "iff [n] is greater than three" と記述されていますが、
文脈から「以上」に修正しました。) *)
Lemma search_depth_1 : forall (P : nat->Prop),
P 0 ->
(P 0 -> P 1) ->
(P 1 -> P 2) ->
(P 2).
Proof.
auto 0. (* does not find the proof *)
auto 1. (* does not find the proof *)
auto 2. (* does not find the proof *)
auto 3. (* finds the proof *)
(* more generally, [auto n] solves the goal if [n >= 3] *)
Qed.
(* We can generalize the example by introducing an assumption
asserting that [P k] is derivable from [P (k-1)] for all [k],
and keep the assumption [P 0]. The tactic [auto], which is the
same as [auto 5], is able to derive [P k] for all values of [k]
less than 5. For example, it can prove [P 4]. *)
(** この例を次のように一般化することができます。
すべての[k]について、[P k] が [P (k-1)] から導出されると仮定します。
また、[P 0] が成立するとします。
タクティック[auto]、つまり [auto 5] と同じですが、これは
5未満のすべての[k]の値について[P k]を導出することができます。
例えば[auto]は[P 4]を証明できます。 *)
Lemma search_depth_3 : forall (P : nat->Prop),
(* Hypothesis H1: *) (P 0) ->
(* Hypothesis H2: *) (forall k, P (k-1) -> P k) ->
(* Goal: *) (P 4).
Proof. auto. Qed.
(* However, to prove [P 5], one needs to call at least [auto 6]. *)
(** しかし、[P 5] を証明するためには、少なくとも [auto 6] を呼ぶ必要があります。 *)
Lemma search_depth_4 : forall (P : nat->Prop),
(* Hypothesis H1: *) (P 0) ->
(* Hypothesis H2: *) (forall k, P (k-1) -> P k) ->
(* Goal: *) (P 5).
Proof. auto. auto 6. Qed.
(* Because [auto] looks for proofs at a limited depth, there are
cases where [auto] can prove a goal [F] and can prove a goal
[F'] but cannot prove [F /\ F']. In the following example,
[auto] can prove [P 4] but it is not able to prove [P 4 /\ P 4],
because the splitting of the conjunction consumes one proof step.
To prove the conjunction, one needs to increase the search depth,
using at least [auto 6]. *)
(** [auto]が限られた深さで証明を探すことから、
[auto]がゴール[F]も[F']も証明できるのに[F /\ F']を証明できない、
という場合があります。
次の例では、[auto]は [P 4] を証明できますが、
[P 4 /\ P 4] を証明できません。
なぜなら連言を分解するには1ステップ必要だからです。
この連言を証明するためには、探索の深さを増やして少なくとも [auto 6] を使う必要があります。*)
Lemma search_depth_5 : forall (P : nat->Prop),
(* Hypothesis H1: *) (P 0) ->
(* Hypothesis H2: *) (forall k, P (k-1) -> P k) ->
(* Goal: *) (P 4 /\ P 4).
Proof. auto. auto 6. Qed.
(* ####################################################### *)
(* ** Backtracking *)
(** ** バックトラック *)
(* In the previous section, we have considered proofs where
at each step there was a unique assumption that [auto]
could apply. In general, [auto] can have several choices
at every step. The strategy of [auto] consists of trying all
of the possibilities (using a depth-first search exploration).
To illustrate how automation works, we are going to extend the
previous example with an additional assumption asserting that
[P k] is also derivable from [P (k+1)]. Adding this hypothesis
offers a new possibility that [auto] could consider at every step.
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 [debug eauto]. (For some reason, the
command [debug auto] does not exist, so we have to use the
command [debug eauto] instead.) *)
(** 前の節で、各ステップで[auto]が適用できる仮定が唯一である証明を考えてきました。
一般には、[auto]の各ステップでいくつかの選択肢がある場合があります。
[auto]の戦略は、すべての可能性を(深さ優先探索によって)試してみる、というものです。
どのように自動証明がはたらくかを示すために、前の例を拡張して、
[P k] が [P (k+1)] からも導出できるとします。
この仮定を追加したことで、[auto]が各ステップで考慮する新たな選択肢が提供されます。
証明探索で考慮するすべてのステップをトレースすることができる特別なコマンドがあります。
そのトレースを見るためには、[debug eauto]と書きます。
(ある理由から、コマンド [debug auto] は存在しないため、
代わりにコマンド [debug eauto] を使う必要があります。) *)
Lemma working_of_auto_1 : forall (P : nat->Prop),
(* Hypothesis H1: *) (P 0) ->
(* Hypothesis H2: *) (forall k, P (k+1) -> P k) ->
(* Hypothesis H3: *) (forall k, P (k-1) -> P k) ->
(* Goal: *) (P 2).
(* Uncomment "debug" in the following line to see the debug trace: *)
Proof. intros P H1 H2 H3. (* debug *) eauto. Qed.
(* The output message produced by [debug eauto] is as follows.
<<
depth=5
depth=4 apply H3
depth=3 apply H3
depth=3 exact H1
>>
The depth indicates the value of [n] with which [eauto n] is
called. The tactics shown in the message indicate that the first
thing that [eauto] has tried to do is to apply [H3]. The effect of
applying [H3] is to replace the goal [P 2] with the goal [P 1].
Then, again, [H3] has been applied, changing the goal [P 1] into
[P 0]. At that point, the goal was exactly the hypothesis [H1].
It seems that [eauto] was quite lucky there, as it never even
tried to use the hypothesis [H2] at any time. The reason is that
[auto] always tries to use the most recently introduced hypothesis
first, and [H3] is a more recent hypothesis than [H2] in the goal.
So, let's permute the hypotheses [H2] and [H3] and see what
happens. *)
(** [debug eauto] の出力メッセージは次の通りです。
<<
depth=5
depth=4 apply H3
depth=3 apply H3
depth=3 exact H1
>>
depth は [eauto n] が呼ばれる[n]の値を示します。
メッセージに見られるタクティックは、
[eauto]が最初にすることは[H3]を適用してみることであることを示します。
[H3]の適用の結果、ゴール [P 1] はゴール [P 2] に代わります。
すると、再度[H3]が適用され、ゴール [P 1] が [P 2] に代わります。
この時点でゴールは仮定 [H1] と一致します。
この場合、[eauto]は非常にラッキーだったようです。
仮定[H2]を一度も使ってみようとすることもありませんでした。
理由は、[auto]は常に最後に導入された仮定を最初に試してみることと、
ゴールにおいて[H3]は[H2]より後で導入された仮定であることです。
それでは、仮定[H2]と[H3]を入れ替えるとどうなるか見てみましょう。*)
Lemma working_of_auto_2 : forall (P : nat->Prop),
(* Hypothesis H1: *) (P 0) ->
(* Hypothesis H3: *) (forall k, P (k-1) -> P k) ->
(* Hypothesis H2: *) (forall k, P (k+1) -> P k) ->
(* Goal: *) (P 2).
Proof. intros P H1 H3 H2. (* debug *) eauto. Qed.
(* This time, the output message suggests that the proof search
investigates many possibilities. Replacing [debug eauto] with
[info eauto], we observe that the proof that [eauto] comes up
with is actually not the simplest one.
[apply H2; apply H3; apply H3; apply H3; exact H1]
This proof goes through the proof obligation [P 3], even though
it is not any useful. The following tree drawing describes
all the goals that automation has been through.
<<
|5||4||3||2||1||0| -- below, tabulation indicates the depth
[P 2]
-> [P 3]
-> [P 4]
-> [P 5]
-> [P 6]
-> [P 7]
-> [P 5]
-> [P 4]
-> [P 5]
-> [P 3]
--> [P 3]
-> [P 4]
-> [P 5]
-> [P 3]
-> [P 2]
-> [P 3]
-> [P 1]
-> [P 2]
-> [P 3]
-> [P 4]
-> [P 5]
-> [P 3]
-> [P 2]
-> [P 3]
-> [P 1]
-> [P 1]
-> [P 2]
-> [P 3]
-> [P 1]
-> [P 0]
-> !! Done !!
>>
The first few lines read as follows. To prove [P 2], [eauto 5]
has first tried to apply [H2], producing the subgoal [P 3].
To solve it, [eauto 4] has tried again to apply [H2], producing
the goal [P 4]. Similarly, the search goes through [P 5], [P 6]
and [P 7]. When reaching [P 7], the tactic [eauto 0] is called
but as it is not allowed to try and apply any lemma, it fails.
So, we come back to the goal [P 6], and try this time to apply
hypothesis [H3], producing the subgoal [P 5]. Here again,
[eauto 0] fails to solve this goal.
The process goes on and on, until backtracking to [P 3] and trying
to apply [H2] three times in a row, going through [P 2] and [P 1]
and [P 0]. This search tree explains why [eauto] came up with a
proof starting with [apply H2]. *)
(** このとき、出力メッセージは証明探索がたくさんの可能性を調べることを示唆しています。
[debug eauto] を [info eauto] に替えると、
[eauto]が見つける証明は実際に単純なものではないことを見ることができます。
[[apply H2; apply H3; apply H3; apply H3; exact H1]]
この証明は、証明課題 [P 3] を調べます。たとえそれが何の役にも立たなくてもです。
以下に描かれた木は自動証明が通ったすべてのゴールを記述しています。
<<
|5||4||3||2||1||0| -- 以下で、タブは深さを示しています
[P 2]
-> [P 3]
-> [P 4]
-> [P 5]
-> [P 6]
-> [P 7]
-> [P 5]
-> [P 4]
-> [P 5]
-> [P 3]
--> [P 3]
-> [P 4]
-> [P 5]
-> [P 3]
-> [P 2]
-> [P 3]
-> [P 1]
-> [P 2]
-> [P 3]
-> [P 4]
-> [P 5]
-> [P 3]
-> [P 2]
-> [P 3]
-> [P 1]
-> [P 1]
-> [P 2]
-> [P 3]
-> [P 1]
-> [P 0]
-> !! 完了です !!
>>
最初の数行は次のように読みます。[P 2] を証明するために [eauto 5]
は最初に[H2]を適用しサブゴール [P 3] を作ります。
これを解くために、[eauto 4] は再度[H2]を適用し、ゴール [P 4] を作ります。
同様に探索は [P 5]、[P 6]、 [P 7] と進みます。
[P 7] に逹したときタクティック [eauto 0] が呼ばれますが、
[eauto 0] は補題を適用することができないため、失敗します。
このためゴール [P 6] に戻り、ここでは仮定[H3]を適用し、サブゴール [P 5] を生成します。
ここでまた [eauto 0] はこのゴールを解くことに失敗します。
このプロセスは延々と続きます。[P 3]までバックトラックし、
[H2]を3回連続して適用して [P 2]、[P 1]、[P 0] と進むまでは。
この探索木は、[eauto]がなぜ [apply H2] から始まる証明を発見できるかを説明しています。*)
(* ####################################################### *)
(* ** Adding Hints *)
(** ** ヒントを追加する *)
(* By default, [auto] (and [eauto]) only tries to apply the
hypotheses that appear in the proof context. There are two
possibilities for telling [auto] to exploit a lemma that have
been proved previously: either adding the lemma as an assumption
just before calling [auto], or adding the lemma as a hint, so
that it can be used by every calls to [auto].
The first possibility is useful to have [auto] exploit a lemma
that only serves at this particular point. To add the lemma as
hypothesis, one can type [generalize mylemma; intros], or simply
[lets: mylemma] (the latter requires [LibTactics.v]).
The second possibility is useful for lemmas that needs to be
exploited several times. The syntax for adding a lemma as a hint
is [Hint Resolve mylemma]. For example, the lemma asserting than
any number is less than or equal to itself, [forall x, x <= x],
called [Le.le_refl] in the Coq standard library, can be added as a
hint as follows. *)
(** デフォルトでは、[auto] (および[eauto])は証明コンテキストに現れる仮定だけを適用しようとします。
それより前に証明した補題を使うことを[auto]に教えてやる方法は2つあります。
1つは[auto]を呼ぶ直前に補題を仮定として加えてやることです。
もう1つは、補題をヒントとして追加することです。
そうすると、[auto]を呼ぶときいつでもそれを使うことができるようになります。
1つ目の方法は、この特定の場所のためだけに補題を[auto]に使わせるのに便利です。
補題を仮定として追加するためには、[generalize mylemma; intros]、
あるいは単に [lets: mylemma] と打ちます(後者には[LibTactics_J.v]
が必要です)。
2つ目の方法は何回も補題を使う必要がある場合に便利です。
補題をヒントに追加する構文は [Hint Resolve mylemma] です。
例えば、任意の数値は自分以下であるという補題 [forall x, x <= x]
はCoq標準ライブラリでは[Le.le_refl]と呼ばれていますが、
これをヒントとして追加するには次のようにします。*)
Hint Resolve Le.le_refl.
(* A convenient shorthand for adding all the constructors of an
inductive datatype as hints is the command [Hint Constructors
mydatatype].
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. *)
(** 帰納的データ型のすべてのコンストラクタをヒントとして追加する便利な略記法がコマンド
[Hint Constructors mydatatype] です。
ワーニング: いくつかの補題、推移律のようなものは、ヒントとして追加するべきではありません。
証明探索のパフォーマンスに非常に悪い影響を与えるからです。
この問題の記述と推移律の一般的な回避策の提示は後で出てきます。*)
(* ####################################################### *)
(* ** Integration of Automation in Tactics *)
(** ** タクティックへの自動証明の統合 *)
(* The library "LibTactics" introduces a convenient feature for
invoking automation after calling a tactic. In short, it suffices
to add the symbol star ([*]) to the name of a tactic. For example,
[apply* H] is equivalent to [apply H; auto_star], where [auto_star]
is a tactic that can be defined as needed. By default, [auto_star]
first tries to solve the goal using [auto], and if this does not
succeed then it tries to call [jauto]. Even though [jauto] is
strictly stronger than [auto], it makes sense to call [auto] first:
when [auto] succeeds it may save a lot of time, and when [auto]
fails to prove the goal, it fails very quickly.
The definition of [auto_star], which determines the meaning of the
star symbol, can be modified whenever needed. Simply write:
[[
Ltac auto_star ::= a_new_definition.
]]
Observe the use of [::=] instead of [:=], which indicates that the
tactic is being rebound to a new definition. So, the default
definition is as follows. *)
(** ライブラリ "LibTactics" はタクティックを呼んだ後で自動証明を呼ぶ便利な機能を提供します。
要するに、タクティック名に星印([*])をつければ良いのです。
例えば、[apply* H] は [apply H; auto_star] と等価です。
ここで[auto_star]は必要なように定義できます。
デフォルトでは、[auto_star]は最初に[auto]を使ってゴールを解こうとします。
そしてそれに成功しなかった場合[jauto]を呼ぼうとします。
[jauto]の強さが[auto]を越えているのに、[auto]を先に呼ぶのは意味があります。
[auto]で成功した場合、かなりの時間を節約できるかもしれません。
そして[auto]が証明に失敗するときには、非常に速く失敗するのです。
星印の意味を定める[auto_star]の定義は、いつでも必要なときに変更できます。
単に次のように書きます:
[[
Ltac auto_star ::= a_new_definition.
]]
ここで、[:=]ではなく[::=]が使われていることを見てください。
これは、このタクティックが新しい定義に再束縛されていることを示しています。
そのデフォルトの定義は次の通りです。*)
Ltac auto_star ::= try solve [ auto | jauto ].
(* Nearly all standard Coq tactics and all the tactics from
"LibTactics" can be called with a star symbol. For example, one
can invoke [subst*], [destruct* H], [inverts* H], [lets* I: H x],
[specializes* H x], and so on... There are two notable exceptions.
The tactic [auto*] is just another name for the tactic
[auto_star]. And the tactic [apply* H] calls [eapply H] (or the
more powerful [applys H] if needed), and then calls [auto_star].
Note that there is no [eapply* H] tactic, use [apply* H]
instead. *)
(** 標準のCoqタクティックのほとんどすべてと、"LibTactics"のタクティックのすべては、
星印を付けて呼ぶことができます。
例えば、[subst*]、[destruct* H]、[inverts* H]、[lets* I: H x]、
[specializes* H x]、等々が可能です。
注記すべき例外が2つあります。
タクティック[auto*]は[auto_star]の別名です。
また、タクティック [apply* H] は [eapply H] (または、
もし必要ならばより強力な [applys H])を呼び、その後[auto_star]を呼びます。
[eapply* H] タクティックは存在しないので、代わりに [apply* H]
を呼ぶように注意してください。*)
(* In large developments, it can be convenient to use two degrees of
automation. Typically, one would use a fast tactic, like [auto],
and a slower but more powerful tactic, like [jauto]. To allow for
a smooth coexistence of the two form of automation, [LibTactics.v[
also defines a "tilde" version of tactics, like [apply~ H],
[destruct~ H], [subst~], [auto~] and so on. The meaning of the
tilde symbol is described by the [auto_tilde] tactic, whose
default implementation is [auto]. *)
(** 大きな開発では、2つの段階の自動化を使うのが便利でしょう。
典型的には、1つは[auto]のような速いタクティック、
もう1つは[jauto]のように遅いけれどもより強力なタクティックです。
2種類の自動化をスムーズに共存させるために、
[LibTactics_J.v]はタクティックにチルダ([~])を付けるバージョンも定義しています。
[apply~ H]、[destruct~ H]、[subst~]、[auto~] などです。
チルダ記号の意味は[auto_tilde]タクティックによって記述されています。
このデフォルトの実装は[auto]です。*)
Ltac auto_tilde ::= auto.
(* In the examples that follow, only [auto_star] is needed. *)
(** 以降の例では、[auto_star]だけが必要です。*)
(* ####################################################### *)
(* * Examples of Use of Automation *)
(** * 自動化の使用例 *)
(* 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 determinacy, preservation and progress... *)
(** 「ソフトウェアの基礎」("Software Foundations")
コースの主要定理に証明探索を実際にどのように使うかを見てみましょう。