matita/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_apply">
  14     <title>apply</title>
  15     <titleabbrev>@</titleabbrev>
  16     <para><userinput>@t</userinput></para>
  17     <para>
  18       <variablelist>
  19         <varlistentry role="tactic.synopsis">
  20           <term>Synopsis:</term>
  21           <listitem>
  22             <para><emphasis role="bold">@</emphasis> &sterm;</para>
  23           </listitem>
  24         </varlistentry>
  25         <varlistentry>
  26           <term>Pre-conditions:</term>
  27           <listitem>
  28             <para><command>t</command> must have type
  29              <command>T<subscript>1</subscript> → … →
  30               T<subscript>n</subscript> → G</command>
  31              where <command>G</command> can be unified with the conclusion
  32              of the current sequent.</para>
  33           </listitem>
  34         </varlistentry>
  35         <varlistentry>
  36           <term>Action:</term>
  37           <listitem>
  38             <para>It closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
  39           </listitem>
  40         </varlistentry>
  41         <varlistentry>
  42           <term>New sequents to prove:</term>
  43           <listitem>
  44             <para>It opens a new sequent for each premise
  45              <command>T<subscript>i</subscript></command> that is not
  46              instantiated by unification. <command>T<subscript>i</subscript></command> is
  47              the conclusion of the <command>i</command>-th new sequent to
  48              prove.</para>
  49           </listitem>
  50         </varlistentry>
  51       </variablelist>
  52     </para>
  53   </sect1>
  54   <sect1 id="tac_auto">
  55     <title>auto</title>
  56     <titleabbrev>//</titleabbrev>
  57     <para><userinput>/params/</userinput></para>
  58     <para>
  59       <variablelist>
  60         <varlistentry role="tactic.synopsis">
  61           <term>Synopsis:</term>
  62           <listitem>
  63             <para><emphasis role="bold">/</emphasis>&autoparams;<emphasis role="bold">/</emphasis>. </para>
  64             <!--<para><emphasis role="bold">autobatch</emphasis> &autoparams;</para>-->
  65           </listitem>
  66         </varlistentry>
  67         <varlistentry>
  68           <term>Pre-conditions:</term>
  69           <listitem>
  70             <para>None, but the tactic may fail finding a proof if every
  71              proof is in the search space that is pruned away. Pruning is
  72              controlled by the optional <command>params</command>.
  73              Moreover, only lemmas whose type signature is a subset of the
  74              signature of the current sequent are considered. The signature of
  75              a sequent is essentially the set of constats appearing in it.
  76            </para>
  77           </listitem>
  78         </varlistentry>
  79         <varlistentry>
  80           <term>Action:</term>
  81           <listitem>
  82             <para>It closes the current sequent by repeated application of
  83              rewriting steps (unless <command>paramodulation</command> is
  84              omitted), hypothesis and lemmas in the library.</para>
  85           </listitem>
  86         </varlistentry>
  87         <varlistentry>
  88           <term>New sequents to prove:</term>
  89           <listitem>
  90             <para>None</para>
  91           </listitem>
  92         </varlistentry>
  93       </variablelist>
  94     </para>
  95   </sect1>
  96   <sect1 id="tac_intro">
  97     <title>intro</title>
  98     <titleabbrev>#</titleabbrev>
  99     <para><userinput>#H</userinput></para>
 100     <para>
 101       <variablelist>
 102         <varlistentry role="tactic.synopsis">
 103           <term>Synopsis:</term>
 104           <listitem>
 105             <para><emphasis role="bold">#</emphasis>&id;</para>
 106           </listitem>
 107         </varlistentry>
 108         <varlistentry>
 109           <term>Pre-conditions:</term>
 110           <listitem>
 111             <para>The conclusion of the sequent to prove must be an implication
 112              or a universal quantification.</para>
 113           </listitem>
 114         </varlistentry>
 115         <varlistentry>
 116           <term>Action:</term>
 117           <listitem>
 118             <para>It applies the right introduction rule for implication,
 119              closing the current sequent.</para>
 120           </listitem>
 121         </varlistentry>
 122         <varlistentry>
 123           <term>New sequents to prove:</term>
 124           <listitem>
 125             <para>It opens a new sequent to prove adding to the hypothesis
 126              the antecedent of the implication and setting the conclusion
 127              to the consequent of the implicaiton. The name of the new
 128              hypothesis is <command>H</command>.</para>
 129           </listitem>
 130         </varlistentry>
 131       </variablelist>
 132     </para>
 133   </sect1>
 134   <sect1 id="tac_intro_clear">
 135     <title>intro_clear</title>
 136     <titleabbrev>#_</titleabbrev>
 137     <para><userinput>#_</userinput></para>
 138     <para>
 139       <variablelist>
 140         <varlistentry role="tactic.synopsis">
 141           <term>Synopsis:</term>
 142           <listitem>
 143             <para><emphasis role="bold">#_</emphasis></para>
 144           </listitem>
 145         </varlistentry>
 146         <varlistentry>
 147           <term>Pre-conditions:</term>
 148           <listitem>
 149             <para>The conclusion of the sequent to prove must be an implication.
 150             </para>
 151           </listitem>
 152         </varlistentry>
 153         <varlistentry>
 154           <term>Action:</term>
 155           <listitem>
 156             <para>It applies the ``a fortiori'' rule for implication,
 157              closing the current sequent.</para>
 158           </listitem>
 159         </varlistentry>
 160         <varlistentry>
 161           <term>New sequents to prove:</term>
 162           <listitem>
 163             <para>It opens a new sequent whose conclusion is the conclusion
 164              of the implication of the original sequent.</para>
 165           </listitem>
 166         </varlistentry>
 167       </variablelist>
 168     </para>
 169   </sect1>
 170   <sect1 id="macro_intro">
 171     <title>macro_input</title>
 172     <titleabbrev>##</titleabbrev>
 173     <para><userinput>##</userinput></para>
 174     <para>
 175       <variablelist>
 176         <varlistentry role="tactic.synopsis">
 177           <term>Synopsis:</term>
 178           <listitem>
 179             <para><emphasis role="bold">##</emphasis></para>
 180           </listitem>
 181         </varlistentry>
 182         <varlistentry>
 183           <term>Pre-conditions:</term>
 184           <listitem>
 185             <para>None.</para>
 186           </listitem>
 187         </varlistentry>
 188         <varlistentry>
 189           <term>Action:</term>
 190           <listitem>
 191             <para>This macro expands to the longest possible list of
 192              <command>#H<subscript>i</subscript></command> tactics. The
 193              names of the introduced hypotheses are automatically
 194              generated.</para>
 195           </listitem>
 196         </varlistentry>
 197       </variablelist>
 198     </para>
 199   </sect1>
 200   <sect1 id="tac_clear">
 201     <title>clear</title>
 202     <titleabbrev>-</titleabbrev>
 203     <para><userinput>-H</userinput></para>
 204     <para>
 205       <variablelist>
 206         <varlistentry role="tactic.synopsis">
 207           <term>Synopsis:</term>
 208           <listitem>
 209             <para>
 210              <emphasis role="bold">-</emphasis>&id;
 211             </para>
 212           </listitem>
 213         </varlistentry>
 214         <varlistentry>
 215           <term>Pre-conditions:</term>
 216           <listitem>
 217             <para>
 218              <command>H</command> must be an hypothesis of the
 219              current sequent to prove.
 220             </para>
 221           </listitem>
 222         </varlistentry>
 223         <varlistentry>
 224           <term>Action:</term>
 225           <listitem>
 226             <para>
 227              It hides the hypothesis <command>H</command>
 228              from the current sequent.
 229             </para>
 230           </listitem>
 231         </varlistentry>
 232         <varlistentry>
 233           <term>New sequents to prove:</term>
 234           <listitem>
 235             <para>None</para>
 236           </listitem>
 237         </varlistentry>
 238       </variablelist>
 239     </para>
 240   </sect1>
 241   <sect1 id="tac_constructor">
 242     <title>constructor</title>
 243     <titleabbrev>%</titleabbrev>
 244     <para><userinput>%n {args}</userinput></para>
 245     <para>
 246       <variablelist>
 247         <varlistentry role="tactic.synopsis">
 248           <term>Synopsis:</term>
 249           <listitem>
 250             <para><emphasis role="bold">%</emphasis> [&nat;] [<emphasis role="bol">{</emphasis>&sterm;…<emphasis role="bol">}</emphasis>]</para>
 251           </listitem>
 252         </varlistentry>
 253         <varlistentry>
 254           <term>Pre-conditions:</term>
 255           <listitem>
 256             <para>The conclusion of the current sequent must be
 257              an inductive type or the application of an inductive type with
 258              at least <command>n</command> constructors.</para>
 259           </listitem>
 260         </varlistentry>
 261         <varlistentry>
 262           <term>Action:</term>
 263           <listitem>
 264             <para>It applies the <command>n</command>-th constructor of the
 265              inductive type of the conclusion of the current sequent to
 266              the arguments <command>args</command>.
 267              If <command>n</command> is omitted, it defaults to 1.</para>
 268           </listitem>
 269         </varlistentry>
 270         <varlistentry>
 271           <term>New sequents to prove:</term>
 272           <listitem>
 273             <para>It opens a new sequent for each premise of the constructor
 274              that can not be inferred by unification. For more details,
 275              see the <command>apply</command> tactic.</para>
 276           </listitem>
 277         </varlistentry>
 278       </variablelist>
 279     </para>
 280   </sect1>
 281   <sect1 id="tac_decompose">
 282     <title>decompose</title>
 283     <titleabbrev>*</titleabbrev>
 284     <para><userinput>
 285      * as H
 286     </userinput></para>
 287     <para>
 288       <variablelist>
 289         <varlistentry role="tactic.synopsis">
 290           <term>Synopsis:</term>
 291           <listitem>
 292             <para>
 293              <emphasis role="bold">*</emphasis>
 294              [<emphasis role="bold">as</emphasis> &id;]
 295             </para>
 296           </listitem>
 297         </varlistentry>
 298         <varlistentry>
 299           <term>Pre-conditions:</term>
 300           <listitem>
 301             <para>The current conclusion must be of the form
 302              <command>T → G</command> where <command>I</command> is
 303              an inductive type applied to its arguments, if any.</para>
 304           </listitem>
 305         </varlistentry>
 306         <varlistentry>
 307           <term>Action:</term>
 308           <listitem>
 309             <para>
 310              It introduces a new hypothesis <command>H</command> of type
 311              <command>T</command>. Then it proceeds by cases over
 312              <command>H</command>. Finally, if the name <command>H</command>
 313              is not specified, it clears the new hypothesis from all contexts.
 314             </para>
 315           </listitem>
 316         </varlistentry>
 317         <varlistentry>
 318           <term>New sequents to prove:</term>
 319           <listitem>
 320             <para>
 321              The ones generated by case analysis.
 322             </para>
 323           </listitem>
 324         </varlistentry>
 325       </variablelist>
 326     </para>
 327   </sect1>
 328   <sect1 id="tac_rewrite">
 329     <title>rewrite</title>
 330     <titleabbrev>></titleabbrev>
 331     <para><userinput>> p patt</userinput></para>
 332     <para>
 333       <variablelist>
 334         <varlistentry role="tactic.synopsis">
 335           <term>Synopsis:</term>
 336           <listitem>
 337             <para>[<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] &sterm; &pattern;</para>
 338           </listitem>
 339         </varlistentry>
 340         <varlistentry>
 341           <term>Pre-conditions:</term>
 342           <listitem>
 343             <para><command>p</command> must be the proof of an equality,
 344              possibly under some hypotheses.</para>
 345           </listitem>
 346         </varlistentry>
 347         <varlistentry>
 348           <term>Action:</term>
 349           <listitem>
 350             <para>It looks in every term matched by <command>patt</command>
 351              for all the occurrences of the
 352              left hand side of the equality that <command>p</command> proves
 353              (resp. the right hand side if <command>&lt;</command> is used).
 354              Every occurence found is replaced with
 355              the opposite side of the equality.</para>
 356           </listitem>
 357         </varlistentry>
 358         <varlistentry>
 359           <term>New sequents to prove:</term>
 360           <listitem>
 361             <para>It opens one new sequent for each hypothesis of the
 362              equality proved by <command>p</command> that is not closed
 363              by unification.</para>
 364           </listitem>
 365         </varlistentry>
 366       </variablelist>
 367     </para>
 368   </sect1>
 369   <sect1 id="tac_applyS">
 370     <title>applyS</title>
 371     <titleabbrev>applyS</titleabbrev>
 372     <para><userinput>applyS t auto_params</userinput></para>
 373     <para>
 374       <variablelist>
 375         <varlistentry role="tactic.synopsis">
 376           <term>Synopsis:</term>
 377           <listitem>
 378             <para><emphasis role="bold">applyS</emphasis> &sterm; &autoparams;</para>
 379           </listitem>
 380         </varlistentry>
 381         <varlistentry>
 382           <term>Pre-conditions:</term>
 383           <listitem>
 384             <para><command>t</command> must have type
 385              <command>T<subscript>1</subscript> → ... →
 386               T<subscript>n</subscript> → G</command>.</para>
 387           </listitem>
 388         </varlistentry>
 389         <varlistentry>
 390           <term>Action:</term>
 391           <listitem>
 392             <para><command>applyS</command> is useful when
 393              <command>apply</command> fails because the current goal
 394              and the conclusion of the applied theorems are extensionally
 395              equivalent up to instantiation of metavariables, but cannot
 396              be unified. E.g. the goal is <command>P(n*O+m)</command> and
 397              the theorem to be applied proves <command>∀m.P(m+O)</command>.
 398             </para>
 399             <para>
 400              It tries to automatically rewrite the current goal using
 401              <link linkend="tac_auto">auto paramodulation</link>
 402              to make it unifiable with <command>G</command>.
 403              Then it closes the current sequent by applying
 404              <command>t</command> to <command>n</command>
 405              implicit arguments (that become new sequents).
 406              The <command>auto_params</command> parameters are passed
 407              directly to <command>auto paramodulation</command>.
 408             </para>
 409           </listitem>
 410         </varlistentry>
 411         <varlistentry>
 412           <term>New sequents to prove:</term>
 413           <listitem>
 414             <para>It opens a new sequent for each premise
 415              <command>T<subscript>i</subscript></command> that is not
 416              instantiated by unification. <command>T<subscript>i</subscript></command> is
 417              the conclusion of the <command>i</command>-th new sequent to
 418              prove.</para>
 419           </listitem>
 420         </varlistentry>
 421       </variablelist>
 422     </para>
 423   </sect1>
 424   <sect1 id="tac_assumption">
 425     <title>assumption</title>
 426     <titleabbrev>assumption</titleabbrev>
 427     <para><userinput>assumption </userinput></para>
 428     <para>
 429       <variablelist>
 430         <varlistentry role="tactic.synopsis">
 431           <term>Synopsis:</term>
 432           <listitem>
 433             <para><emphasis role="bold">assumption</emphasis></para>
 434           </listitem>
 435         </varlistentry>
 436         <varlistentry>
 437           <term>Pre-conditions:</term>
 438           <listitem>
 439             <para>There must exist an hypothesis whose type can be unified with
 440              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 exploiting an hypothesis.</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_cases">
 459     <title>cases</title>
 460     <titleabbrev>cases</titleabbrev>
 461     <para><userinput>
 462      cases t pattern
 463     </userinput></para>
 464     <para>
 465       <variablelist>
 466         <varlistentry role="tactic.synopsis">
 467           <term>Synopsis:</term>
 468           <listitem>
 469             <para>
 470              <emphasis role="bold">cases</emphasis>
 471              &term; &pattern;
 472             </para>
 473           </listitem>
 474         </varlistentry>
 475         <varlistentry>
 476           <term>Pre-conditions:</term>
 477           <listitem>
 478             <para>
 479              <command>t</command> must inhabit an inductive type
 480             </para>
 481           </listitem>
 482         </varlistentry>
 483         <varlistentry>
 484           <term>Action:</term>
 485           <listitem>
 486             <para>
 487              It proceed by cases on <command>t</command>. The new generated
 488              hypothesis in each branch are named according to
 489              <command>hyps</command>.
 490              The elimintation predicate is restricted by
 491              <command>pattern</command>. In particular, if some hypothesis
 492              is listed in <command>pattern</command>, the hypothesis is
 493              generalized and cleared before proceeding by cases on
 494              <command>t</command>. Currently, we only support patterns of the
 495              form <command>H<subscript>1</subscript> … H<subscript>n</subscript> ⊢ %</command>. This limitation will be lifted in the future.
 496             </para>
 497           </listitem>
 498         </varlistentry>
 499         <varlistentry>
 500           <term>New sequents to prove:</term>
 501           <listitem>
 502             <para>One new sequent for each constructor of the type of
 503              <command>t</command>. Each sequent has a new hypothesis for
 504              each argument of the constructor.</para>
 505           </listitem>
 506         </varlistentry>
 507       </variablelist>
 508     </para>
 509   </sect1>
 510   <!--
 511   <sect1 id="tac_clearbody">
 512     <title>clearbody</title>
 513     <titleabbrev>clearbody</titleabbrev>
 514     <para><userinput>clearbody H</userinput></para>
 515     <para>
 516       <variablelist>
 517         <varlistentry role="tactic.synopsis">
 518           <term>Synopsis:</term>
 519           <listitem>
 520             <para><emphasis role="bold">clearbody</emphasis> &id;</para>
 521           </listitem>
 522         </varlistentry>
 523         <varlistentry>
 524           <term>Pre-conditions:</term>
 525           <listitem>
 526             <para><command>H</command> must be an hypothesis of the
 527              current sequent to prove.</para>
 528           </listitem>
 529         </varlistentry>
 530         <varlistentry>
 531           <term>Action:</term>
 532           <listitem>
 533             <para>It hides the definiens of a definition in the current
 534              sequent context. Thus the definition becomes an hypothesis.</para>
 535           </listitem>
 536         </varlistentry>
 537         <varlistentry>
 538           <term>New sequents to prove:</term>
 539           <listitem>
 540             <para>None.</para>
 541           </listitem>
 542         </varlistentry>
 543       </variablelist>
 544     </para>
 545   </sect1>
 546   -->
 547   <!--
 548   <sect1 id="tac_compose">
 549     <title>compose</title>
 550     <titleabbrev>compose</titleabbrev>
 551     <para><userinput>compose n t1 with t2 hyps</userinput></para>
 552     <para>
 553       <variablelist>
 554         <varlistentry role="tactic.synopsis">
 555           <term>Synopsis:</term>
 556           <listitem>
 557             <para><emphasis role="bold">compose</emphasis> [&nat;] &sterm; [<emphasis role="bold">with</emphasis> &sterm;] [&intros-spec;]</para>
 558           </listitem>
 559         </varlistentry>
 560         <varlistentry>
 561           <term>Pre-conditions:</term>
 562           <listitem>
 563             <para></para>
 564           </listitem>
 565         </varlistentry>
 566         <varlistentry>
 567           <term>Action:</term>
 568           <listitem>
 569             <para>Composes t1 with t2 in every possible way
 570               <command>n</command> times introducing generated terms
 571               as if <command>intros hyps</command> was issued.</para>
 572             <para>If <command>t1:∀x:A.B[x]</command> and
 573             <command>t2:∀x,y:A.B[x]→B[y]→C[x,y]</command> it generates:
 574              <itemizedlist>
 575                 <listitem>
 576                   <para><command>λx,y:A.t2 x y (t1 x) : ∀x,y:A.B[y]→C[x,y]</command></para>
 577                 </listitem>
 578                 <listitem>
 579                   <para><command>λx,y:A.λH:B[x].t2 x y H (t1 y) : ∀x,y:A.B[x]→C[x,y]
 580                   </command></para>
 581                 </listitem>
 582              </itemizedlist>
 583           </para>
 584           <para>If <command>t2</command> is omitted it composes
 585             <command>t1</command>
 586               with every hypothesis that can be introduced.
 587               <command>n</command> iterates the process.</para>
 588           </listitem>
 589         </varlistentry>
 590         <varlistentry>
 591           <term>New sequents to prove:</term>
 592           <listitem>
 593             <para>The same, but with more hypothesis eventually introduced
 594             by the &intros-spec;.</para>
 595           </listitem>
 596         </varlistentry>
 597       </variablelist>
 598     </para>
 599   </sect1>
 600   -->
 601   <sect1 id="tac_change">
 602     <title>change</title>
 603     <titleabbrev>change</titleabbrev>
 604     <para><userinput>change patt with t</userinput></para>
 605     <para>
 606       <variablelist>
 607         <varlistentry role="tactic.synopsis">
 608           <term>Synopsis:</term>
 609           <listitem>
 610             <para><emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
 611           </listitem>
 612         </varlistentry>
 613         <varlistentry>
 614           <term>Pre-conditions:</term>
 615           <listitem>
 616             <para>Each subterm matched by the pattern must be convertible
 617              with the term <command>t</command> disambiguated in the context
 618              of the matched subterm.</para>
 619           </listitem>
 620         </varlistentry>
 621         <varlistentry>
 622           <term>Action:</term>
 623           <listitem>
 624             <para>It replaces the subterms of the current sequent matched by
 625              <command>patt</command> with the new term <command>t</command>.
 626              For each subterm matched by the pattern, <command>t</command> is
 627              disambiguated in the context of the subterm.</para>
 628           </listitem>
 629         </varlistentry>
 630         <varlistentry>
 631           <term>New sequents to prove:</term>
 632           <listitem>
 633             <para>None.</para>
 634           </listitem>
 635         </varlistentry>
 636       </variablelist>
 637     </para>
 638   </sect1>
 639   <sect1 id="tac_cut">
 640     <title>cut</title>
 641     <titleabbrev>cut</titleabbrev>
 642     <para><userinput>cut P</userinput></para>
 643     <para>
 644       <variablelist>
 645         <varlistentry role="tactic.synopsis">
 646           <term>Synopsis:</term>
 647           <listitem>
 648             <para><emphasis role="bold">cut</emphasis> &sterm;</para>
 649           </listitem>
 650         </varlistentry>
 651         <varlistentry>
 652           <term>Pre-conditions:</term>
 653           <listitem>
 654             <para><command>P</command> must be a type.</para>
 655           </listitem>
 656         </varlistentry>
 657         <varlistentry>
 658           <term>Action:</term>
 659           <listitem>
 660             <para>It closes the current sequent.</para>
 661           </listitem>
 662         </varlistentry>
 663         <varlistentry>
 664           <term>New sequents to prove:</term>
 665           <listitem>
 666             <para>It opens two new sequents. The first one has conclusion
 667              <command>P → G</command> where <command>G</command> is the
 668              old conclusion.
 669              The second sequent has conclusion <command>P</command> and
 670              hypotheses the hypotheses of the current sequent to prove.</para>
 671           </listitem>
 672         </varlistentry>
 673       </variablelist>
 674     </para>
 675   </sect1>
 676   <!--
 677   <sect1 id="tac_demodulate">
 678     <title>demodulate</title>
 679     <titleabbrev>demodulate</titleabbrev>
 680     <para><userinput>demodulate auto_params</userinput></para>
 681     <para>
 682       <variablelist>
 683         <varlistentry role="tactic.synopsis">
 684           <term>Synopsis:</term>
 685           <listitem>
 686             <para><emphasis role="bold">demodulate</emphasis> &autoparams;</para>
 687           </listitem>
 688         </varlistentry>
 689         <varlistentry>
 690           <term>Pre-conditions:</term>
 691           <listitem>
 692             <para>None.</para>
 693           </listitem>
 694         </varlistentry>
 695         <varlistentry>
 696           <term>Action:</term>
 697           <listitem>
 698             <para>&TODO;</para>
 699           </listitem>
 700         </varlistentry>
 701         <varlistentry>
 702           <term>New sequents to prove:</term>
 703           <listitem>
 704             <para>None.</para>
 705           </listitem>
 706         </varlistentry>
 707       </variablelist>
 708     </para>
 709   </sect1>
 710   -->
 711   <sect1 id="tac_destruct">
 712     <title>destruct</title>
 713     <titleabbrev>destruct</titleabbrev>
 714     <para><userinput>destruct (H<subscript>0</subscript> ... H<subscript>n</subscript>) skip (K<subscript>0</subscript> ... K<subscript>m</subscript>)</userinput></para>
 715     <para>
 716       <variablelist>
 717         <varlistentry role="tactic.synopsis">
 718           <term>Synopsis:</term>
 719           <listitem>
 720             <para><emphasis role="bold">destruct</emphasis>
 721              [<emphasis role="bold">(</emphasis>&id;…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis>&id;…<emphasis role="bold">)</emphasis>]</para>
 722           </listitem>
 723         </varlistentry>
 724         <varlistentry>
 725           <term>Pre-conditions:</term>
 726           <listitem>
 727             <para>Each hypothesis <command>H<subscript>i</subscript></command> must be either a Leibniz or a John Major equality where the two sides of the equality are possibly applied constructors of an inductive type.</para>
 728           </listitem>
 729         </varlistentry>
 730         <varlistentry>
 731           <term>Action:</term>
 732           <listitem>
 733             <para>The tactic recursively compare the two sides of each equality
 734              looking for different constructors in corresponding position.
 735              If two of them are found, the tactic closes the current sequent
 736              by proving the absurdity of <command>p</command>. Otherwise
 737              it adds a new hypothesis for each leaf of the formula that
 738              states the equality of the subformulae in the corresponding
 739              positions on the two sides of the equality. If the newly
 740              added hypothesis is an equality between a variable and a term,
 741              the variable is substituted for the term everywhere in the
 742              sequent, except for the hypotheses <command>K<subscript>j</subscript></command>, and it is then cleared from the list of hypotheses.
 743             </para>
 744           </listitem>
 745         </varlistentry>
 746         <varlistentry>
 747           <term>New sequents to prove:</term>
 748           <listitem>
 749             <para>None.</para>
 750           </listitem>
 751         </varlistentry>
 752       </variablelist>
 753     </para>
 754   </sect1>
 755   <sect1 id="tac_elim">
 756     <title>elim</title>
 757     <titleabbrev>elim</titleabbrev>
 758     <para><userinput>elim t pattern</userinput></para>
 759     <para>
 760       <variablelist>
 761         <varlistentry role="tactic.synopsis">
 762           <term>Synopsis:</term>
 763           <listitem>
 764             <para><emphasis role="bold">elim</emphasis> &sterm; &pattern;</para>
 765           </listitem>
 766         </varlistentry>
 767         <varlistentry>
 768           <term>Pre-conditions:</term>
 769           <listitem>
 770             <para><command>t</command> must inhabit an inductive type.
 771             </para>
 772           </listitem>
 773         </varlistentry>
 774         <varlistentry>
 775           <term>Action:</term>
 776           <listitem>
 777             <para>It proceeds by cases on the values of <command>t</command>,
 778              according to the most appropriate elimination principle for
 779              the current goal.
 780              The induction predicate is restricted by
 781              <command>pattern</command>. In particular, if some hypothesis
 782              is listed in <command>pattern</command>, the hypothesis is
 783              generalized and cleared before eliminating <command>t</command>
 784             </para>
 785           </listitem>
 786         </varlistentry>
 787         <varlistentry>
 788           <term>New sequents to prove:</term>
 789           <listitem>
 790             <para>It opens one new sequent for each case.</para>
 791           </listitem>
 792         </varlistentry>
 793       </variablelist>
 794     </para>
 795   </sect1>
 796   <!--
 797   <sect1 id="tac_fail">
 798     <title>fail</title>
 799     <titleabbrev>fail</titleabbrev>
 800     <para><userinput>fail</userinput></para>
 801     <para>
 802       <variablelist>
 803         <varlistentry role="tactic.synopsis">
 804           <term>Synopsis:</term>
 805           <listitem>
 806             <para><emphasis role="bold">fail</emphasis></para>
 807           </listitem>
 808         </varlistentry>
 809         <varlistentry>
 810           <term>Pre-conditions:</term>
 811           <listitem>
 812             <para>None.</para>
 813           </listitem>
 814         </varlistentry>
 815         <varlistentry>
 816           <term>Action:</term>
 817           <listitem>
 818             <para>This tactic always fail.</para>
 819           </listitem>
 820         </varlistentry>
 821         <varlistentry>
 822           <term>New sequents to prove:</term>
 823           <listitem>
 824             <para>N.A.</para>
 825           </listitem>
 826         </varlistentry>
 827       </variablelist>
 828     </para>
 829   </sect1>
 830   -->
 831   <sect1 id="tac_generalize">
 832     <title>generalize</title>
 833     <titleabbrev>generalize</titleabbrev>
 834     <para><userinput>generalize patt</userinput></para>
 835     <para>
 836       <variablelist>
 837         <varlistentry role="tactic.synopsis">
 838           <term>Synopsis:</term>
 839           <listitem>
 840             <para><emphasis role="bold">generalize</emphasis> &pattern;</para>
 841           </listitem>
 842         </varlistentry>
 843         <varlistentry>
 844           <term>Pre-conditions:</term>
 845           <listitem>
 846             <para>All the terms matched by <command>patt</command> must be
 847              convertible and close in the context of the current sequent.</para>
 848           </listitem>
 849         </varlistentry>
 850         <varlistentry>
 851           <term>Action:</term>
 852           <listitem>
 853             <para>It closes the current sequent by applying a stronger
 854              lemma that is proved using the new generated sequent.</para>
 855           </listitem>
 856         </varlistentry>
 857         <varlistentry>
 858           <term>New sequents to prove:</term>
 859           <listitem>
 860             <para>It opens a new sequent where the current sequent conclusion
 861              <command>G</command> is generalized to
 862              <command>∀x.G{x/t}</command> where <command>{x/t}</command>
 863              is a notation for the replacement with <command>x</command> of all
 864              the occurrences of the term <command>t</command> matched by
 865              <command>patt</command>. If <command>patt</command> matches no
 866              subterm then <command>t</command> is defined as the
 867              <command>wanted</command> part of the pattern.</para>
 868           </listitem>
 869         </varlistentry>
 870       </variablelist>
 871     </para>
 872   </sect1>
 873   <!--
 874   <sect1 id="tac_id">
 875     <title>id</title>
 876     <titleabbrev>id</titleabbrev>
 877     <para><userinput>id </userinput></para>
 878     <para>
 879       <variablelist>
 880         <varlistentry role="tactic.synopsis">
 881           <term>Synopsis:</term>
 882           <listitem>
 883             <para><emphasis role="bold">id</emphasis></para>
 884           </listitem>
 885         </varlistentry>
 886         <varlistentry>
 887           <term>Pre-conditions:</term>
 888           <listitem>
 889             <para>None.</para>
 890           </listitem>
 891         </varlistentry>
 892         <varlistentry>
 893           <term>Action:</term>
 894           <listitem>
 895             <para>This identity tactic does nothing without failing.</para>
 896           </listitem>
 897         </varlistentry>
 898         <varlistentry>
 899           <term>New sequents to prove:</term>
 900           <listitem>
 901             <para>None.</para>
 902           </listitem>
 903         </varlistentry>
 904       </variablelist>
 905     </para>
 906   </sect1>
 907   -->
 908   <sect1 id="tac_inversion">
 909     <title>inversion</title>
 910     <titleabbrev>inversion</titleabbrev>
 911     <para><userinput>inversion t</userinput></para>
 912     <para>
 913       <variablelist>
 914         <varlistentry role="tactic.synopsis">
 915           <term>Synopsis:</term>
 916           <listitem>
 917             <para><emphasis role="bold">inversion</emphasis> &sterm;</para>
 918           </listitem>
 919         </varlistentry>
 920         <varlistentry>
 921           <term>Pre-conditions:</term>
 922           <listitem>
 923             <para>The type of the term <command>t</command> must be an inductive
 924              type or the application of an inductive type.</para>
 925           </listitem>
 926         </varlistentry>
 927         <varlistentry>
 928           <term>Action:</term>
 929           <listitem>
 930             <para>It proceeds by cases on <command>t</command> paying attention
 931              to the constraints imposed by the actual &quot;right arguments&quot;
 932              of the inductive type.</para>
 933           </listitem>
 934         </varlistentry>
 935         <varlistentry>
 936           <term>New sequents to prove:</term>
 937           <listitem>
 938             <para>It opens one new sequent to prove for each case in the
 939              definition of the type of <command>t</command>. With respect to
 940              a simple elimination, each new sequent has additional hypotheses
 941              that states the equalities of the &quot;right parameters&quot;
 942              of the inductive type with terms originally present in the
 943              sequent to prove. It uses either Leibniz or John Major equality
 944              for the new hypotheses, according to the included files.</para>
 945           </listitem>
 946         </varlistentry>
 947       </variablelist>
 948     </para>
 949   </sect1>
 950   <sect1 id="tac_lapply">
 951     <title>lapply</title>
 952     <titleabbrev>lapply</titleabbrev>
 953     <para><userinput>
 954      lapply t
 955     </userinput></para>
 956     <para>
 957       <variablelist>
 958         <varlistentry role="tactic.synopsis">
 959           <term>Synopsis:</term>
 960           <listitem>
 961             <para>
 962              <emphasis role="bold">lapply</emphasis>
 963              &sterm;
 964             </para>
 965           </listitem>
 966         </varlistentry>
 967         <varlistentry>
 968           <term>Pre-conditions:</term>
 969           <listitem>
 970             <para>None.</para>
 971           </listitem>
 972         </varlistentry>
 973         <varlistentry>
 974           <term>Action:</term>
 975           <listitem>
 976             <para>
 977              It generalizes the conclusion of the current goal
 978              adding as a premise the type of <command>t</command>,
 979              closing the current goal.
 980             </para>
 981           </listitem>
 982         </varlistentry>
 983         <varlistentry>
 984           <term>New sequents to prove:</term>
 985           <listitem>
 986             <para>
 987              The new sequent has conclusion <command>T → G</command> where
 988              <command>T</command> is the type of <command>t</command>
 989              and <command>G</command> the old conclusion.
 990             </para>
 991           </listitem>
 992         </varlistentry>
 993       </variablelist>
 994     </para>
 995   </sect1>
 996   <sect1 id="tac_letin">
 997     <title>letin</title>
 998     <titleabbrev>letin</titleabbrev>
 999     <para><userinput>letin x ≝ t</userinput></para>
