2 <!-- ============ Tactics ====================== -->
3 <chapter id="sec_tactics">
6 <sect1 id="tac_absurd">
7 <title>absurd <term></title>
8 <titleabbrev>absurd</titleabbrev>
9 <para><userinput>absurd P</userinput></para>
13 <term>Pre-conditions:</term>
15 <para><command>P</command> must have type <command>Prop</command>.</para>
21 <para>it closes the current sequent by eliminating an
26 <term>New sequents to prove:</term>
28 <para>it opens two new sequents of conclusion <command>P</command>
29 and <command>¬P</command>.</para>
35 <sect1 id="tac_apply">
36 <title>apply <term></title>
37 <titleabbrev>apply</titleabbrev>
38 <para><userinput>apply t</userinput></para>
42 <term>Pre-conditions:</term>
44 <para><command>t</command> must have type
45 <command>T<subscript>1</subscript> → ... →
46 T<subscript>n</subscript> → G</command>
47 where <command>G</command> can be unified with the conclusion
48 of the current sequent.</para>
54 <para>it closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
58 <term>New sequents to prove:</term>
60 <para>it opens a new sequent for each premise
61 <command>T<subscript>i</subscript></command> that is not
62 instantiated by unification. <command>T<subscript>i</subscript></command> is
63 the conclusion of the <command>i</command>-th new sequent to
70 <sect1 id="tac_assumption">
71 <title>assumption</title>
72 <titleabbrev>assumption</titleabbrev>
73 <para><userinput>assumption </userinput></para>
77 <term>Pre-conditions:</term>
79 <para>there must exist an hypothesis whose type can be unified with
80 the conclusion of the current sequent.</para>
86 <para>it closes the current sequent exploiting an hypothesis.</para>
90 <term>New sequents to prove:</term>
99 <title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
100 <titleabbrev>auto</titleabbrev>
101 <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
105 <term>Pre-conditions:</term>
107 <para>none, but the tactic may fail finding a proof if every
108 proof is in the search space that is pruned away. Pruning is
109 controlled by <command>d</command> and <command>w</command>.
110 Moreover, only lemmas whose type signature is a subset of the
111 signature of the current sequent are considered. The signature of
112 a sequent is ...TODO</para>
118 <para>it closes the current sequent by repeated application of
119 rewriting steps (unless <command>paramodulation</command> is
120 omitted), hypothesis and lemmas in the library.</para>
124 <term>New sequents to prove:</term>
132 <sect1 id="tac_clear">
133 <title>clear <id></title>
134 <titleabbrev>clear</titleabbrev>
135 <para><userinput>clear H</userinput></para>
139 <term>Pre-conditions:</term>
141 <para><command>H</command> must be an hypothesis of the
142 current sequent to prove.</para>
148 <para>it hides the hypothesis <command>H</command> from the
149 current sequent.</para>
153 <term>New sequents to prove:</term>
161 <sect1 id="tac_clearbody">
162 <title>clearbody <id></title>
163 <titleabbrev>clearbody</titleabbrev>
164 <para><userinput>clearbody H</userinput></para>
168 <term>Pre-conditions:</term>
170 <para><command>H</command> must be an hypothesis of the
171 current sequent to prove.</para>
177 <para>it hides the definiens of a definition in the current
178 sequent context. Thus the definition becomes an hypothesis.</para>
182 <term>New sequents to prove:</term>
190 <sect1 id="tac_change">
191 <title>change <pattern> with <term></title>
192 <titleabbrev>change</titleabbrev>
193 <para><userinput>change patt with t</userinput></para>
197 <term>Pre-conditions:</term>
199 <para>each subterm matched by the pattern must be convertible
200 with the term <command>t</command> disambiguated in the context
201 of the matched subterm.</para>
207 <para>it replaces the subterms of the current sequent matched by
208 <command>patt</command> with the new term <command>t</command>.
209 For each subterm matched by the pattern, <command>t</command> is
210 disambiguated in the context of the subterm.</para>
214 <term>New sequents to prove:</term>
222 <sect1 id="tac_constructor">
223 <title>constructor <int></title>
224 <titleabbrev>constructor</titleabbrev>
225 <para><userinput>constructor n</userinput></para>
229 <term>Pre-conditions:</term>
231 <para>the conclusion of the current sequent must be
232 an inductive type or the application of an inductive type.</para>
238 <para>it applies the <command>n</command>-th constructor of the
239 inductive type of the conclusion of the current sequent.</para>
243 <term>New sequents to prove:</term>
245 <para>it opens a new sequent for each premise of the constructor
246 that can not be inferred by unification. For more details,
247 see the <command>apply</command> tactic.</para>
253 <sect1 id="tac_contradiction">
254 <title>contradiction</title>
255 <titleabbrev>contradiction</titleabbrev>
256 <para><userinput>contradiction </userinput></para>
260 <term>Pre-conditions:</term>
262 <para>there must be in the current context an hypothesis of type
263 <command>False</command>.</para>
269 <para>it closes the current sequent by applying an hypothesis of
270 type <command>False</command>.</para>
274 <term>New sequents to prove:</term>
283 <title>cut <term> [as <id>]</title>
284 <titleabbrev>cut</titleabbrev>
285 <para><userinput>cut P as H</userinput></para>
289 <term>Pre-conditions:</term>
291 <para><command>P</command> must have type <command>Prop</command>.</para>
297 <para>it closes the current sequent.</para>
301 <term>New sequents to prove:</term>
303 <para>it opens two new sequents. The first one has an extra
304 hypothesis <command>H:P</command>. If <command>H</command> is
305 omitted, the name of the hypothesis is automatically generated.
306 The second sequent has conclusion <command>P</command> and
307 hypotheses the hypotheses of the current sequent to prove.</para>
313 <sect1 id="tac_decompose">
314 <title>decompose [<ident list>] <ident> [<intros_spec>]</title>
315 <titleabbrev>decompose</titleabbrev>
316 <para><userinput>decompose ???</userinput></para>
320 <term>Pre-conditions:</term>
332 <term>New sequents to prove:</term>
340 <sect1 id="tac_discriminate">
341 <title>discriminate <term></title>
342 <titleabbrev>discriminate</titleabbrev>
343 <para><userinput>discriminate p</userinput></para>
347 <term>Pre-conditions:</term>
349 <para><command>p</command> must have type <command>K t<subscript>1</subscript> ... t<subscript>n</subscript> = K' t'<subscript>1</subscript> ... t'<subscript>m</subscript></command> where <command>K</command> and <command>K'</command> must be different constructors of the same inductive type and each argument list can be empty if
350 its constructor takes no arguments.</para>
356 <para>it closes the current sequent by proving the absurdity of
357 <command>p</command>.</para>
361 <term>New sequents to prove:</term>
369 <sect1 id="tac_elim">
370 <title>elim <term> [using <term>] [<intros_spec>]</title>
371 <titleabbrev>elim</titleabbrev>
372 <para><userinput>elim t using th hyps</userinput></para>
376 <term>Pre-conditions:</term>
378 <para><command>t</command> must inhabit an inductive type and
379 <command>th</command> must be an elimination principle for that
380 inductive type. If <command>th</command> is omitted the appropriate
381 standard elimination principle is chosen.</para>
387 <para>it proceeds by cases on the values of <command>t</command>,
388 according to the elimination principle <command>th</command>.
393 <term>New sequents to prove:</term>
395 <para>it opens one new sequent for each case. The names of
396 the new hypotheses are picked by <command>hyps</command>, if
403 <sect1 id="tac_elimType">
404 <title>elimType <term> [using <term>]</title>
405 <titleabbrev>elimType</titleabbrev>
406 <para><userinput>elimType T using th</userinput></para>
410 <term>Pre-conditions:</term>
412 <para><command>T</command> must be an inductive type.</para>
418 <para>TODO (severely bugged now).</para>
422 <term>New sequents to prove:</term>
430 <sect1 id="tac_exact">
431 <title>exact <term></title>
432 <titleabbrev>exact</titleabbrev>
433 <para><userinput>exact p</userinput></para>
437 <term>Pre-conditions:</term>
439 <para>the type of <command>p</command> must be convertible
440 with the conclusion of the current sequent.</para>
446 <para>it closes the current sequent using <command>p</command>.</para>
450 <term>New sequents to prove:</term>
458 <sect1 id="tac_exists">
459 <title>exists</title>
460 <titleabbrev>exists</titleabbrev>
461 <para><userinput>exists </userinput></para>
465 <term>Pre-conditions:</term>
467 <para>the conclusion of the current sequent must be
468 an inductive type or the application of an inductive type.</para>
474 <para>equivalent to <command>constructor 1</command>.</para>
478 <term>New sequents to prove:</term>
480 <para>it opens a new sequent for each premise of the first
481 constructor of the inductive type that is the conclusion of the
482 current sequent. For more details, see the <command>constructor</command> tactic.</para>
488 <sect1 id="tac_fail">
490 <titleabbrev>failt</titleabbrev>
491 <para><userinput>fail</userinput></para>
495 <term>Pre-conditions:</term>
503 <para>this tactic always fail.</para>
507 <term>New sequents to prove:</term>
515 <sect1 id="tac_fold">
516 <title>fold <reduction_kind> <term> <pattern></title>
517 <titleabbrev>fold</titleabbrev>
518 <para><userinput>fold red t patt</userinput></para>
522 <term>Pre-conditions:</term>
524 <para>the pattern must not specify the wanted term.</para>
530 <para>first of all it locates all the subterms matched by
531 <command>patt</command>. In the context of each matched subterm
532 it disambiguates the term <command>t</command> and reduces it
533 to its <command>red</command> normal form; then it replaces with
534 <command>t</command> every occurrence of the normal form in the
535 matched subterm.</para>
539 <term>New sequents to prove:</term>
547 <sect1 id="tac_fourier">
548 <title>fourier</title>
549 <titleabbrev>fourier</titleabbrev>
550 <para><userinput>fourier </userinput></para>
554 <term>Pre-conditions:</term>
556 <para>the conclusion of the current sequent must be a linear
557 inequation over real numbers taken from standard library of
558 Coq. Moreover the inequations in the hypotheses must imply the
559 inequation in the conclusion of the current sequent.</para>
565 <para>it closes the current sequent by applying the Fourier method.</para>
569 <term>New sequents to prove:</term>
578 <title>fwd <ident> [<ident list>]</title>
579 <titleabbrev>fwd</titleabbrev>
580 <para><userinput>fwd ...TODO</userinput></para>
584 <term>Pre-conditions:</term>
596 <term>New sequents to prove:</term>
604 <sect1 id="tac_generalize">
605 <title>generalize <pattern> [as <id>]</title>
606 <titleabbrev>generalize</titleabbrev>
607 <para><userinput>generalize patt as H</userinput></para>
611 <term>Pre-conditions:</term>
613 <para>all the terms matched by <command>patt</command> must be
614 convertible and close in the context of the current sequent.</para>
620 <para>it closes the current sequent by applying a stronger
621 lemma that is proved using the new generated sequent.</para>
625 <term>New sequents to prove:</term>
627 <para>it opens a new sequent where the current sequent conclusion
628 <command>G</command> is generalized to
629 <command>∀x.G{x/t}</command> where <command>{x/t}</command>
630 is a notation for the replacement with <command>x</command> of all
631 the occurrences of the term <command>t</command> matched by
632 <command>patt</command>. If <command>patt</command> matches no
633 subterm then <command>t</command> is defined as the
634 <command>wanted</command> part of the pattern.</para>
642 <titleabbrev>id</titleabbrev>
643 <para><userinput>absurd P</userinput></para>
647 <term>Pre-conditions:</term>
655 <para>this identity tactic does nothing without failing.</para>
659 <term>New sequents to prove:</term>
667 <sect1 id="tac_injection">
668 <title>injection <term></title>
669 <titleabbrev>injection</titleabbrev>
670 <para><userinput>injection p</userinput></para>
674 <term>Pre-conditions:</term>
676 <para><command>p</command> must have type <command>K t<subscript>1</subscript> ... t<subscript>n</subscript> = K t'<subscript>1</subscript> ... t'<subscript>n</subscript></command> where both argument lists are empty if
677 <command>K</command> takes no arguments.</para>
683 <para>it derives new hypotheses by injectivity of
684 <command>K</command>.</para>
688 <term>New sequents to prove:</term>
690 <para>the new sequent to prove is equal to the current sequent
691 with the additional hypotheses
692 <command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
698 <sect1 id="tac_intro">
699 <title>intro [<ident>]</title>
700 <titleabbrev>intro</titleabbrev>
701 <para><userinput>intro H</userinput></para>
705 <term>Pre-conditions:</term>
707 <para>the conclusion of the sequent to prove must be an implication
708 or a universal quantification.</para>
714 <para>it applies the right introduction rule for implication,
715 closing the current sequent.</para>
719 <term>New sequents to prove:</term>
721 <para>it opens a new sequent to prove adding to the hypothesis
722 the antecedent of the implication and setting the conclusion
723 to the consequent of the implicaiton. The name of the new
724 hypothesis is <command>H</command> if provided; otherwise it
725 is automatically generated.</para>
731 <sect1 id="tac_intros">
732 <title>intros <intros_spec></title>
733 <titleabbrev>intros</titleabbrev>
734 <para><userinput>intros hyps</userinput></para>
738 <term>Pre-conditions:</term>
740 <para>If <command>hyps</command> specifies a number of hypotheses
741 to introduce, then the conclusion of the current sequent must
742 be formed by at least that number of imbricated implications
743 or universal quantifications.</para>
749 <para>it applies several times the right introduction rule for
750 implication, closing the current sequent.</para>
754 <term>New sequents to prove:</term>
756 <para>it opens a new sequent to prove adding a number of new
757 hypotheses equal to the number of new hypotheses requested.
758 If the user does not request a precise number of new hypotheses,
759 it adds as many hypotheses as possible.
760 The name of each new hypothesis is either popped from the
761 user provided list of names, or it is automatically generated when
762 the list is (or becomes) empty.</para>
768 <sect1 id="tac_inversion">
769 <title>inversion <term></title>
770 <titleabbrev>inversion</titleabbrev>
771 <para><userinput>inversion t</userinput></para>
775 <term>Pre-conditions:</term>
777 <para>the type of the term <command>t</command> must be an inductive
778 type or the application of an inductive type.</para>
784 <para>it proceeds by cases on <command>t</command> paying attention
785 to the constraints imposed by the actual "right arguments"
786 of the inductive type.</para>
790 <term>New sequents to prove:</term>
792 <para>it opens one new sequent to prove for each case in the
793 definition of the type of <command>t</command>. With respect to
794 a simple elimination, each new sequent has additional hypotheses
795 that states the equalities of the "right parameters"
796 of the inductive type with terms originally present in the
797 sequent to prove.</para>
803 <sect1 id="tac_lapply">
804 <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
805 <titleabbrev>lapply</titleabbrev>
806 <para><userinput>lapply ???</userinput></para>
810 <term>Pre-conditions:</term>
822 <term>New sequents to prove:</term>
830 <sect1 id="tac_left">
832 <titleabbrev>left</titleabbrev>
833 <para><userinput>left </userinput></para>
837 <term>Pre-conditions:</term>
839 <para>the conclusion of the current sequent must be
840 an inductive type or the application of an inductive type.</para>
846 <para>equivalent to <command>constructor 1</command>.</para>
850 <term>New sequents to prove:</term>
852 <para>it opens a new sequent for each premise of the first
853 constructor of the inductive type that is the conclusion of the
854 current sequent. For more details, see the <command>constructor</command> tactic.</para>
860 <sect1 id="tac_letin">
861 <title>letin <ident> ≝ <term></title>
862 <titleabbrev>letin</titleabbrev>
863 <para><userinput>letin x ≝ t</userinput></para>
867 <term>Pre-conditions:</term>
875 <para>it adds to the context of the current sequent to prove a new
876 definition <command>x ≝ t</command>.</para>
880 <term>New sequents to prove:</term>
888 <sect1 id="tac_normalize">
889 <title>normalize <pattern></title>
890 <titleabbrev>normalize</titleabbrev>
891 <para><userinput>normalize patt</userinput></para>
895 <term>Pre-conditions:</term>
903 <para>it replaces all the terms matched by <command>patt</command>
904 with their βδιζ-normal form.</para>
908 <term>New sequents to prove:</term>
916 <sect1 id="tac_paramodulation">
917 <title>paramodulation <pattern></title>
918 <titleabbrev>paramodulation</titleabbrev>
919 <para><userinput>paramodulation patt</userinput></para>
923 <term>Pre-conditions:</term>
935 <term>New sequents to prove:</term>
943 <sect1 id="tac_reduce">
944 <title>reduce <pattern></title>
945 <titleabbrev>reduce</titleabbrev>
946 <para><userinput>reduce patt</userinput></para>
950 <term>Pre-conditions:</term>
958 <para>it replaces all the terms matched by <command>patt</command>
959 with their βδιζ-normal form.</para>
963 <term>New sequents to prove:</term>
971 <sect1 id="tac_reflexivity">
972 <title>reflexivity</title>
973 <titleabbrev>reflexivity</titleabbrev>
974 <para>The tactic <command>reflexivity</command> </para>
976 <sect1 id="tac_replace">
977 <title>replace <pattern> with <term></title>
978 <titleabbrev>replace</titleabbrev>
979 <para>The tactic <command>replace</command> </para>
981 <sect1 id="tac_rewrite">
982 <title>rewrite {<|>} <term> <pattern></title>
983 <titleabbrev>rewrite</titleabbrev>
984 <para>The tactic <command>rewrite</command> </para>
986 <sect1 id="tac_right">
988 <titleabbrev>right</titleabbrev>
989 <para><userinput>right </userinput></para>
993 <term>Pre-conditions:</term>
995 <para>the conclusion of the current sequent must be
996 an inductive type or the application of an inductive type with
997 at least two constructors.</para>
1001 <term>Action:</term>
1003 <para>equivalent to <command>constructor 2</command>.</para>
1007 <term>New sequents to prove:</term>
1009 <para>it opens a new sequent for each premise of the second
1010 constructor of the inductive type that is the conclusion of the
1011 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1017 <sect1 id="tac_ring">
1019 <titleabbrev>ring</titleabbrev>
1020 <para>The tactic <command>ring</command> </para>
1022 <sect1 id="tac_simplify">
1023 <title>simplify <pattern></title>
1024 <titleabbrev>simplify</titleabbrev>
1025 <para><userinput>simplify patt</userinput></para>
1029 <term>Pre-conditions:</term>
1035 <term>Action:</term>
1037 <para>it replaces all the terms matched by <command>patt</command>
1038 with other convertible terms that are supposed to be simpler.</para>
1042 <term>New sequents to prove:</term>
1050 <sect1 id="tac_split">
1051 <title>split</title>
1052 <titleabbrev>split</titleabbrev>
1053 <para>The tactic <command>split</command> </para>
1055 <sect1 id="tac_symmetry">
1056 <title>symmetry</title>
1057 <titleabbrev>symmetry</titleabbrev>
1058 <para>The tactic <command>symmetry</command> </para>
1060 <sect1 id="tac_transitivity">
1061 <title>transitivity <term></title>
1062 <titleabbrev>transitivity</titleabbrev>
1063 <para>The tactic <command>transitivity</command> </para>
1065 <sect1 id="tac_unfold">
1066 <title>unfold [<term>] <pattern></title>
1067 <titleabbrev>unfold</titleabbrev>
1068 <para>The tactic <command>unfold</command> </para>
1070 <sect1 id="tac_whd">
1071 <title>whd <pattern></title>
1072 <titleabbrev>whd</titleabbrev>
1073 <para><userinput>whd patt</userinput></para>
1077 <term>Pre-conditions:</term>
1083 <term>Action:</term>
1085 <para>it replaces all the terms matched by <command>patt</command>
1086 with their βδιζ-weak-head normal form.</para>
1090 <term>New sequents to prove:</term>