]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/help/C/sec_declarative_tactics.xml
Partial implementation of "go to cursor" action.
[helm.git] / matitaB / matita / help / C / sec_declarative_tactics.xml
1 <!-- ================= Tactics ========================= -->
2 <chapter id="sec_declarative_tactics">
3   <title>Declarative Tactics</title>
4
5   <sect1
6   id="declarative_tactics_quickref">
7     <title>Quick reference card</title>
8     <para>
9       &declarativetacticref;
10     </para>
11   </sect1>
12
13   
14   <sect1 id="tac_assume">
15     <title>assume</title>
16     <titleabbrev>assume</titleabbrev>
17     <para><userinput>assume x : t</userinput></para>
18   <para>
19     <variablelist>
20       <varlistentry role="tactic.synopsis">
21        <term>Synopsis:</term>
22        <listitem>
23          <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis> &sterm;</para>
24        </listitem>
25       </varlistentry>
26       <varlistentry>
27         <term>Pre-conditions:</term>
28         <listitem>
29           <para>The conclusion of the current proof must be
30            <command>∀x:T.P</command> or
31            <command>T→P</command> where <command>T</command> is
32            a data type (i.e. <command>T</command> has type
33            <command>Set</command> or <command>Type</command>).</para>
34         </listitem>
35       </varlistentry>
36       <varlistentry>
37         <term>Action:</term>
38         <listitem>
39           <para>It adds to the context of the current sequent to prove a new
40            declaration <command>x : T </command>. The new conclusion becomes
41            <command>P</command>.</para>
42         </listitem>
43       </varlistentry>
44       <varlistentry>
45         <term>New sequents to prove:</term>
46         <listitem>
47           <para>None.</para>
48         </listitem>
49       </varlistentry>
50     </variablelist>
51    </para>
52   </sect1>
53
54     <sect1 id="tac_byinduction">
55       <title>by induction hypothesis we know</title>
56       <titleabbrev>by induction hypothesis we know</titleabbrev>
57       <para><userinput>by induction hypothesis we know t (id)</userinput></para>
58       <para>
59         <variablelist>
60           <varlistentry role="tactic.synopsis">
61             <term>Synopsis:</term>
62             <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
63             </listitem>
64           </varlistentry>
65           <varlistentry>
66             <term>Pre-condition:</term>
67             <listitem>
68         <para>To be used in a proof by induction to state the inductive
69           hypothesis.</para>
70             </listitem>
71           </varlistentry>
72           <varlistentry>
73             <term>Action:</term>
74               <listitem>
75                 <para> Introduces the inductive hypothesis. </para>
76               </listitem>
77           </varlistentry>
78           <varlistentry>
79              <term>New sequents to prove:</term>
80                  <listitem>
81                  <para>None.</para>
82                  </listitem>
83           </varlistentry>
84          </variablelist>
85       </para>
86     </sect1>  
87
88    <sect1 id="tac_case">
89      <title>case</title>
90      <titleabbrev>case</titleabbrev>
91      <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
92      <para>
93        <variablelist>
94          <varlistentry role="tactic.synopsis">
95            <term>Synopsis:</term>
96            <listitem>
97              <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term;  <emphasis role="bold">)</emphasis>] … </para>
98            </listitem>
99          </varlistentry>
100          <varlistentry>
101             <term>Pre-condition:</term>
102             <listitem>
103         <para>To be used in a proof by induction or by cases to start
104           a new case</para>
105             </listitem>
106          </varlistentry>
107          <varlistentry>
108             <term>Action:</term>
109             <listitem>
110               <para>Starts the new case <command>id</command> declaring
111                 the local parameters <command>(id1:t1) … (idn:tn)</command></para>
112             </listitem>
113          </varlistentry>
114          <varlistentry>
115            <term>New sequents to prove:</term>
116            <listitem>
117                <para>None</para>
118            </listitem>
119          </varlistentry>
120        </variablelist>
121      </para>
122   </sect1> 
123
124  <sect1 id="tac_bydone">
125    <title>done</title>
126    <titleabbrev>done</titleabbrev>
127    <para><userinput>justification done</userinput></para>
128    <para>
129      <variablelist>
130        <varlistentry role="tactic.synopsis">
131          <term>Synopsis:</term>
132          <listitem>
133            <para>&justification; <emphasis role="bold">done</emphasis></para>
134          </listitem>
135        </varlistentry>
136        <varlistentry>
137          <term>Pre-condition:</term>
138          <listitem>
139            <para></para>
140          </listitem>
141        </varlistentry>
142        <varlistentry>
143          <term>Action:</term>
144            <listitem> 
145              <para>It closes the current sequent given the justification.</para>
146            </listitem>
147        </varlistentry>
148        <varlistentry>
149            <term>New sequents to prove:</term>
150            <listitem>
151                <para>None.</para>
152            </listitem>
153        </varlistentry>
154    </variablelist>
155      </para>
156   </sect1>
157
158
159   <sect1 id="tac_exitselim">
160     <title>let such that</title>
161     <titleabbrev>let such that</titleabbrev>
162     <para><userinput>justification let x:t such that p (id)</userinput>
163     </para>
164     <para>
165       <variablelist>
166         <varlistentry role="tactic.synopsis">
167           <term>Synopsis:</term>
168           <listitem>
169             <para>&justification; <emphasis role="bold">let</emphasis> &id; 
170                     <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term; 
171                      <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
172           </listitem>
173         </varlistentry>
174         <varlistentry>
175           <term>Pre-condition:</term>
176           <listitem>
177       <para>
178             </para>
179           </listitem>  
180         </varlistentry>
181         <varlistentry>
182           <term>Action:</term>
183           <listitem>
184       <para>It derives <command>∃x:t.p</command> using the
185         <command>justification</command> and then it introduces in the context
186         <command>x</command> and the hypothesis  
187         <command>p</command> labelled with
188         <command>id</command>.
189       </para>
190           </listitem>
191         </varlistentry>
192         <varlistentry>
193           <term>New sequent to prove:</term>
194           <listitem>
195       <para>None.</para>
196           </listitem>
197         </varlistentry>
198      </variablelist>
199     </para>
200   </sect1>
201
202   <sect1 id="tac_obtain">
203     <title>obtain</title>
204     <titleabbrev>obtain</titleabbrev>
205     <para><userinput>obtain H t1 = t2 justification</userinput></para>
206     <para>
207       <variablelist>
208          <varlistentry role="tactic.synopsis">
209            <term>Synopsis:</term>
210            <listitem>
211              <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
212            </listitem>
213          </varlistentry>
214          <varlistentry>
215            <term>Pre-condition:</term>
216              <listitem>
217          <para><command>conclude</command> can be used only if the current
218            sequent is stating an equality. The left hand side must be omitted
219            in an equality chain.</para> 
220        </listitem>
221          </varlistentry>
222          <varlistentry>
223            <term>Action:</term>
224            <listitem>
225        <para>Starts or continues an equality chain. If the chain starts 
226          with <command>obtain H</command> a new subproof named 
227          <command>H</command> is started.</para>
228            </listitem>
229          </varlistentry>
230          <varlistentry>
231            <term>New sequent to prove:</term>
232              <listitem>
233                 <para>If the chain starts 
234             with <command>obtain H</command> a nre sequent for
235             <command>t2 = ?</command> is opened.
236           </para>
237              </listitem>
238          </varlistentry>
239        </variablelist>
240      </para>
241    </sect1>
242
243   <sect1 id="tac_suppose">
244     <title>suppose</title>
245     <titleabbrev>suppose</titleabbrev>
246     <para><userinput>suppose t1 (x) that is equivalent to t2</userinput></para>
247   <para>
248      <variablelist>
249        <varlistentry role="tactic.synopsis">
250          <term>Synopsis:</term>
251          <listitem>
252            <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; 
253              <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis>  &term; ]</para>
254          </listitem>
255        </varlistentry>
256       <varlistentry>
257          <term>Pre-condition:</term>
258          <listitem>
259            <para>The conclusion of the current proof must be
260            <command>∀x:T.P</command> or
261            <command>T→P</command> where <command>T</command> is
262            a proposition (i.e. <command>T</command> has type
263            <command>Prop</command> or <command>CProp</command>).</para>
264          </listitem>
265       </varlistentry>
266       <varlistentry>
267         <term>Action:</term>
268           <listitem>
269             <para>It adds to the context of the current sequent to prove a new
270            declaration <command>x : T </command>. The new conclusion becomes
271            <command>P</command>.</para>
272           </listitem>
273       </varlistentry>
274       <varlistentry>
275         <term>New sequents to prove:</term>
276         <listitem>
277             <para>None.</para>
278         </listitem>
279       </varlistentry>
280     </variablelist>
281    </para>
282   </sect1>
283
284    <sect1 id="tac_thesisbecomes">
285      <title>the thesis becomes</title>
286      <titleabbrev>the thesis becomes</titleabbrev>
287      <para><userinput>the thesis becomes t</userinput></para>
288      <para>
289         <variablelist>
290            <varlistentry role="tactic.synopsis">
291              <term>Synopsis:</term>
292              <listitem>
293                <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
294              </listitem>
295            </varlistentry>
296            <varlistentry>
297              <term>Pre-condition:</term>
298              <listitem>
299          <para>The provided term <command>t</command> must be convertible with
300            current sequent.</para>
301              </listitem>
302            </varlistentry>
303            <varlistentry>
304              <term>Action:</term>
305              <listitem>
306                <para>It changes the current goal to the one provided.</para>
307              </listitem>
308            </varlistentry>
309            <varlistentry>
310              <term>New sequent to prove:</term>
311              <listitem>
312                <para>None.</para>
313              </listitem>
314            </varlistentry>
315          </variablelist>
316        </para>
317    </sect1>
318    
319   <sect1 id="tac_weneedtoprove">
320     <title>we need to prove</title>
321     <titleabbrev>we need to prove</titleabbrev>
322     <para><userinput>we need to prove t1 (id) or equivalently t2</userinput></para>
323     <para>
324       <variablelist>
325         <varlistentry role="tactic.synopsis">
326           <term>Synopsis:</term>
327           <listitem>
328       <para><emphasis role="bold">we need to prove</emphasis> &term;
329         [<emphasis role="bold">(</emphasis>&id;
330         <emphasis role="bold">)</emphasis>]
331         [ <emphasis role="bold">or equivalently</emphasis> &term;]</para> 
332           </listitem>
333         </varlistentry>
334         <varlistentry>
335           <term>Pre-condition:</term>
336           <listitem>
337             <para></para>
338           </listitem>
339         </varlistentry>
340         <varlistentry>
341           <term>Action:</term>
342             <listitem>
343         <para>If <command>id</command> is provided, starts a subproof that once concluded 
344               will be named <command>id</command>. Otherwise states what needs to be proved.
345               If <command>t2</command> is provided, the new goal is 
346               immediately changed to <command>t2</command> wich must
347               be equivalent to <command>t1</command>.
348             </para>
349             </listitem>
350         </varlistentry>
351         <varlistentry>
352            <term>New sequents to prove:</term>
353            <listitem>
354              <para>The stated one if <command>id</command> is provided</para>
355            </listitem>
356         </varlistentry>     
357      </variablelist>
358     </para>
359   </sect1>
360
361
362   <sect1 id="tac_andelim">
363     <title>we have</title>
364     <titleabbrev>we have</titleabbrev>
365     <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
366     </para>
367     <para>
368       <variablelist>
369         <varlistentry role="tactic_synopsis">
370           <term>Synopsis:</term>
371           <listitem>
372             <para>&justification; <emphasis role="bold">we have</emphasis> &term; 
373                     <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term; 
374                       <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
375           </listitem>
376         </varlistentry>
377         <varlistentry>
378           <term>Pre-condition:</term>
379           <listitem>
380             <para></para>
381           </listitem>
382         </varlistentry>
383         <varlistentry>
384           <term>Action:</term>
385           <listitem>
386       <para>It derives <command>t1∧t2</command> using the 
387         <command>justification</command> then it introduces in the context
388         <command>t1</command>   labelled with <command>id1</command> and
389         <command>t2</command>   labelled with <command>id2</command>.
390       </para>
391           </listitem>
392         </varlistentry>
393         <varlistentry>
394           <term>New sequent to prove:</term>
395           <listitem>
396              <para>None.</para>
397           </listitem>
398         </varlistentry>
399       </variablelist>
400     </para>
401   </sect1>
402
403   <sect1 id="tac_weproceedbycases">
404     <title>we proceed by cases on</title>
405       <titleabbrev>we proceed by cases on</titleabbrev>
406       <para><userinput>we proceed by cases on t to prove th</userinput></para>
407       <para>
408         <variablelist>
409           <varlistentry role="tactic.synopsis">
410             <term>Synopsis:</term>
411             <listitem>
412               <para><emphasis role="bold">we proceed by cases on</emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
413              </listitem>
414           </varlistentry>
415           <varlistentry>
416             <term>Pre-condition:</term>
417             <listitem>
418         <para><command>t</command> must inhabitant of an inductive type and
419           <command>th</command> must be the conclusion to be proved by 
420           cases.</para>
421             </listitem>
422           </varlistentry>
423           <varlistentry>
424             <term>Action:</term>
425               <listitem>
426           <para> It proceeds by cases on <command>t</command> </para>
427               </listitem>
428           </varlistentry>
429           <varlistentry>
430             <term>New sequents to prove:</term>
431             <listitem>
432                <para>It opens one new sequent for each constructor of the
433                 type of <command>t</command>.</para>
434             </listitem>
435           </varlistentry>
436          </variablelist>
437        </para>
438     </sect1>
439     
440     <sect1 id="tac_weproceedbyinduction">
441     <title>we proceed by induction on</title>
442     <titleabbrev>we proceed by induction on</titleabbrev>
443     <para><userinput>we proceed by induction on t to prove th</userinput></para>        
444     <para>
445       <variablelist>
446         <varlistentry role="tactic.synopsis">
447           <term>Synopsis:</term>
448           <listitem>
449             <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
450           </listitem>
451         </varlistentry>
452         <varlistentry>
453           <term>Pre-condition:</term>
454           <listitem>
455       <para><command>t</command> must inhabitant of an inductive type and 
456         <command>th</command> must be the conclusion to be proved by induction.
457         </para>
458           </listitem>
459         </varlistentry>
460         <varlistentry>
461           <term>Action:</term>
462             <listitem>
463               <para>It proceed by induction on <command>t</command>.</para>
464             </listitem>
465         </varlistentry>
466         <varlistentry>
467             <term>New sequents to prove:</term>
468             <listitem>
469               <para>It opens one new sequent for each constructor of the
470                 type of <command>t</command>.</para>
471             </listitem>
472         </varlistentry>
473       </variablelist>
474     </para>
475   </sect1>
476
477
478  <sect1 id="tac_bytermweproved">
479    <title>we proved</title>
480      <titleabbrev>we proved</titleabbrev>
481      <para><userinput>justification we proved t (id)</userinput></para>
482      <para>
483        <variablelist>
484          <varlistentry role="tactic.synopsis">
485            <term>Synopsis:</term>
486            <listitem>
487              <para>&justification; <emphasis role="bold">we proved</emphasis> &term; 
488          <emphasis role="bold">(</emphasis> &id; 
489          <emphasis role="bold">)</emphasis></para>
490            </listitem>
491            </varlistentry>
492            <varlistentry>
493              <term>Pre-condition:</term>
494              <listitem>
495                <para><command>t</command>must have type <command>Prop</command>.
496          </para>
497              </listitem>
498            </varlistentry>
499            <varlistentry>
500              <term>Action:</term>
501              <listitem>
502          <para>It derives <command>t</command>
503            using the justification and labels the conclusion with
504            <command>id</command>.
505          </para>
506              </listitem>
507            </varlistentry>
508            <varlistentry>
509              <term>New sequent to prove:</term>
510              <listitem>
511                <para>None.</para>
512              </listitem>
513            </varlistentry>
514          </variablelist>
515        </para>
516     </sect1>
517
518 </chapter>