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_suppose">
  55     <title>suppose</title>
  56     <titleabbrev>suppose</titleabbrev>
  57     <para><userinput>suppose t(x) </userinput></para>
  58   <para>
  59      <variablelist>
  60        <varlistentry role="tactic.synopsis">
  61          <term>Synopsis:</term>
  62          <listitem>
  63            <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
  64              <emphasis role="bold">) </emphasis> [ that is equivalent to  &term; ]</para>
  65          </listitem>
  66        </varlistentry>
  67       <varlistentry>
  68          <term>Pre-condition:</term>
  69          <listitem>
  70            <para> &TODO; </para>
  71          </listitem>
  72       </varlistentry>
  73       <varlistentry>
  74         <term>Action:</term>
  75           <listitem>
  76             <para> &TODO; </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_bydone">
  90    <title>by done</title>
  91    <titleabbrev>by done</titleabbrev>
  92    <para><userinput>by [ t | _ ] done</userinput></para>
  93    <para>
  94      <variablelist>
  95        <varlistentry role="tactic.synopsis">
  96          <term>Synopsis:</term>
  97          <listitem>
  98            <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold"> done </emphasis></para>
  99          </listitem>
 100        </varlistentry>
 101        <varlistentry>
 102          <term>Pre-condition:</term>
 103          <listitem>
 104            <para>The term can be omitted with a "_", the running term will come found automatically. </para>
 105          </listitem>
 106        </varlistentry>
 107        <varlistentry>
 108          <term>Action:</term>
 109            <listitem>
 110              <para>It closes the current sequent by applying <command>t</command>, taht it can be one under proof or the main proof.</para>
 111            </listitem>
 112        </varlistentry>
 113        <varlistentry>
 114            <term>New sequents to prove:</term>
 115            <listitem>
 116                <para>None.</para>
 117            </listitem>
 118        </varlistentry>
 119    </variablelist>
 120      </para>
 121   </sect1>
 122
 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>
 127     <para>
 128       <variablelist>
 129         <varlistentry role="tactic.synopsis">
 130           <term>Synopsis:</term>
 131           <listitem>
 132              <para><emphasis role="bold">we need to prove</emphasis> &term; </para>
 133           </listitem>
 134         </varlistentry>
 135         <varlistentry>
 136           <term>Pre-condition:</term>
 137           <listitem>
 138             <para> &TODO; </para>
 139           </listitem>
 140         </varlistentry>
 141         <varlistentry>
 142           <term>Action:</term>
 143             <listitem>
 144               <para> &TODO; </para>
 145             </listitem>
 146         </varlistentry>
 147         <varlistentry>
 148            <term>New sequents to prove:</term>
 149            <listitem>
 150              <para>None.</para>
 151            </listitem>
 152         </varlistentry>
 153      </variablelist>
 154     </para>
 155   </sect1>
 156
 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>
 161     <para>
 162       <variablelist>
 163         <varlistentry role="tactic.synopsis">
 164           <term>Synopsis:</term>
 165           <listitem>
 166             <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
 167           </listitem>
 168         </varlistentry>
 169         <varlistentry>
 170           <term>Pre-condition:</term>
 171           <listitem>
 172             <para><command>t</command> must inhabit an inductive type and <command>th</command> must be an elimination principle for that inductive type.</para>
 173           </listitem>
 174         </varlistentry>
 175         <varlistentry>
 176           <term>Action:</term>
 177             <listitem>
 178               <para>It proceed on the values of <command>t</command>.</para>
 179             </listitem>
 180         </varlistentry>
 181         <varlistentry>
 182             <term>New sequents to prove:</term>
 183             <listitem>
 184                <para>It opens one new sequent to demonstrate.</para>
 185             </listitem>
 186         </varlistentry>
 187       </variablelist>
 188     </para>
 189   </sect1>
 190
 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>
 195       <para>
 196         <variablelist>
 197           <varlistentry role="tactic.synopsis">
 198             <term>Synopsis:</term>
 199             <listitem>
 200               <para><emphasis role="bold">we proceed by cases on </emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
 201              </listitem>
 202           </varlistentry>
 203           <varlistentry>
 204             <term>Pre-condition:</term>
 205             <listitem>
 206               <para> &TODO; </para>
 207             </listitem>
 208           </varlistentry>
 209           <varlistentry>
 210             <term>Action:</term>
 211               <listitem>
 212                 <para> &TODO; </para>
 213               </listitem>
 214           </varlistentry>
 215           <varlistentry>
 216             <term>New sequents to prove:</term>
 217             <listitem>
 218                <para>None.</para>
 219             </listitem>
 220           </varlistentry>
 221          </variablelist>
 222        </para>
 223     </sect1>
 224
 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>
 229       <para>
 230         <variablelist>
 231           <varlistentry role="tactic.synopsis">
 232             <term>Synopsis:</term>
 233             <listitem>
 234               <para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
 235             </listitem>
 236           </varlistentry>
 237           <varlistentry>
 238             <term>Pre-condition:</term>
 239             <listitem>
 240               <para> &TODO; </para>
 241             </listitem>
 242           </varlistentry>
 243           <varlistentry>
 244             <term>Action:</term>
 245               <listitem>
 246                 <para> &TODO; </para>
 247               </listitem>
 248           </varlistentry>
 249           <varlistentry>
 250              <term>New sequents to prove:</term>
 251                  <listitem>
 252                  <para>None.</para>
 253                  </listitem>
 254           </varlistentry>
 255          </variablelist>
 256       </para>
 257     </sect1>
 258
 259    <sect1 id="tac_thesisbecomes">
 260      <title>thesis becomes</title>
 261      <titleabbrev>thesis becomes</titleabbrev>
 262      <para><userinput>the thesis becomes t</userinput></para>
 263      <para>
 264         <variablelist>
 265            <varlistentry role="tactic.synopsis">
 266              <term>Synopsis:</term>
 267              <listitem>
 268                <para><emphasis role ="bold">the thesis becomes</emphasis> &sterm; </para>
 269              </listitem>
 270            </varlistentry>
 271            <varlistentry>
 272              <term>Pre-condition:</term>
 273              <listitem>
 274                <para>Each subterm must be convertible with the term <command>t</command> disambiguate in the context of the matched subterm.</para>
 275              </listitem>
 276            </varlistentry>
 277            <varlistentry>
 278              <term>Action:</term>
 279              <listitem>
 280                <para>It replaces the subterm of the current sequent with the new term</para>
 281              </listitem>
 282            </varlistentry>
 283            <varlistentry>
 284              <term>New sequence to prove:</term>
 285              <listitem>
 286                <para>None.</para>
 287              </listitem>
 288            </varlistentry>
 289          </variablelist>
 290        </para>
 291    </sect1>
 292
 293    <sect1 id="tac_case">
 294      <title>case</title>
 295      <titleabbrev>case</titleabbrev>
 296      <para><userinput>case id (id:t)list</userinput></para>
 297      <para>
 298        <variablelist>
 299          <varlistentry role="tactic.synopsis">
 300            <term>Synopsis:</term>
 301            <listitem>
 302              <para><emphasis role="bold">case</emphasis> &id; <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis></para>
 303            </listitem>
 304          </varlistentry>
 305          <varlistentry>
 306             <term>Pre-condition:</term>
 307             <listitem>
 308                 <para> &TODO; </para>
 309             </listitem>
 310          </varlistentry>
 311          <varlistentry>
 312             <term>Action:</term>
 313             <listitem>
 314               <para> &TODO; </para>
 315             </listitem>
 316          </varlistentry>
 317          <varlistentry>
 318            <term>New sequents to prove:</term>
 319            <listitem>
 320                <para>&TODO;</para>
 321            </listitem>
 322          </varlistentry>
 323        </variablelist>
 324      </para>
 325   </sect1>
 326
 327   <sect1 id="tac_obtain">
 328     <title>obtain/conclude</title>
 329     <titleabbrev>obtain/conclude</titleabbrev>
 330     <para><userinput>obtain H t=t [auto_params | exact t| proof | using t] done</userinput></para>
 331     <para>
 332       <variablelist>
 333          <varlistentry role="tactic.synopsis">
 334            <term>Synopsis:</term>
 335            <listitem>
 336              <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">exact</emphasis> &term; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
 337            </listitem>
 338          </varlistentry>
 339          <varlistentry>
 340            <term>Pre-condition:</term>
 341              <listitem>
 342                <para> &TODO; </para>
 343              </listitem>
 344          </varlistentry>
 345          <varlistentry>
 346            <term>Action:</term>
 347            <listitem>
 348               <para> &TODO; </para>
 349            </listitem>
 350          </varlistentry>
 351          <varlistentry>
 352            <term>New sequence to prove:</term>
 353              <listitem>
 354                 <para> &TODO; </para>
 355              </listitem>
 356          </varlistentry>
 357        </variablelist>
 358      </para>
 359    </sect1>
 360
 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>
 365      <para>
 366        <variablelist>
 367          <varlistentry role="tactic.synopsis">
 368            <term>Synopsis:</term>
 369            <listitem>
 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>
 372            </listitem>
 373            </varlistentry>
 374            <varlistentry>
 375              <term>Pre-condition:</term>
 376              <listitem>
 377                <para><command>th</command>must have type <command>Prop</command>.
 378                      <command>id</command>can to be omitted with null</para>
 379              </listitem>
 380            </varlistentry>
 381            <varlistentry>
 382              <term>Action:</term>
 383              <listitem>
 384                <para>It closes the current sequent by applying<command>th</command> to <command>t</command>.</para>
 385              </listitem>
 386            </varlistentry>
 387            <varlistentry>
 388              <term>New sequence to prove:</term>
 389              <listitem>
 390                <para> &TODO; </para>
 391              </listitem>
 392            </varlistentry>
 393          </variablelist>
 394        </para>
 395     </sect1>
 396
 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>
 401     <para>
 402       <variablelist>
 403         <varlistentry role="tactic.synopsis">
 404           <term>Synopsis:</term>
 405           <listitem>
 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>
 409           </listitem>
 410         </varlistentry>
 411         <varlistentry>
 412           <term>Pre-condition:</term>
 413           <listitem>
 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.
 416             </para>
 417           </listitem>
 418         </varlistentry>
 419         <varlistentry>
 420           <term>Action:</term>
 421           <listitem>
 422             <para>it proceeds on <command>t</command> to the elimination of the existential one </para>
 423           </listitem>
 424         </varlistentry>
 425         <varlistentry>
 426           <term>New sequence to prove:</term>
 427           <listitem>
 428             <para>It opens one new sequent. The names of the new hypotheses are picked by<command>t (id)</command> </para>
 429           </listitem>
 430         </varlistentry>
 431      </variablelist>
 432     </para>
 433   </sect1>
 434
 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>
 439     <para>
 440       <variablelist>
 441         <varlistentry role="tactic_synopsis">
 442           <term>Synopsis:</term>
 443           <listitem>
 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>
 447           </listitem>
 448         </varlistentry>
 449         <varlistentry>
 450           <term>Pre-condition:</term>
 451           <listitem>
 452             <para><command>t</command> must be an logical type,type and  </para>
 453           </listitem>
 454         </varlistentry>
 455         <varlistentry>
 456           <term>Action:</term>
 457           <listitem>
 458             <para>It proceeds on the values of <command>t</command>, according to the elimination principle </para>
 459           </listitem>
 460         </varlistentry>
 461         <varlistentry>
 462           <term>New sequence to prove:</term>
 463           <listitem>
 464              <para>It opens one new sequent, the names of the new hypotheses are picked by <command>t(id) and t(id)</command> </para>
 465           </listitem>
 466         </varlistentry>
 467       </variablelist>
 468     </para>
 469   </sect1>
 470
 471 </chapter>