]> matita.cs.unibo.it Git - helm.git/blob - matita/help/C/sec_tactics.xml
e9f1567239ef53add4626f8705f6f3d37391d415
[helm.git] / matita / help / C / sec_tactics.xml
1
2 <!-- ============ Tactics ====================== -->
3 <chapter id="sec_tactics">
4   <title>Tactics</title>
5
6   <sect1 id="tactics_quickref">
7     <title>Quick reference card</title>
8     <para>
9       &tacticref;
10     </para>
11   </sect1>
12
13   <sect1 id="tac_absurd">
14     <title>absurd</title>
15     <titleabbrev>absurd</titleabbrev>
16     <para><userinput>absurd P</userinput></para>
17      <para>
18       <variablelist>
19         <varlistentry role="tactic.synopsis">
20           <term>Synopsis:</term>
21           <listitem>
22             <para><emphasis role="bold">absurd</emphasis> &sterm;</para>
23           </listitem>
24         </varlistentry>
25         <varlistentry>
26           <term>Pre-conditions:</term>
27           <listitem>
28             <para><command>P</command> must have type <command>Prop</command>.</para>
29           </listitem>
30         </varlistentry>
31         <varlistentry>
32           <term>Action:</term>
33           <listitem>
34             <para>It closes the current sequent by eliminating an
35              absurd term.</para>
36           </listitem>
37         </varlistentry>
38         <varlistentry>
39           <term>New sequents to prove:</term>
40           <listitem>
41             <para>It opens two new sequents of conclusion <command>P</command>
42              and <command>¬P</command>.</para>
43           </listitem>
44         </varlistentry>
45       </variablelist>
46      </para>
47   </sect1>
48   <sect1 id="tac_apply">
49     <title>apply</title>
50     <titleabbrev>apply</titleabbrev>
51     <para><userinput>apply t</userinput></para>
52     <para>
53       <variablelist>
54         <varlistentry role="tactic.synopsis">
55           <term>Synopsis:</term>
56           <listitem>
57             <para><emphasis role="bold">apply</emphasis> &sterm;</para>
58           </listitem>
59         </varlistentry>
60         <varlistentry>
61           <term>Pre-conditions:</term>
62           <listitem>
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>
68           </listitem>
69         </varlistentry>
70         <varlistentry>
71           <term>Action:</term>
72           <listitem>
73             <para>It closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
74           </listitem>
75         </varlistentry>
76         <varlistentry>
77           <term>New sequents to prove:</term>
78           <listitem>
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
83              prove.</para>
84           </listitem>
85         </varlistentry>
86       </variablelist>
87     </para>
88   </sect1>
89   <sect1 id="tac_assumption">
90     <title>assumption</title>
91     <titleabbrev>assumption</titleabbrev>
92     <para><userinput>assumption </userinput></para>
93     <para>
94       <variablelist>
95         <varlistentry role="tactic.synopsis">
96           <term>Synopsis:</term>
97           <listitem>
98             <para><emphasis role="bold">assumption</emphasis></para>
99           </listitem>
100         </varlistentry>
101         <varlistentry>
102           <term>Pre-conditions:</term>
103           <listitem>
104             <para>There must exist an hypothesis whose type can be unified with
105              the conclusion of the current sequent.</para>
106           </listitem>
107         </varlistentry>
108         <varlistentry>
109           <term>Action:</term>
110           <listitem>
111             <para>It closes the current sequent exploiting an hypothesis.</para>
112           </listitem>
113         </varlistentry>
114         <varlistentry>
115           <term>New sequents to prove:</term>
116           <listitem>
117             <para>None</para>
118           </listitem>
119         </varlistentry>
120       </variablelist>
121     </para>
122   </sect1>
123   <sect1 id="tac_auto">
124     <title>auto</title>
125     <titleabbrev>auto</titleabbrev>
126     <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
127     <para>
128       <variablelist>
129         <varlistentry role="tactic.synopsis">
130           <term>Synopsis:</term>
131           <listitem>
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>
133           </listitem>
134         </varlistentry>
135         <varlistentry>
136           <term>Pre-conditions:</term>
137           <listitem>
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>
144           </listitem>
145         </varlistentry>
146         <varlistentry>
147           <term>Action:</term>
148           <listitem>
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>
152           </listitem>
153         </varlistentry>
154         <varlistentry>
155           <term>New sequents to prove:</term>
156           <listitem>
157             <para>None</para>
158           </listitem>
159         </varlistentry>
160       </variablelist>
161     </para>
162   </sect1>
163   <sect1 id="tac_clear">
164     <title>clear</title>
165     <titleabbrev>clear</titleabbrev>
166     <para><userinput>
167      clear H<subscript>1</subscript> ... H<subscript>m</subscript>
168     </userinput></para>
169     <para>
170       <variablelist>
171         <varlistentry role="tactic.synopsis">
172           <term>Synopsis:</term>
173           <listitem>
174             <para>
175              <emphasis role="bold">clear</emphasis>
176              &id; [&id;…]
177             </para>
178           </listitem>
179         </varlistentry>
180         <varlistentry>
181           <term>Pre-conditions:</term>
182           <listitem>
183             <para>
184              <command>
185               H<subscript>1</subscript> ... H<subscript>m</subscript>
186              </command> must be hypotheses of the
187              current sequent to prove.
188             </para>
189           </listitem>
190         </varlistentry>
191         <varlistentry>
192           <term>Action:</term>
193           <listitem>
194             <para>
195              It hides the hypotheses 
196              <command>
197               H<subscript>1</subscript> ... H<subscript>m</subscript>
198              </command> from the current sequent.
199             </para>
200           </listitem>
201         </varlistentry>
202         <varlistentry>
203           <term>New sequents to prove:</term>
204           <listitem>
205             <para>None</para>
206           </listitem>
207         </varlistentry>
208       </variablelist>
209     </para>
210   </sect1>
211   <sect1 id="tac_clearbody">
212     <title>clearbody</title>
213     <titleabbrev>clearbody</titleabbrev>
214     <para><userinput>clearbody H</userinput></para>
215     <para>
216       <variablelist>
217         <varlistentry role="tactic.synopsis">
218           <term>Synopsis:</term>
219           <listitem>
220             <para><emphasis role="bold">clearbody</emphasis> &id;</para>
221           </listitem>
222         </varlistentry>
223         <varlistentry>
224           <term>Pre-conditions:</term>
225           <listitem>
226             <para><command>H</command> must be an hypothesis of the
227              current sequent to prove.</para>
228           </listitem>
229         </varlistentry>
230         <varlistentry>
231           <term>Action:</term>
232           <listitem>
233             <para>It hides the definiens of a definition in the current
234              sequent context. Thus the definition becomes an hypothesis.</para>
235           </listitem>
236         </varlistentry>
237         <varlistentry>
238           <term>New sequents to prove:</term>
239           <listitem>
240             <para>None.</para>
241           </listitem>
242         </varlistentry>
243       </variablelist>
244     </para>
245   </sect1>
246   <sect1 id="tac_change">
247     <title>change</title>
248     <titleabbrev>change</titleabbrev>
249     <para><userinput>change patt with t</userinput></para>
250     <para>
251       <variablelist>
252         <varlistentry role="tactic.synopsis">
253           <term>Synopsis:</term>
254           <listitem>
255             <para><emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
256           </listitem>
257         </varlistentry>
258         <varlistentry>
259           <term>Pre-conditions:</term>
260           <listitem>
261             <para>Each subterm matched by the pattern must be convertible
262              with the term <command>t</command> disambiguated in the context
263              of the matched subterm.</para>
264           </listitem>
265         </varlistentry>
266         <varlistentry>
267           <term>Action:</term>
268           <listitem>
269             <para>It replaces the subterms of the current sequent matched by
270              <command>patt</command> with the new term <command>t</command>.
271              For each subterm matched by the pattern, <command>t</command> is
272              disambiguated in the context of the subterm.</para>
273           </listitem>
274         </varlistentry>
275         <varlistentry>
276           <term>New sequents to prove:</term>
277           <listitem>
278             <para>None.</para>
279           </listitem>
280         </varlistentry>
281       </variablelist>
282     </para>
283   </sect1>
284   <sect1 id="tac_constructor">
285     <title>constructor</title>
286     <titleabbrev>constructor</titleabbrev>
287     <para><userinput>constructor n</userinput></para>
288     <para>
289       <variablelist>
290         <varlistentry role="tactic.synopsis">
291           <term>Synopsis:</term>
292           <listitem>
293             <para><emphasis role="bold">constructor</emphasis> &nat;</para>
294           </listitem>
295         </varlistentry>
296         <varlistentry>
297           <term>Pre-conditions:</term>
298           <listitem>
299             <para>The conclusion of the current sequent must be
300              an inductive type or the application of an inductive type with
301              at least <command>n</command> constructors.</para>
302           </listitem>
303         </varlistentry>
304         <varlistentry>
305           <term>Action:</term>
306           <listitem>
307             <para>It applies the <command>n</command>-th constructor of the
308              inductive type of the conclusion of the current sequent.</para>
309           </listitem>
310         </varlistentry>
311         <varlistentry>
312           <term>New sequents to prove:</term>
313           <listitem>
314             <para>It opens a new sequent for each premise of the constructor
315              that can not be inferred by unification. For more details,
316              see the <command>apply</command> tactic.</para>
317           </listitem>
318         </varlistentry>
319       </variablelist>
320     </para>
321   </sect1>
322   <sect1 id="tac_contradiction">
323     <title>contradiction</title>
324     <titleabbrev>contradiction</titleabbrev>
325     <para><userinput>contradiction </userinput></para>
326     <para>
327       <variablelist>
328         <varlistentry role="tactic.synopsis">
329           <term>Synopsis:</term>
330           <listitem>
331             <para><emphasis role="bold">contradiction</emphasis></para>
332           </listitem>
333         </varlistentry>
334         <varlistentry>
335           <term>Pre-conditions:</term>
336           <listitem>
337             <para>There must be in the current context an hypothesis of type
338              <command>False</command>.</para>
339           </listitem>
340         </varlistentry>
341         <varlistentry>
342           <term>Action:</term>
343           <listitem>
344             <para>It closes the current sequent by applying an hypothesis of
345              type <command>False</command>.</para>
346           </listitem>
347         </varlistentry>
348         <varlistentry>
349           <term>New sequents to prove:</term>
350           <listitem>
351             <para>None</para>
352           </listitem>
353         </varlistentry>
354       </variablelist>
355     </para>
356   </sect1>
357   <sect1 id="tac_cut">
358     <title>cut</title>
359     <titleabbrev>cut</titleabbrev>
360     <para><userinput>cut P as H</userinput></para>
361     <para>
362       <variablelist>
363         <varlistentry role="tactic.synopsis">
364           <term>Synopsis:</term>
365           <listitem>
366             <para><emphasis role="bold">cut</emphasis> &sterm; [<emphasis role="bold">as</emphasis> &id;]</para>
367           </listitem>
368         </varlistentry>
369         <varlistentry>
370           <term>Pre-conditions:</term>
371           <listitem>
372             <para><command>P</command> must have type <command>Prop</command>.</para>
373           </listitem>
374         </varlistentry>
375         <varlistentry>
376           <term>Action:</term>
377           <listitem>
378             <para>It closes the current sequent.</para>
379           </listitem>
380         </varlistentry>
381         <varlistentry>
382           <term>New sequents to prove:</term>
383           <listitem>
384             <para>It opens two new sequents. The first one has an extra
385              hypothesis <command>H:P</command>. If <command>H</command> is
386              omitted, the name of the hypothesis is automatically generated.
387              The second sequent has conclusion <command>P</command> and
388              hypotheses the hypotheses of the current sequent to prove.</para>
389           </listitem>
390         </varlistentry>
391       </variablelist>
392     </para>
393   </sect1>
394   <sect1 id="tac_decompose">
395     <title>decompose</title>
396     <titleabbrev>decompose</titleabbrev>
397     <para><userinput>
398      decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) 
399      H as H<subscript>1</subscript> ... H<subscript>m</subscript>
400     </userinput></para>
401     <para>
402       <variablelist>
403         <varlistentry role="tactic.synopsis">
404           <term>Synopsis:</term>
405           <listitem>
406             <para>
407              <emphasis role="bold">decompose</emphasis>
408              [<emphasis role="bold">(</emphasis>
409              &id;…
410              <emphasis role="bold">)</emphasis>]
411              [&id;] 
412              [<emphasis role="bold">as</emphasis> &id;…]
413             </para>
414           </listitem>
415         </varlistentry>
416         <varlistentry>
417           <term>Pre-conditions:</term>
418           <listitem>
419             <para> 
420              <command>H</command> must inhabit one inductive type among  
421              <command>
422               T<subscript>1</subscript> ... T<subscript>n</subscript>
423              </command>
424              and the types of a predefined list.
425             </para>
426           </listitem>
427         </varlistentry>
428         <varlistentry>
429           <term>Action:</term>
430           <listitem>
431             <para>
432              Runs <command>
433               elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
434              </command>, clears <command>H</command> and tries to run itself
435              recursively on each new identifier introduced by 
436              <command>elim</command> in the opened sequents. 
437              If <command>H</command> is not provided tries this operation on
438              each premise in the current context.
439             </para>
440           </listitem>
441         </varlistentry>
442         <varlistentry>
443           <term>New sequents to prove:</term>
444           <listitem>
445             <para>
446              The ones generated by all the <command>elim</command> tactics run.
447             </para>
448           </listitem>
449         </varlistentry>
450       </variablelist>
451     </para>
452   </sect1>
453   <sect1 id="tac_demodulate">
454     <title>demodulate</title>
455     <titleabbrev>demodulate</titleabbrev>
456     <para><userinput>demodulate</userinput></para>
457     <para>
458       <variablelist>
459         <varlistentry role="tactic.synopsis">
460           <term>Synopsis:</term>
461           <listitem>
462             <para><emphasis role="bold">demodulate</emphasis></para>
463           </listitem>
464         </varlistentry>
465         <varlistentry>
466           <term>Pre-conditions:</term>
467           <listitem>
468             <para>None.</para>
469           </listitem>
470         </varlistentry>
471         <varlistentry>
472           <term>Action:</term>
473           <listitem>
474             <para>&TODO;</para>
475           </listitem>
476         </varlistentry>
477         <varlistentry>
478           <term>New sequents to prove:</term>
479           <listitem>
480             <para>None.</para>
481           </listitem>
482         </varlistentry>
483       </variablelist>
484     </para>
485   </sect1>
486   <sect1 id="tac_discriminate">
487     <title>discriminate</title>
488     <titleabbrev>discriminate</titleabbrev>
489     <para><userinput>discriminate p</userinput></para>
490     <para>
491       <variablelist>
492         <varlistentry role="tactic.synopsis">
493           <term>Synopsis:</term>
494           <listitem>
495             <para><emphasis role="bold">discriminate</emphasis> &sterm;</para>
496           </listitem>
497         </varlistentry>
498         <varlistentry>
499           <term>Pre-conditions:</term>
500           <listitem>
501             <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
502 its constructor takes no arguments.</para>
503           </listitem>
504         </varlistentry>
505         <varlistentry>
506           <term>Action:</term>
507           <listitem>
508             <para>It closes the current sequent by proving the absurdity of
509              <command>p</command>.</para>
510           </listitem>
511         </varlistentry>
512         <varlistentry>
513           <term>New sequents to prove:</term>
514           <listitem>
515             <para>None.</para>
516           </listitem>
517         </varlistentry>
518       </variablelist>
519     </para>
520   </sect1>
521   <sect1 id="tac_elim">
522     <title>elim</title>
523     <titleabbrev>elim</titleabbrev>
524     <para><userinput>elim t using th hyps</userinput></para>
525     <para>
526       <variablelist>
527         <varlistentry role="tactic.synopsis">
528           <term>Synopsis:</term>
529           <listitem>
530             <para><emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
531           </listitem>
532         </varlistentry>
533         <varlistentry>
534           <term>Pre-conditions:</term>
535           <listitem>
536             <para><command>t</command> must inhabit an inductive type and
537              <command>th</command> must be an elimination principle for that
538              inductive type. If <command>th</command> is omitted the appropriate
539              standard elimination principle is chosen.</para>
540           </listitem>
541         </varlistentry>
542         <varlistentry>
543           <term>Action:</term>
544           <listitem>
545             <para>It proceeds by cases on the values of <command>t</command>,
546              according to the elimination principle <command>th</command>.
547             </para>
548           </listitem>
549         </varlistentry>
550         <varlistentry>
551           <term>New sequents to prove:</term>
552           <listitem>
553             <para>It opens one new sequent for each case. The names of
554              the new hypotheses are picked by <command>hyps</command>, if
555              provided. If hyps specifies also a number of hypotheses that
556              is less than the number of new hypotheses for a new sequent,
557              then the exceeding hypothesis will be kept as implications in
558              the conclusion of the sequent.</para>
559           </listitem>
560         </varlistentry>
561       </variablelist>
562     </para>
563   </sect1>
564   <sect1 id="tac_elimType">
565     <title>elimType</title>
566     <titleabbrev>elimType</titleabbrev>
567     <para><userinput>elimType T using th hyps</userinput></para>
568     <para>
569       <variablelist>
570         <varlistentry role="tactic.synopsis">
571           <term>Synopsis:</term>
572           <listitem>
573             <para><emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
574           </listitem>
575         </varlistentry>
576         <varlistentry>
577           <term>Pre-conditions:</term>
578           <listitem>
579             <para><command>T</command> must be an inductive type.</para>
580           </listitem>
581         </varlistentry>
582         <varlistentry>
583           <term>Action:</term>
584           <listitem>
585             <para>TODO (severely bugged now).</para>
586           </listitem>
587         </varlistentry>
588         <varlistentry>
589           <term>New sequents to prove:</term>
590           <listitem>
591             <para>TODO</para>
592           </listitem>
593         </varlistentry>
594       </variablelist>
595     </para>
596   </sect1>
597   <sect1 id="tac_exact">
598     <title>exact</title>
599     <titleabbrev>exact</titleabbrev>
600     <para><userinput>exact p</userinput></para>
601     <para>
602       <variablelist>
603         <varlistentry role="tactic.synopsis">
604           <term>Synopsis:</term>
605           <listitem>
606             <para><emphasis role="bold">exact</emphasis> &sterm;</para>
607           </listitem>
608         </varlistentry>
609         <varlistentry>
610           <term>Pre-conditions:</term>
611           <listitem>
612             <para>The type of <command>p</command> must be convertible
613              with the conclusion of the current sequent.</para>
614           </listitem>
615         </varlistentry>
616         <varlistentry>
617           <term>Action:</term>
618           <listitem>
619             <para>It closes the current sequent using <command>p</command>.</para>
620           </listitem>
621         </varlistentry>
622         <varlistentry>
623           <term>New sequents to prove:</term>
624           <listitem>
625             <para>None.</para>
626           </listitem>
627         </varlistentry>
628       </variablelist>
629     </para>
630   </sect1>
631   <sect1 id="tac_exists">
632     <title>exists</title>
633     <titleabbrev>exists</titleabbrev>
634     <para><userinput>exists </userinput></para>
635     <para>
636       <variablelist>
637         <varlistentry role="tactic.synopsis">
638           <term>Synopsis:</term>
639           <listitem>
640             <para><emphasis role="bold">exists</emphasis></para>
641           </listitem>
642         </varlistentry>
643         <varlistentry>
644           <term>Pre-conditions:</term>
645           <listitem>
646             <para>The conclusion of the current sequent must be
647              an inductive type or the application of an inductive type
648              with at least one constructor.</para>
649           </listitem>
650         </varlistentry>
651         <varlistentry>
652           <term>Action:</term>
653           <listitem>
654             <para>Equivalent to <command>constructor 1</command>.</para>
655           </listitem>
656         </varlistentry>
657         <varlistentry>
658           <term>New sequents to prove:</term>
659           <listitem>
660             <para>It opens a new sequent for each premise of the first
661              constructor of the inductive type that is the conclusion of the
662              current sequent. For more details, see the <command>constructor</command> tactic.</para>
663           </listitem>
664         </varlistentry>
665       </variablelist>
666     </para>
667   </sect1>
668   <sect1 id="tac_fail">
669     <title>fail</title>
670     <titleabbrev>fail</titleabbrev>
671     <para><userinput>fail</userinput></para>
672     <para>
673       <variablelist>
674         <varlistentry role="tactic.synopsis">
675           <term>Synopsis:</term>
676           <listitem>
677             <para><emphasis role="bold">fail</emphasis></para>
678           </listitem>
679         </varlistentry>
680         <varlistentry>
681           <term>Pre-conditions:</term>
682           <listitem>
683             <para>None.</para>
684           </listitem>
685         </varlistentry>
686         <varlistentry>
687           <term>Action:</term>
688           <listitem>
689             <para>This tactic always fail.</para>
690           </listitem>
691         </varlistentry>
692         <varlistentry>
693           <term>New sequents to prove:</term>
694           <listitem>
695             <para>N.A.</para>
696           </listitem>
697         </varlistentry>
698       </variablelist>
699     </para>
700   </sect1>
701   <sect1 id="tac_fold">
702     <title>fold</title>
703     <titleabbrev>fold</titleabbrev>
704     <para><userinput>fold red t patt</userinput></para>
705     <para>
706       <variablelist>
707         <varlistentry role="tactic.synopsis">
708           <term>Synopsis:</term>
709           <listitem>
710             <para><emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern;</para>
711           </listitem>
712         </varlistentry>
713         <varlistentry>
714           <term>Pre-conditions:</term>
715           <listitem>
716             <para>The pattern must not specify the wanted term.</para>
717           </listitem>
718         </varlistentry>
719         <varlistentry>
720           <term>Action:</term>
721           <listitem>
722             <para>First of all it locates all the subterms matched by
723              <command>patt</command>. In the context of each matched subterm
724              it disambiguates the term <command>t</command> and reduces it
725              to its <command>red</command> normal form; then it replaces with
726              <command>t</command> every occurrence of the normal form in the
727              matched subterm.</para>
728           </listitem>
729         </varlistentry>
730         <varlistentry>
731           <term>New sequents to prove:</term>
732           <listitem>
733             <para>None.</para>
734           </listitem>
735         </varlistentry>
736       </variablelist>
737     </para>
738   </sect1>
739   <sect1 id="tac_fourier">
740     <title>fourier</title>
741     <titleabbrev>fourier</titleabbrev>
742     <para><userinput>fourier </userinput></para>
743     <para>
744       <variablelist>
745         <varlistentry role="tactic.synopsis">
746           <term>Synopsis:</term>
747           <listitem>
748             <para><emphasis role="bold">fourier</emphasis></para>
749           </listitem>
750         </varlistentry>
751         <varlistentry>
752           <term>Pre-conditions:</term>
753           <listitem>
754             <para>The conclusion of the current sequent must be a linear
755              inequation over real numbers taken from standard library of
756              Coq. Moreover the inequations in the hypotheses must imply the
757              inequation in the conclusion of the current sequent.</para>
758           </listitem>
759         </varlistentry>
760         <varlistentry>
761           <term>Action:</term>
762           <listitem>
763             <para>It closes the current sequent by applying the Fourier method.</para>
764           </listitem>
765         </varlistentry>
766         <varlistentry>
767           <term>New sequents to prove:</term>
768           <listitem>
769             <para>None.</para>
770           </listitem>
771         </varlistentry>
772       </variablelist>
773     </para>
774   </sect1>
775   <sect1 id="tac_fwd">
776     <title>fwd</title>
777     <titleabbrev>fwd</titleabbrev>
778     <para><userinput>fwd H as H<subscript>0</subscript> ... H<subscript>n</subscript></userinput></para>
779     <para>
780       <variablelist>
781         <varlistentry role="tactic.synopsis">
782           <term>Synopsis:</term>
783           <listitem>
784             <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">as</emphasis> &id; [&id;]…]</para>
785           </listitem>
786         </varlistentry>
787         <varlistentry>
788           <term>Pre-conditions:</term>
789           <listitem>
790             <para>
791                The type of <command>H</command> must be the premise of a
792                forward simplification theorem.
793             </para>
794           </listitem>
795         </varlistentry>
796         <varlistentry>
797           <term>Action:</term>
798           <listitem>
799             <para>
800              This tactic is under development.
801              It simplifies the current context by removing
802              <command>H</command> using the following methods:
803              forward application (by <command>lapply</command>) of a suitable
804              simplification theorem, chosen automatically, of which the type
805              of <command>H</command> is a premise, 
806              decomposition (by <command>decompose</command>),
807              rewriting (by <command>rewrite</command>).
808              <command>H<subscript>0</subscript> ... H<subscript>n</subscript></command>
809              are passed to the tactics <command>fwd</command> invokes, as
810              names for the premise they introduce.
811             </para>
812           </listitem>
813         </varlistentry>
814         <varlistentry>
815           <term>New sequents to prove:</term>
816           <listitem>
817             <para>
818              The ones opened by the tactics <command>fwd</command> invokes.
819             </para>
820           </listitem>
821         </varlistentry>
822       </variablelist>
823     </para>
824   </sect1>
825   <sect1 id="tac_generalize">
826     <title>generalize</title>
827     <titleabbrev>generalize</titleabbrev>
828     <para><userinput>generalize patt as H</userinput></para>
829     <para>
830       <variablelist>
831         <varlistentry role="tactic.synopsis">
832           <term>Synopsis:</term>
833           <listitem>
834             <para><emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;]</para>
835           </listitem>
836         </varlistentry>
837         <varlistentry>
838           <term>Pre-conditions:</term>
839           <listitem>
840             <para>All the terms matched by <command>patt</command> must be
841              convertible and close in the context of the current sequent.</para>
842           </listitem>
843         </varlistentry>
844         <varlistentry>
845           <term>Action:</term>
846           <listitem>
847             <para>It closes the current sequent by applying a stronger
848              lemma that is proved using the new generated sequent.</para>
849           </listitem>
850         </varlistentry>
851         <varlistentry>
852           <term>New sequents to prove:</term>
853           <listitem>
854             <para>It opens a new sequent where the current sequent conclusion
855              <command>G</command> is generalized to
856              <command>∀x.G{x/t}</command> where <command>{x/t}</command>
857              is a notation for the replacement with <command>x</command> of all
858              the occurrences of the term <command>t</command> matched by
859              <command>patt</command>. If <command>patt</command> matches no
860              subterm then <command>t</command> is defined as the
861              <command>wanted</command> part of the pattern.</para>
862           </listitem>
863         </varlistentry>
864       </variablelist>
865     </para>
866   </sect1>
867   <sect1 id="tac_id">
868     <title>id</title>
869     <titleabbrev>id</titleabbrev>
870     <para><userinput>id </userinput></para>
871     <para>
872       <variablelist>
873         <varlistentry role="tactic.synopsis">
874           <term>Synopsis:</term>
875           <listitem>
876             <para><emphasis role="bold">id</emphasis></para>
877           </listitem>
878         </varlistentry>
879         <varlistentry>
880           <term>Pre-conditions:</term>
881           <listitem>
882             <para>None.</para>
883           </listitem>
884         </varlistentry>
885         <varlistentry>
886           <term>Action:</term>
887           <listitem>
888             <para>This identity tactic does nothing without failing.</para>
889           </listitem>
890         </varlistentry>
891         <varlistentry>
892           <term>New sequents to prove:</term>
893           <listitem>
894             <para>None.</para>
895           </listitem>
896         </varlistentry>
897       </variablelist>
898     </para>
899   </sect1>
900   <sect1 id="tac_injection">
901     <title>injection</title>
902     <titleabbrev>injection</titleabbrev>
903     <para><userinput>injection p</userinput></para>
904     <para>
905       <variablelist>
906         <varlistentry role="tactic.synopsis">
907           <term>Synopsis:</term>
908           <listitem>
909             <para><emphasis role="bold">injection</emphasis> &sterm;</para>
910           </listitem>
911         </varlistentry>
912         <varlistentry>
913           <term>Pre-conditions:</term>
914           <listitem>
915             <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
916 <command>K</command> takes no arguments.</para>
917           </listitem>
918         </varlistentry>
919         <varlistentry>
920           <term>Action:</term>
921           <listitem>
922             <para>It derives new hypotheses by injectivity of
923              <command>K</command>.</para>
924           </listitem>
925         </varlistentry>
926         <varlistentry>
927           <term>New sequents to prove:</term>
928           <listitem>
929             <para>The new sequent to prove is equal to the current sequent
930              with the additional hypotheses
931              <command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
932           </listitem>
933         </varlistentry>
934       </variablelist>
935     </para>
936   </sect1>
937   <sect1 id="tac_intro">
938     <title>intro</title>
939     <titleabbrev>intro</titleabbrev>
940     <para><userinput>intro H</userinput></para>
941     <para>
942       <variablelist>
943         <varlistentry role="tactic.synopsis">
944           <term>Synopsis:</term>
945           <listitem>
946             <para><emphasis role="bold">intro</emphasis> [&id;]</para>
947           </listitem>
948         </varlistentry>
949         <varlistentry>
950           <term>Pre-conditions:</term>
951           <listitem>
952             <para>The conclusion of the sequent to prove must be an implication
953              or a universal quantification.</para>
954           </listitem>
955         </varlistentry>
956         <varlistentry>
957           <term>Action:</term>
958           <listitem>
959             <para>It applies the right introduction rule for implication,
960              closing the current sequent.</para>
961           </listitem>
962         </varlistentry>
963         <varlistentry>
964           <term>New sequents to prove:</term>
965           <listitem>
966             <para>It opens a new sequent to prove adding to the hypothesis
967              the antecedent of the implication and setting the conclusion
968              to the consequent of the implicaiton. The name of the new
969              hypothesis is <command>H</command> if provided; otherwise it
970              is automatically generated.</para>
971           </listitem>
972         </varlistentry>
973       </variablelist>
974     </para>
975   </sect1>
976   <sect1 id="tac_intros">
977     <title>intros</title>
978     <titleabbrev>intros</titleabbrev>
979     <para><userinput>intros hyps</userinput></para>
980     <para>
981       <variablelist>
982         <varlistentry role="tactic.synopsis">
983           <term>Synopsis:</term>
984           <listitem>
985             <para><emphasis role="bold">intros</emphasis> &intros-spec;</para>
986           </listitem>
987         </varlistentry>
988         <varlistentry>
989           <term>Pre-conditions:</term>
990           <listitem>
991             <para>If <command>hyps</command> specifies a number of hypotheses
992              to introduce, then the conclusion of the current sequent must
993              be formed by at least that number of imbricated implications
994              or universal quantifications.</para>
995           </listitem>
996         </varlistentry>
997         <varlistentry>
998           <term>Action:</term>
999           <listitem>
1000             <para>It applies several times the right introduction rule for
1001              implication, closing the current sequent.</para>
1002           </listitem>
1003         </varlistentry>
1004         <varlistentry>
1005           <term>New sequents to prove:</term>
1006           <listitem>
1007             <para>It opens a new sequent to prove adding a number of new
1008              hypotheses equal to the number of new hypotheses requested.
1009              If the user does not request a precise number of new hypotheses,
1010              it adds as many hypotheses as possible.
1011              The name of each new hypothesis is either popped from the
1012              user provided list of names, or it is automatically generated when
1013              the list is (or becomes) empty.</para>
1014           </listitem>
1015         </varlistentry>
1016       </variablelist>
1017     </para>
1018   </sect1>
1019   <sect1 id="tac_inversion">
1020     <title>inversion</title>
1021     <titleabbrev>inversion</titleabbrev>
1022     <para><userinput>inversion t</userinput></para>
1023     <para>
1024       <variablelist>
1025         <varlistentry role="tactic.synopsis">
1026           <term>Synopsis:</term>
1027           <listitem>
1028             <para><emphasis role="bold">inversion</emphasis> &sterm;</para>
1029           </listitem>
1030         </varlistentry>
1031         <varlistentry>
1032           <term>Pre-conditions:</term>
1033           <listitem>
1034             <para>The type of the term <command>t</command> must be an inductive
1035              type or the application of an inductive type.</para>
1036           </listitem>
1037         </varlistentry>
1038         <varlistentry>
1039           <term>Action:</term>
1040           <listitem>
1041             <para>It proceeds by cases on <command>t</command> paying attention
1042              to the constraints imposed by the actual &quot;right arguments&quot;
1043              of the inductive type.</para>
1044           </listitem>
1045         </varlistentry>
1046         <varlistentry>
1047           <term>New sequents to prove:</term>
1048           <listitem>
1049             <para>It opens one new sequent to prove for each case in the
1050              definition of the type of <command>t</command>. With respect to
1051              a simple elimination, each new sequent has additional hypotheses
1052              that states the equalities of the &quot;right parameters&quot;
1053              of the inductive type with terms originally present in the
1054              sequent to prove.</para>
1055           </listitem>
1056         </varlistentry>
1057       </variablelist>
1058     </para>
1059   </sect1>
1060   <sect1 id="tac_lapply">
1061     <title>lapply</title>
1062     <titleabbrev>lapply</titleabbrev>
1063     <para><userinput>
1064      lapply linear depth=d t 
1065      to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
1066     </userinput></para>
1067     <para>
1068       <variablelist>
1069         <varlistentry role="tactic.synopsis">
1070           <term>Synopsis:</term>
1071           <listitem>
1072             <para>
1073              <emphasis role="bold">lapply</emphasis> 
1074              [<emphasis role="bold">linear</emphasis>]
1075              [<emphasis role="bold">depth=</emphasis>&nat;] 
1076              &sterm; 
1077              [<emphasis role="bold">to</emphasis>
1078               &sterm;
1079               [<emphasis role="bold">,</emphasis>&sterm;…]
1080              ] 
1081              [<emphasis role="bold">as</emphasis> &id;]
1082             </para>
1083           </listitem>
1084         </varlistentry>
1085         <varlistentry>
1086           <term>Pre-conditions:</term>
1087           <listitem>
1088             <para>
1089              <command>t</command> must have at least <command>d</command>
1090              independent premises and <command>n</command> must not be
1091              greater than <command>d</command>.
1092             </para>
1093           </listitem>
1094         </varlistentry>
1095         <varlistentry>
1096           <term>Action:</term>
1097           <listitem>
1098             <para>
1099              Invokes <command>letin H ≝ (t ? ... ?)</command>
1100              with enough <command>?</command>'s to reach the 
1101              <command>d</command>-th independent premise of
1102              <command>t</command>
1103              (<command>d</command> is maximum if unspecified).       
1104              Then istantiates (by <command>apply</command>) with
1105              t<subscript>1</subscript>, ..., t<subscript>n</subscript>
1106              the <command>?</command>'s corresponding to the first 
1107              <command>n</command> independent premises of
1108              <command>t</command>.
1109              Usually the other <command>?</command>'s preceding the 
1110              <command>n</command>-th independent premise of
1111              <command>t</command> are istantiated as a consequence.
1112              If the <command>linear</command> flag is specified and if 
1113              <command>t, t<subscript>1</subscript>, ..., t<subscript>n</subscript></command>
1114              are (applications of) premises in the current context, they are
1115              <command>clear</command>ed. 
1116             </para>
1117           </listitem>
1118         </varlistentry>
1119         <varlistentry>
1120           <term>New sequents to prove:</term>
1121           <listitem>
1122             <para>
1123              The ones opened by the tactics <command>lapply</command> invokes.
1124             </para>
1125           </listitem>
1126         </varlistentry>
1127       </variablelist>
1128     </para>
1129   </sect1>
1130   <sect1 id="tac_left">
1131     <title>left</title>
1132     <titleabbrev>left</titleabbrev>
1133     <para><userinput>left </userinput></para>
1134     <para>
1135       <variablelist>
1136         <varlistentry role="tactic.synopsis">
1137           <term>Synopsis:</term>
1138           <listitem>
1139             <para><emphasis role="bold">left</emphasis></para>
1140           </listitem>
1141         </varlistentry>
1142         <varlistentry>
1143           <term>Pre-conditions:</term>
1144           <listitem>
1145             <para>The conclusion of the current sequent must be
1146              an inductive type or the application of an inductive type
1147              with at least one constructor.</para>
1148           </listitem>
1149         </varlistentry>
1150         <varlistentry>
1151           <term>Action:</term>
1152           <listitem>
1153             <para>Equivalent to <command>constructor 1</command>.</para>
1154           </listitem>
1155         </varlistentry>
1156         <varlistentry>
1157           <term>New sequents to prove:</term>
1158           <listitem>
1159             <para>It opens a new sequent for each premise of the first
1160              constructor of the inductive type that is the conclusion of the
1161              current sequent. For more details, see the <command>constructor</command> tactic.</para>
1162           </listitem>
1163         </varlistentry>
1164       </variablelist>
1165     </para>
1166   </sect1>
1167   <sect1 id="tac_letin">
1168     <title>letin</title>
1169     <titleabbrev>letin</titleabbrev>
1170     <para><userinput>letin x ≝ t</userinput></para>
1171     <para>
1172       <variablelist>
1173         <varlistentry role="tactic.synopsis">
1174           <term>Synopsis:</term>
1175           <listitem>
1176             <para><emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm;</para>
1177           </listitem>
1178         </varlistentry>
1179         <varlistentry>
1180           <term>Pre-conditions:</term>
1181           <listitem>
1182             <para>None.</para>
1183           </listitem>
1184         </varlistentry>
1185         <varlistentry>
1186           <term>Action:</term>
1187           <listitem>
1188             <para>It adds to the context of the current sequent to prove a new
1189              definition <command>x ≝ t</command>.</para>
1190           </listitem>
1191         </varlistentry>
1192         <varlistentry>
1193           <term>New sequents to prove:</term>
1194           <listitem>
1195             <para>None.</para>
1196           </listitem>
1197         </varlistentry>
1198       </variablelist>
1199     </para>
1200   </sect1>
1201   <sect1 id="tac_normalize">
1202     <title>normalize</title>
1203     <titleabbrev>normalize</titleabbrev>
1204     <para><userinput>normalize patt</userinput></para>
1205     <para>
1206       <variablelist>
1207         <varlistentry role="tactic.synopsis">
1208           <term>Synopsis:</term>
1209           <listitem>
1210             <para><emphasis role="bold">normalize</emphasis> &pattern;</para>
1211           </listitem>
1212         </varlistentry>
1213         <varlistentry>
1214           <term>Pre-conditions:</term>
1215           <listitem>
1216             <para>None.</para>
1217           </listitem>
1218         </varlistentry>
1219         <varlistentry>
1220           <term>Action:</term>
1221           <listitem>
1222             <para>It replaces all the terms matched by <command>patt</command>
1223              with their βδιζ-normal form.</para>
1224           </listitem>
1225         </varlistentry>
1226         <varlistentry>
1227           <term>New sequents to prove:</term>
1228           <listitem>
1229             <para>None.</para>
1230           </listitem>
1231         </varlistentry>
1232       </variablelist>
1233     </para>
1234   </sect1>
1235   <sect1 id="tac_reduce">
1236     <title>reduce</title>
1237     <titleabbrev>reduce</titleabbrev>
1238     <para><userinput>reduce patt</userinput></para>
1239     <para>
1240       <variablelist>
1241         <varlistentry role="tactic.synopsis">
1242           <term>Synopsis:</term>
1243           <listitem>
1244             <para><emphasis role="bold">reduce</emphasis> &pattern;</para>
1245           </listitem>
1246         </varlistentry>
1247         <varlistentry>
1248           <term>Pre-conditions:</term>
1249           <listitem>
1250             <para>None.</para>
1251           </listitem>
1252         </varlistentry>
1253         <varlistentry>
1254           <term>Action:</term>
1255           <listitem>
1256             <para>It replaces all the terms matched by <command>patt</command>
1257              with their βδιζ-normal form.</para>
1258           </listitem>
1259         </varlistentry>
1260         <varlistentry>
1261           <term>New sequents to prove:</term>
1262           <listitem>
1263             <para>None.</para>
1264           </listitem>
1265         </varlistentry>
1266       </variablelist>
1267     </para>
1268   </sect1>
1269   <sect1 id="tac_reflexivity">
1270     <title>reflexivity</title>
1271     <titleabbrev>reflexivity</titleabbrev>
1272     <para><userinput>reflexivity </userinput></para>
1273     <para>
1274       <variablelist>
1275         <varlistentry role="tactic.synopsis">
1276           <term>Synopsis:</term>
1277           <listitem>
1278             <para><emphasis role="bold">reflexivity</emphasis></para>
1279           </listitem>
1280         </varlistentry>
1281         <varlistentry>
1282           <term>Pre-conditions:</term>
1283           <listitem>
1284             <para>The conclusion of the current sequent must be
1285              <command>t=t</command> for some term <command>t</command></para>
1286           </listitem>
1287         </varlistentry>
1288         <varlistentry>
1289           <term>Action:</term>
1290           <listitem>
1291             <para>It closes the current sequent by reflexivity
1292              of equality.</para>
1293           </listitem>
1294         </varlistentry>
1295         <varlistentry>
1296           <term>New sequents to prove:</term>
1297           <listitem>
1298             <para>None.</para>
1299           </listitem>
1300         </varlistentry>
1301       </variablelist>
1302     </para>
1303   </sect1>
1304   <sect1 id="tac_replace">
1305     <title>replace</title>
1306     <titleabbrev>change</titleabbrev>
1307     <para><userinput>change patt with t</userinput></para>
1308     <para>
1309       <variablelist>
1310         <varlistentry role="tactic.synopsis">
1311           <term>Synopsis:</term>
1312           <listitem>
1313             <para><emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
1314           </listitem>
1315         </varlistentry>
1316         <varlistentry>
1317           <term>Pre-conditions:</term>
1318           <listitem>
1319             <para>None.</para>
1320           </listitem>
1321         </varlistentry>
1322         <varlistentry>
1323           <term>Action:</term>
1324           <listitem>
1325             <para>It replaces the subterms of the current sequent matched by
1326              <command>patt</command> with the new term <command>t</command>.
1327              For each subterm matched by the pattern, <command>t</command> is
1328              disambiguated in the context of the subterm.</para>
1329           </listitem>
1330         </varlistentry>
1331         <varlistentry>
1332           <term>New sequents to prove:</term>
1333           <listitem>
1334             <para>For each matched term <command>t'</command> it opens
1335              a new sequent to prove whose conclusion is
1336              <command>t'=t</command>.</para>
1337           </listitem>
1338         </varlistentry>
1339       </variablelist>
1340     </para>
1341   </sect1>
1342   <sect1 id="tac_rewrite">
1343     <title>rewrite</title>
1344     <titleabbrev>rewrite</titleabbrev>
1345     <para><userinput>rewrite dir p patt</userinput></para>
1346     <para>
1347       <variablelist>
1348         <varlistentry role="tactic.synopsis">
1349           <term>Synopsis:</term>
1350           <listitem>
1351             <para><emphasis role="bold">rewrite</emphasis> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] &sterm; &pattern;</para>
1352           </listitem>
1353         </varlistentry>
1354         <varlistentry>
1355           <term>Pre-conditions:</term>
1356           <listitem>
1357             <para><command>p</command> must be the proof of an equality,
1358              possibly under some hypotheses.</para>
1359           </listitem>
1360         </varlistentry>
1361         <varlistentry>
1362           <term>Action:</term>
1363           <listitem>
1364             <para>It looks in every term matched by <command>patt</command>
1365              for all the occurrences of the
1366              left hand side of the equality that <command>p</command> proves
1367              (resp. the right hand side if <command>dir</command> is
1368              <command>&lt;</command>). Every occurence found is replaced with
1369              the opposite side of the equality.</para>
1370           </listitem>
1371         </varlistentry>
1372         <varlistentry>
1373           <term>New sequents to prove:</term>
1374           <listitem>
1375             <para>It opens one new sequent for each hypothesis of the
1376              equality proved by <command>p</command> that is not closed
1377              by unification.</para>
1378           </listitem>
1379         </varlistentry>
1380       </variablelist>
1381     </para>
1382   </sect1>
1383   <sect1 id="tac_right">
1384     <title>right</title>
1385     <titleabbrev>right</titleabbrev>
1386     <para><userinput>right </userinput></para>
1387     <para>
1388       <variablelist>
1389         <varlistentry role="tactic.synopsis">
1390           <term>Synopsis:</term>
1391           <listitem>
1392             <para><emphasis role="bold">right</emphasis></para>
1393           </listitem>
1394         </varlistentry>
1395         <varlistentry>
1396           <term>Pre-conditions:</term>
1397           <listitem>
1398             <para>The conclusion of the current sequent must be
1399              an inductive type or the application of an inductive type with
1400              at least two constructors.</para>
1401           </listitem>
1402         </varlistentry>
1403         <varlistentry>
1404           <term>Action:</term>
1405           <listitem>
1406             <para>Equivalent to <command>constructor 2</command>.</para>
1407           </listitem>
1408         </varlistentry>
1409         <varlistentry>
1410           <term>New sequents to prove:</term>
1411           <listitem>
1412             <para>It opens a new sequent for each premise of the second
1413              constructor of the inductive type that is the conclusion of the
1414              current sequent. For more details, see the <command>constructor</command> tactic.</para>
1415           </listitem>
1416         </varlistentry>
1417       </variablelist>
1418     </para>
1419   </sect1>
1420   <sect1 id="tac_ring">
1421     <title>ring</title>
1422     <titleabbrev>ring</titleabbrev>
1423     <para><userinput>ring </userinput></para>
1424     <para>
1425       <variablelist>
1426         <varlistentry role="tactic.synopsis">
1427           <term>Synopsis:</term>
1428           <listitem>
1429             <para><emphasis role="bold">ring</emphasis></para>
1430           </listitem>
1431         </varlistentry>
1432         <varlistentry>
1433           <term>Pre-conditions:</term>
1434           <listitem>
1435             <para>The conclusion of the current sequent must be an
1436              equality over Coq's real numbers that can be proved using
1437              the ring properties of the real numbers only.</para>
1438           </listitem>
1439         </varlistentry>
1440         <varlistentry>
1441           <term>Action:</term>
1442           <listitem>
1443             <para>It closes the current sequent veryfying the equality by
1444              means of computation (i.e. this is a reflexive tactic, implemented
1445              exploiting the &quot;two level reasoning&quot; technique).</para>
1446           </listitem>
1447         </varlistentry>
1448         <varlistentry>
1449           <term>New sequents to prove:</term>
1450           <listitem>
1451             <para>None.</para>
1452           </listitem>
1453         </varlistentry>
1454       </variablelist>
1455     </para>
1456   </sect1>
1457   <sect1 id="tac_simplify">
1458     <title>simplify</title>
1459     <titleabbrev>simplify</titleabbrev>
1460     <para><userinput>simplify patt</userinput></para>
1461     <para>
1462       <variablelist>
1463         <varlistentry role="tactic.synopsis">
1464           <term>Synopsis:</term>
1465           <listitem>
1466             <para><emphasis role="bold">simplify</emphasis> &pattern;</para>
1467           </listitem>
1468         </varlistentry>
1469         <varlistentry>
1470           <term>Pre-conditions:</term>
1471           <listitem>
1472             <para>None.</para>
1473           </listitem>
1474         </varlistentry>
1475         <varlistentry>
1476           <term>Action:</term>
1477           <listitem>
1478             <para>It replaces all the terms matched by <command>patt</command>
1479              with other convertible terms that are supposed to be simpler.</para>
1480           </listitem>
1481         </varlistentry>
1482         <varlistentry>
1483           <term>New sequents to prove:</term>
1484           <listitem>
1485             <para>None.</para>
1486           </listitem>
1487         </varlistentry>
1488       </variablelist>
1489     </para>
1490   </sect1>
1491   <sect1 id="tac_split">
1492     <title>split</title>
1493     <titleabbrev>split</titleabbrev>
1494     <para><userinput>split </userinput></para>
1495     <para>
1496       <variablelist>
1497         <varlistentry role="tactic.synopsis">
1498           <term>Synopsis:</term>
1499           <listitem>
1500             <para><emphasis role="bold">split</emphasis></para>
1501           </listitem>
1502         </varlistentry>
1503         <varlistentry>
1504           <term>Pre-conditions:</term>
1505           <listitem>
1506             <para>The conclusion of the current sequent must be
1507              an inductive type or the application of an inductive type with
1508              at least one constructor.</para>
1509           </listitem>
1510         </varlistentry>
1511         <varlistentry>
1512           <term>Action:</term>
1513           <listitem>
1514             <para>Equivalent to <command>constructor 1</command>.</para>
1515           </listitem>
1516         </varlistentry>
1517         <varlistentry>
1518           <term>New sequents to prove:</term>
1519           <listitem>
1520             <para>It opens a new sequent for each premise of the first
1521              constructor of the inductive type that is the conclusion of the
1522              current sequent. For more details, see the <command>constructor</command> tactic.</para>
1523           </listitem>
1524         </varlistentry>
1525       </variablelist>
1526     </para>
1527   </sect1>
1528   <sect1 id="tac_symmetry">
1529     <title>symmetry</title>
1530     <titleabbrev>symmetry</titleabbrev>
1531     <para>The tactic <command>symmetry</command> </para>
1532     <para><userinput>symmetry </userinput></para>
1533     <para>
1534       <variablelist>
1535         <varlistentry role="tactic.synopsis">
1536           <term>Synopsis:</term>
1537           <listitem>
1538             <para><emphasis role="bold">symmetry</emphasis></para>
1539           </listitem>
1540         </varlistentry>
1541         <varlistentry>
1542           <term>Pre-conditions:</term>
1543           <listitem>
1544             <para>The conclusion of the current proof must be an equality.</para>
1545           </listitem>
1546         </varlistentry>
1547         <varlistentry>
1548           <term>Action:</term>
1549           <listitem>
1550             <para>It swaps the two sides of the equalityusing the symmetric
1551              property.</para>
1552           </listitem>
1553         </varlistentry>
1554         <varlistentry>
1555           <term>New sequents to prove:</term>
1556           <listitem>
1557             <para>None.</para>
1558           </listitem>
1559         </varlistentry>
1560       </variablelist>
1561     </para>
1562   </sect1>
1563   <sect1 id="tac_transitivity">
1564     <title>transitivity</title>
1565     <titleabbrev>transitivity</titleabbrev>
1566     <para><userinput>transitivity t</userinput></para>
1567     <para>
1568       <variablelist>
1569         <varlistentry role="tactic.synopsis">
1570           <term>Synopsis:</term>
1571           <listitem>
1572             <para><emphasis role="bold">transitivity</emphasis> &sterm;</para>
1573           </listitem>
1574         </varlistentry>
1575         <varlistentry>
1576           <term>Pre-conditions:</term>
1577           <listitem>
1578             <para>The conclusion of the current proof must be an equality.</para>
1579           </listitem>
1580         </varlistentry>
1581         <varlistentry>
1582           <term>Action:</term>
1583           <listitem>
1584             <para>It closes the current sequent by transitivity of the equality.</para>
1585           </listitem>
1586         </varlistentry>
1587         <varlistentry>
1588           <term>New sequents to prove:</term>
1589           <listitem>
1590             <para>It opens two new sequents <command>l=t</command> and
1591              <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
1592 the current sequent to prove.</para>
1593           </listitem>
1594         </varlistentry>
1595       </variablelist>
1596     </para>
1597   </sect1>
1598   <sect1 id="tac_unfold">
1599     <title>unfold</title>
1600     <titleabbrev>unfold</titleabbrev>
1601     <para><userinput>unfold t patt</userinput></para>
1602     <para>
1603       <variablelist>
1604         <varlistentry role="tactic.synopsis">
1605           <term>Synopsis:</term>
1606           <listitem>
1607             <para><emphasis role="bold">unfold</emphasis> [&sterm;] &pattern;</para>
1608           </listitem>
1609         </varlistentry>
1610         <varlistentry>
1611           <term>Pre-conditions:</term>
1612           <listitem>
1613             <para>None.</para>
1614           </listitem>
1615         </varlistentry>
1616         <varlistentry>
1617           <term>Action:</term>
1618           <listitem>
1619             <para>It finds all the occurrences of <command>t</command>
1620              (possibly applied to arguments) in the subterms matched by
1621              <command>patt</command>. Then it δ-expands each occurrence,
1622              also performing β-reduction of the obtained term. If
1623              <command>t</command> is omitted it defaults to each
1624              subterm matched by <command>patt</command>.</para>
1625           </listitem>
1626         </varlistentry>
1627         <varlistentry>
1628           <term>New sequents to prove:</term>
1629           <listitem>
1630             <para>None.</para>
1631           </listitem>
1632         </varlistentry>
1633       </variablelist>
1634     </para>
1635   </sect1>
1636   <sect1 id="tac_whd">
1637     <title>whd</title>
1638     <titleabbrev>whd</titleabbrev>
1639     <para><userinput>whd patt</userinput></para>
1640     <para>
1641       <variablelist>
1642         <varlistentry role="tactic.synopsis">
1643           <term>Synopsis:</term>
1644           <listitem>
1645             <para><emphasis role="bold">whd</emphasis> &pattern;</para>
1646           </listitem>
1647         </varlistentry>
1648         <varlistentry>
1649           <term>Pre-conditions:</term>
1650           <listitem>
1651             <para>None.</para>
1652           </listitem>
1653         </varlistentry>
1654         <varlistentry>
1655           <term>Action:</term>
1656           <listitem>
1657             <para>It replaces all the terms matched by <command>patt</command>
1658              with their βδιζ-weak-head normal form.</para>
1659           </listitem>
1660         </varlistentry>
1661         <varlistentry>
1662           <term>New sequents to prove:</term>
1663           <listitem>
1664             <para>None.</para>
1665           </listitem>
1666         </varlistentry>
1667       </variablelist>
1668     </para>
1669   </sect1>
1670
1671 </chapter>
1672