helm/software/matita/help/C/sec_tacticals.xml

   1
   2 <!-- ============ Tacticals ====================== -->
   3 <chapter id="sec_tacticals">
   4  <title>Tacticals</title>
   5  <sect1>
   6    <title>Interactive proofs and definitions</title>
   7    <para>
   8     An interactive definition is started by giving a
   9     <link linkend="definition">definition</link> command omitting
  10     the definiens.
  11     An interactive proof is started by using one of the
  12     <link linkend="proofs">proof commands</link> omitting
  13     an explicit proof term.
  14    </para>
  15    <para>An interactive proof or definition can and must be terminated by
  16     a <link linkend="command_qed">qed</link> command when no more sequents are
  17     left to prove. Between the command that starts the interactive session and
  18     the qed command the user must provide a procedural proof script made
  19     of <link linkend="sec_tactics">tactics</link> structured by means of
  20     <link linkend="tacticals">tacticals</link>.</para>
  21    <para>In the tradition of the LCF system, tacticals can be considered
  22     higher order tactics. Their syntax is structured and they are executed
  23     atomically. On the contrary, in Matita the syntax of several tacticals is
  24     destructured into a sequence of tokens and tactics in such a way that is
  25     is possible to stop execution after every single token or tactic.
  26     The original semantics is preserved: the execution of the whole sequence
  27     yields the result expected by the original LCF-like tactical.</para>
  28  </sect1>
  29  <sect1 id="tacticals">
  30   <title>Tacticals</title>
  31    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  32      <title>proof script</title>
  33      <tgroup cols="4">
  34      <tbody>
  35       <row>
  36        <entry id="grammar.proofscript">&proofscript;</entry>
  37        <entry>::=</entry>
  38        <entry>&proofstep; [&proofstep;]…</entry>
  39       </row>
  40      </tbody>
  41     </tgroup>
  42    </table>
  43    <para>Every proof step can be immediately executed.</para>
  44    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  45      <title>proof steps</title>
  46      <tgroup cols="4">
  47      <tbody>
  48       <row>
  49        <entry id="grammar.proofstep">&proofstep;</entry>
  50        <entry>::=</entry>
  51        <entry>&LCFtactical;</entry>
  52       </row>
  53       <row>
  54        <entry/>
  55        <entry>|</entry>
  56        <entry><emphasis role="bold">.</emphasis></entry>
  57       </row>
  58       <row>
  59        <entry/>
  60        <entry>|</entry>
  61        <entry><emphasis role="bold">;</emphasis></entry>
  62       </row>
  63       <row>
  64        <entry/>
  65        <entry>|</entry>
  66        <entry><emphasis role="bold">[</emphasis></entry>
  67       </row>
  68       <row>
  69        <entry/>
  70        <entry>|</entry>
  71        <entry><emphasis role="bold">|</emphasis></entry>
  72       </row>
  73       <row>
  74        <entry/>
  75        <entry>|</entry>
  76        <entry>&nat;[<emphasis role="bold">,</emphasis>&nat;]…<emphasis role="bold">:</emphasis></entry>
  77       </row>
  78       <row>
  79        <entry/>
  80        <entry>|</entry>
  81        <entry><emphasis role="bold">*:</emphasis></entry>
  82       </row>
  83       <row>
  84        <entry/>
  85        <entry>|</entry>
  86        <entry><emphasis role="bold">skip</emphasis></entry>
  87       </row>
  88       <row>
  89        <entry/>
  90        <entry>|</entry>
  91        <entry><emphasis role="bold">]</emphasis></entry>
  92       </row>
  93       <row>
  94        <entry/>
  95        <entry>|</entry>
  96        <entry><emphasis role="bold">focus</emphasis> &nat; [&nat;]…</entry>
  97       </row>
  98       <row>
  99        <entry/>
 100        <entry>|</entry>
 101        <entry><emphasis role="bold">unfocus</emphasis></entry>
 102       </row>
 103      </tbody>
 104     </tgroup>
 105    </table>
 106    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 107      <title>tactics and LCF tacticals</title>
 108      <tgroup cols="4">
 109      <tbody>
 110       <row>
 111        <entry id="grammar.LCFtactical">&LCFtactical;</entry>
 112        <entry>::=</entry>
 113        <entry>&tactic;</entry>
 114       </row>
 115       <row>
 116        <entry/>
 117        <entry>|</entry>
 118        <entry>&LCFtactical; <emphasis role="bold">;</emphasis> &LCFtactical;</entry>
 119       </row>
 120       <row>
 121        <entry/>
 122        <entry>|</entry>
 123        <entry>&LCFtactical;
 124         <emphasis role="bold">[</emphasis>
 125         [&LCFtactical;]
 126         [<emphasis role="bold">|</emphasis> &LCFtactical;]…
 127         <emphasis role="bold">]</emphasis>
 128        </entry>
 129       </row>
 130       <row>
 131        <entry/>
 132        <entry>|</entry>
 133        <entry><emphasis role="bold">do</emphasis> &nat;
 134         &LCFtactical; <emphasis role="bold">end</emphasis>
 135        </entry>
 136       </row>
 137       <row>
 138        <entry/>
 139        <entry>|</entry>
 140        <entry><emphasis role="bold">repeat</emphasis>
 141         &LCFtactical; <emphasis role="bold">end</emphasis>
 142        </entry>
 143       </row>
 144       <row>
 145        <entry/>
 146        <entry>|</entry>
 147        <entry>
 148         <emphasis role="bold">first [</emphasis>
 149         [&LCFtactical;]
 150         [<emphasis role="bold">|</emphasis> &LCFtactical;]…
 151         <emphasis role="bold">]</emphasis>
 152        </entry>
 153       </row>
 154       <row>
 155        <entry/>
 156        <entry>|</entry>
 157        <entry><emphasis role="bold">try</emphasis> &LCFtactical;</entry>
 158       </row>
 159       <row>
 160        <entry/>
 161        <entry>|</entry>
 162        <entry>
 163         <emphasis role="bold">solve [</emphasis>
 164         [&LCFtactical;]
 165         [<emphasis role="bold">|</emphasis> &LCFtactical;]…
 166         <emphasis role="bold">]</emphasis>
 167        </entry>
 168       </row>
 169       <row>
 170        <entry/>
 171        <entry>|</entry>
 172        <entry><emphasis role="bold">(</emphasis>&LCFtactical;<emphasis role="bold">)</emphasis></entry>
 173       </row>
 174      </tbody>
 175     </tgroup>
 176    </table>
 177    <para>&TODO;</para>
 178  </sect1>
 179 </chapter>
 180