2 <!-- ============ Tactics ====================== -->
3 <chapter id="sec_tactics">
6 <sect1 id="tactics_quickref">
7 <title>Quick reference card</title>
13 <sect1 id="tac_absurd">
15 <titleabbrev>absurd</titleabbrev>
16 <para><userinput>absurd P</userinput></para>
19 <varlistentry role="tactic.synopsis">
20 <term>Synopsis:</term>
22 <para><emphasis role="bold">absurd</emphasis> &sterm;</para>
26 <term>Pre-conditions:</term>
28 <para><command>P</command> must have type <command>Prop</command>.</para>
34 <para>It closes the current sequent by eliminating an
39 <term>New sequents to prove:</term>
41 <para>It opens two new sequents of conclusion <command>P</command>
42 and <command>¬P</command>.</para>
48 <sect1 id="tac_apply">
50 <titleabbrev>apply</titleabbrev>
51 <para><userinput>apply t</userinput></para>
54 <varlistentry role="tactic.synopsis">
55 <term>Synopsis:</term>
57 <para><emphasis role="bold">apply</emphasis> &sterm;</para>
61 <term>Pre-conditions:</term>
63 <para><command>t</command> must have type
64 <command>T<subscript>1</subscript> → ... →
65 T<subscript>n</subscript> → G</command>
66 where <command>G</command> can be unified with the conclusion
67 of the current sequent.</para>
73 <para>It closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
77 <term>New sequents to prove:</term>
79 <para>It opens a new sequent for each premise
80 <command>T<subscript>i</subscript></command> that is not
81 instantiated by unification. <command>T<subscript>i</subscript></command> is
82 the conclusion of the <command>i</command>-th new sequent to
89 <sect1 id="tac_assumption">
90 <title>assumption</title>
91 <titleabbrev>assumption</titleabbrev>
92 <para><userinput>assumption </userinput></para>
95 <varlistentry role="tactic.synopsis">
96 <term>Synopsis:</term>
98 <para><emphasis role="bold">assumption</emphasis></para>
102 <term>Pre-conditions:</term>
104 <para>There must exist an hypothesis whose type can be unified with
105 the conclusion of the current sequent.</para>
111 <para>It closes the current sequent exploiting an hypothesis.</para>
115 <term>New sequents to prove:</term>
123 <sect1 id="tac_auto">
125 <titleabbrev>auto</titleabbrev>
126 <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
129 <varlistentry role="tactic.synopsis">
130 <term>Synopsis:</term>
132 <para><emphasis role="bold">auto</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] [<emphasis role="bold">width=</emphasis>&nat;] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>]</para>
136 <term>Pre-conditions:</term>
138 <para>None, but the tactic may fail finding a proof if every
139 proof is in the search space that is pruned away. Pruning is
140 controlled by <command>d</command> and <command>w</command>.
141 Moreover, only lemmas whose type signature is a subset of the
142 signature of the current sequent are considered. The signature of
143 a sequent is ...TODO</para>
149 <para>It closes the current sequent by repeated application of
150 rewriting steps (unless <command>paramodulation</command> is
151 omitted), hypothesis and lemmas in the library.</para>
155 <term>New sequents to prove:</term>
163 <sect1 id="tac_clear">
165 <titleabbrev>clear</titleabbrev>
166 <para><userinput>clear H</userinput></para>
169 <varlistentry role="tactic.synopsis">
170 <term>Synopsis:</term>
172 <para><emphasis role="bold">clear</emphasis> &id;</para>
176 <term>Pre-conditions:</term>
178 <para><command>H</command> must be an hypothesis of the
179 current sequent to prove.</para>
185 <para>It hides the hypothesis <command>H</command> from the
186 current sequent.</para>
190 <term>New sequents to prove:</term>
198 <sect1 id="tac_clearbody">
199 <title>clearbody</title>
200 <titleabbrev>clearbody</titleabbrev>
201 <para><userinput>clearbody H</userinput></para>
204 <varlistentry role="tactic.synopsis">
205 <term>Synopsis:</term>
207 <para><emphasis role="bold">clearbody</emphasis> &id;</para>
211 <term>Pre-conditions:</term>
213 <para><command>H</command> must be an hypothesis of the
214 current sequent to prove.</para>
220 <para>It hides the definiens of a definition in the current
221 sequent context. Thus the definition becomes an hypothesis.</para>
225 <term>New sequents to prove:</term>
233 <sect1 id="tac_change">
234 <title>change</title>
235 <titleabbrev>change</titleabbrev>
236 <para><userinput>change patt with t</userinput></para>
239 <varlistentry role="tactic.synopsis">
240 <term>Synopsis:</term>
242 <para><emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
246 <term>Pre-conditions:</term>
248 <para>Each subterm matched by the pattern must be convertible
249 with the term <command>t</command> disambiguated in the context
250 of the matched subterm.</para>
256 <para>It replaces the subterms of the current sequent matched by
257 <command>patt</command> with the new term <command>t</command>.
258 For each subterm matched by the pattern, <command>t</command> is
259 disambiguated in the context of the subterm.</para>
263 <term>New sequents to prove:</term>
271 <sect1 id="tac_constructor">
272 <title>constructor</title>
273 <titleabbrev>constructor</titleabbrev>
274 <para><userinput>constructor n</userinput></para>
277 <varlistentry role="tactic.synopsis">
278 <term>Synopsis:</term>
280 <para><emphasis role="bold">constructor</emphasis> &nat;</para>
284 <term>Pre-conditions:</term>
286 <para>The conclusion of the current sequent must be
287 an inductive type or the application of an inductive type with
288 at least <command>n</command> constructors.</para>
294 <para>It applies the <command>n</command>-th constructor of the
295 inductive type of the conclusion of the current sequent.</para>
299 <term>New sequents to prove:</term>
301 <para>It opens a new sequent for each premise of the constructor
302 that can not be inferred by unification. For more details,
303 see the <command>apply</command> tactic.</para>
309 <sect1 id="tac_contradiction">
310 <title>contradiction</title>
311 <titleabbrev>contradiction</titleabbrev>
312 <para><userinput>contradiction </userinput></para>
315 <varlistentry role="tactic.synopsis">
316 <term>Synopsis:</term>
318 <para><emphasis role="bold">contradiction</emphasis></para>
322 <term>Pre-conditions:</term>
324 <para>There must be in the current context an hypothesis of type
325 <command>False</command>.</para>
331 <para>It closes the current sequent by applying an hypothesis of
332 type <command>False</command>.</para>
336 <term>New sequents to prove:</term>
346 <titleabbrev>cut</titleabbrev>
347 <para><userinput>cut P as H</userinput></para>
350 <varlistentry role="tactic.synopsis">
351 <term>Synopsis:</term>
353 <para><emphasis role="bold">cut</emphasis> &sterm; [<emphasis role="bold">as</emphasis> &id;]</para>
357 <term>Pre-conditions:</term>
359 <para><command>P</command> must have type <command>Prop</command>.</para>
365 <para>It closes the current sequent.</para>
369 <term>New sequents to prove:</term>
371 <para>It opens two new sequents. The first one has an extra
372 hypothesis <command>H:P</command>. If <command>H</command> is
373 omitted, the name of the hypothesis is automatically generated.
374 The second sequent has conclusion <command>P</command> and
375 hypotheses the hypotheses of the current sequent to prove.</para>
381 <sect1 id="tac_decompose">
382 <title>decompose</title>
383 <titleabbrev>decompose</titleabbrev>
385 decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) H hips
389 <varlistentry role="tactic.synopsis">
390 <term>Synopsis:</term>
393 <emphasis role="bold">decompose</emphasis>
394 [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
400 <term>Pre-conditions:</term>
403 <command>H</command> must inhabit one inductive type among
405 T<subscript>1</subscript> ... T<subscript>n</subscript>
407 and the types of a predefined list.
415 Runs <command>elim H hyps</command>, clears H and tries to run
416 itself recursively on each new identifier introduced by
417 <command>elim</command> in the opened sequents.
422 <term>New sequents to prove:</term>
425 The ones generated by all the <command>elim</command> tactics run.
432 <sect1 id="tac_demodulation">
433 <title>demodulation</title>
434 <titleabbrev>demodulation</titleabbrev>
435 <para><userinput>demodulation patt</userinput></para>
438 <varlistentry role="tactic.synopsis">
439 <term>Synopsis:</term>
441 <para><emphasis role="bold">demodulation</emphasis> &pattern;</para>
445 <term>Pre-conditions:</term>
457 <term>New sequents to prove:</term>
465 <sect1 id="tac_discriminate">
466 <title>discriminate</title>
467 <titleabbrev>discriminate</titleabbrev>
468 <para><userinput>discriminate p</userinput></para>
471 <varlistentry role="tactic.synopsis">
472 <term>Synopsis:</term>
474 <para><emphasis role="bold">discriminate</emphasis> &sterm;</para>
478 <term>Pre-conditions:</term>
480 <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
481 its constructor takes no arguments.</para>
487 <para>It closes the current sequent by proving the absurdity of
488 <command>p</command>.</para>
492 <term>New sequents to prove:</term>
500 <sect1 id="tac_elim">
502 <titleabbrev>elim</titleabbrev>
503 <para><userinput>elim t using th hyps</userinput></para>
506 <varlistentry role="tactic.synopsis">
507 <term>Synopsis:</term>
509 <para><emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
513 <term>Pre-conditions:</term>
515 <para><command>t</command> must inhabit an inductive type and
516 <command>th</command> must be an elimination principle for that
517 inductive type. If <command>th</command> is omitted the appropriate
518 standard elimination principle is chosen.</para>
524 <para>It proceeds by cases on the values of <command>t</command>,
525 according to the elimination principle <command>th</command>.
530 <term>New sequents to prove:</term>
532 <para>It opens one new sequent for each case. The names of
533 the new hypotheses are picked by <command>hyps</command>, if
534 provided. If hyps specifies also a number of hypotheses that
535 is less than the number of new hypotheses for a new sequent,
536 then the exceeding hypothesis will be kept as implications in
537 the conclusion of the sequent.</para>
543 <sect1 id="tac_elimType">
544 <title>elimType</title>
545 <titleabbrev>elimType</titleabbrev>
546 <para><userinput>elimType T using th hyps</userinput></para>
549 <varlistentry role="tactic.synopsis">
550 <term>Synopsis:</term>
552 <para><emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
556 <term>Pre-conditions:</term>
558 <para><command>T</command> must be an inductive type.</para>
564 <para>TODO (severely bugged now).</para>
568 <term>New sequents to prove:</term>
576 <sect1 id="tac_exact">
578 <titleabbrev>exact</titleabbrev>
579 <para><userinput>exact p</userinput></para>
582 <varlistentry role="tactic.synopsis">
583 <term>Synopsis:</term>
585 <para><emphasis role="bold">exact</emphasis> &sterm;</para>
589 <term>Pre-conditions:</term>
591 <para>The type of <command>p</command> must be convertible
592 with the conclusion of the current sequent.</para>
598 <para>It closes the current sequent using <command>p</command>.</para>
602 <term>New sequents to prove:</term>
610 <sect1 id="tac_exists">
611 <title>exists</title>
612 <titleabbrev>exists</titleabbrev>
613 <para><userinput>exists </userinput></para>
616 <varlistentry role="tactic.synopsis">
617 <term>Synopsis:</term>
619 <para><emphasis role="bold">exists</emphasis></para>
623 <term>Pre-conditions:</term>
625 <para>The conclusion of the current sequent must be
626 an inductive type or the application of an inductive type
627 with at least one constructor.</para>
633 <para>Equivalent to <command>constructor 1</command>.</para>
637 <term>New sequents to prove:</term>
639 <para>It opens a new sequent for each premise of the first
640 constructor of the inductive type that is the conclusion of the
641 current sequent. For more details, see the <command>constructor</command> tactic.</para>
647 <sect1 id="tac_fail">
649 <titleabbrev>fail</titleabbrev>
650 <para><userinput>fail</userinput></para>
653 <varlistentry role="tactic.synopsis">
654 <term>Synopsis:</term>
656 <para><emphasis role="bold">fail</emphasis></para>
660 <term>Pre-conditions:</term>
668 <para>This tactic always fail.</para>
672 <term>New sequents to prove:</term>
680 <sect1 id="tac_fold">
682 <titleabbrev>fold</titleabbrev>
683 <para><userinput>fold red t patt</userinput></para>
686 <varlistentry role="tactic.synopsis">
687 <term>Synopsis:</term>
689 <para><emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern;</para>
693 <term>Pre-conditions:</term>
695 <para>The pattern must not specify the wanted term.</para>
701 <para>First of all it locates all the subterms matched by
702 <command>patt</command>. In the context of each matched subterm
703 it disambiguates the term <command>t</command> and reduces it
704 to its <command>red</command> normal form; then it replaces with
705 <command>t</command> every occurrence of the normal form in the
706 matched subterm.</para>
710 <term>New sequents to prove:</term>
718 <sect1 id="tac_fourier">
719 <title>fourier</title>
720 <titleabbrev>fourier</titleabbrev>
721 <para><userinput>fourier </userinput></para>
724 <varlistentry role="tactic.synopsis">
725 <term>Synopsis:</term>
727 <para><emphasis role="bold">fourier</emphasis></para>
731 <term>Pre-conditions:</term>
733 <para>The conclusion of the current sequent must be a linear
734 inequation over real numbers taken from standard library of
735 Coq. Moreover the inequations in the hypotheses must imply the
736 inequation in the conclusion of the current sequent.</para>
742 <para>It closes the current sequent by applying the Fourier method.</para>
746 <term>New sequents to prove:</term>
756 <titleabbrev>fwd</titleabbrev>
757 <para><userinput>fwd H as H<subscript>0</subscript> ... H<subscript>n</subscript></userinput></para>
760 <varlistentry role="tactic.synopsis">
761 <term>Synopsis:</term>
763 <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">as</emphasis> &id; [&id;]…]</para>
767 <term>Pre-conditions:</term>
770 The type of <command>H</command> must be the premise of a
771 forward simplification theorem.
779 This tactic is under development.
780 It simplifies the current context by removing
781 <command>H</command> using the following methods:
782 forward application (by <command>lapply</command>) of a suitable
783 simplification theorem, chosen automatically, of which the type
784 of <command>H</command> is a premise,
785 decomposition (by <command>decompose</command>),
786 rewriting (by <command>rewrite</command>).
787 <command>H<subscript>0</subscript> ... H<subscript>n</subscript></command>
788 are passed to the tactics <command>fwd</command> invokes, as
789 names for the premise they introduce.
794 <term>New sequents to prove:</term>
797 The ones opened by the tactics <command>fwd</command> invokes.
804 <sect1 id="tac_generalize">
805 <title>generalize</title>
806 <titleabbrev>generalize</titleabbrev>
807 <para><userinput>generalize patt as H</userinput></para>
810 <varlistentry role="tactic.synopsis">
811 <term>Synopsis:</term>
813 <para><emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;]</para>
817 <term>Pre-conditions:</term>
819 <para>All the terms matched by <command>patt</command> must be
820 convertible and close in the context of the current sequent.</para>
826 <para>It closes the current sequent by applying a stronger
827 lemma that is proved using the new generated sequent.</para>
831 <term>New sequents to prove:</term>
833 <para>It opens a new sequent where the current sequent conclusion
834 <command>G</command> is generalized to
835 <command>∀x.G{x/t}</command> where <command>{x/t}</command>
836 is a notation for the replacement with <command>x</command> of all
837 the occurrences of the term <command>t</command> matched by
838 <command>patt</command>. If <command>patt</command> matches no
839 subterm then <command>t</command> is defined as the
840 <command>wanted</command> part of the pattern.</para>
848 <titleabbrev>id</titleabbrev>
849 <para><userinput>id </userinput></para>
852 <varlistentry role="tactic.synopsis">
853 <term>Synopsis:</term>
855 <para><emphasis role="bold">id</emphasis></para>
859 <term>Pre-conditions:</term>
867 <para>This identity tactic does nothing without failing.</para>
871 <term>New sequents to prove:</term>
879 <sect1 id="tac_injection">
880 <title>injection</title>
881 <titleabbrev>injection</titleabbrev>
882 <para><userinput>injection p</userinput></para>
885 <varlistentry role="tactic.synopsis">
886 <term>Synopsis:</term>
888 <para><emphasis role="bold">injection</emphasis> &sterm;</para>
892 <term>Pre-conditions:</term>
894 <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
895 <command>K</command> takes no arguments.</para>
901 <para>It derives new hypotheses by injectivity of
902 <command>K</command>.</para>
906 <term>New sequents to prove:</term>
908 <para>The new sequent to prove is equal to the current sequent
909 with the additional hypotheses
910 <command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
916 <sect1 id="tac_intro">
918 <titleabbrev>intro</titleabbrev>
919 <para><userinput>intro H</userinput></para>
922 <varlistentry role="tactic.synopsis">
923 <term>Synopsis:</term>
925 <para><emphasis role="bold">intro</emphasis> [&id;]</para>
929 <term>Pre-conditions:</term>
931 <para>The conclusion of the sequent to prove must be an implication
932 or a universal quantification.</para>
938 <para>It applies the right introduction rule for implication,
939 closing the current sequent.</para>
943 <term>New sequents to prove:</term>
945 <para>It opens a new sequent to prove adding to the hypothesis
946 the antecedent of the implication and setting the conclusion
947 to the consequent of the implicaiton. The name of the new
948 hypothesis is <command>H</command> if provided; otherwise it
949 is automatically generated.</para>
955 <sect1 id="tac_intros">
956 <title>intros</title>
957 <titleabbrev>intros</titleabbrev>
958 <para><userinput>intros hyps</userinput></para>
961 <varlistentry role="tactic.synopsis">
962 <term>Synopsis:</term>
964 <para><emphasis role="bold">intros</emphasis> &intros-spec;</para>
968 <term>Pre-conditions:</term>
970 <para>If <command>hyps</command> specifies a number of hypotheses
971 to introduce, then the conclusion of the current sequent must
972 be formed by at least that number of imbricated implications
973 or universal quantifications.</para>
979 <para>It applies several times the right introduction rule for
980 implication, closing the current sequent.</para>
984 <term>New sequents to prove:</term>
986 <para>It opens a new sequent to prove adding a number of new
987 hypotheses equal to the number of new hypotheses requested.
988 If the user does not request a precise number of new hypotheses,
989 it adds as many hypotheses as possible.
990 The name of each new hypothesis is either popped from the
991 user provided list of names, or it is automatically generated when
992 the list is (or becomes) empty.</para>
998 <sect1 id="tac_inversion">
999 <title>inversion</title>
1000 <titleabbrev>inversion</titleabbrev>
1001 <para><userinput>inversion t</userinput></para>
1004 <varlistentry role="tactic.synopsis">
1005 <term>Synopsis:</term>
1007 <para><emphasis role="bold">inversion</emphasis> &sterm;</para>
1011 <term>Pre-conditions:</term>
1013 <para>The type of the term <command>t</command> must be an inductive
1014 type or the application of an inductive type.</para>
1018 <term>Action:</term>
1020 <para>It proceeds by cases on <command>t</command> paying attention
1021 to the constraints imposed by the actual "right arguments"
1022 of the inductive type.</para>
1026 <term>New sequents to prove:</term>
1028 <para>It opens one new sequent to prove for each case in the
1029 definition of the type of <command>t</command>. With respect to
1030 a simple elimination, each new sequent has additional hypotheses
1031 that states the equalities of the "right parameters"
1032 of the inductive type with terms originally present in the
1033 sequent to prove.</para>
1039 <sect1 id="tac_lapply">
1040 <title>lapply</title>
1041 <titleabbrev>lapply</titleabbrev>
1044 to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
1048 <varlistentry role="tactic.synopsis">
1049 <term>Synopsis:</term>
1051 <para><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">as</emphasis> &id;]</para>
1055 <term>Pre-conditions:</term>
1058 <command>t</command> must have at least <command>d</command>
1059 independent premises and <command>n</command> must not be
1060 greater than <command>d</command>.
1065 <term>Action:</term>
1068 It invokes <command>letin H ≝ (t ? ... ?)</command>
1069 with enough <command>?</command>'s to reach the
1070 <command>d</command>-th independent premise of
1071 <command>t</command>
1072 (<command>d</command> is maximum if unspecified).
1073 Then it istantiates (by <command>apply</command>) with
1074 t<subscript>1</subscript>, ..., t<subscript>n</subscript>
1075 the <command>?</command>'s corresponding to the first
1076 <command>n</command> independent premises of
1077 <command>t</command>.
1078 Usually the other <command>?</command>'s preceding the
1079 <command>n</command>-th independent premise of
1080 <command>t</command> are istantiated as a consequence.
1085 <term>New sequents to prove:</term>
1088 The ones opened by the tactics <command>lapply</command> invokes.
1095 <sect1 id="tac_left">
1097 <titleabbrev>left</titleabbrev>
1098 <para><userinput>left </userinput></para>
1101 <varlistentry role="tactic.synopsis">
1102 <term>Synopsis:</term>
1104 <para><emphasis role="bold">left</emphasis></para>
1108 <term>Pre-conditions:</term>
1110 <para>The conclusion of the current sequent must be
1111 an inductive type or the application of an inductive type
1112 with at least one constructor.</para>
1116 <term>Action:</term>
1118 <para>Equivalent to <command>constructor 1</command>.</para>
1122 <term>New sequents to prove:</term>
1124 <para>It opens a new sequent for each premise of the first
1125 constructor of the inductive type that is the conclusion of the
1126 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1132 <sect1 id="tac_letin">
1133 <title>letin</title>
1134 <titleabbrev>letin</titleabbrev>
1135 <para><userinput>letin x ≝ t</userinput></para>
1138 <varlistentry role="tactic.synopsis">
1139 <term>Synopsis:</term>
1141 <para><emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm;</para>
1145 <term>Pre-conditions:</term>
1151 <term>Action:</term>
1153 <para>It adds to the context of the current sequent to prove a new
1154 definition <command>x ≝ t</command>.</para>
1158 <term>New sequents to prove:</term>
1166 <sect1 id="tac_normalize">
1167 <title>normalize</title>
1168 <titleabbrev>normalize</titleabbrev>
1169 <para><userinput>normalize patt</userinput></para>
1172 <varlistentry role="tactic.synopsis">
1173 <term>Synopsis:</term>
1175 <para><emphasis role="bold">normalize</emphasis> &pattern;</para>
1179 <term>Pre-conditions:</term>
1185 <term>Action:</term>
1187 <para>It replaces all the terms matched by <command>patt</command>
1188 with their βδιζ-normal form.</para>
1192 <term>New sequents to prove:</term>
1200 <sect1 id="tac_paramodulation">
1201 <title>paramodulation</title>
1202 <titleabbrev>paramodulation</titleabbrev>
1203 <para><userinput>paramodulation patt</userinput></para>
1206 <varlistentry role="tactic.synopsis">
1207 <term>Synopsis:</term>
1209 <para><emphasis role="bold">paramodulation</emphasis> &pattern;</para>
1213 <term>Pre-conditions:</term>
1219 <term>Action:</term>
1225 <term>New sequents to prove:</term>
1233 <sect1 id="tac_reduce">
1234 <title>reduce</title>
1235 <titleabbrev>reduce</titleabbrev>
1236 <para><userinput>reduce patt</userinput></para>
1239 <varlistentry role="tactic.synopsis">
1240 <term>Synopsis:</term>
1242 <para><emphasis role="bold">reduce</emphasis> &pattern;</para>
1246 <term>Pre-conditions:</term>
1252 <term>Action:</term>
1254 <para>It replaces all the terms matched by <command>patt</command>
1255 with their βδιζ-normal form.</para>
1259 <term>New sequents to prove:</term>
1267 <sect1 id="tac_reflexivity">
1268 <title>reflexivity</title>
1269 <titleabbrev>reflexivity</titleabbrev>
1270 <para><userinput>reflexivity </userinput></para>
1273 <varlistentry role="tactic.synopsis">
1274 <term>Synopsis:</term>
1276 <para><emphasis role="bold">reflexivity</emphasis></para>
1280 <term>Pre-conditions:</term>
1282 <para>The conclusion of the current sequent must be
1283 <command>t=t</command> for some term <command>t</command></para>
1287 <term>Action:</term>
1289 <para>It closes the current sequent by reflexivity
1294 <term>New sequents to prove:</term>
1302 <sect1 id="tac_replace">
1303 <title>replace</title>
1304 <titleabbrev>change</titleabbrev>
1305 <para><userinput>change patt with t</userinput></para>
1308 <varlistentry role="tactic.synopsis">
1309 <term>Synopsis:</term>
1311 <para><emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
1315 <term>Pre-conditions:</term>
1321 <term>Action:</term>
1323 <para>It replaces the subterms of the current sequent matched by
1324 <command>patt</command> with the new term <command>t</command>.
1325 For each subterm matched by the pattern, <command>t</command> is
1326 disambiguated in the context of the subterm.</para>
1330 <term>New sequents to prove:</term>
1332 <para>For each matched term <command>t'</command> it opens
1333 a new sequent to prove whose conclusion is
1334 <command>t'=t</command>.</para>
1340 <sect1 id="tac_rewrite">
1341 <title>rewrite</title>
1342 <titleabbrev>rewrite</titleabbrev>
1343 <para><userinput>rewrite dir p patt</userinput></para>
1346 <varlistentry role="tactic.synopsis">
1347 <term>Synopsis:</term>
1349 <para><emphasis role="bold">rewrite</emphasis> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] &sterm; &pattern;</para>
1353 <term>Pre-conditions:</term>
1355 <para><command>p</command> must be the proof of an equality,
1356 possibly under some hypotheses.</para>
1360 <term>Action:</term>
1362 <para>It looks in every term matched by <command>patt</command>
1363 for all the occurrences of the
1364 left hand side of the equality that <command>p</command> proves
1365 (resp. the right hand side if <command>dir</command> is
1366 <command><</command>). Every occurence found is replaced with
1367 the opposite side of the equality.</para>
1371 <term>New sequents to prove:</term>
1373 <para>It opens one new sequent for each hypothesis of the
1374 equality proved by <command>p</command> that is not closed
1375 by unification.</para>
1381 <sect1 id="tac_right">
1382 <title>right</title>
1383 <titleabbrev>right</titleabbrev>
1384 <para><userinput>right </userinput></para>
1387 <varlistentry role="tactic.synopsis">
1388 <term>Synopsis:</term>
1390 <para><emphasis role="bold">right</emphasis></para>
1394 <term>Pre-conditions:</term>
1396 <para>The conclusion of the current sequent must be
1397 an inductive type or the application of an inductive type with
1398 at least two constructors.</para>
1402 <term>Action:</term>
1404 <para>Equivalent to <command>constructor 2</command>.</para>
1408 <term>New sequents to prove:</term>
1410 <para>It opens a new sequent for each premise of the second
1411 constructor of the inductive type that is the conclusion of the
1412 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1418 <sect1 id="tac_ring">
1420 <titleabbrev>ring</titleabbrev>
1421 <para><userinput>ring </userinput></para>
1424 <varlistentry role="tactic.synopsis">
1425 <term>Synopsis:</term>
1427 <para><emphasis role="bold">ring</emphasis></para>
1431 <term>Pre-conditions:</term>
1433 <para>The conclusion of the current sequent must be an
1434 equality over Coq's real numbers that can be proved using
1435 the ring properties of the real numbers only.</para>
1439 <term>Action:</term>
1441 <para>It closes the current sequent veryfying the equality by
1442 means of computation (i.e. this is a reflexive tactic, implemented
1443 exploiting the "two level reasoning" technique).</para>
1447 <term>New sequents to prove:</term>
1455 <sect1 id="tac_simplify">
1456 <title>simplify</title>
1457 <titleabbrev>simplify</titleabbrev>
1458 <para><userinput>simplify patt</userinput></para>
1461 <varlistentry role="tactic.synopsis">
1462 <term>Synopsis:</term>
1464 <para><emphasis role="bold">simplify</emphasis> &pattern;</para>
1468 <term>Pre-conditions:</term>
1474 <term>Action:</term>
1476 <para>It replaces all the terms matched by <command>patt</command>
1477 with other convertible terms that are supposed to be simpler.</para>
1481 <term>New sequents to prove:</term>
1489 <sect1 id="tac_split">
1490 <title>split</title>
1491 <titleabbrev>split</titleabbrev>
1492 <para><userinput>split </userinput></para>
1495 <varlistentry role="tactic.synopsis">
1496 <term>Synopsis:</term>
1498 <para><emphasis role="bold">split</emphasis></para>
1502 <term>Pre-conditions:</term>
1504 <para>The conclusion of the current sequent must be
1505 an inductive type or the application of an inductive type with
1506 at least one constructor.</para>
1510 <term>Action:</term>
1512 <para>Equivalent to <command>constructor 1</command>.</para>
1516 <term>New sequents to prove:</term>
1518 <para>It opens a new sequent for each premise of the first
1519 constructor of the inductive type that is the conclusion of the
1520 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1526 <sect1 id="tac_symmetry">
1527 <title>symmetry</title>
1528 <titleabbrev>symmetry</titleabbrev>
1529 <para>The tactic <command>symmetry</command> </para>
1530 <para><userinput>symmetry </userinput></para>
1533 <varlistentry role="tactic.synopsis">
1534 <term>Synopsis:</term>
1536 <para><emphasis role="bold">symmetry</emphasis></para>
1540 <term>Pre-conditions:</term>
1542 <para>The conclusion of the current proof must be an equality.</para>
1546 <term>Action:</term>
1548 <para>It swaps the two sides of the equalityusing the symmetric
1553 <term>New sequents to prove:</term>
1561 <sect1 id="tac_transitivity">
1562 <title>transitivity</title>
1563 <titleabbrev>transitivity</titleabbrev>
1564 <para><userinput>transitivity t</userinput></para>
1567 <varlistentry role="tactic.synopsis">
1568 <term>Synopsis:</term>
1570 <para><emphasis role="bold">transitivity</emphasis> &sterm;</para>
1574 <term>Pre-conditions:</term>
1576 <para>The conclusion of the current proof must be an equality.</para>
1580 <term>Action:</term>
1582 <para>It closes the current sequent by transitivity of the equality.</para>
1586 <term>New sequents to prove:</term>
1588 <para>It opens two new sequents <command>l=t</command> and
1589 <command>t=r</command> where <command>l</command> and <command>r</command> are the left and right hand side of the equality in the conclusion of
1590 the current sequent to prove.</para>
1596 <sect1 id="tac_unfold">
1597 <title>unfold</title>
1598 <titleabbrev>unfold</titleabbrev>
1599 <para><userinput>unfold t patt</userinput></para>
1602 <varlistentry role="tactic.synopsis">
1603 <term>Synopsis:</term>
1605 <para><emphasis role="bold">unfold</emphasis> [&sterm;] &pattern;</para>
1609 <term>Pre-conditions:</term>
1615 <term>Action:</term>
1617 <para>It finds all the occurrences of <command>t</command>
1618 (possibly applied to arguments) in the subterms matched by
1619 <command>patt</command>. Then it δ-expands each occurrence,
1620 also performing β-reduction of the obtained term. If
1621 <command>t</command> is omitted it defaults to each
1622 subterm matched by <command>patt</command>.</para>
1626 <term>New sequents to prove:</term>
1634 <sect1 id="tac_whd">
1636 <titleabbrev>whd</titleabbrev>
1637 <para><userinput>whd patt</userinput></para>
1640 <varlistentry role="tactic.synopsis">
1641 <term>Synopsis:</term>
1643 <para><emphasis role="bold">whd</emphasis> &pattern;</para>
1647 <term>Pre-conditions:</term>
1653 <term>Action:</term>
1655 <para>It replaces all the terms matched by <command>patt</command>
1656 with their βδιζ-weak-head normal form.</para>
1660 <term>New sequents to prove:</term>