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_applyS">
91 <titleabbrev>applyS</titleabbrev>
92 <para><userinput>applyS t auto_params</userinput></para>
95 <varlistentry role="tactic.synopsis">
96 <term>Synopsis:</term>
98 <para><emphasis role="bold">applyS</emphasis> &sterm; &autoparams;</para>
102 <term>Pre-conditions:</term>
104 <para><command>t</command> must have type
105 <command>T<subscript>1</subscript> → ... →
106 T<subscript>n</subscript> → G</command>.</para>
112 <para><command>applyS</command> is useful when
113 <command>apply</command> fails because the current goal
114 and the conclusion of the applied theorems are extensionally
115 equivalent up to instantiation of metavariables, but cannot
116 be unified. E.g. the goal is <command>P(n*O+m)</command> and
117 the theorem to be applied proves <command>∀m.P(m+O)</command>.
120 It tries to automatically rewrite the current goal using
121 <link linkend="tac_auto">auto paramodulation</link>
122 to make it unifiable with <command>G</command>.
123 Then it closes the current sequent by applying
124 <command>t</command> to <command>n</command>
125 implicit arguments (that become new sequents).
126 The <command>auto_params</command> parameters are passed
127 directly to <command>auto paramodulation</command>.
132 <term>New sequents to prove:</term>
134 <para>It opens a new sequent for each premise
135 <command>T<subscript>i</subscript></command> that is not
136 instantiated by unification. <command>T<subscript>i</subscript></command> is
137 the conclusion of the <command>i</command>-th new sequent to
144 <sect1 id="tac_assumption">
145 <title>assumption</title>
146 <titleabbrev>assumption</titleabbrev>
147 <para><userinput>assumption </userinput></para>
150 <varlistentry role="tactic.synopsis">
151 <term>Synopsis:</term>
153 <para><emphasis role="bold">assumption</emphasis></para>
157 <term>Pre-conditions:</term>
159 <para>There must exist an hypothesis whose type can be unified with
160 the conclusion of the current sequent.</para>
166 <para>It closes the current sequent exploiting an hypothesis.</para>
170 <term>New sequents to prove:</term>
178 <sect1 id="tac_auto">
180 <titleabbrev>auto</titleabbrev>
181 <para><userinput>auto params</userinput></para>
184 <varlistentry role="tactic.synopsis">
185 <term>Synopsis:</term>
187 <para><emphasis role="bold">auto</emphasis> &autoparams;</para>
191 <term>Pre-conditions:</term>
193 <para>None, but the tactic may fail finding a proof if every
194 proof is in the search space that is pruned away. Pruning is
195 controlled by the optional <command>params</command>.
196 Moreover, only lemmas whose type signature is a subset of the
197 signature of the current sequent are considered. The signature of
198 a sequent is ...&TODO;</para>
204 <para>It closes the current sequent by repeated application of
205 rewriting steps (unless <command>paramodulation</command> is
206 omitted), hypothesis and lemmas in the library.</para>
210 <term>New sequents to prove:</term>
218 <sect1 id="tac_cases">
220 <titleabbrev>cases</titleabbrev>
226 <varlistentry role="tactic.synopsis">
227 <term>Synopsis:</term>
230 <emphasis role="bold">cases</emphasis>
231 &term; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
236 <term>Pre-conditions:</term>
239 <command>t</command> must inhabit an inductive type
247 It proceed by cases on <command>t</command>. The new generated
248 hypothesis in each branch are named according to
249 <command>hyps</command>.
254 <term>New sequents to prove:</term>
256 <para>One new sequent for each constructor of the type of
257 <command>t</command>. Each sequent has a new hypothesis for
258 each argument of the constructor.</para>
264 <sect1 id="tac_clear">
266 <titleabbrev>clear</titleabbrev>
268 clear H<subscript>1</subscript> ... H<subscript>m</subscript>
272 <varlistentry role="tactic.synopsis">
273 <term>Synopsis:</term>
276 <emphasis role="bold">clear</emphasis>
282 <term>Pre-conditions:</term>
286 H<subscript>1</subscript> ... H<subscript>m</subscript>
287 </command> must be hypotheses of the
288 current sequent to prove.
296 It hides the hypotheses
298 H<subscript>1</subscript> ... H<subscript>m</subscript>
299 </command> from the current sequent.
304 <term>New sequents to prove:</term>
312 <sect1 id="tac_clearbody">
313 <title>clearbody</title>
314 <titleabbrev>clearbody</titleabbrev>
315 <para><userinput>clearbody H</userinput></para>
318 <varlistentry role="tactic.synopsis">
319 <term>Synopsis:</term>
321 <para><emphasis role="bold">clearbody</emphasis> &id;</para>
325 <term>Pre-conditions:</term>
327 <para><command>H</command> must be an hypothesis of the
328 current sequent to prove.</para>
334 <para>It hides the definiens of a definition in the current
335 sequent context. Thus the definition becomes an hypothesis.</para>
339 <term>New sequents to prove:</term>
347 <sect1 id="tac_compose">
348 <title>compose</title>
349 <titleabbrev>compose</titleabbrev>
350 <para><userinput>compose n t1 with t2 hyps</userinput></para>
353 <varlistentry role="tactic.synopsis">
354 <term>Synopsis:</term>
356 <para><emphasis role="bold">compose</emphasis> [&nat;] &sterm; [<emphasis role="bold">with</emphasis> &sterm;] [&intros-spec;]</para>
360 <term>Pre-conditions:</term>
368 <para>Composes t1 with t2 in every possible way
369 <command>n</command> times introducing generated terms
370 as if <command>intros hyps</command> was issued.</para>
371 <para>If <command>t1:∀x:A.B[x]</command> and
372 <command>t2:∀x,y:A.B[x]→B[y]→C[x,y]</command> it generates:
375 <command>λx,y:A.t2 x y (t1 x) : ∀x,y:A.B[y]→C[x,y]</command>
378 <command>λx,y:A.λH:B[x].t2 x y H (t1 y) : ∀x,y:A.B[x]→C[x,y]
383 <para>If <command>t2</command> is omitted it composes
384 <command>t1</command>
385 with every hypothesis that can be introduced.
386 <command>n</command> iterates the process.</para>
390 <term>New sequents to prove:</term>
392 <para>The same, but with more hypothesis eventually introduced
393 by the &intros-spec;.</para>
399 <sect1 id="tac_change">
400 <title>change</title>
401 <titleabbrev>change</titleabbrev>
402 <para><userinput>change patt with t</userinput></para>
405 <varlistentry role="tactic.synopsis">
406 <term>Synopsis:</term>
408 <para><emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
412 <term>Pre-conditions:</term>
414 <para>Each subterm matched by the pattern must be convertible
415 with the term <command>t</command> disambiguated in the context
416 of the matched subterm.</para>
422 <para>It replaces the subterms of the current sequent matched by
423 <command>patt</command> with the new term <command>t</command>.
424 For each subterm matched by the pattern, <command>t</command> is
425 disambiguated in the context of the subterm.</para>
429 <term>New sequents to prove:</term>
437 <sect1 id="tac_constructor">
438 <title>constructor</title>
439 <titleabbrev>constructor</titleabbrev>
440 <para><userinput>constructor n</userinput></para>
443 <varlistentry role="tactic.synopsis">
444 <term>Synopsis:</term>
446 <para><emphasis role="bold">constructor</emphasis> &nat;</para>
450 <term>Pre-conditions:</term>
452 <para>The conclusion of the current sequent must be
453 an inductive type or the application of an inductive type with
454 at least <command>n</command> constructors.</para>
460 <para>It applies the <command>n</command>-th constructor of the
461 inductive type of the conclusion of the current sequent.</para>
465 <term>New sequents to prove:</term>
467 <para>It opens a new sequent for each premise of the constructor
468 that can not be inferred by unification. For more details,
469 see the <command>apply</command> tactic.</para>
475 <sect1 id="tac_contradiction">
476 <title>contradiction</title>
477 <titleabbrev>contradiction</titleabbrev>
478 <para><userinput>contradiction </userinput></para>
481 <varlistentry role="tactic.synopsis">
482 <term>Synopsis:</term>
484 <para><emphasis role="bold">contradiction</emphasis></para>
488 <term>Pre-conditions:</term>
490 <para>There must be in the current context an hypothesis of type
491 <command>False</command>.</para>
497 <para>It closes the current sequent by applying an hypothesis of
498 type <command>False</command>.</para>
502 <term>New sequents to prove:</term>
512 <titleabbrev>cut</titleabbrev>
513 <para><userinput>cut P as H</userinput></para>
516 <varlistentry role="tactic.synopsis">
517 <term>Synopsis:</term>
519 <para><emphasis role="bold">cut</emphasis> &sterm; [<emphasis role="bold">as</emphasis> &id;]</para>
523 <term>Pre-conditions:</term>
525 <para><command>P</command> must have type <command>Prop</command>.</para>
531 <para>It closes the current sequent.</para>
535 <term>New sequents to prove:</term>
537 <para>It opens two new sequents. The first one has an extra
538 hypothesis <command>H:P</command>. If <command>H</command> is
539 omitted, the name of the hypothesis is automatically generated.
540 The second sequent has conclusion <command>P</command> and
541 hypotheses the hypotheses of the current sequent to prove.</para>
547 <sect1 id="tac_decompose">
548 <title>decompose</title>
549 <titleabbrev>decompose</titleabbrev>
551 decompose as H<subscript>1</subscript> ... H<subscript>m</subscript>
555 <varlistentry role="tactic.synopsis">
556 <term>Synopsis:</term>
559 <emphasis role="bold">decompose</emphasis>
560 [<emphasis role="bold">as</emphasis> &id;…]
565 <term>Pre-conditions:</term>
574 For each each premise <command>H</command> of type
575 <command>T</command> in the current context where
576 <command>T</command> is a non-recursive inductive type without
577 right parameters and of sort Prop or CProp, the tactic runs
579 elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
580 </command>, clears <command>H</command> and runs itself
581 recursively on each new premise introduced by
582 <command>elim</command> in the opened sequents.
587 <term>New sequents to prove:</term>
590 The ones generated by all the <command>elim</command> tactics run.
597 <sect1 id="tac_demodulate">
598 <title>demodulate</title>
599 <titleabbrev>demodulate</titleabbrev>
600 <para><userinput>demodulate</userinput></para>
603 <varlistentry role="tactic.synopsis">
604 <term>Synopsis:</term>
606 <para><emphasis role="bold">demodulate</emphasis></para>
610 <term>Pre-conditions:</term>
622 <term>New sequents to prove:</term>
630 <sect1 id="tac_destruct">
631 <title>destruct</title>
632 <titleabbrev>destruct</titleabbrev>
633 <para><userinput>destruct p</userinput></para>
636 <varlistentry role="tactic.synopsis">
637 <term>Synopsis:</term>
639 <para><emphasis role="bold">destruct</emphasis> &sterm;</para>
643 <term>Pre-conditions:</term>
645 <para><command>p</command> must have type <command>E<subscript>1</subscript> = E<subscript>2</subscript></command> where the two sides of the equality are possibly applied constructors of an inductive type.</para>
651 <para>The tactic recursively compare the two sides of the equality
652 looking for different constructors in corresponding position.
653 If two of them are found, the tactic closes the current sequent
654 by proving the absurdity of <command>p</command>. Otherwise
655 it adds a new hypothesis for each leaf of the formula that
656 states the equality of the subformulae in the corresponding
657 positions on the two sides of the equality.
662 <term>New sequents to prove:</term>
670 <sect1 id="tac_elim">
672 <titleabbrev>elim</titleabbrev>
673 <para><userinput>elim t using th hyps</userinput></para>
676 <varlistentry role="tactic.synopsis">
677 <term>Synopsis:</term>
679 <para><emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
683 <term>Pre-conditions:</term>
685 <para><command>t</command> must inhabit an inductive type and
686 <command>th</command> must be an elimination principle for that
687 inductive type. If <command>th</command> is omitted the appropriate
688 standard elimination principle is chosen.</para>
694 <para>It proceeds by cases on the values of <command>t</command>,
695 according to the elimination principle <command>th</command>.
700 <term>New sequents to prove:</term>
702 <para>It opens one new sequent for each case. The names of
703 the new hypotheses are picked by <command>hyps</command>, if
704 provided. If hyps specifies also a number of hypotheses that
705 is less than the number of new hypotheses for a new sequent,
706 then the exceeding hypothesis will be kept as implications in
707 the conclusion of the sequent.</para>
713 <sect1 id="tac_elimType">
714 <title>elimType</title>
715 <titleabbrev>elimType</titleabbrev>
716 <para><userinput>elimType T using th hyps</userinput></para>
719 <varlistentry role="tactic.synopsis">
720 <term>Synopsis:</term>
722 <para><emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
726 <term>Pre-conditions:</term>
728 <para><command>T</command> must be an inductive type.</para>
734 <para>TODO (severely bugged now).</para>
738 <term>New sequents to prove:</term>
746 <sect1 id="tac_exact">
748 <titleabbrev>exact</titleabbrev>
749 <para><userinput>exact p</userinput></para>
752 <varlistentry role="tactic.synopsis">
753 <term>Synopsis:</term>
755 <para><emphasis role="bold">exact</emphasis> &sterm;</para>
759 <term>Pre-conditions:</term>
761 <para>The type of <command>p</command> must be convertible
762 with the conclusion of the current sequent.</para>
768 <para>It closes the current sequent using <command>p</command>.</para>
772 <term>New sequents to prove:</term>
780 <sect1 id="tac_exists">
781 <title>exists</title>
782 <titleabbrev>exists</titleabbrev>
783 <para><userinput>exists </userinput></para>
786 <varlistentry role="tactic.synopsis">
787 <term>Synopsis:</term>
789 <para><emphasis role="bold">exists</emphasis></para>
793 <term>Pre-conditions:</term>
795 <para>The conclusion of the current sequent must be
796 an inductive type or the application of an inductive type
797 with at least one constructor.</para>
803 <para>Equivalent to <command>constructor 1</command>.</para>
807 <term>New sequents to prove:</term>
809 <para>It opens a new sequent for each premise of the first
810 constructor of the inductive type that is the conclusion of the
811 current sequent. For more details, see the <command>constructor</command> tactic.</para>
817 <sect1 id="tac_fail">
819 <titleabbrev>fail</titleabbrev>
820 <para><userinput>fail</userinput></para>
823 <varlistentry role="tactic.synopsis">
824 <term>Synopsis:</term>
826 <para><emphasis role="bold">fail</emphasis></para>
830 <term>Pre-conditions:</term>
838 <para>This tactic always fail.</para>
842 <term>New sequents to prove:</term>
850 <sect1 id="tac_fold">
852 <titleabbrev>fold</titleabbrev>
853 <para><userinput>fold red t patt</userinput></para>
856 <varlistentry role="tactic.synopsis">
857 <term>Synopsis:</term>
859 <para><emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern;</para>
863 <term>Pre-conditions:</term>
865 <para>The pattern must not specify the wanted term.</para>
871 <para>First of all it locates all the subterms matched by
872 <command>patt</command>. In the context of each matched subterm
873 it disambiguates the term <command>t</command> and reduces it
874 to its <command>red</command> normal form; then it replaces with
875 <command>t</command> every occurrence of the normal form in the
876 matched subterm.</para>
880 <term>New sequents to prove:</term>
888 <sect1 id="tac_fourier">
889 <title>fourier</title>
890 <titleabbrev>fourier</titleabbrev>
891 <para><userinput>fourier </userinput></para>
894 <varlistentry role="tactic.synopsis">
895 <term>Synopsis:</term>
897 <para><emphasis role="bold">fourier</emphasis></para>
901 <term>Pre-conditions:</term>
903 <para>The conclusion of the current sequent must be a linear
904 inequation over real numbers taken from standard library of
905 Coq. Moreover the inequations in the hypotheses must imply the
906 inequation in the conclusion of the current sequent.</para>
912 <para>It closes the current sequent by applying the Fourier method.</para>
916 <term>New sequents to prove:</term>
926 <titleabbrev>fwd</titleabbrev>
927 <para><userinput>fwd H as H<subscript>0</subscript> ... H<subscript>n</subscript></userinput></para>
930 <varlistentry role="tactic.synopsis">
931 <term>Synopsis:</term>
933 <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">as</emphasis> &id; [&id;]…]</para>
937 <term>Pre-conditions:</term>
940 The type of <command>H</command> must be the premise of a
941 forward simplification theorem.
949 This tactic is under development.
950 It simplifies the current context by removing
951 <command>H</command> using the following methods:
952 forward application (by <command>lapply</command>) of a suitable
953 simplification theorem, chosen automatically, of which the type
954 of <command>H</command> is a premise,
955 decomposition (by <command>decompose</command>),
956 rewriting (by <command>rewrite</command>).
957 <command>H<subscript>0</subscript> ... H<subscript>n</subscript></command>
958 are passed to the tactics <command>fwd</command> invokes, as
959 names for the premise they introduce.
964 <term>New sequents to prove:</term>
967 The ones opened by the tactics <command>fwd</command> invokes.
974 <sect1 id="tac_generalize">
975 <title>generalize</title>
976 <titleabbrev>generalize</titleabbrev>
977 <para><userinput>generalize patt as H</userinput></para>
980 <varlistentry role="tactic.synopsis">
981 <term>Synopsis:</term>
983 <para><emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;]</para>
987 <term>Pre-conditions:</term>
989 <para>All the terms matched by <command>patt</command> must be
990 convertible and close in the context of the current sequent.</para>
996 <para>It closes the current sequent by applying a stronger
997 lemma that is proved using the new generated sequent.</para>
1001 <term>New sequents to prove:</term>
1003 <para>It opens a new sequent where the current sequent conclusion
1004 <command>G</command> is generalized to
1005 <command>∀x.G{x/t}</command> where <command>{x/t}</command>
1006 is a notation for the replacement with <command>x</command> of all
1007 the occurrences of the term <command>t</command> matched by
1008 <command>patt</command>. If <command>patt</command> matches no
1009 subterm then <command>t</command> is defined as the
1010 <command>wanted</command> part of the pattern.</para>
1018 <titleabbrev>id</titleabbrev>
1019 <para><userinput>id </userinput></para>
1022 <varlistentry role="tactic.synopsis">
1023 <term>Synopsis:</term>
1025 <para><emphasis role="bold">id</emphasis></para>
1029 <term>Pre-conditions:</term>
1035 <term>Action:</term>
1037 <para>This identity tactic does nothing without failing.</para>
1041 <term>New sequents to prove:</term>
1049 <sect1 id="tac_intro">
1050 <title>intro</title>
1051 <titleabbrev>intro</titleabbrev>
1052 <para><userinput>intro H</userinput></para>
1055 <varlistentry role="tactic.synopsis">
1056 <term>Synopsis:</term>
1058 <para><emphasis role="bold">intro</emphasis> [&id;]</para>
1062 <term>Pre-conditions:</term>
1064 <para>The conclusion of the sequent to prove must be an implication
1065 or a universal quantification.</para>
1069 <term>Action:</term>
1071 <para>It applies the right introduction rule for implication,
1072 closing the current sequent.</para>
1076 <term>New sequents to prove:</term>
1078 <para>It opens a new sequent to prove adding to the hypothesis
1079 the antecedent of the implication and setting the conclusion
1080 to the consequent of the implicaiton. The name of the new
1081 hypothesis is <command>H</command> if provided; otherwise it
1082 is automatically generated.</para>
1088 <sect1 id="tac_intros">
1089 <title>intros</title>
1090 <titleabbrev>intros</titleabbrev>
1091 <para><userinput>intros hyps</userinput></para>
1094 <varlistentry role="tactic.synopsis">
1095 <term>Synopsis:</term>
1097 <para><emphasis role="bold">intros</emphasis> &intros-spec;</para>
1101 <term>Pre-conditions:</term>
1103 <para>If <command>hyps</command> specifies a number of hypotheses
1104 to introduce, then the conclusion of the current sequent must
1105 be formed by at least that number of imbricated implications
1106 or universal quantifications.</para>
1110 <term>Action:</term>
1112 <para>It applies several times the right introduction rule for
1113 implication, closing the current sequent.</para>
1117 <term>New sequents to prove:</term>
1119 <para>It opens a new sequent to prove adding a number of new
1120 hypotheses equal to the number of new hypotheses requested.
1121 If the user does not request a precise number of new hypotheses,
1122 it adds as many hypotheses as possible.
1123 The name of each new hypothesis is either popped from the
1124 user provided list of names, or it is automatically generated when
1125 the list is (or becomes) empty.</para>
1131 <sect1 id="tac_inversion">
1132 <title>inversion</title>
1133 <titleabbrev>inversion</titleabbrev>
1134 <para><userinput>inversion t</userinput></para>
1137 <varlistentry role="tactic.synopsis">
1138 <term>Synopsis:</term>
1140 <para><emphasis role="bold">inversion</emphasis> &sterm;</para>
1144 <term>Pre-conditions:</term>
1146 <para>The type of the term <command>t</command> must be an inductive
1147 type or the application of an inductive type.</para>
1151 <term>Action:</term>
1153 <para>It proceeds by cases on <command>t</command> paying attention
1154 to the constraints imposed by the actual "right arguments"
1155 of the inductive type.</para>
1159 <term>New sequents to prove:</term>
1161 <para>It opens one new sequent to prove for each case in the
1162 definition of the type of <command>t</command>. With respect to
1163 a simple elimination, each new sequent has additional hypotheses
1164 that states the equalities of the "right parameters"
1165 of the inductive type with terms originally present in the
1166 sequent to prove.</para>
1172 <sect1 id="tac_lapply">
1173 <title>lapply</title>
1174 <titleabbrev>lapply</titleabbrev>
1176 lapply linear depth=d t
1177 to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
1181 <varlistentry role="tactic.synopsis">
1182 <term>Synopsis:</term>
1185 <emphasis role="bold">lapply</emphasis>
1186 [<emphasis role="bold">linear</emphasis>]
1187 [<emphasis role="bold">depth=</emphasis>&nat;]
1189 [<emphasis role="bold">to</emphasis>
1191 [<emphasis role="bold">,</emphasis>&sterm;…]
1193 [<emphasis role="bold">as</emphasis> &id;]
1198 <term>Pre-conditions:</term>
1201 <command>t</command> must have at least <command>d</command>
1202 independent premises and <command>n</command> must not be
1203 greater than <command>d</command>.
1208 <term>Action:</term>
1211 Invokes <command>letin H ≝ (t ? ... ?)</command>
1212 with enough <command>?</command>'s to reach the
1213 <command>d</command>-th independent premise of
1214 <command>t</command>
1215 (<command>d</command> is maximum if unspecified).
1216 Then istantiates (by <command>apply</command>) with
1217 t<subscript>1</subscript>, ..., t<subscript>n</subscript>
1218 the <command>?</command>'s corresponding to the first
1219 <command>n</command> independent premises of
1220 <command>t</command>.
1221 Usually the other <command>?</command>'s preceding the
1222 <command>n</command>-th independent premise of
1223 <command>t</command> are istantiated as a consequence.
1224 If the <command>linear</command> flag is specified and if
1225 <command>t, t<subscript>1</subscript>, ..., t<subscript>n</subscript></command>
1226 are (applications of) premises in the current context, they are
1227 <command>clear</command>ed.
1232 <term>New sequents to prove:</term>
1235 The ones opened by the tactics <command>lapply</command> invokes.
1242 <sect1 id="tac_left">
1244 <titleabbrev>left</titleabbrev>
1245 <para><userinput>left </userinput></para>
1248 <varlistentry role="tactic.synopsis">
1249 <term>Synopsis:</term>
1251 <para><emphasis role="bold">left</emphasis></para>
1255 <term>Pre-conditions:</term>
1257 <para>The conclusion of the current sequent must be
1258 an inductive type or the application of an inductive type
1259 with at least one constructor.</para>
1263 <term>Action:</term>
1265 <para>Equivalent to <command>constructor 1</command>.</para>
1269 <term>New sequents to prove:</term>
1271 <para>It opens a new sequent for each premise of the first
1272 constructor of the inductive type that is the conclusion of the
1273 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1279 <sect1 id="tac_letin">
1280 <title>letin</title>
1281 <titleabbrev>letin</titleabbrev>
1282 <para><userinput>letin x ≝ t</userinput></para>
1285 <varlistentry role="tactic.synopsis">
1286 <term>Synopsis:</term>
1288 <para><emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm;</para>
1292 <term>Pre-conditions:</term>
1298 <term>Action:</term>
1300 <para>It adds to the context of the current sequent to prove a new
1301 definition <command>x ≝ t</command>.</para>
1305 <term>New sequents to prove:</term>
1313 <sect1 id="tac_normalize">
1314 <title>normalize</title>
1315 <titleabbrev>normalize</titleabbrev>
1316 <para><userinput>normalize patt</userinput></para>
1319 <varlistentry role="tactic.synopsis">
1320 <term>Synopsis:</term>
1322 <para><emphasis role="bold">normalize</emphasis> &pattern;</para>
1326 <term>Pre-conditions:</term>
1332 <term>Action:</term>
1334 <para>It replaces all the terms matched by <command>patt</command>
1335 with their βδιζ-normal form.</para>
1339 <term>New sequents to prove:</term>
1347 <sect1 id="tac_reduce">
1348 <title>reduce</title>
1349 <titleabbrev>reduce</titleabbrev>
1350 <para><userinput>reduce patt</userinput></para>
1353 <varlistentry role="tactic.synopsis">
1354 <term>Synopsis:</term>
1356 <para><emphasis role="bold">reduce</emphasis> &pattern;</para>
1360 <term>Pre-conditions:</term>
1366 <term>Action:</term>
1368 <para>It replaces all the terms matched by <command>patt</command>
1369 with their βδιζ-normal form.</para>
1373 <term>New sequents to prove:</term>
1381 <sect1 id="tac_reflexivity">
1382 <title>reflexivity</title>
1383 <titleabbrev>reflexivity</titleabbrev>
1384 <para><userinput>reflexivity </userinput></para>
1387 <varlistentry role="tactic.synopsis">
1388 <term>Synopsis:</term>
1390 <para><emphasis role="bold">reflexivity</emphasis></para>
1394 <term>Pre-conditions:</term>
1396 <para>The conclusion of the current sequent must be
1397 <command>t=t</command> for some term <command>t</command></para>
1401 <term>Action:</term>
1403 <para>It closes the current sequent by reflexivity
1408 <term>New sequents to prove:</term>
1416 <sect1 id="tac_replace">
1417 <title>replace</title>
1418 <titleabbrev>change</titleabbrev>
1419 <para><userinput>change patt with t</userinput></para>
1422 <varlistentry role="tactic.synopsis">
1423 <term>Synopsis:</term>
1425 <para><emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
1429 <term>Pre-conditions:</term>
1435 <term>Action:</term>
1437 <para>It replaces the subterms of the current sequent matched by
1438 <command>patt</command> with the new term <command>t</command>.
1439 For each subterm matched by the pattern, <command>t</command> is
1440 disambiguated in the context of the subterm.</para>
1444 <term>New sequents to prove:</term>
1446 <para>For each matched term <command>t'</command> it opens
1447 a new sequent to prove whose conclusion is
1448 <command>t'=t</command>.</para>
1454 <sect1 id="tac_rewrite">
1455 <title>rewrite</title>
1456 <titleabbrev>rewrite</titleabbrev>
1457 <para><userinput>rewrite dir p patt</userinput></para>
1460 <varlistentry role="tactic.synopsis">
1461 <term>Synopsis:</term>
1463 <para><emphasis role="bold">rewrite</emphasis> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] &sterm; &pattern;</para>
1467 <term>Pre-conditions:</term>
1469 <para><command>p</command> must be the proof of an equality,
1470 possibly under some hypotheses.</para>
1474 <term>Action:</term>
1476 <para>It looks in every term matched by <command>patt</command>
1477 for all the occurrences of the
1478 left hand side of the equality that <command>p</command> proves
1479 (resp. the right hand side if <command>dir</command> is
1480 <command><</command>). Every occurence found is replaced with
1481 the opposite side of the equality.</para>
1485 <term>New sequents to prove:</term>
1487 <para>It opens one new sequent for each hypothesis of the
1488 equality proved by <command>p</command> that is not closed
1489 by unification.</para>
1495 <sect1 id="tac_right">
1496 <title>right</title>
1497 <titleabbrev>right</titleabbrev>
1498 <para><userinput>right </userinput></para>
1501 <varlistentry role="tactic.synopsis">
1502 <term>Synopsis:</term>
1504 <para><emphasis role="bold">right</emphasis></para>
1508 <term>Pre-conditions:</term>
1510 <para>The conclusion of the current sequent must be
1511 an inductive type or the application of an inductive type with
1512 at least two constructors.</para>
1516 <term>Action:</term>
1518 <para>Equivalent to <command>constructor 2</command>.</para>
1522 <term>New sequents to prove:</term>
1524 <para>It opens a new sequent for each premise of the second
1525 constructor of the inductive type that is the conclusion of the
1526 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1532 <sect1 id="tac_ring">
1534 <titleabbrev>ring</titleabbrev>
1535 <para><userinput>ring </userinput></para>
1538 <varlistentry role="tactic.synopsis">
1539 <term>Synopsis:</term>
1541 <para><emphasis role="bold">ring</emphasis></para>
1545 <term>Pre-conditions:</term>
1547 <para>The conclusion of the current sequent must be an
1548 equality over Coq's real numbers that can be proved using
1549 the ring properties of the real numbers only.</para>
1553 <term>Action:</term>
1555 <para>It closes the current sequent veryfying the equality by
1556 means of computation (i.e. this is a reflexive tactic, implemented
1557 exploiting the "two level reasoning" technique).</para>
1561 <term>New sequents to prove:</term>
1569 <sect1 id="tac_simplify">
1570 <title>simplify</title>
1571 <titleabbrev>simplify</titleabbrev>
1572 <para><userinput>simplify patt</userinput></para>
1575 <varlistentry role="tactic.synopsis">
1576 <term>Synopsis:</term>
1578 <para><emphasis role="bold">simplify</emphasis> &pattern;</para>
1582 <term>Pre-conditions:</term>
1588 <term>Action:</term>
1590 <para>It replaces all the terms matched by <command>patt</command>
1591 with other convertible terms that are supposed to be simpler.</para>
1595 <term>New sequents to prove:</term>
1603 <sect1 id="tac_split">
1604 <title>split</title>
1605 <titleabbrev>split</titleabbrev>
1606 <para><userinput>split </userinput></para>
1609 <varlistentry role="tactic.synopsis">
1610 <term>Synopsis:</term>
1612 <para><emphasis role="bold">split</emphasis></para>
1616 <term>Pre-conditions:</term>
1618 <para>The conclusion of the current sequent must be
1619 an inductive type or the application of an inductive type with
1620 at least one constructor.</para>
1624 <term>Action:</term>
1626 <para>Equivalent to <command>constructor 1</command>.</para>
1630 <term>New sequents to prove:</term>
1632 <para>It opens a new sequent for each premise of the first
1633 constructor of the inductive type that is the conclusion of the
1634 current sequent. For more details, see the <command>constructor</command> tactic.</para>
1641 <sect1 id="tac_subst">
1642 <title>subst</title>
1643 <titleabbrev>subst</titleabbrev>
1644 <para><userinput>subst</userinput></para>
1647 <varlistentry role="tactic.synopsis">
1648 <term>Synopsis:</term>
1650 <para><emphasis role="bold">subst</emphasis></para>
1654 <term>Pre-conditions:</term>
1660 <term>Action:</term>
1662 For each premise of the form
1663 <command>H: x = t</command> or <command>H: t = x</command>
1664 where <command>x</command> is a local variable and
1665 <command>t</command> does not depend on <command>x</command>,
1666 the tactic rewrites <command>H</command> wherever
1667 <command>x</command> appears clearing <command>H</command> and
1668 <command>x</command> afterwards.
1672 <term>New sequents to prove:</term>
1674 The one opened by the applied tactics.
1680 <sect1 id="tac_symmetry">
1681 <title>symmetry</title>
1682 <titleabbrev>symmetry</titleabbrev>
1683 <para>The tactic <command>symmetry</command> </para>
1684 <para><userinput>symmetry </userinput></para>
1687 <varlistentry role="tactic.synopsis">
1688 <term>Synopsis:</term>
1690 <para><emphasis role="bold">symmetry</emphasis></para>
1694 <term>Pre-conditions:</term>
1696 <para>The conclusion of the current proof must be an equality.</para>
1700 <term>Action:</term>
1702 <para>It swaps the two sides of the equalityusing the symmetric
1707 <term>New sequents to prove:</term>
1715 <sect1 id="tac_transitivity">
1716 <title>transitivity</title>
1717 <titleabbrev>transitivity</titleabbrev>
1718 <para><userinput>transitivity t</userinput></para>
1721 <varlistentry role="tactic.synopsis">
1722 <term>Synopsis:</term>
1724 <para><emphasis role="bold">transitivity</emphasis> &sterm;</para>
1728 <term>Pre-conditions:</term>
1730 <para>The conclusion of the current proof must be an equality.</para>
1734 <term>Action:</term>
1736 <para>It closes the current sequent by transitivity of the equality.</para>
1740 <term>New sequents to prove:</term>
1742 <para>It opens two new sequents <command>l=t</command> and
1743 <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
1744 the current sequent to prove.</para>
1750 <sect1 id="tac_unfold">
1751 <title>unfold</title>
1752 <titleabbrev>unfold</titleabbrev>
1753 <para><userinput>unfold t patt</userinput></para>
1756 <varlistentry role="tactic.synopsis">
1757 <term>Synopsis:</term>
1759 <para><emphasis role="bold">unfold</emphasis> [&sterm;] &pattern;</para>
1763 <term>Pre-conditions:</term>
1769 <term>Action:</term>
1771 <para>It finds all the occurrences of <command>t</command>
1772 (possibly applied to arguments) in the subterms matched by
1773 <command>patt</command>. Then it δ-expands each occurrence,
1774 also performing β-reduction of the obtained term. If
1775 <command>t</command> is omitted it defaults to each
1776 subterm matched by <command>patt</command>.</para>
1780 <term>New sequents to prove:</term>
1788 <sect1 id="tac_whd">
1790 <titleabbrev>whd</titleabbrev>
1791 <para><userinput>whd patt</userinput></para>
1794 <varlistentry role="tactic.synopsis">
1795 <term>Synopsis:</term>
1797 <para><emphasis role="bold">whd</emphasis> &pattern;</para>
1801 <term>Pre-conditions:</term>
1807 <term>Action:</term>
1809 <para>It replaces all the terms matched by <command>patt</command>
1810 with their βδιζ-weak-head normal form.</para>
1814 <term>New sequents to prove:</term>