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 -->