2 <!-- ============ Tactics ====================== -->
3 <chapter id="sec_tactics">
6 <sect1 id="tactics_quickref">
7 <title>Quick reference card</title>
13 <sect1 id="tac_apply">
15 <titleabbrev>@</titleabbrev>
16 <para><userinput>@t</userinput></para>
19 <varlistentry role="tactic.synopsis">
20 <term>Synopsis:</term>
22 <para><emphasis role="bold">@</emphasis> &sterm;</para>
26 <term>Pre-conditions:</term>
28 <para><command>t</command> must have type
29 <command>T<subscript>1</subscript> → … →
30 T<subscript>n</subscript> → G</command>
31 where <command>G</command> can be unified with the conclusion
32 of the current sequent.</para>
38 <para>It closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
42 <term>New sequents to prove:</term>
44 <para>It opens a new sequent for each premise
45 <command>T<subscript>i</subscript></command> that is not
46 instantiated by unification. <command>T<subscript>i</subscript></command> is
47 the conclusion of the <command>i</command>-th new sequent to
56 <titleabbrev>//</titleabbrev>
57 <para><userinput>/params/</userinput></para>
60 <varlistentry role="tactic.synopsis">
61 <term>Synopsis:</term>
63 <para><emphasis role="bold">/</emphasis>&autoparams;<emphasis role="bold">/</emphasis>. </para>
64 <!--<para><emphasis role="bold">autobatch</emphasis> &autoparams;</para>-->
68 <term>Pre-conditions:</term>
70 <para>None, but the tactic may fail finding a proof if every
71 proof is in the search space that is pruned away. Pruning is
72 controlled by the optional <command>params</command>.
73 Moreover, only lemmas whose type signature is a subset of the
74 signature of the current sequent are considered. The signature of
75 a sequent is essentially the set of constats appearing in it.
82 <para>It closes the current sequent by repeated application of
83 rewriting steps (unless <command>paramodulation</command> is
84 omitted), hypothesis and lemmas in the library.</para>
88 <term>New sequents to prove:</term>
96 <sect1 id="tac_intro">
98 <titleabbrev>#</titleabbrev>
99 <para><userinput>#H</userinput></para>
102 <varlistentry role="tactic.synopsis">
103 <term>Synopsis:</term>
105 <para><emphasis role="bold">#</emphasis>&id;</para>
109 <term>Pre-conditions:</term>
111 <para>The conclusion of the sequent to prove must be an implication
112 or a universal quantification.</para>
118 <para>It applies the right introduction rule for implication,
119 closing the current sequent.</para>
123 <term>New sequents to prove:</term>
125 <para>It opens a new sequent to prove adding to the hypothesis
126 the antecedent of the implication and setting the conclusion
127 to the consequent of the implicaiton. The name of the new
128 hypothesis is <command>H</command>.</para>
134 <sect1 id="tac_intro_clear">
136 <titleabbrev>#_</titleabbrev>
137 <para><userinput>#_</userinput></para>
140 <varlistentry role="tactic.synopsis">
141 <term>Synopsis:</term>
143 <para><emphasis role="bold">#_</emphasis></para>
147 <term>Pre-conditions:</term>
149 <para>The conclusion of the sequent to prove must be an implication.
156 <para>It applies the ``a fortiori'' rule for implication,
157 closing the current sequent.</para>
161 <term>New sequents to prove:</term>
163 <para>It opens a new sequent whose conclusion is the conclusion
164 of the implication of the original sequent.</para>
170 <sect1 id="macro_intro">
172 <titleabbrev>##</titleabbrev>
173 <para><userinput>##</userinput></para>
176 <varlistentry role="tactic.synopsis">
177 <term>Synopsis:</term>
179 <para><emphasis role="bold">##</emphasis></para>
183 <term>Pre-conditions:</term>
191 <para>This macro expands to the longest possible list of
192 <command>#H<subscript>i</subscript></command> tactics. The
193 names of the introduced hypotheses are automatically
200 <sect1 id="tac_clear">
202 <titleabbrev>-</titleabbrev>
203 <para><userinput>-H</userinput></para>
206 <varlistentry role="tactic.synopsis">
207 <term>Synopsis:</term>
210 <emphasis role="bold">-</emphasis>&id;
215 <term>Pre-conditions:</term>
218 <command>H</command> must be an hypothesis of the
219 current sequent to prove.
227 It hides the hypothesis <command>H</command>
228 from the current sequent.
233 <term>New sequents to prove:</term>
241 <sect1 id="tac_constructor">
243 <titleabbrev>%</titleabbrev>
244 <para><userinput>%n {args}</userinput></para>
247 <varlistentry role="tactic.synopsis">
248 <term>Synopsis:</term>
250 <para><emphasis role="bold">%</emphasis> [&nat;] [<emphasis role="bol">{</emphasis>&sterm;…<emphasis role="bol">}</emphasis>]</para>
254 <term>Pre-conditions:</term>
256 <para>The conclusion of the current sequent must be
257 an inductive type or the application of an inductive type with
258 at least <command>n</command> constructors.</para>
264 <para>It applies the <command>n</command>-th constructor of the
265 inductive type of the conclusion of the current sequent to
266 the arguments <command>args</command>.
267 If <command>n</command> is omitted, it defaults to 1.</para>
271 <term>New sequents to prove:</term>
273 <para>It opens a new sequent for each premise of the constructor
274 that can not be inferred by unification. For more details,
275 see the <command>apply</command> tactic.</para>
281 <sect1 id="tac_decompose">
283 <titleabbrev>*</titleabbrev>
289 <varlistentry role="tactic.synopsis">
290 <term>Synopsis:</term>
293 <emphasis role="bold">*</emphasis>
294 [<emphasis role="bold">as</emphasis> &id;]
299 <term>Pre-conditions:</term>
301 <para>The current conclusion must be of the form
302 <command>T → G</command> where <command>I</command> is
303 an inductive type applied to its arguments, if any.</para>
310 It introduces a new hypothesis <command>H</command> of type
311 <command>T</command>. Then it proceeds by cases over
312 <command>H</command>. Finally, if the name <command>H</command>
313 is not specified, it clears the new hypothesis from all contexts.
318 <term>New sequents to prove:</term>
321 The ones generated by case analysis.
328 <sect1 id="tac_rewrite">
330 <titleabbrev>></titleabbrev>
331 <para><userinput>> p patt</userinput></para>
334 <varlistentry role="tactic.synopsis">
335 <term>Synopsis:</term>
337 <para>[<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] &sterm; &pattern;</para>
341 <term>Pre-conditions:</term>
343 <para><command>p</command> must be the proof of an equality,
344 possibly under some hypotheses.</para>
350 <para>It looks in every term matched by <command>patt</command>
351 for all the occurrences of the
352 left hand side of the equality that <command>p</command> proves
353 (resp. the right hand side if <command><</command> is used).
354 Every occurence found is replaced with
355 the opposite side of the equality.</para>
359 <term>New sequents to prove:</term>
361 <para>It opens one new sequent for each hypothesis of the
362 equality proved by <command>p</command> that is not closed
363 by unification.</para>
369 <sect1 id="tac_applyS">
370 <title>applyS</title>
371 <titleabbrev>applyS</titleabbrev>
372 <para><userinput>applyS t auto_params</userinput></para>
375 <varlistentry role="tactic.synopsis">
376 <term>Synopsis:</term>
378 <para><emphasis role="bold">applyS</emphasis> &sterm; &autoparams;</para>
382 <term>Pre-conditions:</term>
384 <para><command>t</command> must have type
385 <command>T<subscript>1</subscript> → ... →
386 T<subscript>n</subscript> → G</command>.</para>
392 <para><command>applyS</command> is useful when
393 <command>apply</command> fails because the current goal
394 and the conclusion of the applied theorems are extensionally
395 equivalent up to instantiation of metavariables, but cannot
396 be unified. E.g. the goal is <command>P(n*O+m)</command> and
397 the theorem to be applied proves <command>∀m.P(m+O)</command>.
400 It tries to automatically rewrite the current goal using
401 <link linkend="tac_auto">auto paramodulation</link>
402 to make it unifiable with <command>G</command>.
403 Then it closes the current sequent by applying
404 <command>t</command> to <command>n</command>
405 implicit arguments (that become new sequents).
406 The <command>auto_params</command> parameters are passed
407 directly to <command>auto paramodulation</command>.
412 <term>New sequents to prove:</term>
414 <para>It opens a new sequent for each premise
415 <command>T<subscript>i</subscript></command> that is not
416 instantiated by unification. <command>T<subscript>i</subscript></command> is
417 the conclusion of the <command>i</command>-th new sequent to
424 <sect1 id="tac_assumption">
425 <title>assumption</title>
426 <titleabbrev>assumption</titleabbrev>
427 <para><userinput>assumption </userinput></para>
430 <varlistentry role="tactic.synopsis">
431 <term>Synopsis:</term>
433 <para><emphasis role="bold">assumption</emphasis></para>
437 <term>Pre-conditions:</term>
439 <para>There must exist an hypothesis whose type can be unified with
440 the conclusion of the current sequent.</para>
446 <para>It closes the current sequent exploiting an hypothesis.</para>
450 <term>New sequents to prove:</term>
458 <sect1 id="tac_cases">
460 <titleabbrev>cases</titleabbrev>
466 <varlistentry role="tactic.synopsis">
467 <term>Synopsis:</term>
470 <emphasis role="bold">cases</emphasis>
476 <term>Pre-conditions:</term>
479 <command>t</command> must inhabit an inductive type
487 It proceed by cases on <command>t</command>. The new generated
488 hypothesis in each branch are named according to
489 <command>hyps</command>.
490 The elimintation predicate is restricted by
491 <command>pattern</command>. In particular, if some hypothesis
492 is listed in <command>pattern</command>, the hypothesis is
493 generalized and cleared before proceeding by cases on
494 <command>t</command>. Currently, we only support patterns of the
495 form <command>H<subscript>1</subscript> … H<subscript>n</subscript> ⊢ %</command>. This limitation will be lifted in the future.
500 <term>New sequents to prove:</term>
502 <para>One new sequent for each constructor of the type of
503 <command>t</command>. Each sequent has a new hypothesis for
504 each argument of the constructor.</para>
511 <sect1 id="tac_clearbody">
512 <title>clearbody</title>
513 <titleabbrev>clearbody</titleabbrev>
514 <para><userinput>clearbody H</userinput></para>
517 <varlistentry role="tactic.synopsis">
518 <term>Synopsis:</term>
520 <para><emphasis role="bold">clearbody</emphasis> &id;</para>
524 <term>Pre-conditions:</term>
526 <para><command>H</command> must be an hypothesis of the
527 current sequent to prove.</para>
533 <para>It hides the definiens of a definition in the current
534 sequent context. Thus the definition becomes an hypothesis.</para>
538 <term>New sequents to prove:</term>
548 <sect1 id="tac_compose">
549 <title>compose</title>
550 <titleabbrev>compose</titleabbrev>
551 <para><userinput>compose n t1 with t2 hyps</userinput></para>
554 <varlistentry role="tactic.synopsis">
555 <term>Synopsis:</term>
557 <para><emphasis role="bold">compose</emphasis> [&nat;] &sterm; [<emphasis role="bold">with</emphasis> &sterm;] [&intros-spec;]</para>
561 <term>Pre-conditions:</term>
569 <para>Composes t1 with t2 in every possible way
570 <command>n</command> times introducing generated terms
571 as if <command>intros hyps</command> was issued.</para>
572 <para>If <command>t1:∀x:A.B[x]</command> and
573 <command>t2:∀x,y:A.B[x]→B[y]→C[x,y]</command> it generates:
576 <para><command>λx,y:A.t2 x y (t1 x) : ∀x,y:A.B[y]→C[x,y]</command></para>
579 <para><command>λx,y:A.λH:B[x].t2 x y H (t1 y) : ∀x,y:A.B[x]→C[x,y]
584 <para>If <command>t2</command> is omitted it composes
585 <command>t1</command>
586 with every hypothesis that can be introduced.
587 <command>n</command> iterates the process.</para>
591 <term>New sequents to prove:</term>
593 <para>The same, but with more hypothesis eventually introduced
594 by the &intros-spec;.</para>
601 <sect1 id="tac_change">
602 <title>change</title>
603 <titleabbrev>change</titleabbrev>
604 <para><userinput>change patt with t</userinput></para>
607 <varlistentry role="tactic.synopsis">
608 <term>Synopsis:</term>
610 <para><emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
614 <term>Pre-conditions:</term>
616 <para>Each subterm matched by the pattern must be convertible
617 with the term <command>t</command> disambiguated in the context
618 of the matched subterm.</para>
624 <para>It replaces the subterms of the current sequent matched by
625 <command>patt</command> with the new term <command>t</command>.
626 For each subterm matched by the pattern, <command>t</command> is
627 disambiguated in the context of the subterm.</para>
631 <term>New sequents to prove:</term>
641 <titleabbrev>cut</titleabbrev>
642 <para><userinput>cut P</userinput></para>
645 <varlistentry role="tactic.synopsis">
646 <term>Synopsis:</term>
648 <para><emphasis role="bold">cut</emphasis> &sterm;</para>
652 <term>Pre-conditions:</term>
654 <para><command>P</command> must be a type.</para>
660 <para>It closes the current sequent.</para>
664 <term>New sequents to prove:</term>
666 <para>It opens two new sequents. The first one has conclusion
667 <command>P → G</command> where <command>G</command> is the
669 The second sequent has conclusion <command>P</command> and
670 hypotheses the hypotheses of the current sequent to prove.</para>
677 <sect1 id="tac_demodulate">
678 <title>demodulate</title>
679 <titleabbrev>demodulate</titleabbrev>
680 <para><userinput>demodulate auto_params</userinput></para>
683 <varlistentry role="tactic.synopsis">
684 <term>Synopsis:</term>
686 <para><emphasis role="bold">demodulate</emphasis> &autoparams;</para>
690 <term>Pre-conditions:</term>
702 <term>New sequents to prove:</term>
711 <sect1 id="tac_destruct">
712 <title>destruct</title>
713 <titleabbrev>destruct</titleabbrev>
714 <para><userinput>destruct (H<subscript>0</subscript> ... H<subscript>n</subscript>) skip (K<subscript>0</subscript> ... K<subscript>m</subscript>)</userinput></para>
717 <varlistentry role="tactic.synopsis">
718 <term>Synopsis:</term>
720 <para><emphasis role="bold">destruct</emphasis>
721 [<emphasis role="bold">(</emphasis>&id;…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis>&id;…<emphasis role="bold">)</emphasis>]</para>
725 <term>Pre-conditions:</term>
727 <para>Each hypothesis <command>H<subscript>i</subscript></command> must be either a Leibniz or a John Major equality where the two sides of the equality are possibly applied constructors of an inductive type.</para>
733 <para>The tactic recursively compare the two sides of each equality
734 looking for different constructors in corresponding position.
735 If two of them are found, the tactic closes the current sequent
736 by proving the absurdity of <command>p</command>. Otherwise
737 it adds a new hypothesis for each leaf of the formula that
738 states the equality of the subformulae in the corresponding
739 positions on the two sides of the equality. If the newly
740 added hypothesis is an equality between a variable and a term,
741 the variable is substituted for the term everywhere in the
742 sequent, except for the hypotheses <command>K<subscript>j</subscript></command>, and it is then cleared from the list of hypotheses.
747 <term>New sequents to prove:</term>
755 <sect1 id="tac_elim">
757 <titleabbrev>elim</titleabbrev>
758 <para><userinput>elim t pattern</userinput></para>
761 <varlistentry role="tactic.synopsis">
762 <term>Synopsis:</term>
764 <para><emphasis role="bold">elim</emphasis> &sterm; &pattern;</para>
768 <term>Pre-conditions:</term>
770 <para><command>t</command> must inhabit an inductive type.
777 <para>It proceeds by cases on the values of <command>t</command>,
778 according to the most appropriate elimination principle for
780 The induction predicate is restricted by
781 <command>pattern</command>. In particular, if some hypothesis
782 is listed in <command>pattern</command>, the hypothesis is
783 generalized and cleared before eliminating <command>t</command>
788 <term>New sequents to prove:</term>
790 <para>It opens one new sequent for each case.</para>
797 <sect1 id="tac_fail">
799 <titleabbrev>fail</titleabbrev>
800 <para><userinput>fail</userinput></para>
803 <varlistentry role="tactic.synopsis">
804 <term>Synopsis:</term>
806 <para><emphasis role="bold">fail</emphasis></para>
810 <term>Pre-conditions:</term>
818 <para>This tactic always fail.</para>
822 <term>New sequents to prove:</term>
831 <sect1 id="tac_generalize">
832 <title>generalize</title>
833 <titleabbrev>generalize</titleabbrev>
834 <para><userinput>generalize patt</userinput></para>
837 <varlistentry role="tactic.synopsis">
838 <term>Synopsis:</term>
840 <para><emphasis role="bold">generalize</emphasis> &pattern;</para>
844 <term>Pre-conditions:</term>
846 <para>All the terms matched by <command>patt</command> must be
847 convertible and close in the context of the current sequent.</para>
853 <para>It closes the current sequent by applying a stronger
854 lemma that is proved using the new generated sequent.</para>
858 <term>New sequents to prove:</term>
860 <para>It opens a new sequent where the current sequent conclusion
861 <command>G</command> is generalized to
862 <command>∀x.G{x/t}</command> where <command>{x/t}</command>
863 is a notation for the replacement with <command>x</command> of all
864 the occurrences of the term <command>t</command> matched by
865 <command>patt</command>. If <command>patt</command> matches no
866 subterm then <command>t</command> is defined as the
867 <command>wanted</command> part of the pattern.</para>
876 <titleabbrev>id</titleabbrev>
877 <para><userinput>id </userinput></para>
880 <varlistentry role="tactic.synopsis">
881 <term>Synopsis:</term>
883 <para><emphasis role="bold">id</emphasis></para>
887 <term>Pre-conditions:</term>
895 <para>This identity tactic does nothing without failing.</para>
899 <term>New sequents to prove:</term>
908 <sect1 id="tac_inversion">
909 <title>inversion</title>
910 <titleabbrev>inversion</titleabbrev>
911 <para><userinput>inversion t</userinput></para>
914 <varlistentry role="tactic.synopsis">
915 <term>Synopsis:</term>
917 <para><emphasis role="bold">inversion</emphasis> &sterm;</para>
921 <term>Pre-conditions:</term>
923 <para>The type of the term <command>t</command> must be an inductive
924 type or the application of an inductive type.</para>
930 <para>It proceeds by cases on <command>t</command> paying attention
931 to the constraints imposed by the actual "right arguments"
932 of the inductive type.</para>
936 <term>New sequents to prove:</term>
938 <para>It opens one new sequent to prove for each case in the
939 definition of the type of <command>t</command>. With respect to
940 a simple elimination, each new sequent has additional hypotheses
941 that states the equalities of the "right parameters"
942 of the inductive type with terms originally present in the
943 sequent to prove. It uses either Leibniz or John Major equality
944 for the new hypotheses, according to the included files.</para>
950 <sect1 id="tac_lapply">
951 <title>lapply</title>
952 <titleabbrev>lapply</titleabbrev>
958 <varlistentry role="tactic.synopsis">
959 <term>Synopsis:</term>
962 <emphasis role="bold">lapply</emphasis>
968 <term>Pre-conditions:</term>
977 It generalizes the conclusion of the current goal
978 adding as a premise the type of <command>t</command>,
979 closing the current goal.
984 <term>New sequents to prove:</term>
987 The new sequent has conclusion <command>T → G</command> where
988 <command>T</command> is the type of <command>t</command>
989 and <command>G</command> the old conclusion.
996 <sect1 id="tac_letin">
998 <titleabbrev>letin</titleabbrev>
999 <para><userinput>letin x ≝ t</userinput></para>
1002 <varlistentry role="tactic.synopsis">
1003 <term>Synopsis:</term>
1005 <para><emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm;</para>
1009 <term>Pre-conditions:</term>
1015 <term>Action:</term>
1017 <para>It adds to the context of the current sequent to prove a new
1018 definition <command>x ≝ t</command>.</para>
1022 <term>New sequents to prove:</term>
1030 <sect1 id="tac_normalize">
1031 <title>normalize</title>
1032 <titleabbrev>normalize</titleabbrev>
1033 <para><userinput>normalize patt nodelta</userinput></para>
1036 <varlistentry role="tactic.synopsis">
1037 <term>Synopsis:</term>
1039 <para><emphasis role="bold">normalize</emphasis> &pattern;
1040 [<emphasis role="bold">nodelta</emphasis>]</para>
1044 <term>Pre-conditions:</term>
1050 <term>Action:</term>
1052 <para>It replaces all the terms matched by <command>patt</command>
1053 with their βδιζ-normal form. If <command>nodelta</command> is
1054 specified, δ-expansions are not performed.</para>
1058 <term>New sequents to prove:</term>
1066 <sect1 id="tac_whd">
1068 <titleabbrev>whd</titleabbrev>
1069 <para><userinput>whd patt nodelta</userinput></para>
1072 <varlistentry role="tactic.synopsis">
1073 <term>Synopsis:</term>
1075 <para><emphasis role="bold">whd</emphasis> &pattern; [<emphasis role="bold">nodelta</emphasis>]</para>
1079 <term>Pre-conditions:</term>
1085 <term>Action:</term>
1087 <para>It replaces all the terms matched by <command>patt</command>
1088 with their βδιζ-weak-head normal form. If <command>nodelta</command> is specified, δ-expansions are not performed.</para>
1092 <term>New sequents to prove:</term>