matita/help/C/sec_tactics.xml

   1
   2 <!-- ============ Tactics ====================== -->
   3 <sect1 id="sec_tactics">
   4  <title>Tactics</title>
   5
   6   <sect2 id="tac_absurd">
   7     <title>absurd &lt;term&gt;</title>
   8     <para><userinput>absurd P</userinput></para>
   9     <para>
  10         <varlistentry>
  11           <term>Pre-conditions:</term>
  12           <listitem>
  13             <para><command>P</command> must have type <command>Prop</command>.</para>
  14           </listitem>
  15         </varlistentry>
  16       <variablelist>
  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   </sect2>
  34   <sect2 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   </sect2>
  68   <sect2 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   </sect2>
  95   <sect2 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   </sect2>
 128   <sect2 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   </sect2>
 156   <sect2 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   </sect2>
 184   <sect2 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   </sect2>
 215   <sect2 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   </sect2>
 245   <sect2 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   </sect2>
 273   <sect2 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   </sect2>
 303   <sect2 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   </sect2>
 329   <sect2 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   </sect2>
 357   <sect2 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   </sect2>
 390   <sect2 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   </sect2>
 416   <sect2 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   </sect2>
 443   <sect2 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   </sect2>
 472   <sect2 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   </sect2>
 498   <sect2 id="tac_fold">
 499     <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
 500     <para>The tactic <command>fold</command> </para>
 501   </sect2>
 502   <sect2 id="tac_fourier">
 503     <title>fourier</title>
 504     <para>The tactic <command>fourier</command> </para>
 505   </sect2>
 506   <sect2 id="tac_fwd">
 507     <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
 508     <para>The tactic <command>fwd</command> </para>
 509   </sect2>
 510   <sect2 id="tac_generalize">
 511     <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
 512     <para>The tactic <command>generalize</command> </para>
 513   </sect2>
 514   <sect2 id="tac_id">
 515     <title>id</title>
 516     <para>The tactic <command>id</command> </para>
 517   </sect2>
 518   <sect2 id="tac_injection">
 519     <title>injection &lt;term&gt;</title>
 520     <para>The tactic <command>injection</command> </para>
 521   </sect2>
 522   <sect2 id="tac_intro">
 523     <title>intro [&lt;ident&gt;]</title>
 524     <para>The tactic <command>intro</command> </para>
 525   </sect2>
 526   <sect2 id="tac_intros">
 527     <title>intros &lt;intros_spec&gt;</title>
 528     <para>The tactic <command>intros</command> </para>
 529   </sect2>
 530   <sect2 id="tac_inversion">
 531     <title>intros &lt;term&gt;</title>
 532     <para>The tactic <command>intros</command> </para>
 533   </sect2>
 534   <sect2 id="tac_lapply">
 535     <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
 536     <para>The tactic <command>lapply</command> </para>
 537   </sect2>
 538   <sect2 id="tac_left">
 539     <title>left</title>
 540     <para>The tactic <command>left</command> </para>
 541   </sect2>
 542   <sect2 id="tac_letin">
 543     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
 544     <para>The tactic <command>letin</command> </para>
 545   </sect2>
 546   <sect2 id="tac_normalize">
 547     <title>normalize &lt;pattern&gt;</title>
 548     <para>The tactic <command>normalize</command> </para>
 549   </sect2>
 550   <sect2 id="tac_paramodulation">
 551     <title>paramodulation &lt;pattern&gt;</title>
 552     <para>The tactic <command>paramodulation</command> </para>
 553   </sect2>
 554   <sect2 id="tac_reduce">
 555     <title>reduce &lt;pattern&gt;</title>
 556     <para>The tactic <command>reduce</command> </para>
 557   </sect2>
 558   <sect2 id="tac_reflexivity">
 559     <title>reflexivity</title>
 560     <para>The tactic <command>reflexivity</command> </para>
 561   </sect2>
 562   <sect2 id="tac_replace">
 563     <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
 564     <para>The tactic <command>replace</command> </para>
 565   </sect2>
 566   <sect2 id="tac_rewrite">
 567     <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
 568     <para>The tactic <command>rewrite</command> </para>
 569   </sect2>
 570   <sect2 id="tac_right">
 571     <title>right</title>
 572     <para>The tactic <command>right</command> </para>
 573   </sect2>
 574   <sect2 id="tac_ring">
 575     <title>ring</title>
 576     <para>The tactic <command>ring</command> </para>
 577   </sect2>
 578   <sect2 id="tac_simplify">
 579     <title>simplify &lt;pattern&gt;</title>
 580     <para>The tactic <command>simplify</command> </para>
 581   </sect2>
 582   <sect2 id="tac_split">
 583     <title>split</title>
 584     <para>The tactic <command>split</command> </para>
 585   </sect2>
 586   <sect2 id="tac_symmetry">
 587     <title>symmetry</title>
 588     <para>The tactic <command>symmetry</command> </para>
 589   </sect2>
 590   <sect2 id="tac_transitivity">
 591     <title>transitivity &lt;term&gt;</title>
 592     <para>The tactic <command>transitivity</command> </para>
 593   </sect2>
 594   <sect2 id="tac_unfold">
 595     <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
 596     <para>The tactic <command>unfold</command> </para>
 597   </sect2>
 598   <sect2 id="tac_whd">
 599     <title>whd &lt;pattern&gt;</title>
 600     <para>The tactic <command>whd</command> </para>
 601   </sect2>
 602
 603 </sect1>
 604