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 V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><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="introsspec"></a>intros-spec</h3></div></div></div><div class="table"><a id="idp69423248"></a><p class="title"><strong>Table 4.13. intros-spec</strong></p><div class="table-contents"><table summary="intros-spec" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.intros-spec"></a><span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.intros-spec">intros-spec</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="bold"><strong>(</strong></span>[<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]…<span class="bold"><strong>)</strong></span>]</td><td class="auto-generated" style=""> </td></tr></tbody></table></div></div><br class="table-break" /><p>The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses.</p></div><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="idp69433952"></a><p class="title"><strong>Table 4.14. pattern</strong></p><div class="table-contents"><table summary="pattern" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt 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>]]</td><td style="">simple pattern</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>in 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>]]</td><td style="">full pattern</td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp69453472"></a><p class="title"><strong>Table 4.15. path</strong></p><div class="table-contents"><table summary="path" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><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><td class="auto-generated" style=""> </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>in 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>⊢ in 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="idp69506592"></a><p class="title"><strong>Table 4.16. reduction-kind</strong></p><div class="table-contents"><table summary="reduction-kind" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt 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></td><td style="">Computes the βδιζ-normal form</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>simplify</strong></span></td><td style="">Computes a form supposed to be simpler</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>unfold</strong></span> [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>]</td><td style="">δ-reduces the constant or variable if specified, or that
76 in head position</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>whd</strong></span></td><td style="">Computes the βδιζ-weak-head normal form</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="idp69522400"></a><p class="title"><strong>Table 4.17. auto-params</strong></p><div class="table-contents"><table summary="auto-params" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt 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="tacticargs.html#grammar.simpleautoparam">simple_auto_param</a></em></span>]…
77 [<span class="bold"><strong>by</strong></span>
78 <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span> [,<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>]…]
79 </td><td class="auto-generated" style=""> </td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp69531952"></a><p class="title"><strong>Table 4.18. simple-auto-param</strong></p><div class="table-contents"><table summary="simple-auto-param" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt 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>depth=<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></strong></span></td><td style="">Give a bound to the depth of the search tree</td></tr><tr><td style=""> </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>library</strong></span></td><td style="">Search everywhere (not only in included files)</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>type</strong></span></td><td style="">Try to close also goals of sort Type, otherwise only goals
80 living in sort Prop are attacked.
81 </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>paramodulation</strong></span></td><td style="">Try to close the goal performing unit-equality paramodulation
82 </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>timeout=<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></strong></span></td><td style="">Timeout in seconds
83 </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="idp69555152"></a><p class="title"><strong>Table 4.19. justification</strong></p><div class="table-contents"><table summary="justification" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt 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>
projects / helm.git / blob