matita/help/C/sec_tactics.xml

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