2 <!-- ============ Tactics ====================== -->
3 <chapter id="sec_tactics">
6 <sect1 id="tac_absurd">
7 <title><emphasis role="bold">absurd</emphasis> &sterm;</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><emphasis role="bold">apply</emphasis> &sterm;</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><emphasis role="bold">assumption</emphasis></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><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>]</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><emphasis role="bold">clear</emphasis> &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><emphasis role="bold">clearbody</emphasis> &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><emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</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><emphasis role="bold">constructor</emphasis> &nat;</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 with
233 at least <command>n</command> constructors.</para>
239 <para>It applies the <command>n</command>-th constructor of the
240 inductive type of the conclusion of the current sequent.</para>
244 <term>New sequents to prove:</term>
246 <para>It opens a new sequent for each premise of the constructor
247 that can not be inferred by unification. For more details,
248 see the <command>apply</command> tactic.</para>
254 <sect1 id="tac_contradiction">
255 <title><emphasis role="bold">contradiction</emphasis></title>
256 <titleabbrev>contradiction</titleabbrev>
257 <para><userinput>contradiction </userinput></para>
261 <term>Pre-conditions:</term>
263 <para>There must be in the current context an hypothesis of type
264 <command>False</command>.</para>
270 <para>It closes the current sequent by applying an hypothesis of
271 type <command>False</command>.</para>
275 <term>New sequents to prove:</term>
284 <title><emphasis role="bold">cut</emphasis> &sterm; [<emphasis role="bold">as</emphasis> &id;]</title>
285 <titleabbrev>cut</titleabbrev>
286 <para><userinput>cut P as H</userinput></para>
290 <term>Pre-conditions:</term>
292 <para><command>P</command> must have type <command>Prop</command>.</para>
298 <para>It closes the current sequent.</para>
302 <term>New sequents to prove:</term>
304 <para>It opens two new sequents. The first one has an extra
305 hypothesis <command>H:P</command>. If <command>H</command> is
306 omitted, the name of the hypothesis is automatically generated.
307 The second sequent has conclusion <command>P</command> and
308 hypotheses the hypotheses of the current sequent to prove.</para>
314 <sect1 id="tac_decompose">
315 <title><emphasis role="bold">decompose</emphasis> &id; [&id;]… &intros-spec;</title>
316 <titleabbrev>decompose</titleabbrev>
317 <para><userinput>decompose ???</userinput></para>
321 <term>Pre-conditions:</term>
333 <term>New sequents to prove:</term>
341 <sect1 id="tac_demodulation">
342 <title><emphasis role="bold">demodulation</emphasis> &pattern;</title>
343 <titleabbrev>demodulation</titleabbrev>
344 <para><userinput>demodulation patt</userinput></para>
348 <term>Pre-conditions:</term>
360 <term>New sequents to prove:</term>
368 <sect1 id="tac_discriminate">
369 <title><emphasis role="bold">discriminate</emphasis> &sterm;</title>
370 <titleabbrev>discriminate</titleabbrev>
371 <para><userinput>discriminate p</userinput></para>
375 <term>Pre-conditions:</term>
377 <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
378 its constructor takes no arguments.</para>
384 <para>It closes the current sequent by proving the absurdity of
385 <command>p</command>.</para>
389 <term>New sequents to prove:</term>
397 <sect1 id="tac_elim">
398 <title><emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</title>
399 <titleabbrev>elim</titleabbrev>
400 <para><userinput>elim t using th hyps</userinput></para>
404 <term>Pre-conditions:</term>
406 <para><command>t</command> must inhabit an inductive type and
407 <command>th</command> must be an elimination principle for that
408 inductive type. If <command>th</command> is omitted the appropriate
409 standard elimination principle is chosen.</para>
415 <para>It proceeds by cases on the values of <command>t</command>,
416 according to the elimination principle <command>th</command>.
421 <term>New sequents to prove:</term>
423 <para>It opens one new sequent for each case. The names of
424 the new hypotheses are picked by <command>hyps</command>, if
425 provided. If hyps specifies also a number of hypotheses that
426 is less than the number of new hypotheses for a new sequent,
427 then the exceeding hypothesis will be kept as implications in
428 the conclusion of the sequent.</para>
434 <sect1 id="tac_elimType">
435 <title><emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</title>
436 <titleabbrev>elimType</titleabbrev>
437 <para><userinput>elimType T using th hyps</userinput></para>
441 <term>Pre-conditions:</term>
443 <para><command>T</command> must be an inductive type.</para>
449 <para>TODO (severely bugged now).</para>
453 <term>New sequents to prove:</term>
461 <sect1 id="tac_exact">
462 <title><emphasis role="bold">exact</emphasis> &sterm;</title>
463 <titleabbrev>exact</titleabbrev>
464 <para><userinput>exact p</userinput></para>
468 <term>Pre-conditions:</term>
470 <para>The type of <command>p</command> must be convertible
471 with the conclusion of the current sequent.</para>
477 <para>It closes the current sequent using <command>p</command>.</para>
481 <term>New sequents to prove:</term>
489 <sect1 id="tac_exists">
490 <title><emphasis role="bold">exists</emphasis></title>
491 <titleabbrev>exists</titleabbrev>
492 <para><userinput>exists </userinput></para>
496 <term>Pre-conditions:</term>
498 <para>The conclusion of the current sequent must be
499 an inductive type or the application of an inductive type
500 with at least one constructor.</para>
506 <para>Equivalent to <command>constructor 1</command>.</para>
510 <term>New sequents to prove:</term>
512 <para>It opens a new sequent for each premise of the first
513 constructor of the inductive type that is the conclusion of the
514 current sequent. For more details, see the <command>constructor</command> tactic.</para>
520 <sect1 id="tac_fail">
521 <title><emphasis role="bold">fail</emphasis></title>
522 <titleabbrev>fail</titleabbrev>
523 <para><userinput>fail</userinput></para>
527 <term>Pre-conditions:</term>
535 <para>This tactic always fail.</para>
539 <term>New sequents to prove:</term>
547 <sect1 id="tac_fold">
548 <title><emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern;</title>
549 <titleabbrev>fold</titleabbrev>
550 <para><userinput>fold red t patt</userinput></para>
554 <term>Pre-conditions:</term>
556 <para>The pattern must not specify the wanted term.</para>
562 <para>First of all it locates all the subterms matched by
563 <command>patt</command>. In the context of each matched subterm
564 it disambiguates the term <command>t</command> and reduces it
565 to its <command>red</command> normal form; then it replaces with
566 <command>t</command> every occurrence of the normal form in the
567 matched subterm.</para>
571 <term>New sequents to prove:</term>
579 <sect1 id="tac_fourier">
580 <title><emphasis role="bold">fourier</emphasis></title>
581 <titleabbrev>fourier</titleabbrev>
582 <para><userinput>fourier </userinput></para>
586 <term>Pre-conditions:</term>
588 <para>The conclusion of the current sequent must be a linear
589 inequation over real numbers taken from standard library of
590 Coq. Moreover the inequations in the hypotheses must imply the
591 inequation in the conclusion of the current sequent.</para>
597 <para>It closes the current sequent by applying the Fourier method.</para>
601 <term>New sequents to prove:</term>
610 <title><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</title>
611 <titleabbrev>fwd</titleabbrev>
612 <para><userinput>fwd ...TODO</userinput></para>
616 <term>Pre-conditions:</term>
628 <term>New sequents to prove:</term>
636 <sect1 id="tac_generalize">
637 <title><emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;]</title>
638 <titleabbrev>generalize</titleabbrev>
639 <para><userinput>generalize patt as H</userinput></para>
643 <term>Pre-conditions:</term>
645 <para>All the terms matched by <command>patt</command> must be
646 convertible and close in the context of the current sequent.</para>
652 <para>It closes the current sequent by applying a stronger
653 lemma that is proved using the new generated sequent.</para>
657 <term>New sequents to prove:</term>
659 <para>It opens a new sequent where the current sequent conclusion
660 <command>G</command> is generalized to
661 <command>∀x.G{x/t}</command> where <command>{x/t}</command>
662 is a notation for the replacement with <command>x</command> of all
663 the occurrences of the term <command>t</command> matched by
664 <command>patt</command>. If <command>patt</command> matches no
665 subterm then <command>t</command> is defined as the
666 <command>wanted</command> part of the pattern.</para>
673 <title><emphasis role="bold">id</emphasis></title>
674 <titleabbrev>id</titleabbrev>
675 <para><userinput>id </userinput></para>
679 <term>Pre-conditions:</term>
687 <para>This identity tactic does nothing without failing.</para>
691 <term>New sequents to prove:</term>
699 <sect1 id="tac_injection">
700 <title><emphasis role="bold">injection</emphasis> &sterm;</title>
701 <titleabbrev><emphasis role="bold">injection</emphasis></titleabbrev>
702 <para><userinput>injection p</userinput></para>
706 <term>Pre-conditions:</term>
708 <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
709 <command>K</command> takes no arguments.</para>
715 <para>It derives new hypotheses by injectivity of
716 <command>K</command>.</para>
720 <term>New sequents to prove:</term>
722 <para>The new sequent to prove is equal to the current sequent
723 with the additional hypotheses
724 <command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
730 <sect1 id="tac_intro">
731 <title><emphasis role="bold">intro</emphasis> [&id;]</title>
732 <titleabbrev>intro</titleabbrev>
733 <para><userinput>intro H</userinput></para>
737 <term>Pre-conditions:</term>
739 <para>The conclusion of the sequent to prove must be an implication
740 or a universal quantification.</para>
746 <para>It applies the right introduction rule for implication,
747 closing the current sequent.</para>
751 <term>New sequents to prove:</term>
753 <para>It opens a new sequent to prove adding to the hypothesis
754 the antecedent of the implication and setting the conclusion
755 to the consequent of the implicaiton. The name of the new
756 hypothesis is <command>H</command> if provided; otherwise it
757 is automatically generated.</para>
763 <sect1 id="tac_intros">
764 <title><emphasis role="bold">intros</emphasis> &intros-spec;</title>
765 <titleabbrev>intros</titleabbrev>
766 <para><userinput>intros hyps</userinput></para>
770 <term>Pre-conditions:</term>
772 <para>If <command>hyps</command> specifies a number of hypotheses
773 to introduce, then the conclusion of the current sequent must
774 be formed by at least that number of imbricated implications
775 or universal quantifications.</para>
781 <para>It applies several times the right introduction rule for
782 implication, closing the current sequent.</para>
786 <term>New sequents to prove:</term>
788 <para>It opens a new sequent to prove adding a number of new
789 hypotheses equal to the number of new hypotheses requested.
790 If the user does not request a precise number of new hypotheses,
791 it adds as many hypotheses as possible.
792 The name of each new hypothesis is either popped from the
793 user provided list of names, or it is automatically generated when
794 the list is (or becomes) empty.</para>
800 <sect1 id="tac_inversion">
801 <title><emphasis role="bold">inversion</emphasis> &sterm;</title>
802 <titleabbrev>inversion</titleabbrev>
803 <para><userinput>inversion t</userinput></para>
807 <term>Pre-conditions:</term>
809 <para>The type of the term <command>t</command> must be an inductive
810 type or the application of an inductive type.</para>
816 <para>It proceeds by cases on <command>t</command> paying attention
817 to the constraints imposed by the actual "right arguments"
818 of the inductive type.</para>
822 <term>New sequents to prove:</term>
824 <para>It opens one new sequent to prove for each case in the
825 definition of the type of <command>t</command>. With respect to
826 a simple elimination, each new sequent has additional hypotheses
827 that states the equalities of the "right parameters"
828 of the inductive type with terms originally present in the
829 sequent to prove.</para>
835 <sect1 id="tac_lapply">
836 <title><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">using</emphasis> &id;]</title>
837 <titleabbrev>lapply</titleabbrev>
838 <para><userinput>lapply ???</userinput></para>
842 <term>Pre-conditions:</term>
854 <term>New sequents to prove:</term>
862 <sect1 id="tac_left">
863 <title><emphasis role="bold">left</emphasis></title>
864 <titleabbrev>left</titleabbrev>
865 <para><userinput>left </userinput></para>
869 <term>Pre-conditions:</term>
871 <para>The conclusion of the current sequent must be
872 an inductive type or the application of an inductive type
873 with at least one constructor.</para>
879 <para>Equivalent to <command>constructor 1</command>.</para>
883 <term>New sequents to prove:</term>
885 <para>It opens a new sequent for each premise of the first
886 constructor of the inductive type that is the conclusion of the
887 current sequent. For more details, see the <command>constructor</command> tactic.</para>
893 <sect1 id="tac_letin">
894 <title><emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm;</title>
895 <titleabbrev>letin</titleabbrev>
896 <para><userinput>letin x ≝ t</userinput></para>
900 <term>Pre-conditions:</term>
908 <para>It adds to the context of the current sequent to prove a new
909 definition <command>x ≝ t</command>.</para>
913 <term>New sequents to prove:</term>
921 <sect1 id="tac_normalize">
922 <title><emphasis role="bold">normalize</emphasis> &pattern;</title>
923 <titleabbrev>normalize</titleabbrev>
924 <para><userinput>normalize patt</userinput></para>
928 <term>Pre-conditions:</term>
936 <para>It replaces all the terms matched by <command>patt</command>
937 with their βδιζ-normal form.</para>
941 <term>New sequents to prove:</term>
949 <sect1 id="tac_paramodulation">
950 <title><emphasis role="bold">paramodulation</emphasis> &pattern;</title>
951 <titleabbrev>paramodulation</titleabbrev>
952 <para><userinput>paramodulation patt</userinput></para>
956 <term>Pre-conditions:</term>
968 <term>New sequents to prove:</term>
976 <sect1 id="tac_reduce">
977 <title><emphasis role="bold">reduce</emphasis> &pattern;</title>
978 <titleabbrev>reduce</titleabbrev>
979 <para><userinput>reduce patt</userinput></para>
983 <term>Pre-conditions:</term>
991 <para>It replaces all the terms matched by <command>patt</command>
992 with their βδιζ-normal form.</para>
996 <term>New sequents to prove:</term>
1004 <sect1 id="tac_reflexivity">
1005 <title><emphasis role="bold">reflexivity</emphasis></title>
1006 <titleabbrev>reflexivity</titleabbrev>
1007 <para><userinput>reflexivity </userinput></para>
1011 <term>Pre-conditions:</term>
1013 <para>The conclusion of the current sequent must be
1014 <command>t=t</command> for some term <command>t</command></para>
1018 <term>Action:</term>
1020 <para>It closes the current sequent by reflexivity
1025 <term>New sequents to prove:</term>
1033 <sect1 id="tac_replace">
1034 <title><emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</title>
1035 <titleabbrev>change</titleabbrev>
1036 <para><userinput>change patt with t</userinput></para>
1040 <term>Pre-conditions:</term>
1046 <term>Action:</term>
1048 <para>It replaces the subterms of the current sequent matched by
1049 <command>patt</command> with the new term <command>t</command>.
1050 For each subterm matched by the pattern, <command>t</command> is
1051 disambiguated in the context of the subterm.</para>
1055 <term>New sequents to prove:</term>
1057 <para>For each matched term <command>t'</command> it opens
1058 a new sequent to prove whose conclusion is
1059 <command>t'=t</command>.</para>
1065 <sect1 id="tac_rewrite">
1066 <title><emphasis role="bold">rewrite</emphasis> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] &sterm; &pattern;</title>
1067 <titleabbrev>rewrite</titleabbrev>
1068 <para><userinput>rewrite dir p patt</userinput></para>
1072 <term>Pre-conditions:</term>
1074 <para><command>p</command> must be the proof of an equality,
1075 possibly under some hypotheses.</para>
1079 <term>Action:</term>
1081 <para>It looks in every term matched by <command>patt</command>
1082 for all the occurrences of the
1083 left hand side of the equality that <command>p</command> proves
1084 (resp. the right hand side if <command>dir</command> is
1085 <command><</command>). Every occurence found is replaced with
1086 the opposite side of the equality.</para>
1090 <term>New sequents to prove:</term>
1092 <para>It opens one new sequent for each hypothesis of the
1093 equality proved by <command>p</command> that is not closed
1094 by unification.</para>
1100 <sect1 id="tac_right">
1101 <title><emphasis role="bold">right</emphasis></title>
1102 <titleabbrev>right</titleabbrev>
1103 <para><userinput>right </userinput></para>
1107 <term>Pre-conditions:</term>
1109 <para>The conclusion of the current sequent must be
1110 an inductive type or the application of an inductive type with
1111 at least two constructors.</para>
1115 <term>Action:</term>
1117 <para>Equivalent to <command>constructor 2</command>.</para>
1121 <term>New sequents to prove:</term>
1123 <para>It opens a new sequent for each premise of the second
1124 constructor of the inductive type that is the conclusion of the
1125 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1131 <sect1 id="tac_ring">
1132 <title><emphasis role="bold">ring</emphasis></title>
1133 <titleabbrev>ring</titleabbrev>
1134 <para><userinput>ring </userinput></para>
1138 <term>Pre-conditions:</term>
1140 <para>The conclusion of the current sequent must be an
1141 equality over Coq's real numbers that can be proved using
1142 the ring properties of the real numbers only.</para>
1146 <term>Action:</term>
1148 <para>It closes the current sequent veryfying the equality by
1149 means of computation (i.e. this is a reflexive tactic, implemented
1150 exploiting the "two level reasoning" technique).</para>
1154 <term>New sequents to prove:</term>
1162 <sect1 id="tac_simplify">
1163 <title><emphasis role="bold">simplify</emphasis> &pattern;</title>
1164 <titleabbrev>simplify</titleabbrev>
1165 <para><userinput>simplify patt</userinput></para>
1169 <term>Pre-conditions:</term>
1175 <term>Action:</term>
1177 <para>It replaces all the terms matched by <command>patt</command>
1178 with other convertible terms that are supposed to be simpler.</para>
1182 <term>New sequents to prove:</term>
1190 <sect1 id="tac_split">
1191 <title><emphasis role="bold">split</emphasis></title>
1192 <titleabbrev>split</titleabbrev>
1193 <para><userinput>split </userinput></para>
1197 <term>Pre-conditions:</term>
1199 <para>The conclusion of the current sequent must be
1200 an inductive type or the application of an inductive type with
1201 at least one constructor.</para>
1205 <term>Action:</term>
1207 <para>Equivalent to <command>constructor 1</command>.</para>
1211 <term>New sequents to prove:</term>
1213 <para>It opens a new sequent for each premise of the first
1214 constructor of the inductive type that is the conclusion of the
1215 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1221 <sect1 id="tac_symmetry">
1222 <title><emphasis role="bold">symmetry</emphasis></title>
1223 <titleabbrev>symmetry</titleabbrev>
1224 <para>The tactic <command>symmetry</command> </para>
1225 <para><userinput>symmetry </userinput></para>
1229 <term>Pre-conditions:</term>
1231 <para>The conclusion of the current proof must be an equality.</para>
1235 <term>Action:</term>
1237 <para>It swaps the two sides of the equalityusing the symmetric
1242 <term>New sequents to prove:</term>
1250 <sect1 id="tac_transitivity">
1251 <title><emphasis role="bold">transitivity</emphasis> &sterm;</title>
1252 <titleabbrev>transitivity</titleabbrev>
1253 <para><userinput>transitivity t</userinput></para>
1257 <term>Pre-conditions:</term>
1259 <para>The conclusion of the current proof must be an equality.</para>
1263 <term>Action:</term>
1265 <para>It closes the current sequent by transitivity of the equality.</para>
1269 <term>New sequents to prove:</term>
1271 <para>It opens two new sequents <command>l=t</command> and
1272 <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
1273 the current sequent to prove.</para>
1279 <sect1 id="tac_unfold">
1280 <title><emphasis role="bold">unfold</emphasis> [&sterm;] &pattern;</title>
1281 <titleabbrev>unfold</titleabbrev>
1282 <para><userinput>unfold t patt</userinput></para>
1286 <term>Pre-conditions:</term>
1292 <term>Action:</term>
1294 <para>It finds all the occurrences of <command>t</command>
1295 (possibly applied to arguments) in the subterms matched by
1296 <command>patt</command>. Then it δ-expands each occurrence,
1297 also performing β-reduction of the obtained term. If
1298 <command>t</command> is omitted it defaults to each
1299 subterm matched by <command>patt</command>.</para>
1303 <term>New sequents to prove:</term>
1311 <sect1 id="tac_whd">
1312 <title><emphasis role="bold">whd</emphasis> &pattern;</title>
1313 <titleabbrev>whd</titleabbrev>
1314 <para><userinput>whd patt</userinput></para>
1318 <term>Pre-conditions:</term>
1324 <term>Action:</term>
1326 <para>It replaces all the terms matched by <command>patt</command>
1327 with their βδιζ-weak-head normal form.</para>
1331 <term>New sequents to prove:</term>