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