2 <!-- ============ Tactics ====================== -->
3 <sect1 id="sec_tactics">
6 <sect2 id="tac_absurd">
7 <title>absurd <term></title>
8 <para><userinput>absurd P</userinput></para>
11 <term>Pre-conditions:</term>
13 <para><command>P</command> must have type <command>Prop</command>.</para>
20 <para>it closes the current sequent by eliminating an
25 <term>New sequents to prove:</term>
27 <para>it opens two new sequents of conclusion <command>P</command>
28 and <command>¬P</command>.</para>
34 <sect2 id="tac_apply">
35 <title>apply <term></title>
36 <para><userinput>apply t</userinput></para>
40 <term>Pre-conditions:</term>
42 <para><command>t</command> must have type
43 <command>T<subscript>1</subscript> → ... →
44 T<subscript>n</subscript> → G</command>
45 where <command>G</command> can be unified with the conclusion
46 of the current sequent.</para>
52 <para>it closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
56 <term>New sequents to prove:</term>
58 <para>it opens a new sequent for each premise
59 <command>T<subscript>i</subscript></command> that is not
60 instantiated by unification. <command>T<subscript>i</subscript></command> is
61 the conclusion of the <command>i</command>-th new sequent to
68 <sect2 id="tac_assumption">
69 <title>assumption</title>
70 <para><userinput>assumption</userinput></para>
74 <term>Pre-conditions:</term>
76 <para>there must exist an hypothesis whose type can be unified with
77 the conclusion of the current sequent.</para>
83 <para>it closes the current sequent exploiting an hypothesis.</para>
87 <term>New sequents to prove:</term>
96 <title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
97 <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
101 <term>Pre-conditions:</term>
103 <para>none, but the tactic may fail finding a proof if every
104 proof is in the search space that is pruned away. Pruning is
105 controlled by <command>d</command> and <command>w</command>.
106 Moreover, only lemmas whose type signature is a subset of the
107 signature of the current sequent are considered. The signature of
108 a sequent is ...TODO</para>
114 <para>it closes the current sequent by repeated application of
115 rewriting steps (unless <command>paramodulation</command> is
116 omitted), hypothesis and lemmas in the library.</para>
120 <term>New sequents to prove:</term>
128 <sect2 id="tac_clear">
129 <title>clear <id></title>
130 <para><userinput>clear H</userinput></para>
134 <term>Pre-conditions:</term>
136 <para><command>H</command> must be an hypothesis of the
137 current sequent to prove.</para>
143 <para>it hides the hypothesis <command>H</command> from the
144 current sequent.</para>
148 <term>New sequents to prove:</term>
156 <sect2 id="tac_clearbody">
157 <title>clearbody <id></title>
158 <para><userinput>clearbody H</userinput></para>
162 <term>Pre-conditions:</term>
164 <para><command>H</command> must be an hypothesis of the
165 current sequent to prove.</para>
171 <para>it hides the definiens of a definition in the current
172 sequent context. Thus the definition becomes an hypothesis.</para>
176 <term>New sequents to prove:</term>
184 <sect2 id="tac_change">
185 <title>change <pattern> with <term></title>
186 <para><userinput>change patt with t</userinput></para>
190 <term>Pre-conditions:</term>
192 <para>each subterm matched by the pattern must be convertible
193 with the term <command>t</command> disambiguated in the context
194 of the matched subterm.</para>
200 <para>it replaces the subterms of the current sequent matched by
201 <command>patt</command> with the new term <command>t</command>.
202 For each subterm matched by the pattern, <command>t</command> is
203 disambiguated in the context of the subterm.</para>
207 <term>New sequents to prove:</term>
215 <sect2 id="tac_constructor">
216 <title>constructor <int></title>
217 <para><userinput>constructor n</userinput></para>
221 <term>Pre-conditions:</term>
223 <para>the conclusion of the current sequent must be
224 an inductive type or the application of an inductive type.</para>
230 <para>it applies the <command>n</command>-th constructor of the
231 inductive type of the conclusion of the current sequent.</para>
235 <term>New sequents to prove:</term>
237 <para>it opens a new sequent for each premise of the constructor
238 that can not be inferred by unification. For more details,
239 see the <command>apply</command> tactic.</para>
245 <sect2 id="tac_contradiction">
246 <title>contradiction</title>
247 <para><userinput>contradiction</userinput></para>
251 <term>Pre-conditions:</term>
253 <para>there must be in the current context an hypothesis of type
254 <command>False</command>.</para>
260 <para>it closes the current sequent by applying an hypothesis of
261 type <command>False</command>.</para>
265 <term>New sequents to prove:</term>
274 <title>cut <term> [as <id>]</title>
275 <para><userinput>cut P as H</userinput></para>
279 <term>Pre-conditions:</term>
281 <para><command>P</command> must have type <command>Prop</command>.</para>
287 <para>it closes the current sequent.</para>
291 <term>New sequents to prove:</term>
293 <para>it opens two new sequents. The first one has an extra
294 hypothesis <command>H:P</command>. If <command>H</command> is
295 omitted, the name of the hypothesis is automatically generated.
296 The second sequent has conclusion <command>P</command> and
297 hypotheses the hypotheses of the current sequent to prove.</para>
303 <sect2 id="tac_decompose">
304 <title>decompose [<ident list>] <ident> [<intros_spec>]</title>
305 <para><userinput>decompose ???</userinput></para>
309 <term>Pre-conditions:</term>
321 <term>New sequents to prove:</term>
329 <sect2 id="tac_discriminate">
330 <title>discriminate <term></title>
331 <para><userinput>discriminate p</userinput></para>
335 <term>Pre-conditions:</term>
337 <para><command>p</command> must have type <command>K<subscript>1</subscript> t<subscript>1</subscript> ... t<subscript>n</subscript> = K'<subscript>1</subscript> 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
338 its constructor takes no arguments.</para>
344 <para>it closes the current sequent by proving the absurdity of
345 <command>p</command>.</para>
349 <term>New sequents to prove:</term>
357 <sect2 id="tac_elim">
358 <title>elim <term> [using <term>] [<intros_spec>]</title>
359 <para><userinput>elim t using th hyps</userinput></para>
363 <term>Pre-conditions:</term>
365 <para><command>t</command> must inhabit an inductive type and
366 <command>th</command> must be an elimination principle for that
367 inductive type. If <command>th</command> is omitted the appropriate
368 standard elimination principle is chosen.</para>
374 <para>it proceeds by cases on the values of <command>t</command>,
375 according to the elimination principle <command>th</command>.
380 <term>New sequents to prove:</term>
382 <para>it opens one new sequent for each case. The names of
383 the new hypotheses are picked by <command>hyps</command>, if
390 <sect2 id="tac_elimType">
391 <title>elimType <term> [using <term>]</title>
392 <para><userinput>elimType T using th</userinput></para>
396 <term>Pre-conditions:</term>
398 <para><command>T</command> must be an inductive type.</para>
404 <para>TODO (severely bugged now).</para>
408 <term>New sequents to prove:</term>
416 <sect2 id="tac_exact">
417 <title>exact <term></title>
418 <para><userinput>exact p</userinput></para>
422 <term>Pre-conditions:</term>
424 <para>the type of <command>p</command> must be convertible
425 with the conclusion of the current sequent.</para>
431 <para>it closes the current sequent using <command>p</command>.</para>
435 <term>New sequents to prove:</term>
443 <sect2 id="tac_exists">
444 <title>exists</title>
445 <para><userinput>exists</userinput></para>
449 <term>Pre-conditions:</term>
451 <para>the conclusion of the current sequent must be
452 an inductive type or the application of an inductive type.</para>
458 <para>equivalent to <command>constructor 1</command>.</para>
462 <term>New sequents to prove:</term>
464 <para>it opens a new sequent for each premise of the first
465 constructor of the inductive type that is the conclusion of the
466 current sequent. For more details, see the <command>constructor</command> tactic.</para>
472 <sect2 id="tac_fail">
474 <para><userinput>fail</userinput></para>
478 <term>Pre-conditions:</term>
486 <para>this tactic always fail.</para>
490 <term>New sequents to prove:</term>
498 <sect2 id="tac_fold">
499 <title>fold <reduction_kind> <term> <pattern></title>
500 <para><userinput>fold red t patt</userinput></para>
504 <term>Pre-conditions:</term>
506 <para>the pattern must not specify the wanted term.</para>
512 <para>first of all it locates all the subterms matched by
513 <command>patt</command>. In the context of each matched subterm
514 it disambiguates the term <command>t</command> and reduces it
515 to its <command>red</command> normal form; then it replaces with
516 <command>t</command> every occurrence of the normal form in the
517 matched subterm.</para>
521 <term>New sequents to prove:</term>
529 <sect2 id="tac_fourier">
530 <title>fourier</title>
531 <para><userinput>fourier</userinput></para>
535 <term>Pre-conditions:</term>
537 <para>the conclusion of the current sequent must be a linear
538 inequation over real numbers taken from standard library of
539 Coq. Moreover the inequations in the hypotheses must imply the
540 inequation in the conclusion of the current sequent.</para>
546 <para>it closes the current sequent by applying the Fourier method.</para>
550 <term>New sequents to prove:</term>
559 <title>fwd <ident> [<ident list>]</title>
560 <para><userinput>fwd ...TODO</userinput></para>
564 <term>Pre-conditions:</term>
576 <term>New sequents to prove:</term>
584 <sect2 id="tac_generalize">
585 <title>generalize <pattern> [as <id>]</title>
586 <para>The tactic <command>generalize</command> </para>
590 <para>The tactic <command>id</command> </para>
592 <sect2 id="tac_injection">
593 <title>injection <term></title>
594 <para>The tactic <command>injection</command> </para>
596 <sect2 id="tac_intro">
597 <title>intro [<ident>]</title>
598 <para>The tactic <command>intro</command> </para>
600 <sect2 id="tac_intros">
601 <title>intros <intros_spec></title>
602 <para>The tactic <command>intros</command> </para>
604 <sect2 id="tac_inversion">
605 <title>intros <term></title>
606 <para>The tactic <command>intros</command> </para>
608 <sect2 id="tac_lapply">
609 <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
610 <para>The tactic <command>lapply</command> </para>
612 <sect2 id="tac_left">
614 <para>The tactic <command>left</command> </para>
616 <sect2 id="tac_letin">
617 <title>letin <ident> ≝ <term></title>
618 <para>The tactic <command>letin</command> </para>
620 <sect2 id="tac_normalize">
621 <title>normalize <pattern></title>
622 <para>The tactic <command>normalize</command> </para>
624 <sect2 id="tac_paramodulation">
625 <title>paramodulation <pattern></title>
626 <para>The tactic <command>paramodulation</command> </para>
628 <sect2 id="tac_reduce">
629 <title>reduce <pattern></title>
630 <para>The tactic <command>reduce</command> </para>
632 <sect2 id="tac_reflexivity">
633 <title>reflexivity</title>
634 <para>The tactic <command>reflexivity</command> </para>
636 <sect2 id="tac_replace">
637 <title>replace <pattern> with <term></title>
638 <para>The tactic <command>replace</command> </para>
640 <sect2 id="tac_rewrite">
641 <title>rewrite {<|>} <term> <pattern></title>
642 <para>The tactic <command>rewrite</command> </para>
644 <sect2 id="tac_right">
646 <para>The tactic <command>right</command> </para>
648 <sect2 id="tac_ring">
650 <para>The tactic <command>ring</command> </para>
652 <sect2 id="tac_simplify">
653 <title>simplify <pattern></title>
654 <para>The tactic <command>simplify</command> </para>
656 <sect2 id="tac_split">
658 <para>The tactic <command>split</command> </para>
660 <sect2 id="tac_symmetry">
661 <title>symmetry</title>
662 <para>The tactic <command>symmetry</command> </para>
664 <sect2 id="tac_transitivity">
665 <title>transitivity <term></title>
666 <para>The tactic <command>transitivity</command> </para>
668 <sect2 id="tac_unfold">
669 <title>unfold [<term>] <pattern></title>
670 <para>The tactic <command>unfold</command> </para>
673 <title>whd <pattern></title>
674 <para>The tactic <command>whd</command> </para>