matita/help/C/sec_tactics.xml

   1
   2 <!-- ============ Tactics ====================== -->
   3 <chapter id="sec_tactics">
   4  <title>Tactics</title>
   5
   6   <sect1 id="tac_absurd">
   7     <title>absurd &lt;term&gt;</title>
   8     <titleabbrev>absurd</titleabbrev>
   9     <para><userinput>absurd P</userinput></para>
  10      <para>
  11       <variablelist>
  12         <varlistentry>
  13           <term>Pre-conditions:</term>
  14           <listitem>
  15             <para><command>P</command> must have type <command>Prop</command>.</para>
  16           </listitem>
  17         </varlistentry>
  18         <varlistentry>
  19           <term>Action:</term>
  20           <listitem>
  21             <para>it closes the current sequent by eliminating an
  22              absurd term.</para>
  23           </listitem>
  24         </varlistentry>
  25         <varlistentry>
  26           <term>New sequents to prove:</term>
  27           <listitem>
  28             <para>it opens two new sequents of conclusion <command>P</command>
  29              and <command>¬P</command>.</para>
  30           </listitem>
  31         </varlistentry>
  32       </variablelist>
  33      </para>
  34   </sect1>
  35   <sect1 id="tac_apply">
  36     <title>apply &lt;term&gt;</title>
  37     <titleabbrev>apply</titleabbrev>
  38     <para><userinput>apply t</userinput></para>
  39     <para>
  40       <variablelist>
  41         <varlistentry>
  42           <term>Pre-conditions:</term>
  43           <listitem>
  44             <para><command>t</command> must have type
  45              <command>T<subscript>1</subscript> → ... →
  46               T<subscript>n</subscript> → G</command>
  47              where <command>G</command> can be unified with the conclusion
  48              of the current sequent.</para>
  49           </listitem>
  50         </varlistentry>
  51         <varlistentry>
  52           <term>Action:</term>
  53           <listitem>
  54             <para>it closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
  55           </listitem>
  56         </varlistentry>
  57         <varlistentry>
  58           <term>New sequents to prove:</term>
  59           <listitem>
  60             <para>it opens a new sequent for each premise
  61              <command>T<subscript>i</subscript></command> that is not
  62              instantiated by unification. <command>T<subscript>i</subscript></command> is
  63              the conclusion of the <command>i</command>-th new sequent to
  64              prove.</para>
  65           </listitem>
  66         </varlistentry>
  67       </variablelist>
  68     </para>
  69   </sect1>
  70   <sect1 id="tac_assumption">
  71     <title>assumption</title>
  72     <titleabbrev>assumption</titleabbrev>
  73     <para><userinput>assumption </userinput></para>
  74     <para>
  75       <variablelist>
  76         <varlistentry>
  77           <term>Pre-conditions:</term>
  78           <listitem>
  79             <para>there must exist an hypothesis whose type can be unified with
  80              the conclusion of the current sequent.</para>
  81           </listitem>
  82         </varlistentry>
  83         <varlistentry>
  84           <term>Action:</term>
  85           <listitem>
  86             <para>it closes the current sequent exploiting an hypothesis.</para>
  87           </listitem>
  88         </varlistentry>
  89         <varlistentry>
  90           <term>New sequents to prove:</term>
  91           <listitem>
  92             <para>none</para>
  93           </listitem>
  94         </varlistentry>
  95       </variablelist>
  96     </para>
  97   </sect1>
  98   <sect1 id="tac_auto">
  99     <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
 100     <titleabbrev>auto</titleabbrev>
 101     <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
 102     <para>
 103       <variablelist>
 104         <varlistentry>
 105           <term>Pre-conditions:</term>
 106           <listitem>
 107             <para>none, but the tactic may fail finding a proof if every
 108              proof is in the search space that is pruned away. Pruning is
 109              controlled by <command>d</command> and <command>w</command>.
 110              Moreover, only lemmas whose type signature is a subset of the
 111              signature of the current sequent are considered. The signature of
 112              a sequent is ...TODO</para>
 113           </listitem>
 114         </varlistentry>
 115         <varlistentry>
 116           <term>Action:</term>
 117           <listitem>
 118             <para>it closes the current sequent by repeated application of
 119              rewriting steps (unless <command>paramodulation</command> is
 120              omitted), hypothesis and lemmas in the library.</para>
 121           </listitem>
 122         </varlistentry>
 123         <varlistentry>
 124           <term>New sequents to prove:</term>
 125           <listitem>
 126             <para>none</para>
 127           </listitem>
 128         </varlistentry>
 129       </variablelist>
 130     </para>
 131   </sect1>
 132   <sect1 id="tac_clear">
 133     <title>clear &lt;id&gt;</title>
 134     <titleabbrev>clear</titleabbrev>
 135     <para><userinput>clear H</userinput></para>
 136     <para>
 137       <variablelist>
 138         <varlistentry>
 139           <term>Pre-conditions:</term>
 140           <listitem>
 141             <para><command>H</command> must be an hypothesis of the
 142              current sequent to prove.</para>
 143           </listitem>
 144         </varlistentry>
 145         <varlistentry>
 146           <term>Action:</term>
 147           <listitem>
 148             <para>it hides the hypothesis <command>H</command> from the
 149              current sequent.</para>
 150           </listitem>
 151         </varlistentry>
 152         <varlistentry>
 153           <term>New sequents to prove:</term>
 154           <listitem>
 155             <para>none</para>
 156           </listitem>
 157         </varlistentry>
 158       </variablelist>
 159     </para>
 160   </sect1>
 161   <sect1 id="tac_clearbody">
 162     <title>clearbody &lt;id&gt;</title>
 163     <titleabbrev>clearbody</titleabbrev>
 164     <para><userinput>clearbody H</userinput></para>
 165     <para>
 166       <variablelist>
 167         <varlistentry>
 168           <term>Pre-conditions:</term>
 169           <listitem>
 170             <para><command>H</command> must be an hypothesis of the
 171              current sequent to prove.</para>
 172           </listitem>
 173         </varlistentry>
 174         <varlistentry>
 175           <term>Action:</term>
 176           <listitem>
 177             <para>it hides the definiens of a definition in the current
 178              sequent context. Thus the definition becomes an hypothesis.</para>
 179           </listitem>
 180         </varlistentry>
 181         <varlistentry>
 182           <term>New sequents to prove:</term>
 183           <listitem>
 184             <para>none.</para>
 185           </listitem>
 186         </varlistentry>
 187       </variablelist>
 188     </para>
 189   </sect1>
 190   <sect1 id="tac_change">
 191     <title>change &lt;pattern&gt; with &lt;term&gt;</title>
 192     <titleabbrev>change</titleabbrev>
 193     <para><userinput>change patt with t</userinput></para>
 194     <para>
 195       <variablelist>
 196         <varlistentry>
 197           <term>Pre-conditions:</term>
 198           <listitem>
 199             <para>each subterm matched by the pattern must be convertible
 200              with the term <command>t</command> disambiguated in the context
 201              of the matched subterm.</para>
 202           </listitem>
 203         </varlistentry>
 204         <varlistentry>
 205           <term>Action:</term>
 206           <listitem>
 207             <para>it replaces the subterms of the current sequent matched by
 208              <command>patt</command> with the new term <command>t</command>.
 209              For each subterm matched by the pattern, <command>t</command> is
 210              disambiguated in the context of the subterm.</para>
 211           </listitem>
 212         </varlistentry>
 213         <varlistentry>
 214           <term>New sequents to prove:</term>
 215           <listitem>
 216             <para>none.</para>
 217           </listitem>
 218         </varlistentry>
 219       </variablelist>
 220     </para>
 221   </sect1>
 222   <sect1 id="tac_constructor">
 223     <title>constructor &lt;int&gt;</title>
 224     <titleabbrev>constructor</titleabbrev>
 225     <para><userinput>constructor n</userinput></para>
 226     <para>
 227       <variablelist>
 228         <varlistentry>
 229           <term>Pre-conditions:</term>
 230           <listitem>
 231             <para>the conclusion of the current sequent must be
 232              an inductive type or the application of an inductive type.</para>
 233           </listitem>
 234         </varlistentry>
 235         <varlistentry>
 236           <term>Action:</term>
 237           <listitem>
 238             <para>it applies the <command>n</command>-th constructor of the
 239              inductive type of the conclusion of the current sequent.</para>
 240           </listitem>
 241         </varlistentry>
 242         <varlistentry>
 243           <term>New sequents to prove:</term>
 244           <listitem>
 245             <para>it opens a new sequent for each premise of the constructor
 246              that can not be inferred by unification. For more details,
 247              see the <command>apply</command> tactic.</para>
 248           </listitem>
 249         </varlistentry>
 250       </variablelist>
 251     </para>
 252   </sect1>
 253   <sect1 id="tac_contradiction">
 254     <title>contradiction</title>
 255     <titleabbrev>contradiction</titleabbrev>
 256     <para><userinput>contradiction </userinput></para>
 257     <para>
 258       <variablelist>
 259         <varlistentry>
 260           <term>Pre-conditions:</term>
 261           <listitem>
 262             <para>there must be in the current context an hypothesis of type
 263              <command>False</command>.</para>
 264           </listitem>
 265         </varlistentry>
 266         <varlistentry>
 267           <term>Action:</term>
 268           <listitem>
 269             <para>it closes the current sequent by applying an hypothesis of
 270              type <command>False</command>.</para>
 271           </listitem>
 272         </varlistentry>
 273         <varlistentry>
 274           <term>New sequents to prove:</term>
 275           <listitem>
 276             <para>none</para>
 277           </listitem>
 278         </varlistentry>
 279       </variablelist>
 280     </para>
 281   </sect1>
 282   <sect1 id="tac_cut">
 283     <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
 284     <titleabbrev>cut</titleabbrev>
 285     <para><userinput>cut P as H</userinput></para>
 286     <para>
 287       <variablelist>
 288         <varlistentry>
 289           <term>Pre-conditions:</term>
 290           <listitem>
 291             <para><command>P</command> must have type <command>Prop</command>.</para>
 292           </listitem>
 293         </varlistentry>
 294         <varlistentry>
 295           <term>Action:</term>
 296           <listitem>
 297             <para>it closes the current sequent.</para>
 298           </listitem>
 299         </varlistentry>
 300         <varlistentry>
 301           <term>New sequents to prove:</term>
 302           <listitem>
 303             <para>it opens two new sequents. The first one has an extra
 304              hypothesis <command>H:P</command>. If <command>H</command> is
 305              omitted, the name of the hypothesis is automatically generated.
 306              The second sequent has conclusion <command>P</command> and
 307              hypotheses the hypotheses of the current sequent to prove.</para>
 308           </listitem>
 309         </varlistentry>
 310       </variablelist>
 311     </para>
 312   </sect1>
 313   <sect1 id="tac_decompose">
 314     <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
 315     <titleabbrev>decompose</titleabbrev>
 316     <para><userinput>decompose ???</userinput></para>
 317     <para>
 318       <variablelist>
 319         <varlistentry>
 320           <term>Pre-conditions:</term>
 321           <listitem>
 322             <para>TODO.</para>
 323           </listitem>
 324         </varlistentry>
 325         <varlistentry>
 326           <term>Action:</term>
 327           <listitem>
 328             <para>TODO.</para>
 329           </listitem>
 330         </varlistentry>
 331         <varlistentry>
 332           <term>New sequents to prove:</term>
 333           <listitem>
 334             <para>TODO.</para>
 335           </listitem>
 336         </varlistentry>
 337       </variablelist>
 338     </para>
 339   </sect1>
 340   <sect1 id="tac_discriminate">
 341     <title>discriminate &lt;term&gt;</title>
 342     <titleabbrev>discriminate</titleabbrev>
 343     <para><userinput>discriminate p</userinput></para>
 344     <para>
 345       <variablelist>
 346         <varlistentry>
 347           <term>Pre-conditions:</term>
 348           <listitem>
 349             <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
 350 its constructor takes no arguments.</para>
 351           </listitem>
 352         </varlistentry>
 353         <varlistentry>
 354           <term>Action:</term>
 355           <listitem>
 356             <para>it closes the current sequent by proving the absurdity of
 357              <command>p</command>.</para>
 358           </listitem>
 359         </varlistentry>
 360         <varlistentry>
 361           <term>New sequents to prove:</term>
 362           <listitem>
 363             <para>none.</para>
 364           </listitem>
 365         </varlistentry>
 366       </variablelist>
 367     </para>
 368   </sect1>
 369   <sect1 id="tac_elim">
 370     <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
 371     <titleabbrev>elim</titleabbrev>
 372     <para><userinput>elim t using th hyps</userinput></para>
 373     <para>
 374       <variablelist>
 375         <varlistentry>
 376           <term>Pre-conditions:</term>
 377           <listitem>
 378             <para><command>t</command> must inhabit an inductive type and
 379              <command>th</command> must be an elimination principle for that
 380              inductive type. If <command>th</command> is omitted the appropriate
 381              standard elimination principle is chosen.</para>
 382           </listitem>
 383         </varlistentry>
 384         <varlistentry>
 385           <term>Action:</term>
 386           <listitem>
 387             <para>it proceeds by cases on the values of <command>t</command>,
 388              according to the elimination principle <command>th</command>.
 389             </para>
 390           </listitem>
 391         </varlistentry>
 392         <varlistentry>
 393           <term>New sequents to prove:</term>
 394           <listitem>
 395             <para>it opens one new sequent for each case. The names of
 396              the new hypotheses are picked by <command>hyps</command>, if
 397              provided.</para>
 398           </listitem>
 399         </varlistentry>
 400       </variablelist>
 401     </para>
 402   </sect1>
 403   <sect1 id="tac_elimType">
 404     <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
 405     <titleabbrev>elimType</titleabbrev>
 406     <para><userinput>elimType T using th</userinput></para>
 407     <para>
 408       <variablelist>
 409         <varlistentry>
 410           <term>Pre-conditions:</term>
 411           <listitem>
 412             <para><command>T</command> must be an inductive type.</para>
 413           </listitem>
 414         </varlistentry>
 415         <varlistentry>
 416           <term>Action:</term>
 417           <listitem>
 418             <para>TODO (severely bugged now).</para>
 419           </listitem>
 420         </varlistentry>
 421         <varlistentry>
 422           <term>New sequents to prove:</term>
 423           <listitem>
 424             <para>TODO</para>
 425           </listitem>
 426         </varlistentry>
 427       </variablelist>
 428     </para>
 429   </sect1>
 430   <sect1 id="tac_exact">
 431     <title>exact &lt;term&gt;</title>
 432     <titleabbrev>exact</titleabbrev>
 433     <para><userinput>exact p</userinput></para>
 434     <para>
 435       <variablelist>
 436         <varlistentry>
 437           <term>Pre-conditions:</term>
 438           <listitem>
 439             <para>the type of <command>p</command> must be convertible
 440              with the conclusion of the current sequent.</para>
 441           </listitem>
 442         </varlistentry>
 443         <varlistentry>
 444           <term>Action:</term>
 445           <listitem>
 446             <para>it closes the current sequent using <command>p</command>.</para>
 447           </listitem>
 448         </varlistentry>
 449         <varlistentry>
 450           <term>New sequents to prove:</term>
 451           <listitem>
 452             <para>none.</para>
 453           </listitem>
 454         </varlistentry>
 455       </variablelist>
 456     </para>
 457   </sect1>
 458   <sect1 id="tac_exists">
 459     <title>exists</title>
 460     <titleabbrev>exists</titleabbrev>
 461     <para><userinput>exists </userinput></para>
 462     <para>
 463       <variablelist>
 464         <varlistentry>
 465           <term>Pre-conditions:</term>
 466           <listitem>
 467             <para>the conclusion of the current sequent must be
 468              an inductive type or the application of an inductive type.</para>
 469           </listitem>
 470         </varlistentry>
 471         <varlistentry>
 472           <term>Action:</term>
 473           <listitem>
 474             <para>equivalent to <command>constructor 1</command>.</para>
 475           </listitem>
 476         </varlistentry>
 477         <varlistentry>
 478           <term>New sequents to prove:</term>
 479           <listitem>
 480             <para>it opens a new sequent for each premise of the first
 481              constructor of the inductive type that is the conclusion of the
 482              current sequent. For more details, see the <command>constructor</command> tactic.</para>
 483           </listitem>
 484         </varlistentry>
 485       </variablelist>
 486     </para>
 487   </sect1>
 488   <sect1 id="tac_fail">
 489     <title>fail </title>
 490     <titleabbrev>failt</titleabbrev>
 491     <para><userinput>fail</userinput></para>
 492     <para>
 493       <variablelist>
 494         <varlistentry>
 495           <term>Pre-conditions:</term>
 496           <listitem>
 497             <para>none.</para>
 498           </listitem>
 499         </varlistentry>
 500         <varlistentry>
 501           <term>Action:</term>
 502           <listitem>
 503             <para>this tactic always fail.</para>
 504           </listitem>
 505         </varlistentry>
 506         <varlistentry>
 507           <term>New sequents to prove:</term>
 508           <listitem>
 509             <para>N.A.</para>
 510           </listitem>
 511         </varlistentry>
 512       </variablelist>
 513     </para>
 514   </sect1>
 515   <sect1 id="tac_fold">
 516     <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
 517     <titleabbrev>fold</titleabbrev>
 518     <para><userinput>fold red t patt</userinput></para>
 519     <para>
 520       <variablelist>
 521         <varlistentry>
 522           <term>Pre-conditions:</term>
 523           <listitem>
 524             <para>the pattern must not specify the wanted term.</para>
 525           </listitem>
 526         </varlistentry>
 527         <varlistentry>
 528           <term>Action:</term>
 529           <listitem>
 530             <para>first of all it locates all the subterms matched by
 531              <command>patt</command>. In the context of each matched subterm
 532              it disambiguates the term <command>t</command> and reduces it
 533              to its <command>red</command> normal form; then it replaces with
 534              <command>t</command> every occurrence of the normal form in the
 535              matched subterm.</para>
 536           </listitem>
 537         </varlistentry>
 538         <varlistentry>
 539           <term>New sequents to prove:</term>
 540           <listitem>
 541             <para>none.</para>
 542           </listitem>
 543         </varlistentry>
 544       </variablelist>
 545     </para>
 546   </sect1>
 547   <sect1 id="tac_fourier">
 548     <title>fourier</title>
 549     <titleabbrev>fourier</titleabbrev>
 550     <para><userinput>fourier </userinput></para>
 551     <para>
 552       <variablelist>
 553         <varlistentry>
 554           <term>Pre-conditions:</term>
 555           <listitem>
 556             <para>the conclusion of the current sequent must be a linear
 557              inequation over real numbers taken from standard library of
 558              Coq. Moreover the inequations in the hypotheses must imply the
 559              inequation in the conclusion of the current sequent.</para>
 560           </listitem>
 561         </varlistentry>
 562         <varlistentry>
 563           <term>Action:</term>
 564           <listitem>
 565             <para>it closes the current sequent by applying the Fourier method.</para>
 566           </listitem>
 567         </varlistentry>
 568         <varlistentry>
 569           <term>New sequents to prove:</term>
 570           <listitem>
 571             <para>none.</para>
 572           </listitem>
 573         </varlistentry>
 574       </variablelist>
 575     </para>
 576   </sect1>
 577   <sect1 id="tac_fwd">
 578     <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
 579     <titleabbrev>fwd</titleabbrev>
 580     <para><userinput>fwd ...TODO</userinput></para>
 581     <para>
 582       <variablelist>
 583         <varlistentry>
 584           <term>Pre-conditions:</term>
 585           <listitem>
 586             <para>TODO.</para>
 587           </listitem>
 588         </varlistentry>
 589         <varlistentry>
 590           <term>Action:</term>
 591           <listitem>
 592             <para>TODO.</para>
 593           </listitem>
 594         </varlistentry>
 595         <varlistentry>
 596           <term>New sequents to prove:</term>
 597           <listitem>
 598             <para>TODO.</para>
 599           </listitem>
 600         </varlistentry>
 601       </variablelist>
 602     </para>
 603   </sect1>
 604   <sect1 id="tac_generalize">
 605     <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
 606     <titleabbrev>generalize</titleabbrev>
 607     <para><userinput>generalize patt as H</userinput></para>
 608     <para>
 609       <variablelist>
 610         <varlistentry>
 611           <term>Pre-conditions:</term>
 612           <listitem>
 613             <para>all the terms matched by <command>patt</command> must be
 614              convertible and close in the context of the current sequent.</para>
 615           </listitem>
 616         </varlistentry>
 617         <varlistentry>
 618           <term>Action:</term>
 619           <listitem>
 620             <para>it closes the current sequent by applying a stronger
 621              lemma that is proved using the new generated sequent.</para>
 622           </listitem>
 623         </varlistentry>
 624         <varlistentry>
 625           <term>New sequents to prove:</term>
 626           <listitem>
 627             <para>it opens a new sequent where the current sequent conclusion
 628              <command>G</command> is generalized to
 629              <command>∀x.G{x/t}</command> where <command>{x/t}</command>
 630              is a notation for the replacement with <command>x</command> of all
 631              the occurrences of the term <command>t</command> matched by
 632              <command>patt</command>. If <command>patt</command> matches no
 633              subterm then <command>t</command> is defined as the
 634              <command>wanted</command> part of the pattern.</para>
 635           </listitem>
 636         </varlistentry>
 637       </variablelist>
 638     </para>
 639   </sect1>
 640   <sect1 id="tac_id">
 641     <title>id</title>
 642     <titleabbrev>id</titleabbrev>
 643     <para><userinput>absurd P</userinput></para>
 644     <para>
 645       <variablelist>
 646         <varlistentry>
 647           <term>Pre-conditions:</term>
 648           <listitem>
 649             <para>none.</para>
 650           </listitem>
 651         </varlistentry>
 652         <varlistentry>
 653           <term>Action:</term>
 654           <listitem>
 655             <para>this identity tactic does nothing without failing.</para>
 656           </listitem>
 657         </varlistentry>
 658         <varlistentry>
 659           <term>New sequents to prove:</term>
 660           <listitem>
 661             <para>none.</para>
 662           </listitem>
 663         </varlistentry>
 664       </variablelist>
 665     </para>
 666   </sect1>
 667   <sect1 id="tac_injection">
 668     <title>injection &lt;term&gt;</title>
 669     <titleabbrev>injection</titleabbrev>
 670     <para><userinput>injection p</userinput></para>
 671     <para>
 672       <variablelist>
 673         <varlistentry>
 674           <term>Pre-conditions:</term>
 675           <listitem>
 676             <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
 677 <command>K</command> takes no arguments.</para>
 678           </listitem>
 679         </varlistentry>
 680         <varlistentry>
 681           <term>Action:</term>
 682           <listitem>
 683             <para>it derives new hypotheses by injectivity of
 684              <command>K</command>.</para>
 685           </listitem>
 686         </varlistentry>
 687         <varlistentry>
 688           <term>New sequents to prove:</term>
 689           <listitem>
 690             <para>the new sequent to prove is equal to the current sequent
 691              with the additional hypotheses
 692              <command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
 693           </listitem>
 694         </varlistentry>
 695       </variablelist>
 696     </para>
 697   </sect1>
 698   <sect1 id="tac_intro">
 699     <title>intro [&lt;ident&gt;]</title>
 700     <titleabbrev>intro</titleabbrev>
 701     <para><userinput>intro H</userinput></para>
 702     <para>
 703       <variablelist>
 704         <varlistentry>
 705           <term>Pre-conditions:</term>
 706           <listitem>
 707             <para>the conclusion of the sequent to prove must be an implication
 708              or a universal quantification.</para>
 709           </listitem>
 710         </varlistentry>
 711         <varlistentry>
 712           <term>Action:</term>
 713           <listitem>
 714             <para>it applies the right introduction rule for implication,
 715              closing the current sequent.</para>
 716           </listitem>
 717         </varlistentry>
 718         <varlistentry>
 719           <term>New sequents to prove:</term>
 720           <listitem>
 721             <para>it opens a new sequent to prove adding to the hypothesis
 722              the antecedent of the implication and setting the conclusion
 723              to the consequent of the implicaiton. The name of the new
 724              hypothesis is <command>H</command> if provided; otherwise it
 725              is automatically generated.</para>
 726           </listitem>
 727         </varlistentry>
 728       </variablelist>
 729     </para>
 730   </sect1>
 731   <sect1 id="tac_intros">
 732     <title>intros &lt;intros_spec&gt;</title>
 733     <titleabbrev>intros</titleabbrev>
 734     <para><userinput>intros hyps</userinput></para>
 735     <para>
 736       <variablelist>
 737         <varlistentry>
 738           <term>Pre-conditions:</term>
 739           <listitem>
 740             <para>If <command>hyps</command> specifies a number of hypotheses
 741              to introduce, then the conclusion of the current sequent must
 742              be formed by at least that number of imbricated implications
 743              or universal quantifications.</para>
 744           </listitem>
 745         </varlistentry>
 746         <varlistentry>
 747           <term>Action:</term>
 748           <listitem>
 749             <para>it applies several times the right introduction rule for
 750              implication, closing the current sequent.</para>
 751           </listitem>
 752         </varlistentry>
 753         <varlistentry>
 754           <term>New sequents to prove:</term>
 755           <listitem>
 756             <para>it opens a new sequent to prove adding a number of new
 757              hypotheses equal to the number of new hypotheses requested.
 758              If the user does not request a precise number of new hypotheses,
 759              it adds as many hypotheses as possible.
 760              The name of each new hypothesis is either popped from the
 761              user provided list of names, or it is automatically generated when
 762              the list is (or becomes) empty.</para>
 763           </listitem>
 764         </varlistentry>
 765       </variablelist>
 766     </para>
 767   </sect1>
 768   <sect1 id="tac_inversion">
 769     <title>inversion &lt;term&gt;</title>
 770     <titleabbrev>inversion</titleabbrev>
 771     <para><userinput>inversion t</userinput></para>
 772     <para>
 773       <variablelist>
 774         <varlistentry>
 775           <term>Pre-conditions:</term>
 776           <listitem>
 777             <para>the type of the term <command>t</command> must be an inductive
 778              type or the application of an inductive type.</para>
 779           </listitem>
 780         </varlistentry>
 781         <varlistentry>
 782           <term>Action:</term>
 783           <listitem>
 784             <para>it proceeds by cases on <command>t</command> paying attention
 785              to the constraints imposed by the actual &quot;right arguments&quot;
 786              of the inductive type.</para>
 787           </listitem>
 788         </varlistentry>
 789         <varlistentry>
 790           <term>New sequents to prove:</term>
 791           <listitem>
 792             <para>it opens one new sequent to prove for each case in the
 793              definition of the type of <command>t</command>. With respect to
 794              a simple elimination, each new sequent has additional hypotheses
 795              that states the equalities of the &quot;right parameters&quot;
 796              of the inductive type with terms originally present in the
 797              sequent to prove.</para>
 798           </listitem>
 799         </varlistentry>
 800       </variablelist>
 801     </para>
 802   </sect1>
 803   <sect1 id="tac_lapply">
 804     <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
 805     <titleabbrev>lapply</titleabbrev>
 806     <para><userinput>lapply ???</userinput></para>
 807     <para>
 808       <variablelist>
 809         <varlistentry>
 810           <term>Pre-conditions:</term>
 811           <listitem>
 812             <para>TODO.</para>
 813           </listitem>
 814         </varlistentry>
 815         <varlistentry>
 816           <term>Action:</term>
 817           <listitem>
 818             <para>TODO.</para>
 819           </listitem>
 820         </varlistentry>
 821         <varlistentry>
 822           <term>New sequents to prove:</term>
 823           <listitem>
 824             <para>TODO.</para>
 825           </listitem>
 826         </varlistentry>
 827       </variablelist>
 828     </para>
 829   </sect1>
 830   <sect1 id="tac_left">
 831     <title>left</title>
 832     <titleabbrev>left</titleabbrev>
 833     <para><userinput>left </userinput></para>
 834     <para>
 835       <variablelist>
 836         <varlistentry>
 837           <term>Pre-conditions:</term>
 838           <listitem>
 839             <para>the conclusion of the current sequent must be
 840              an inductive type or the application of an inductive type.</para>
 841           </listitem>
 842         </varlistentry>
 843         <varlistentry>
 844           <term>Action:</term>
 845           <listitem>
 846             <para>equivalent to <command>constructor 1</command>.</para>
 847           </listitem>
 848         </varlistentry>
 849         <varlistentry>
 850           <term>New sequents to prove:</term>
 851           <listitem>
 852             <para>it opens a new sequent for each premise of the first
 853              constructor of the inductive type that is the conclusion of the
 854              current sequent. For more details, see the <command>constructor</command> tactic.</para>
 855           </listitem>
 856         </varlistentry>
 857       </variablelist>
 858     </para>
 859   </sect1>
 860   <sect1 id="tac_letin">
 861     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
 862     <titleabbrev>letin</titleabbrev>
 863     <para>The tactic <command>letin</command> </para>
 864   </sect1>
 865   <sect1 id="tac_normalize">
 866     <title>normalize &lt;pattern&gt;</title>
 867     <titleabbrev>normalize</titleabbrev>
 868     <para>The tactic <command>normalize</command> </para>
 869   </sect1>
 870   <sect1 id="tac_paramodulation">
 871     <title>paramodulation &lt;pattern&gt;</title>
 872     <titleabbrev>paramodulation</titleabbrev>
 873     <para>The tactic <command>paramodulation</command> </para>
 874   </sect1>
 875   <sect1 id="tac_reduce">
 876     <title>reduce &lt;pattern&gt;</title>
 877     <titleabbrev>reduce</titleabbrev>
 878     <para>The tactic <command>reduce</command> </para>
 879   </sect1>
 880   <sect1 id="tac_reflexivity">
 881     <title>reflexivity</title>
 882     <titleabbrev>reflexivity</titleabbrev>
 883     <para>The tactic <command>reflexivity</command> </para>
 884   </sect1>
 885   <sect1 id="tac_replace">
 886     <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
 887     <titleabbrev>replace</titleabbrev>
 888     <para>The tactic <command>replace</command> </para>
 889   </sect1>
 890   <sect1 id="tac_rewrite">
 891     <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
 892     <titleabbrev>rewrite</titleabbrev>
 893     <para>The tactic <command>rewrite</command> </para>
 894   </sect1>
 895   <sect1 id="tac_right">
 896     <title>right</title>
 897     <titleabbrev>right</titleabbrev>
 898     <para><userinput>right </userinput></para>
 899     <para>
 900       <variablelist>
 901         <varlistentry>
 902           <term>Pre-conditions:</term>
 903           <listitem>
 904             <para>the conclusion of the current sequent must be
 905              an inductive type or the application of an inductive type with
 906              at least two constructors.</para>
 907           </listitem>
 908         </varlistentry>
 909         <varlistentry>
 910           <term>Action:</term>
 911           <listitem>
 912             <para>equivalent to <command>constructor 2</command>.</para>
 913           </listitem>
 914         </varlistentry>
 915         <varlistentry>
 916           <term>New sequents to prove:</term>
 917           <listitem>
 918             <para>it opens a new sequent for each premise of the second
 919              constructor of the inductive type that is the conclusion of the
 920              current sequent. For more details, see the <command>constructor</command> tactic.</para>
 921           </listitem>
 922         </varlistentry>
 923       </variablelist>
 924     </para>
 925   </sect1>
 926   <sect1 id="tac_ring">
 927     <title>ring</title>
 928     <titleabbrev>ring</titleabbrev>
 929     <para>The tactic <command>ring</command> </para>
 930   </sect1>
 931   <sect1 id="tac_simplify">
 932     <title>simplify &lt;pattern&gt;</title>
 933     <titleabbrev>simplify</titleabbrev>
 934     <para>The tactic <command>simplify</command> </para>
 935   </sect1>
 936   <sect1 id="tac_split">
 937     <title>split</title>
 938     <titleabbrev>split</titleabbrev>
 939     <para>The tactic <command>split</command> </para>
 940   </sect1>
 941   <sect1 id="tac_symmetry">
 942     <title>symmetry</title>
 943     <titleabbrev>symmetry</titleabbrev>
 944     <para>The tactic <command>symmetry</command> </para>
 945   </sect1>
 946   <sect1 id="tac_transitivity">
 947     <title>transitivity &lt;term&gt;</title>
 948     <titleabbrev>transitivity</titleabbrev>
 949     <para>The tactic <command>transitivity</command> </para>
 950   </sect1>
 951   <sect1 id="tac_unfold">
 952     <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
 953     <titleabbrev>unfold</titleabbrev>
 954     <para>The tactic <command>unfold</command> </para>
 955   </sect1>
 956   <sect1 id="tac_whd">
 957     <title>whd &lt;pattern&gt;</title>
 958     <titleabbrev>whd</titleabbrev>
 959     <para>The tactic <command>whd</command> </para>
 960   </sect1>
 961
 962 </chapter>
 963