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="proofstatus">
  30   <title>The proof status</title>
  31   <para>
  32    During an interactive proof, the proof status is made of
  33    the set of sequents to prove and the partial proof built so far.
  34   </para>
  35   <para>The partial proof can be <link linkend="aboutproof">inspected</link>
  36    on demand in the CIC browser. It will be shown in pseudo-natural language
  37    produced on the fly from the proof term.</para>
  38   <para>The set of sequents to prove is shown in the notebook of the
  39    <link linkend="authoringinterface">authoring interface</link>, in the
  40    top-right corner of the main window of Matita. Each tab shows a different
  41    sequent, named with a question mark followed by a number. The current
  42    role of the sequent, according to the following description, is also
  43    shown in the tab tag.
  44   </para>
  45   <orderedlist>
  46    <listitem id="selectedsequents">
  47     <para>
  48      <emphasis role="bold">Selected sequents</emphasis>
  49       (name in boldface, e.g. <emphasis role="bold">?3</emphasis>).
  50       The next tactic will be applied to every selected sequent, producing
  51       new selected sequents. <link linkend="tacticals">Tacticals</link>
  52       such as branching (&quot;<emphasis role="bold">[</emphasis>&quot;)
  53       or &quot;<emphasis role="bold">focus</emphasis>&quot; can be used
  54       to change the set of selected sequents.
  55     </para>
  56    </listitem>
  57    <listitem id="siblingsequents">
  58     <para>
  59      <emphasis role="bold">Sibling sequents</emphasis>
  60      (name prefixed by a vertical bar and their position, e.g.
  61       |<subscript>3</subscript>?2). When the set of selected sequents
  62      has more than one element, the user can decide to focus in turn on each
  63      of them. The branching <link linkend="tacticals">tactical</link>
  64      (&quot;<emphasis role="bold">[</emphasis>&quot;) selects the first
  65      sequent only, marking every previously selected sequent as a sibling
  66      sequent. Each sibling sequent is given a different position. The
  67      tactical &quot;<emphasis role="bold">2,3:</emphasis>&quot; can be used to
  68      select one or more sibling sequents, different from the one proposed,
  69      according to their position. Once the user starts to work on the
  70      selected sibling sequents it becomes impossible to select a new
  71      set of siblings until the (&quot;<emphasis role="bold">|</emphasis>&quot;)
  72      tactical is used to end work on the current one.
  73     </para>
  74    </listitem>
  75    <listitem id="solvedsequents">
  76     <para>
  77      <emphasis role="bold">Automatically solved sibling sequents</emphasis>
  78      (name strokethrough, e.g. |<subscript>3</subscript><emphasis role="strikethrough">?2</emphasis>).
  79      Sometimes a tactic can close by side effects a sibling sequent the
  80      user has not selected yet. The sequent is left in the automatically
  81      solved status in order for the user to explicitly accept
  82      (using the &quot;<emphasis role="bold">skip</emphasis>&quot;
  83      <link linkend="tacticals">tactical</link>) the automatic
  84      instantiation in the proof script. This way the correspondence between
  85      the number of branches in the proof script and the number of sequents
  86      generated in the proof is preserved.
  87     </para>
  88    </listitem>
  89   </orderedlist>
  90  </sect1>
  91  <sect1 id="tacticals">
  92   <title>Tacticals</title>
  93    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  94      <title>proof script</title>
  95      <tgroup cols="4">
  96      <tbody>
  97       <row>
  98        <entry id="grammar.proofscript">&proofscript;</entry>
  99        <entry>::=</entry>
 100        <entry>&proofstep; [&proofstep;]…</entry>
 101       </row>
 102      </tbody>
 103     </tgroup>
 104    </table>
 105    <para>Every proof step can be immediately executed.</para>
 106    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 107      <title>proof steps</title>
 108      <tgroup cols="4">
 109      <tbody>
 110       <row>
 111        <entry id="grammar.proofstep">&proofstep;</entry>
 112        <entry>::=</entry>
 113        <entry>&LCFtactical;</entry>
 114        <entry>The tactical is applied to each
 115         <link linkend="selectedsequents">selected sequent</link>.
 116         Each new sequent becomes a selected sequent.</entry>
 117       </row>
 118       <row>
 119        <entry/>
 120        <entry>|</entry>
 121        <entry><emphasis role="bold">.</emphasis></entry>
 122        <entry>The first
 123         <link linkend="selectedsequents">selected sequent</link> becomes
 124         the only one selected. All the remaining previously selected sequents
 125         are proposed to the user one at a time when the next
 126         &quot;<emphasis role="bold">.</emphasis>&quot; is used.
 127        </entry>
 128       </row>
 129       <row>
 130        <entry/>
 131        <entry>|</entry>
 132        <entry><emphasis role="bold">;</emphasis></entry>
 133        <entry>Nothing changes. Use this proof step as a separator in
 134         concrete syntax.</entry>
 135       </row>
 136       <row>
 137        <entry/>
 138        <entry>|</entry>
 139        <entry><emphasis role="bold">[</emphasis></entry>
 140        <entry>Every <link linkend="selectedsequents">selected sequent</link>
 141         becomes a <link linkend="siblingsequents">sibling sequent</link>
 142         that constitute a branch in the proof.
 143         Moreover, the first sequent is also selected.
 144        </entry>
 145       </row>
 146       <row>
 147        <entry/>
 148        <entry>|</entry>
 149        <entry><emphasis role="bold">|</emphasis></entry>
 150        <entry>Stop working on the current branch of the innermost branching
 151         proof.
 152         The sibling branches become the <link linkend="siblingsequents">sibling
 153         sequents</link> and the first one is also selected.
 154        </entry>
 155       </row>
 156       <row>
 157        <entry/>
 158        <entry>|</entry>
 159        <entry>&nat;[<emphasis role="bold">,</emphasis>&nat;]…<emphasis role="bold">:</emphasis></entry>
 160        <entry>The <link linkend="siblingsequents">sibling sequents</link>
 161         specified by the user become the next
 162         <link linkend="selectedsequents">selected sequents</link>.
 163        </entry>
 164       </row>
 165       <row>
 166        <entry/>
 167        <entry>|</entry>
 168        <entry><emphasis role="bold">*:</emphasis></entry>
 169        <entry>Every sibling branch not considered yet in the innermost
 170         branching proof becomes a
 171         <link linkend="selectedsequents">selected sequent</link>.
 172        </entry>
 173       </row>
 174       <row>
 175        <entry/>
 176        <entry>|</entry>
 177        <entry><emphasis role="bold">skip</emphasis></entry>
 178        <entry>Accept the automatically provided instantiation (not shown
 179         to the user) for the currently selected
 180         <link linkend="solvedsequents">automatically closed sibling sequent</link>.
 181        </entry>
 182       </row>
 183       <row>
 184        <entry/>
 185        <entry>|</entry>
 186        <entry><emphasis role="bold">]</emphasis></entry>
 187        <entry>Stop analyzing branches for the innermost branching proof.
 188         Every sequent opened during the branching proof and not closed yet
 189         becomes a <link linkend="selectedsequents">selected sequent</link>.
 190        </entry>
 191       </row>
 192       <row>
 193        <entry/>
 194        <entry>|</entry>
 195        <entry><emphasis role="bold">focus</emphasis>&nbsp;&nat;&nbsp;[&nat;]…</entry>
 196        <entry>
 197         Selects the sequents specified by the user. The selected sequents
 198         must be completely closed (no new sequents left open) before doing an
 199         &quot;<emphasis role="bold">unfocus</emphasis> that restores
 200         the current set of sibling branches.
 201        </entry>
 202       </row>
 203       <row>
 204        <entry/>
 205        <entry>|</entry>
 206        <entry><emphasis role="bold">unfocus</emphasis></entry>
 207        <entry>
 208         Used to match the innermost
 209         &quot;<emphasis role="bold">focus</emphasis>&quot; tactical
 210         when all the sequents selected by it have been closed.
 211         Until &quot;<emphasis role="bold">unfocus</emphasis>&quot; is
 212         performed, it is not possible to progress in the rest of the
 213         proof.
 214        </entry>
 215       </row>
 216      </tbody>
 217     </tgroup>
 218    </table>
 219    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 220      <title>tactics and LCF tacticals</title>
 221      <tgroup cols="4">
 222      <tbody>
 223       <row>
 224        <entry id="grammar.LCFtactical">&LCFtactical;</entry>
 225        <entry>::=</entry>
 226        <entry>&tactic;</entry>
 227        <entry>Applies the specified tactic.</entry>
 228       </row>
 229       <row>
 230        <entry/>
 231        <entry>|</entry>
 232        <entry>&LCFtactical; <emphasis role="bold">;</emphasis> &LCFtactical;</entry>
 233        <entry>Applies the first tactical first and the second tactical
 234         to each sequent opened by the first one.</entry>
 235       </row>
 236       <row>
 237        <entry/>
 238        <entry>|</entry>
 239        <entry>&LCFtactical;
 240         <emphasis role="bold">[</emphasis>
 241         [&LCFtactical;]
 242         [<emphasis role="bold">|</emphasis> &LCFtactical;]…
 243         <emphasis role="bold">]</emphasis>
 244        </entry>
 245        <entry>Applies the first tactical first and each tactical in the
 246         list of tacticals to the corresponding sequent opened by the
 247         first one. The number of tacticals provided in the list must be
 248         equal to the number of sequents opened by the first tactical.</entry>
 249       </row>
 250       <row>
 251        <entry/>
 252        <entry>|</entry>
 253        <entry><emphasis role="bold">do</emphasis> &nat;
 254         &LCFtactical; <emphasis role="bold">end</emphasis>
 255        </entry>
 256        <entry>&TODO;</entry>
 257       </row>
 258       <row>
 259        <entry/>
 260        <entry>|</entry>
 261        <entry><emphasis role="bold">repeat</emphasis>
 262         &LCFtactical; <emphasis role="bold">end</emphasis>
 263        </entry>
 264        <entry>&TODO;</entry>
 265       </row>
 266       <row>
 267        <entry/>
 268        <entry>|</entry>
 269        <entry>
 270         <emphasis role="bold">first [</emphasis>
 271         [&LCFtactical;]
 272         [<emphasis role="bold">|</emphasis> &LCFtactical;]…
 273         <emphasis role="bold">]</emphasis>
 274        </entry>
 275        <entry>&TODO;</entry>
 276       </row>
 277       <row>
 278        <entry/>
 279        <entry>|</entry>
 280        <entry><emphasis role="bold">try</emphasis> &LCFtactical;</entry>
 281        <entry>&TODO;</entry>
 282       </row>
 283       <row>
 284        <entry/>
 285        <entry>|</entry>
 286        <entry>
 287         <emphasis role="bold">solve [</emphasis>
 288         [&LCFtactical;]
 289         [<emphasis role="bold">|</emphasis> &LCFtactical;]…
 290         <emphasis role="bold">]</emphasis>
 291        </entry>
 292        <entry>&TODO;</entry>
 293       </row>
 294       <row>
 295        <entry/>
 296        <entry>|</entry>
 297        <entry><emphasis role="bold">(</emphasis>&LCFtactical;<emphasis role="bold">)</emphasis></entry>
 298        <entry>Used for grouping during parsing.</entry>
 299       </row>
 300      </tbody>
 301     </tgroup>
 302    </table>
 303  </sect1>
 304 </chapter>
 305