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>absurd &lt;term&gt;</title>
   8     <para><userinput>absurd P</userinput></para>
   9      <para>
  10       <variablelist>
  11         <varlistentry>
  12           <term>Pre-conditions:</term>
  13           <listitem>
  14             <para><command>P</command> must have type <command>Prop</command>.</para>
  15           </listitem>
  16         </varlistentry>
  17         <varlistentry>
  18           <term>Action:</term>
  19           <listitem>
  20             <para>it closes the current sequent by eliminating an
  21              absurd term.</para>
  22           </listitem>
  23         </varlistentry>
  24         <varlistentry>
  25           <term>New sequents to prove:</term>
  26           <listitem>
  27             <para>it opens two new sequents of conclusion <command>P</command>
  28              and <command>¬P</command>.</para>
  29           </listitem>
  30         </varlistentry>
  31       </variablelist>
  32      </para>
  33   </sect1>
  34   <sect1 id="tac_apply">
  35     <title>apply &lt;term&gt;</title>
  36     <para><userinput>apply t</userinput></para>
  37     <para>
  38       <variablelist>
  39         <varlistentry>
  40           <term>Pre-conditions:</term>
  41           <listitem>
  42             <para><command>t</command> must have type
  43              <command>T<subscript>1</subscript> → ... →
  44               T<subscript>n</subscript> → G</command>
  45              where <command>G</command> can be unified with the conclusion
  46              of the current sequent.</para>
  47           </listitem>
  48         </varlistentry>
  49         <varlistentry>
  50           <term>Action:</term>
  51           <listitem>
  52             <para>it closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
  53           </listitem>
  54         </varlistentry>
  55         <varlistentry>
  56           <term>New sequents to prove:</term>
  57           <listitem>
  58             <para>it opens a new sequent for each premise
  59              <command>T<subscript>i</subscript></command> that is not
  60              instantiated by unification. <command>T<subscript>i</subscript></command> is
  61              the conclusion of the <command>i</command>-th new sequent to
  62              prove.</para>
  63           </listitem>
  64         </varlistentry>
  65       </variablelist>
  66     </para>
  67   </sect1>
  68   <sect1 id="tac_assumption">
  69     <title>assumption</title>
  70     <para><userinput>assumption </userinput></para>
  71     <para>
  72       <variablelist>
  73         <varlistentry>
  74           <term>Pre-conditions:</term>
  75           <listitem>
  76             <para>there must exist an hypothesis whose type can be unified with
  77              the conclusion of the current sequent.</para>
  78           </listitem>
  79         </varlistentry>
  80         <varlistentry>
  81           <term>Action:</term>
  82           <listitem>
  83             <para>it closes the current sequent exploiting an hypothesis.</para>
  84           </listitem>
  85         </varlistentry>
  86         <varlistentry>
  87           <term>New sequents to prove:</term>
  88           <listitem>
  89             <para>none</para>
  90           </listitem>
  91         </varlistentry>
  92       </variablelist>
  93     </para>
  94   </sect1>
  95   <sect1 id="tac_auto">
  96     <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
  97     <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
  98     <para>
  99       <variablelist>
 100         <varlistentry>
 101           <term>Pre-conditions:</term>
 102           <listitem>
 103             <para>none, but the tactic may fail finding a proof if every
 104              proof is in the search space that is pruned away. Pruning is
 105              controlled by <command>d</command> and <command>w</command>.
 106              Moreover, only lemmas whose type signature is a subset of the
 107              signature of the current sequent are considered. The signature of
 108              a sequent is ...TODO</para>
 109           </listitem>
 110         </varlistentry>
 111         <varlistentry>
 112           <term>Action:</term>
 113           <listitem>
 114             <para>it closes the current sequent by repeated application of
 115              rewriting steps (unless <command>paramodulation</command> is
 116              omitted), hypothesis and lemmas in the library.</para>
 117           </listitem>
 118         </varlistentry>
 119         <varlistentry>
 120           <term>New sequents to prove:</term>
 121           <listitem>
 122             <para>none</para>
 123           </listitem>
 124         </varlistentry>
 125       </variablelist>
 126     </para>
 127   </sect1>
 128   <sect1 id="tac_clear">
 129     <title>clear &lt;id&gt;</title>
 130     <para><userinput>clear H</userinput></para>
 131     <para>
 132       <variablelist>
 133         <varlistentry>
 134           <term>Pre-conditions:</term>
 135           <listitem>
 136             <para><command>H</command> must be an hypothesis of the
 137              current sequent to prove.</para>
 138           </listitem>
 139         </varlistentry>
 140         <varlistentry>
 141           <term>Action:</term>
 142           <listitem>
 143             <para>it hides the hypothesis <command>H</command> from the
 144              current sequent.</para>
 145           </listitem>
 146         </varlistentry>
 147         <varlistentry>
 148           <term>New sequents to prove:</term>
 149           <listitem>
 150             <para>none</para>
 151           </listitem>
 152         </varlistentry>
 153       </variablelist>
 154     </para>
 155   </sect1>
 156   <sect1 id="tac_clearbody">
 157     <title>clearbody &lt;id&gt;</title>
 158     <para><userinput>clearbody H</userinput></para>
 159     <para>
 160       <variablelist>
 161         <varlistentry>
 162           <term>Pre-conditions:</term>
 163           <listitem>
 164             <para><command>H</command> must be an hypothesis of the
 165              current sequent to prove.</para>
 166           </listitem>
 167         </varlistentry>
 168         <varlistentry>
 169           <term>Action:</term>
 170           <listitem>
 171             <para>it hides the definiens of a definition in the current
 172              sequent context. Thus the definition becomes an hypothesis.</para>
 173           </listitem>
 174         </varlistentry>
 175         <varlistentry>
 176           <term>New sequents to prove:</term>
 177           <listitem>
 178             <para>none.</para>
 179           </listitem>
 180         </varlistentry>
 181       </variablelist>
 182     </para>
 183   </sect1>
 184   <sect1 id="tac_change">
 185     <title>change &lt;pattern&gt; with &lt;term&gt;</title>
 186     <para><userinput>change patt with t</userinput></para>
 187     <para>
 188       <variablelist>
 189         <varlistentry>
 190           <term>Pre-conditions:</term>
 191           <listitem>
 192             <para>each subterm matched by the pattern must be convertible
 193              with the term <command>t</command> disambiguated in the context
 194              of the matched subterm.</para>
 195           </listitem>
 196         </varlistentry>
 197         <varlistentry>
 198           <term>Action:</term>
 199           <listitem>
 200             <para>it replaces the subterms of the current sequent matched by
 201              <command>patt</command> with the new term <command>t</command>.
 202              For each subterm matched by the pattern, <command>t</command> is
 203              disambiguated in the context of the subterm.</para>
 204           </listitem>
 205         </varlistentry>
 206         <varlistentry>
 207           <term>New sequents to prove:</term>
 208           <listitem>
 209             <para>none.</para>
 210           </listitem>
 211         </varlistentry>
 212       </variablelist>
 213     </para>
 214   </sect1>
 215   <sect1 id="tac_constructor">
 216     <title>constructor &lt;int&gt;</title>
 217     <para><userinput>constructor n</userinput></para>
 218     <para>
 219       <variablelist>
 220         <varlistentry>
 221           <term>Pre-conditions:</term>
 222           <listitem>
 223             <para>the conclusion of the current sequent must be
 224              an inductive type or the application of an inductive type.</para>
 225           </listitem>
 226         </varlistentry>
 227         <varlistentry>
 228           <term>Action:</term>
 229           <listitem>
 230             <para>it applies the <command>n</command>-th constructor of the
 231              inductive type of the conclusion of the current sequent.</para>
 232           </listitem>
 233         </varlistentry>
 234         <varlistentry>
 235           <term>New sequents to prove:</term>
 236           <listitem>
 237             <para>it opens a new sequent for each premise of the constructor
 238              that can not be inferred by unification. For more details,
 239              see the <command>apply</command> tactic.</para>
 240           </listitem>
 241         </varlistentry>
 242       </variablelist>
 243     </para>
 244   </sect1>
 245   <sect1 id="tac_contradiction">
 246     <title>contradiction</title>
 247     <para><userinput>contradiction </userinput></para>
 248     <para>
 249       <variablelist>
 250         <varlistentry>
 251           <term>Pre-conditions:</term>
 252           <listitem>
 253             <para>there must be in the current context an hypothesis of type
 254              <command>False</command>.</para>
 255           </listitem>
 256         </varlistentry>
 257         <varlistentry>
 258           <term>Action:</term>
 259           <listitem>
 260             <para>it closes the current sequent by applying an hypothesis of
 261              type <command>False</command>.</para>
 262           </listitem>
 263         </varlistentry>
 264         <varlistentry>
 265           <term>New sequents to prove:</term>
 266           <listitem>
 267             <para>none</para>
 268           </listitem>
 269         </varlistentry>
 270       </variablelist>
 271     </para>
 272   </sect1>
 273   <sect1 id="tac_cut">
 274     <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
 275     <para><userinput>cut P as H</userinput></para>
 276     <para>
 277       <variablelist>
 278         <varlistentry>
 279           <term>Pre-conditions:</term>
 280           <listitem>
 281             <para><command>P</command> must have type <command>Prop</command>.</para>
 282           </listitem>
 283         </varlistentry>
 284         <varlistentry>
 285           <term>Action:</term>
 286           <listitem>
 287             <para>it closes the current sequent.</para>
 288           </listitem>
 289         </varlistentry>
 290         <varlistentry>
 291           <term>New sequents to prove:</term>
 292           <listitem>
 293             <para>it opens two new sequents. The first one has an extra
 294              hypothesis <command>H:P</command>. If <command>H</command> is
 295              omitted, the name of the hypothesis is automatically generated.
 296              The second sequent has conclusion <command>P</command> and
 297              hypotheses the hypotheses of the current sequent to prove.</para>
 298           </listitem>
 299         </varlistentry>
 300       </variablelist>
 301     </para>
 302   </sect1>
 303   <sect1 id="tac_decompose">
 304     <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
 305     <para><userinput>decompose ???</userinput></para>
 306     <para>
 307       <variablelist>
 308         <varlistentry>
 309           <term>Pre-conditions:</term>
 310           <listitem>
 311             <para>TODO.</para>
 312           </listitem>
 313         </varlistentry>
 314         <varlistentry>
 315           <term>Action:</term>
 316           <listitem>
 317             <para>TODO.</para>
 318           </listitem>
 319         </varlistentry>
 320         <varlistentry>
 321           <term>New sequents to prove:</term>
 322           <listitem>
 323             <para>TODO.</para>
 324           </listitem>
 325         </varlistentry>
 326       </variablelist>
 327     </para>
 328   </sect1>
 329   <sect1 id="tac_discriminate">
 330     <title>discriminate &lt;term&gt;</title>
 331     <para><userinput>discriminate p</userinput></para>
 332     <para>
 333       <variablelist>
 334         <varlistentry>
 335           <term>Pre-conditions:</term>
 336           <listitem>
 337             <para><command>p</command> must have type <command>K<subscript>1</subscript> t<subscript>1</subscript> ... t<subscript>n</subscript> = K'<subscript>1</subscript> 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
 338 its constructor takes no arguments.</para>
 339           </listitem>
 340         </varlistentry>
 341         <varlistentry>
 342           <term>Action:</term>
 343           <listitem>
 344             <para>it closes the current sequent by proving the absurdity of
 345              <command>p</command>.</para>
 346           </listitem>
 347         </varlistentry>
 348         <varlistentry>
 349           <term>New sequents to prove:</term>
 350           <listitem>
 351             <para>none.</para>
 352           </listitem>
 353         </varlistentry>
 354       </variablelist>
 355     </para>
 356   </sect1>
 357   <sect1 id="tac_elim">
 358     <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
 359     <para><userinput>elim t using th hyps</userinput></para>
 360     <para>
 361       <variablelist>
 362         <varlistentry>
 363           <term>Pre-conditions:</term>
 364           <listitem>
 365             <para><command>t</command> must inhabit an inductive type and
 366              <command>th</command> must be an elimination principle for that
 367              inductive type. If <command>th</command> is omitted the appropriate
 368              standard elimination principle is chosen.</para>
 369           </listitem>
 370         </varlistentry>
 371         <varlistentry>
 372           <term>Action:</term>
 373           <listitem>
 374             <para>it proceeds by cases on the values of <command>t</command>,
 375              according to the elimination principle <command>th</command>.
 376             </para>
 377           </listitem>
 378         </varlistentry>
 379         <varlistentry>
 380           <term>New sequents to prove:</term>
 381           <listitem>
 382             <para>it opens one new sequent for each case. The names of
 383              the new hypotheses are picked by <command>hyps</command>, if
 384              provided.</para>
 385           </listitem>
 386         </varlistentry>
 387       </variablelist>
 388     </para>
 389   </sect1>
 390   <sect1 id="tac_elimType">
 391     <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
 392     <para><userinput>elimType T using th</userinput></para>
 393     <para>
 394       <variablelist>
 395         <varlistentry>
 396           <term>Pre-conditions:</term>
 397           <listitem>
 398             <para><command>T</command> must be an inductive type.</para>
 399           </listitem>
 400         </varlistentry>
 401         <varlistentry>
 402           <term>Action:</term>
 403           <listitem>
 404             <para>TODO (severely bugged now).</para>
 405           </listitem>
 406         </varlistentry>
 407         <varlistentry>
 408           <term>New sequents to prove:</term>
 409           <listitem>
 410             <para>TODO</para>
 411           </listitem>
 412         </varlistentry>
 413       </variablelist>
 414     </para>
 415   </sect1>
 416   <sect1 id="tac_exact">
 417     <title>exact &lt;term&gt;</title>
 418     <para><userinput>exact p</userinput></para>
 419     <para>
 420       <variablelist>
 421         <varlistentry>
 422           <term>Pre-conditions:</term>
 423           <listitem>
 424             <para>the type of <command>p</command> must be convertible
 425              with the conclusion of the current sequent.</para>
 426           </listitem>
 427         </varlistentry>
 428         <varlistentry>
 429           <term>Action:</term>
 430           <listitem>
 431             <para>it closes the current sequent using <command>p</command>.</para>
 432           </listitem>
 433         </varlistentry>
 434         <varlistentry>
 435           <term>New sequents to prove:</term>
 436           <listitem>
 437             <para>none.</para>
 438           </listitem>
 439         </varlistentry>
 440       </variablelist>
 441     </para>
 442   </sect1>
 443   <sect1 id="tac_exists">
 444     <title>exists</title>
 445     <para><userinput>exists </userinput></para>
 446     <para>
 447       <variablelist>
 448         <varlistentry>
 449           <term>Pre-conditions:</term>
 450           <listitem>
 451             <para>the conclusion of the current sequent must be
 452              an inductive type or the application of an inductive type.</para>
 453           </listitem>
 454         </varlistentry>
 455         <varlistentry>
 456           <term>Action:</term>
 457           <listitem>
 458             <para>equivalent to <command>constructor 1</command>.</para>
 459           </listitem>
 460         </varlistentry>
 461         <varlistentry>
 462           <term>New sequents to prove:</term>
 463           <listitem>
 464             <para>it opens a new sequent for each premise of the first
 465              constructor of the inductive type that is the conclusion of the
 466              current sequent. For more details, see the <command>constructor</command> tactic.</para>
 467           </listitem>
 468         </varlistentry>
 469       </variablelist>
 470     </para>
 471   </sect1>
 472   <sect1 id="tac_fail">
 473     <title>fail </title>
 474     <para><userinput>fail</userinput></para>
 475     <para>
 476       <variablelist>
 477         <varlistentry>
 478           <term>Pre-conditions:</term>
 479           <listitem>
 480             <para>none.</para>
 481           </listitem>
 482         </varlistentry>
 483         <varlistentry>
 484           <term>Action:</term>
 485           <listitem>
 486             <para>this tactic always fail.</para>
 487           </listitem>
 488         </varlistentry>
 489         <varlistentry>
 490           <term>New sequents to prove:</term>
 491           <listitem>
 492             <para>N.A.</para>
 493           </listitem>
 494         </varlistentry>
 495       </variablelist>
 496     </para>
 497   </sect1>
 498   <sect1 id="tac_fold">
 499     <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
 500     <para><userinput>fold red t patt</userinput></para>
 501     <para>
 502       <variablelist>
 503         <varlistentry>
 504           <term>Pre-conditions:</term>
 505           <listitem>
 506             <para>the pattern must not specify the wanted term.</para>
 507           </listitem>
 508         </varlistentry>
 509         <varlistentry>
 510           <term>Action:</term>
 511           <listitem>
 512             <para>first of all it locates all the subterms matched by
 513              <command>patt</command>. In the context of each matched subterm
 514              it disambiguates the term <command>t</command> and reduces it
 515              to its <command>red</command> normal form; then it replaces with
 516              <command>t</command> every occurrence of the normal form in the
 517              matched subterm.</para>
 518           </listitem>
 519         </varlistentry>
 520         <varlistentry>
 521           <term>New sequents to prove:</term>
 522           <listitem>
 523             <para>none.</para>
 524           </listitem>
 525         </varlistentry>
 526       </variablelist>
 527     </para>
 528   </sect1>
 529   <sect1 id="tac_fourier">
 530     <title>fourier</title>
 531     <para><userinput>fourier </userinput></para>
 532     <para>
 533       <variablelist>
 534         <varlistentry>
 535           <term>Pre-conditions:</term>
 536           <listitem>
 537             <para>the conclusion of the current sequent must be a linear
 538              inequation over real numbers taken from standard library of
 539              Coq. Moreover the inequations in the hypotheses must imply the
 540              inequation in the conclusion of the current sequent.</para>
 541           </listitem>
 542         </varlistentry>
 543         <varlistentry>
 544           <term>Action:</term>
 545           <listitem>
 546             <para>it closes the current sequent by applying the Fourier method.</para>
 547           </listitem>
 548         </varlistentry>
 549         <varlistentry>
 550           <term>New sequents to prove:</term>
 551           <listitem>
 552             <para>none.</para>
 553           </listitem>
 554         </varlistentry>
 555       </variablelist>
 556     </para>
 557   </sect1>
 558   <sect1 id="tac_fwd">
 559     <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
 560     <para><userinput>fwd ...TODO</userinput></para>
 561     <para>
 562       <variablelist>
 563         <varlistentry>
 564           <term>Pre-conditions:</term>
 565           <listitem>
 566             <para>TODO.</para>
 567           </listitem>
 568         </varlistentry>
 569         <varlistentry>
 570           <term>Action:</term>
 571           <listitem>
 572             <para>TODO.</para>
 573           </listitem>
 574         </varlistentry>
 575         <varlistentry>
 576           <term>New sequents to prove:</term>
 577           <listitem>
 578             <para>TODO.</para>
 579           </listitem>
 580         </varlistentry>
 581       </variablelist>
 582     </para>
 583   </sect1>
 584   <sect1 id="tac_generalize">
 585     <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
 586     <para>The tactic <command>generalize</command> </para>
 587   </sect1>
 588   <sect1 id="tac_id">
 589     <title>id</title>
 590     <para>The tactic <command>id</command> </para>
 591   </sect1>
 592   <sect1 id="tac_injection">
 593     <title>injection &lt;term&gt;</title>
 594     <para>The tactic <command>injection</command> </para>
 595   </sect1>
 596   <sect1 id="tac_intro">
 597     <title>intro [&lt;ident&gt;]</title>
 598     <para>The tactic <command>intro</command> </para>
 599   </sect1>
 600   <sect1 id="tac_intros">
 601     <title>intros &lt;intros_spec&gt;</title>
 602     <para>The tactic <command>intros</command> </para>
 603   </sect1>
 604   <sect1 id="tac_inversion">
 605     <title>intros &lt;term&gt;</title>
 606     <para>The tactic <command>intros</command> </para>
 607   </sect1>
 608   <sect1 id="tac_lapply">
 609     <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
 610     <para>The tactic <command>lapply</command> </para>
 611   </sect1>
 612   <sect1 id="tac_left">
 613     <title>left</title>
 614     <para>The tactic <command>left</command> </para>
 615   </sect1>
 616   <sect1 id="tac_letin">
 617     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
 618     <para>The tactic <command>letin</command> </para>
 619   </sect1>
 620   <sect1 id="tac_normalize">
 621     <title>normalize &lt;pattern&gt;</title>
 622     <para>The tactic <command>normalize</command> </para>
 623   </sect1>
 624   <sect1 id="tac_paramodulation">
 625     <title>paramodulation &lt;pattern&gt;</title>
 626     <para>The tactic <command>paramodulation</command> </para>
 627   </sect1>
 628   <sect1 id="tac_reduce">
 629     <title>reduce &lt;pattern&gt;</title>
 630     <para>The tactic <command>reduce</command> </para>
 631   </sect1>
 632   <sect1 id="tac_reflexivity">
 633     <title>reflexivity</title>
 634     <para>The tactic <command>reflexivity</command> </para>
 635   </sect1>
 636   <sect1 id="tac_replace">
 637     <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
 638     <para>The tactic <command>replace</command> </para>
 639   </sect1>
 640   <sect1 id="tac_rewrite">
 641     <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
 642     <para>The tactic <command>rewrite</command> </para>
 643   </sect1>
 644   <sect1 id="tac_right">
 645     <title>right</title>
 646     <para>The tactic <command>right</command> </para>
 647   </sect1>
 648   <sect1 id="tac_ring">
 649     <title>ring</title>
 650     <para>The tactic <command>ring</command> </para>
 651   </sect1>
 652   <sect1 id="tac_simplify">
 653     <title>simplify &lt;pattern&gt;</title>
 654     <para>The tactic <command>simplify</command> </para>
 655   </sect1>
 656   <sect1 id="tac_split">
 657     <title>split</title>
 658     <para>The tactic <command>split</command> </para>
 659   </sect1>
 660   <sect1 id="tac_symmetry">
 661     <title>symmetry</title>
 662     <para>The tactic <command>symmetry</command> </para>
 663   </sect1>
 664   <sect1 id="tac_transitivity">
 665     <title>transitivity &lt;term&gt;</title>
 666     <para>The tactic <command>transitivity</command> </para>
 667   </sect1>
 668   <sect1 id="tac_unfold">
 669     <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
 670     <para>The tactic <command>unfold</command> </para>
 671   </sect1>
 672   <sect1 id="tac_whd">
 673     <title>whd &lt;pattern&gt;</title>
 674     <para>The tactic <command>whd</command> </para>
 675   </sect1>
 676
 677 </chapter>
 678