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