1 <!-- ================= Tactics ========================= -->
2 <chapter id="sec_declarative_tactics">
3 <title>Declarative Tactics</title>
6 id="declarative_tactics_quickref">
7 <title>Quick reference card</title>
14 <sect1 id="tac_assume">
16 <titleabbrev>assume</titleabbrev>
17 <para><userinput>assume x : T that is equivalent to T'</userinput></para>
20 <varlistentry role="tactic.synopsis">
21 <term>Synopsis:</term>
23 <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis>
24 &sterm; [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
28 <term>Pre-conditions:</term>
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>
40 <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
41 </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
42 <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new declaration that is added to the context is
43 <command>x:T'</command>.</para>
47 <term>New sequents to prove:</term>
56 <sect1 id="tac_suppose">
57 <title>suppose</title>
58 <titleabbrev>suppose</titleabbrev>
59 <para><userinput>suppose T (x) that is equivalent to T'</userinput></para>
62 <varlistentry role="tactic.synopsis">
63 <term>Synopsis:</term>
65 <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
66 <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
70 <term>Pre-condition:</term>
72 <para>The conclusion of the current proof must be
73 <command>∀x:T.P</command> or
74 <command>T→P</command> where <command>T</command> is
75 a proposition (i.e. <command>T</command> has type
76 <command>Prop</command> or <command>CProp</command>).</para>
82 <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
83 </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
84 <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new declaration that is added to the context is
85 <command>x:T'</command>.
90 <term>New sequents to prove:</term>
101 <titleabbrev>letin</titleabbrev>
102 <para><userinput>let x := T </userinput></para>
105 <varlistentry role="tactic.synopsis">
106 <term>Synopsis:</term>
108 <para><emphasis role="bold">let</emphasis> &id; <emphasis role="bold"> = </emphasis> &term;</para>
112 <term>Pre-condition:</term>
120 <para>It adds a new local definition <command>x := T</command> to the context of the sequent to prove.</para>
124 <term>New sequents to prove:</term>
133 <sect1 id="tac_bytermweproved">
134 <title>we proved</title>
135 <titleabbrev>we proved</titleabbrev>
136 <para><userinput>justification we proved T (id) that is equivalent to T'</userinput></para>
139 <varlistentry role="tactic.synopsis">
140 <term>Synopsis:</term>
142 <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
143 <emphasis role="bold">(</emphasis> &id;
144 <emphasis role="bold">)</emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term;] [ <emphasis role="bold">done</emphasis>]</para>
148 <term>Pre-condition:</term>
150 <para><command>T</command> must have type <command>Prop</command>.
157 <para>It derives <command>T</command>
158 using the justification and labels the conclusion with
159 <command>id</command>. Alternatively, if a proposition
160 <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new hypothesis that is added to the context is
161 <command>id:T'</command>.
163 If the user does not supply a label and ends the command with <command>done</command> then if T is alpha equivalent to the conclusion of the current sequent then it closes it (if <command>T'</command> is supplied this must be alpha equivalent to the conclusion, but in this case <command>T</command> does not need to).
168 <term>New sequent to prove:</term>
177 <sect1 id="tac_bydone">
179 <titleabbrev>done</titleabbrev>
180 <para><userinput>justification done</userinput></para>
183 <varlistentry role="tactic.synopsis">
184 <term>Synopsis:</term>
186 <para>&justification; <emphasis role="bold">done</emphasis></para>
190 <term>Pre-condition:</term>
198 <para>It closes the current sequent given the justification.</para>
202 <term>New sequents to prove:</term>
211 <sect1 id="tac_existselim">
212 <title>let such that</title>
213 <titleabbrev>let such that</titleabbrev>
214 <para><userinput>justification let x:t such that p (id)</userinput>
218 <varlistentry role="tactic.synopsis">
219 <term>Synopsis:</term>
221 <para>&justification; <emphasis role="bold">let</emphasis> &id;
222 <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term;
223 <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
227 <term>Pre-condition:</term>
236 <para>It derives <command>∃x:t.p</command> using the
237 <command>justification</command> and then it introduces in the context
238 <command>x</command> and the hypothesis
239 <command>p</command> labelled with
240 <command>id</command>.
245 <term>New sequent to prove:</term>
254 <sect1 id="tac_andelim">
255 <title>we have</title>
256 <titleabbrev>we have</titleabbrev>
257 <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
261 <varlistentry role="tactic_synopsis">
262 <term>Synopsis:</term>
264 <para>&justification; <emphasis role="bold">we have</emphasis> &term;
265 <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
266 <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
270 <term>Pre-condition:</term>
278 <para>It derives <command>t1∧t2</command> using the
279 <command>justification</command> then it introduces in the context
280 <command>t1</command> labelled with <command>id1</command> and
281 <command>t2</command> labelled with <command>id2</command>.
286 <term>New sequent to prove:</term>
295 <sect1 id="tac_weneedtoprove">
296 <title>we need to prove</title>
297 <titleabbrev>we need to prove</titleabbrev>
298 <para><userinput>we need to prove t1 (id) or equivalently t2</userinput></para>
301 <varlistentry role="tactic.synopsis">
302 <term>Synopsis:</term>
304 <para><emphasis role="bold">we need to prove</emphasis> &term;
305 [<emphasis role="bold">(</emphasis>&id;
306 <emphasis role="bold">)</emphasis>]
307 [ <emphasis role="bold">or equivalently</emphasis> &term;]</para>
311 <term>Pre-condition:</term>
319 <para>If <command>id</command> is provided, starts a subproof that once concluded
320 will be named <command>id</command>. Otherwise states what needs to be proved.
321 If <command>t2</command> is provided, the new goal is
322 immediately changed to <command>t2</command> wich must
323 be equivalent to <command>t1</command>.
328 <term>New sequents to prove:</term>
330 <para>The stated one if <command>id</command> is provided</para>
337 <sect1 id="tac_weproceedbyinduction">
338 <title>we proceed by induction on</title>
339 <titleabbrev>we proceed by induction on</titleabbrev>
340 <para><userinput>we proceed by induction on t to prove th</userinput></para>
343 <varlistentry role="tactic.synopsis">
344 <term>Synopsis:</term>
346 <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
350 <term>Pre-condition:</term>
352 <para><command>t</command> must inhabitant of an inductive type and
353 <command>th</command> must be the conclusion to be proved by induction.
360 <para>It proceed by induction on <command>t</command>.</para>
364 <term>New sequents to prove:</term>
366 <para>It opens one new sequent for each constructor of the
367 type of <command>t</command>.</para>
374 <sect1 id="tac_weproceedbycases">
375 <title>we proceed by cases on</title>
376 <titleabbrev>we proceed by cases on</titleabbrev>
377 <para><userinput>we proceed by cases on t to prove th</userinput></para>
380 <varlistentry role="tactic.synopsis">
381 <term>Synopsis:</term>
383 <para><emphasis role="bold">we proceed by cases on</emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
387 <term>Pre-condition:</term>
389 <para><command>t</command> must inhabitant of an inductive type and
390 <command>th</command> must be the conclusion to be proved by
397 <para> It proceeds by cases on <command>t</command> </para>
401 <term>New sequents to prove:</term>
403 <para>It opens one new sequent for each constructor of the
404 type of <command>t</command>.</para>
411 <sect1 id="tac_case">
413 <titleabbrev>case</titleabbrev>
414 <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
417 <varlistentry role="tactic.synopsis">
418 <term>Synopsis:</term>
420 <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis>] … </para>
424 <term>Pre-condition:</term>
426 <para>To be used in a proof by induction or by cases to start
433 <para>Starts the new case <command>id</command> declaring
434 the local parameters <command>(id1:t1) … (idn:tn)</command></para>
438 <term>New sequents to prove:</term>
447 <sect1 id="tac_byinduction">
448 <title>by induction hypothesis we know</title>
449 <titleabbrev>by induction hypothesis we know</titleabbrev>
450 <para><userinput>by induction hypothesis we know t (id)</userinput></para>
453 <varlistentry role="tactic.synopsis">
454 <term>Synopsis:</term>
455 <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
459 <term>Pre-condition:</term>
461 <para>To be used in a proof by induction to state the inductive
468 <para> Introduces the inductive hypothesis. </para>
472 <term>New sequents to prove:</term>
481 <sect1 id="tac_thesisbecomes">
482 <title>the thesis becomes</title>
483 <titleabbrev>the thesis becomes</titleabbrev>
484 <para><userinput>the thesis becomes t</userinput></para>
487 <varlistentry role="tactic.synopsis">
488 <term>Synopsis:</term>
490 <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
494 <term>Pre-condition:</term>
496 <para>The provided term <command>t</command> must be convertible with
497 current sequent.</para>
503 <para>It changes the current goal to the one provided.</para>
507 <term>New sequent to prove:</term>
516 <sect1 id="tac_obtain">
517 <title>conclude/obtain</title>
518 <titleabbrev>conclude/obtain</titleabbrev>
519 <para><userinput>conclude/obtain (H) t1 = t2 justification</userinput></para>
522 <varlistentry role="tactic.synopsis">
523 <term>Synopsis:</term>
525 <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>
529 <term>Pre-condition:</term>
531 <para><command>conclude</command> can be used only if the current
532 sequent is stating an equality. The left hand side must be omitted
533 in an equality chain.</para>
539 <para>Starts or continues an equality chain. If the chain starts
540 with <command>obtain H</command> a new subproof named
541 <command>H</command> is started.</para>
545 <term>New sequent to prove:</term>
547 <para>If the chain starts
548 with <command>obtain H</command> a nre sequent for
549 <command>t2 = ?</command> is opened.