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</userinput></para>
20 <varlistentry role="tactic.synopsis">
21 <term>Synopsis:</term>
23 <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis> &sterm;</para>
27 <term>Pre-conditions:</term>
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>
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>
45 <term>New sequents to prove:</term>
54 <sect1 id="tac_suppose">
55 <title>suppose</title>
56 <titleabbrev>suppose</titleabbrev>
57 <para><userinput>suppose t(x) </userinput></para>
60 <varlistentry role="tactic.synopsis">
61 <term>Synopsis:</term>
63 <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
64 <emphasis role="bold">) </emphasis> [ that is equivalent to &term; ]</para>
68 <term>Pre-condition:</term>
70 <para> Da Fare </para>
76 <para> Da Fare </para>
80 <term>New sequents to prove:</term>
89 <sect1 id="tac_bydone">
90 <title>by done</title>
91 <titleabbrev>by done</titleabbrev>
92 <para><userinput>by [ t | _ ] done</userinput></para>
95 <varlistentry role="tactic.synopsis">
96 <term>Synopsis:</term>
98 <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold"> done </emphasis></para>
102 <term>Pre-condition:</term>
104 <para>The term can be omitted with a "_", the running term will come found automatically. </para>
110 <para>It closes the current sequent by applying <command>t</command>, taht it can be one under proof or the main proof.</para>
114 <term>New sequents to prove:</term>
123 <sect1 id="tac_weneedtoprove">
124 <title> we need to prove</title>
125 <titleabbrev>we need to prove</titleabbrev>
126 <para><userinput>we need to prove t [(id)] [or equivalent t]</userinput></para>
129 <varlistentry role="tactic.synopsis">
130 <term>Synopsis:</term>
132 <para><emphasis role="bold">we need to prove</emphasis> &term; </para>
136 <term>Pre-condition:</term>
138 <para> Da Fare </para>
144 <para> Da Fare </para>
148 <term>New sequents to prove:</term>
157 <sect1 id="tac_weproceedbyinduction">
158 <title> we proceed by induction</title>
159 <titleabbrev>we proceed by induction</titleabbrev>
160 <para><userinput>we proceed by induction on t to prove th</userinput></para>
163 <varlistentry role="tactic.synopsis">
164 <term>Synopsis:</term>
166 <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
170 <term>Pre-condition:</term>
172 <para><command>t</command> must inhabit an inductive type and <command>th</command> must be an elimination principle for that inductive type.</para>
178 <para>It proceed on the values of <command>t</command>.</para>
182 <term>New sequents to prove:</term>
184 <para>It opens one new sequent to demonstrate.</para>
191 <sect1 id="tac_weproceedbycases">
192 <title>we proceed by cases</title>
193 <titleabbrev>we proceed by cases</titleabbrev>
194 <para><userinput>we proceed by cases on t to prove t</userinput></para>
197 <varlistentry role="tactic.synopsis">
198 <term>Synopsis:</term>
200 <para><emphasis role="bold">we proceed by cases on </emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
204 <term>Pre-condition:</term>
206 <para> Da Fare </para>
212 <para> Da Fare </para>
216 <term>New sequents to prove:</term>
225 <sect1 id="tac_byinduction">
226 <title>by induction</title>
227 <titleabbrev>by induction</titleabbrev>
228 <para><userinput>by induction hypothesis we know t (id)</userinput></para>
231 <varlistentry role="tactic.synopsis">
232 <term>Synopsis:</term>
234 <para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
238 <term>Pre-condition:</term>
240 <para> Da Fare </para>
246 <para> Da Fare </para>
250 <term>New sequents to prove:</term>
259 <sect1 id="tac_thesisbecomes">
260 <title>thesis becomes</title>
261 <titleabbrev>thesis becomes</titleabbrev>
262 <para><userinput>the thesis becomes t</userinput></para>
265 <varlistentry role="tactic.synopsis">
266 <term>Synopsis:</term>
268 <para><emphasis role ="bold">the thesis becomes</emphasis> &sterm; </para>
272 <term>Pre-condition:</term>
274 <para>Each subterm must be convertible with the term <command>t</command> disambiguate in the context of the matched subterm.</para>
280 <para>It replaces the subterm of the current sequent with the new term</para>
284 <term>New sequence to prove:</term>
293 <sect1 id="tac_case">
295 <titleabbrev>case</titleabbrev>
296 <para><userinput>case id (id:t)list</userinput></para>
299 <varlistentry role="tactic.synopsis">
300 <term>Synopsis:</term>
302 <para><emphasis role="bold">case</emphasis> &id; <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis></para>
306 <term>Pre-condition:</term>
308 <para> Da Fare </para>
314 <para> Da Fare </para>
318 <term>New sequents to prove:</term>
327 <sect1 id="tac_obtain">
328 <title>obtain/conclude</title>
329 <titleabbrev>obtain/conclude</titleabbrev>
330 <para><userinput>obtain H t=t by [t|_] done</userinput></para>
333 <varlistentry role="tactic.synopsis">
334 <term>Synopsis:</term>
336 <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; <emphasis role="bold">by</emphasis> [ &term; | <emphasis role="bold">_</emphasis> [<emphasis role="bold">(</emphasis>&autoparams;<emphasis role="bold">)</emphasis>]] [<emphasis role="bold">done</emphasis>]</para>
340 <term>Pre-condition:</term>
342 <para> Da Fare </para>
348 <para> Da Fare </para>
352 <term>New sequence to prove:</term>
354 <para> Da Fare </para>
361 <sect1 id="tac_bytermweproved">
362 <title>by term we proved</title>
363 <titleabbrev>by term we proved</titleabbrev>
364 <para><userinput>by th we proved t [""|(id)]</userinput></para>
367 <varlistentry role="tactic.synopsis">
368 <term>Synopsis:</term>
370 <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">we proved</emphasis> &term;
371 <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
375 <term>Pre-condition:</term>
377 <para><command>th</command>must have type <command>Prop</command>.
378 <command>id</command>can to be omitted with null</para>
384 <para>It closes the current sequent by applying<command>th</command> to <command>t</command>.</para>
388 <term>New sequence to prove:</term>
390 <para> Da fare </para>
397 <sect1 id="tac_exitselim">
398 <title>exits elim</title>
399 <titleabbrev>exits elim</titleabbrev>
400 <para><userinput>by t let id:t such that t (id)</userinput></para>
403 <varlistentry role="tactic.synopsis">
404 <term>Synopsis:</term>
406 <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">let</emphasis> &id;
407 <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term;
408 <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
412 <term>Pre-condition:</term>
414 <para><command>t</command> must be an inductive type,existential and
415 <command>t (id)</command> must be an elimanation priciple for that inductive type.
422 <para>it proceeds on <command>t</command> to the elimination of the existential one </para>
426 <term>New sequence to prove:</term>
428 <para>It opens one new sequent. The names of the new hypotheses are picked by<command>t (id)</command> </para>
435 <sect1 id="tac_andelim">
436 <title>and elim</title>
437 <titleabbrev>and elim</titleabbrev>
438 <para><userinput>by t we have t (id) and t (id)</userinput></para>
441 <varlistentry role="tactic_synopsis">
442 <term>Synopsis:</term>
444 <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">we have</emphasis> &term;
445 <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
446 <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
450 <term>Pre-condition:</term>
452 <para><command>t</command> must be an logical type,type and </para>
458 <para>It proceeds on the values of <command>t</command>, according to the elimination principle </para>
462 <term>New sequence to prove:</term>
464 <para>It opens one new sequent, the names of the new hypotheses are picked by <command>t(id) and t(id)</command> </para>