]> matita.cs.unibo.it Git - helm.git/blob - matita/help/C/sec_tacticals.xml
Integration f_algebras declassed.
[helm.git] / 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