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