matita/matita/help/C/html/tacticargs.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Tactic arguments</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><link rel="up" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="proofs.html" title="Proofs" /><link rel="next" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Tactic arguments</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="proofs.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="sec_usernotation.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tacticargs"></a>Tactic arguments</h2></div></div></div><p>This section documents the syntax of some recurring arguments for
   3     tactics.</p><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="pattern"></a>pattern</h3></div></div></div><div class="table"><a id="idm1235"></a><p class="title"><strong>Table 4.13. pattern</strong></p><div class="table-contents"><table class="table" summary="pattern" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.pattern"></a><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>in</strong></span>
   4           [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>]]…
   5           [<span class="bold"><strong>⊢</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>]]<span class="bold"><strong>;</strong></span></td><td style="">simple pattern</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>in</strong></span> <span class="bold"><strong>match</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>
   6           [<span class="bold"><strong>in</strong></span>
   7           [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>]]…
   8           [<span class="bold"><strong>⊢</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>]]<span class="bold"><strong>;</strong></span></td><td style="">full pattern</td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idm1275"></a><p class="title"><strong>Table 4.14. path</strong></p><div class="table-contents"><table class="table" summary="path" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.path"></a><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em>〈〈any <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> without occurrences of <span class="bold"><strong>Set</strong></span>, <span class="bold"><strong>Prop</strong></span>, <span class="bold"><strong>CProp</strong></span>, <span class="bold"><strong>Type</strong></span>, <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>, <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.uri">uri</a></em></span> and user provided notation; however, <span class="bold"><strong>%</strong></span> is now an additional production for <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>〉〉</em></span></td></tr></tbody></table></div></div><br class="table-break" /><p>A <span class="emphasis"><em>path</em></span> locates zero or more subterms of a given term by mimicking the term structure up to:</p><div class="orderedlist"><ol class="orderedlist" type="1"><li class="listitem"><p>Occurrences of the subterms to locate that are
   9        represented by <span class="bold"><strong>%</strong></span>.</p></li><li class="listitem"><p>Subterms without any occurrence of subterms to locate
  10        that can be represented by <span class="bold"><strong>?</strong></span>.
  11        </p></li></ol></div><p>Warning: the format for a path for a <span class="bold"><strong>match</strong></span> … <span class="bold"><strong>with</strong></span>
  12      expression is restricted to: <span class="bold"><strong>match</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>
  13      <span class="bold"><strong>with</strong></span>
  14      <span class="bold"><strong>[</strong></span>
  15      <span class="bold"><strong>_</strong></span>
  16      <span class="bold"><strong>⇒</strong></span>
  17      <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>
  18      <span class="bold"><strong>|</strong></span> …
  19      <span class="bold"><strong>|</strong></span>
  20      <span class="bold"><strong>_</strong></span>
  21      <span class="bold"><strong>⇒</strong></span>
  22      <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>
  23      <span class="bold"><strong>]</strong></span>
  24      Its semantics is the following: the n-th
  25      "<span class="bold"><strong>_</strong></span>
  26      <span class="bold"><strong>⇒</strong></span>
  27      <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span>" branch is matched against the n-th constructor of the
  28      inductive data type. The head λ-abstractions of <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.path">path</a></em></span> are matched
  29      against the corresponding constructor arguments.
  30     </p><p>For instance, the path
  31       <strong class="userinput"><code>∀_,_:?.(? ? % ?)→(? ? ? %)</code></strong>
  32        locates at once the subterms
  33       <strong class="userinput"><code>x+y</code></strong> and <strong class="userinput"><code>x*y</code></strong> in the
  34       term <strong class="userinput"><code>∀x,y:nat.x+y=1→0=x*y</code></strong>
  35       (where the notation <strong class="userinput"><code>A=B</code></strong> hides the term
  36       <strong class="userinput"><code>(eq T A B)</code></strong> for some type <strong class="userinput"><code>T</code></strong>).
  37     </p><p>A <span class="emphasis"><em>simple pattern</em></span> extends paths to locate
  38      subterms in a whole sequent. In particular, the pattern
  39      <strong class="userinput"><code>{ H: p  K: q ⊢ r }</code></strong> locates at once all the subterms
  40      located by the pattern <strong class="userinput"><code>r</code></strong> in the conclusion of the
  41      sequent and by the patterns <strong class="userinput"><code>p</code></strong> and
  42      <strong class="userinput"><code>q</code></strong> in the hypotheses <strong class="userinput"><code>H</code></strong>
  43      and <strong class="userinput"><code>K</code></strong> of the sequent.
  44     </p><p>If no list of hypotheses is provided in a simple pattern, no subterm
  45      is selected in the hypothesis. If the <strong class="userinput"><code>⊢ p</code></strong>
  46      part of the pattern is not provided, no subterm will be matched in the
  47      conclusion if at least one hypothesis is provided; otherwise the whole
  48      conclusion is selected.
  49     </p><p>Finally, a <span class="emphasis"><em>full pattern</em></span> is interpreted in three
  50      steps. In the first step the <strong class="userinput"><code>match T in</code></strong>
  51      part is ignored and a set <span class="emphasis"><em>S</em></span> of subterms is
  52      located as for the case of
  53      simple patterns. In the second step the term <strong class="userinput"><code>T</code></strong>
  54      is parsed and interpreted in the context of each subterm
  55      <span class="emphasis"><em>s ∈ S</em></span>. In the last term for each
  56      <span class="emphasis"><em>s ∈ S</em></span> the interpreted term <strong class="userinput"><code>T</code></strong>
  57      computed in the previous step is looked for. The final set of subterms
  58      located by the full pattern is the set of occurrences of
  59      the interpreted <strong class="userinput"><code>T</code></strong> in the subterms <span class="emphasis"><em>s</em></span>.
  60     </p><p>A full pattern can always be replaced by a simple pattern,
  61       often at the cost of increased verbosity or decreased readability.</p><p>Example: the pattern
  62       <strong class="userinput"><code>{ match x+y in ⊢ ∀_,_:?.(? ? % ?) }</code></strong>
  63       locates only the first occurrence of <strong class="userinput"><code>x+y</code></strong>
  64       in the sequent <strong class="userinput"><code>x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) =
  65       z * (x+y) + w * (x+y)</code></strong>. The corresponding simple pattern
  66       is <strong class="userinput"><code>{ ⊢ ∀_,_:?.(? ? (? % ?) ?) }</code></strong>.
  67     </p><p>Every tactic that acts on subterms of the selected sequents have
  68      a pattern argument for uniformity. To automatically generate a simple
  69      pattern:</p><div class="orderedlist"><ol class="orderedlist" type="1"><li class="listitem"><p>Select in the current goal the subterms to pass to the
  70       tactic by using the mouse. In order to perform a multiple selection of
  71       subterms, hold the Ctrl key while selecting every subterm after the
  72       first one.</p></li><li class="listitem"><p>From the contextual menu select "Copy".</p></li><li class="listitem"><p>From the "Edit" or the contextual menu select
  73       "Paste as pattern"</p></li></ol></div></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="reduction-kind"></a>reduction-kind</h3></div></div></div><p>Reduction kinds are normalization functions that transform a term
  74      to a convertible but simpler one. Each reduction kind can be used both
  75      as a tactic argument and as a stand-alone tactic.</p><div class="table"><a id="idm1378"></a><p class="title"><strong>Table 4.15. reduction-kind</strong></p><div class="table-contents"><table class="table" summary="reduction-kind" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.reduction-kind"></a><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.reduction-kind">reduction-kind</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>normalize</strong></span> [<span class="bold"><strong>nodelta</strong></span>]</td><td style="">Computes the βδιζ-normal form. If <strong class="userinput"><code>nodelta</code></strong>
  76          is specified, δ-expansions are not performed.</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>whd</strong></span> [<span class="bold"><strong>nodelta</strong></span>]</td><td style="">Computes the βδιζ-weak-head normal form. If <strong class="userinput"><code>nodelta</code></strong>
  77          is specified, δ-expansions are not performed.</td></tr></tbody></table></div></div><br class="table-break" /></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="auto-params"></a>auto-params</h3></div></div></div><div class="table"><a id="idm1402"></a><p class="title"><strong>Table 4.16. auto-params</strong></p><div class="table-contents"><table class="table" summary="auto-params" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.autoparams"></a><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.autoparams">auto_params</a></em></span></td><td style="">::=</td><td style="">[<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>] [<span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.simpleautoparam">simple_auto_param</a></em></span>]…
  78                [<span class="bold"><strong>by</strong></span>
  79                 [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>… | <span class="bold"><strong>_</strong></span>]]
  80         </td><td style="">The natural number, which defaults to 1, gives a bound to
  81         the depth of the search tree. The terms listed is the only
  82         knowledge base used by automation together with all indexed factual
  83         and equational theorems in the included library. If the list of terms
  84         is empty, only equational theorems and facts in the library are
  85         used. If the list is omitted, it defaults to all indexed theorems
  86         in the library. Finally, if the list is <span class="command"><strong>_</strong></span>,
  87         the automation command becomes a macro that is expanded in a new
  88         automation command where <span class="command"><strong>_</strong></span> is replaced with the
  89         list of theorems required to prove the sequent.
  90         </td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idm1423"></a><p class="title"><strong>Table 4.17. simple-auto-param</strong></p><div class="table-contents"><table class="table" summary="simple-auto-param" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.simpleautoparam"></a><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.simpleautoparam">simple_auto_param</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>width=<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></strong></span></td><td style="">The maximal width of the search tree</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>size=<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></strong></span></td><td style="">The maximal number of nodes in the proof</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>demod</strong></span></td><td style="">Simplifies the current sequent using the current set of
  91          equations known to automation
  92         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>paramod</strong></span></td><td style="">Try to close the goal performing unit-equality paramodulation
  93         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>fast_paramod</strong></span></td><td style="">A bounded version of <span class="command"><strong>paramod</strong></span> that is granted to terminate quickly
  94         </td></tr></tbody></table></div></div><br class="table-break" /></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="justification"></a>justification</h3></div></div></div><div class="table"><a id="idm1466"></a><p class="title"><strong>Table 4.18. justification</strong></p><div class="table-contents"><table class="table" summary="justification" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.justification"></a><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.justification">justification</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>using</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span></td><td style="">Proof term manually provided</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.autoparams">auto_params</a></em></span></td><td style="">Call automation</td></tr></tbody></table></div></div><br class="table-break" /></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="proofs.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_terms.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_usernotation.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Proofs </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 5. Extending the syntax</td></tr></table></div></body></html>