matita/help/C/sec_tactics.xml

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