1000     <para>
1001       <variablelist>
1002         <varlistentry role="tactic.synopsis">
1003           <term>Synopsis:</term>
1004           <listitem>
1005             <para><emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm;</para>
1006           </listitem>
1007         </varlistentry>
1008         <varlistentry>
1009           <term>Pre-conditions:</term>
1010           <listitem>
1011             <para>None.</para>
1012           </listitem>
1013         </varlistentry>
1014         <varlistentry>
1015           <term>Action:</term>
1016           <listitem>
1017             <para>It adds to the context of the current sequent to prove a new
1018              definition <command>x ≝ t</command>.</para>
1019           </listitem>
1020         </varlistentry>
1021         <varlistentry>
1022           <term>New sequents to prove:</term>
1023           <listitem>
1024             <para>None.</para>
1025           </listitem>
1026         </varlistentry>
1027       </variablelist>
1028     </para>
1029   </sect1>
1030   <sect1 id="tac_normalize">
1031     <title>normalize</title>
1032     <titleabbrev>normalize</titleabbrev>
1033     <para><userinput>normalize patt nodelta</userinput></para>
1034     <para>
1035       <variablelist>
1036         <varlistentry role="tactic.synopsis">
1037           <term>Synopsis:</term>
1038           <listitem>
1039             <para><emphasis role="bold">normalize</emphasis> &pattern;
1040              [<emphasis role="bold">nodelta</emphasis>]</para>
1041           </listitem>
1042         </varlistentry>
1043         <varlistentry>
1044           <term>Pre-conditions:</term>
1045           <listitem>
1046             <para>None.</para>
1047           </listitem>
1048         </varlistentry>
1049         <varlistentry>
1050           <term>Action:</term>
1051           <listitem>
1052             <para>It replaces all the terms matched by <command>patt</command>
1053              with their βδιζ-normal form. If <command>nodelta</command> is
1054              specified, δ-expansions are not performed.</para>
1055           </listitem>
1056         </varlistentry>
1057         <varlistentry>
1058           <term>New sequents to prove:</term>
1059           <listitem>
1060             <para>None.</para>
1061           </listitem>
1062         </varlistentry>
1063       </variablelist>
1064     </para>
1065   </sect1>
1066   <sect1 id="tac_whd">
1067     <title>whd</title>
1068     <titleabbrev>whd</titleabbrev>
1069     <para><userinput>whd patt nodelta</userinput></para>
1070     <para>
1071       <variablelist>
1072         <varlistentry role="tactic.synopsis">
1073           <term>Synopsis:</term>
1074           <listitem>
1075             <para><emphasis role="bold">whd</emphasis> &pattern; [<emphasis role="bold">nodelta</emphasis>]</para>
1076           </listitem>
1077         </varlistentry>
1078         <varlistentry>
1079           <term>Pre-conditions:</term>
1080           <listitem>
1081             <para>None.</para>
1082           </listitem>
1083         </varlistentry>
1084         <varlistentry>
1085           <term>Action:</term>
1086           <listitem>
1087             <para>It replaces all the terms matched by <command>patt</command>
1088              with their βδιζ-weak-head normal form. If <command>nodelta</command> is specified, δ-expansions are not performed.</para>
1089           </listitem>
1090         </varlistentry>
1091         <varlistentry>
1092           <term>New sequents to prove:</term>
1093           <listitem>
1094             <para>None.</para>
1095           </listitem>
1096         </varlistentry>
1097       </variablelist>
1098     </para>
1099   </sect1>
1100
1101 </chapter>
1102