matita/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 that is equivalent to 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>
  24              &sterm; [ <emphasis role="bold">that is equivalent to</emphasis>  &term; ]</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 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>
  44         </listitem>
  45       </varlistentry>
  46       <varlistentry>
  47         <term>New sequents to prove:</term>
  48         <listitem>
  49           <para>None.</para>
  50         </listitem>
  51       </varlistentry>
  52     </variablelist>
  53    </para>
  54   </sect1>
  55
  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>
  60   <para>
  61      <variablelist>
  62        <varlistentry role="tactic.synopsis">
  63          <term>Synopsis:</term>
  64          <listitem>
  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>
  67          </listitem>
  68        </varlistentry>
  69       <varlistentry>
  70          <term>Pre-condition:</term>
  71          <listitem>
  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>
  77     </listitem>
  78     </varlistentry>
  79       <varlistentry>
  80          <term>Action:</term>
  81         <listitem>
  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>.
  86         </para>
  87         </listitem>
  88       </varlistentry>
  89       <varlistentry>
  90         <term>New sequents to prove:</term>
  91         <listitem>
  92           <para>None.</para>
  93         </listitem>
  94       </varlistentry>
  95     </variablelist>
  96    </para>
  97   </sect1>
  98
  99 <sect1 id="tac_let">
 100     <title>letin</title>
 101     <titleabbrev>letin</titleabbrev>
 102     <para><userinput>let x := T </userinput></para>
 103   <para>
 104      <variablelist>
 105        <varlistentry role="tactic.synopsis">
 106          <term>Synopsis:</term>
 107          <listitem>
 108          <para><emphasis role="bold">let</emphasis> &id; <emphasis role="bold"> = </emphasis> &term;</para>
 109          </listitem>
 110        </varlistentry>
 111       <varlistentry>
 112          <term>Pre-condition:</term>
 113          <listitem>
 114            <para>None</para>
 115         </listitem>
 116       </varlistentry>
 117       <varlistentry>
 118         <term>Action:</term>
 119         <listitem>
 120         <para>It adds a new local definition <command>x := T</command> to the context of the sequent to prove.</para>
 121         </listitem>
 122       </varlistentry>
 123       <varlistentry>
 124         <term>New sequents to prove:</term>
 125         <listitem>
 126           <para>None.</para>
 127         </listitem>
 128       </varlistentry>
 129     </variablelist>
 130    </para>
 131   </sect1>
 132
 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>
 137      <para>
 138        <variablelist>
 139          <varlistentry role="tactic.synopsis">
 140            <term>Synopsis:</term>
 141            <listitem>
 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>
 145            </listitem>
 146            </varlistentry>
 147            <varlistentry>
 148              <term>Pre-condition:</term>
 149              <listitem>
 150                <para><command>T</command> must have type <command>Prop</command>.
 151          </para>
 152              </listitem>
 153            </varlistentry>
 154            <varlistentry>
 155              <term>Action:</term>
 156              <listitem>
 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>.
 162
 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).
 164          </para>
 165              </listitem>
 166            </varlistentry>
 167            <varlistentry>
 168              <term>New sequent to prove:</term>
 169              <listitem>
 170                <para>None.</para>
 171              </listitem>
 172            </varlistentry>
 173          </variablelist>
 174        </para>
 175     </sect1>
 176
 177  <sect1 id="tac_bydone">
 178    <title>done</title>
 179    <titleabbrev>done</titleabbrev>
 180    <para><userinput>justification done</userinput></para>
 181    <para>
 182      <variablelist>
 183        <varlistentry role="tactic.synopsis">
 184          <term>Synopsis:</term>
 185          <listitem>
 186            <para>&justification; <emphasis role="bold">done</emphasis></para>
 187          </listitem>
 188        </varlistentry>
 189        <varlistentry>
 190          <term>Pre-condition:</term>
 191          <listitem>
 192            <para></para>
 193          </listitem>
 194        </varlistentry>
 195        <varlistentry>
 196          <term>Action:</term>
 197            <listitem>
 198              <para>It closes the current sequent given the justification.</para>
 199            </listitem>
 200        </varlistentry>
 201        <varlistentry>
 202            <term>New sequents to prove:</term>
 203            <listitem>
 204                <para>None.</para>
 205            </listitem>
 206        </varlistentry>
 207    </variablelist>
 208      </para>
 209   </sect1>
 210
 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>
 215     </para>
 216     <para>
 217       <variablelist>
 218         <varlistentry role="tactic.synopsis">
 219           <term>Synopsis:</term>
 220           <listitem>
 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>
 224           </listitem>
 225         </varlistentry>
 226         <varlistentry>
 227           <term>Pre-condition:</term>
 228           <listitem>
 229       <para>
 230             </para>
 231           </listitem>
 232         </varlistentry>
 233         <varlistentry>
 234           <term>Action:</term>
 235           <listitem>
 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>.
 241       </para>
 242           </listitem>
 243         </varlistentry>
 244         <varlistentry>
 245           <term>New sequent to prove:</term>
 246           <listitem>
 247       <para>None.</para>
 248           </listitem>
 249         </varlistentry>
 250      </variablelist>
 251     </para>
 252   </sect1>
 253
 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>
 258     </para>
 259     <para>
 260       <variablelist>
 261         <varlistentry role="tactic_synopsis">
 262           <term>Synopsis:</term>
 263           <listitem>
 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>
 267           </listitem>
 268         </varlistentry>
 269         <varlistentry>
 270           <term>Pre-condition:</term>
 271           <listitem>
 272             <para></para>
 273           </listitem>
 274         </varlistentry>
 275         <varlistentry>
 276           <term>Action:</term>
 277           <listitem>
 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>.
 282       </para>
 283           </listitem>
 284         </varlistentry>
 285         <varlistentry>
 286           <term>New sequent to prove:</term>
 287           <listitem>
 288              <para>None.</para>
 289           </listitem>
 290         </varlistentry>
 291       </variablelist>
 292     </para>
 293   </sect1>
 294
 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>
 299     <para>
 300       <variablelist>
 301         <varlistentry role="tactic.synopsis">
 302           <term>Synopsis:</term>
 303           <listitem>
 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>
 308           </listitem>
 309         </varlistentry>
 310         <varlistentry>
 311           <term>Pre-condition:</term>
 312           <listitem>
 313             <para></para>
 314           </listitem>
 315         </varlistentry>
 316         <varlistentry>
 317           <term>Action:</term>
 318             <listitem>
 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>.
 324             </para>
 325             </listitem>
 326         </varlistentry>
 327         <varlistentry>
 328            <term>New sequents to prove:</term>
 329            <listitem>
 330              <para>The stated one if <command>id</command> is provided</para>
 331            </listitem>
 332         </varlistentry>
 333      </variablelist>
 334     </para>
 335   </sect1>
 336
 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>
 341     <para>
 342       <variablelist>
 343         <varlistentry role="tactic.synopsis">
 344           <term>Synopsis:</term>
 345           <listitem>
 346             <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
 347           </listitem>
 348         </varlistentry>
 349         <varlistentry>
 350           <term>Pre-condition:</term>
 351           <listitem>
 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.
 354         </para>
 355           </listitem>
 356         </varlistentry>
 357         <varlistentry>
 358           <term>Action:</term>
 359             <listitem>
 360               <para>It proceed by induction on <command>t</command>.</para>
 361             </listitem>
 362         </varlistentry>
 363         <varlistentry>
 364             <term>New sequents to prove:</term>
 365             <listitem>
 366               <para>It opens one new sequent for each constructor of the
 367                 type of <command>t</command>.</para>
 368             </listitem>
 369         </varlistentry>
 370       </variablelist>
 371     </para>
 372   </sect1>
 373
 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>
 378       <para>
 379         <variablelist>
 380           <varlistentry role="tactic.synopsis">
 381             <term>Synopsis:</term>
 382             <listitem>
 383               <para><emphasis role="bold">we proceed by cases on</emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
 384              </listitem>
 385           </varlistentry>
 386           <varlistentry>
 387             <term>Pre-condition:</term>
 388             <listitem>
 389         <para><command>t</command> must inhabitant of an inductive type and
 390           <command>th</command> must be the conclusion to be proved by
 391           cases.</para>
 392             </listitem>
 393           </varlistentry>
 394           <varlistentry>
 395             <term>Action:</term>
 396               <listitem>
 397           <para> It proceeds by cases on <command>t</command> </para>
 398               </listitem>
 399           </varlistentry>
 400           <varlistentry>
 401             <term>New sequents to prove:</term>
 402             <listitem>
 403                <para>It opens one new sequent for each constructor of the
 404                 type of <command>t</command>.</para>
 405             </listitem>
 406           </varlistentry>
 407          </variablelist>
 408        </para>
 409     </sect1>
 410
 411    <sect1 id="tac_case">
 412      <title>case</title>
 413      <titleabbrev>case</titleabbrev>
 414      <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
 415      <para>
 416        <variablelist>
 417          <varlistentry role="tactic.synopsis">
 418            <term>Synopsis:</term>
 419            <listitem>
 420              <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term;  <emphasis role="bold">)</emphasis>] … </para>
 421            </listitem>
 422          </varlistentry>
 423          <varlistentry>
 424             <term>Pre-condition:</term>
 425             <listitem>
 426         <para>To be used in a proof by induction or by cases to start
 427           a new case</para>
 428             </listitem>
 429          </varlistentry>
 430          <varlistentry>
 431             <term>Action:</term>
 432             <listitem>
 433               <para>Starts the new case <command>id</command> declaring
 434                 the local parameters <command>(id1:t1) … (idn:tn)</command></para>
 435             </listitem>
 436          </varlistentry>
 437          <varlistentry>
 438            <term>New sequents to prove:</term>
 439            <listitem>
 440                <para>None</para>
 441            </listitem>
 442          </varlistentry>
 443        </variablelist>
 444      </para>
 445   </sect1>
 446
 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>
 451       <para>
 452         <variablelist>
 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>
 456             </listitem>
 457           </varlistentry>
 458           <varlistentry>
 459             <term>Pre-condition:</term>
 460             <listitem>
 461         <para>To be used in a proof by induction to state the inductive
 462           hypothesis.</para>
 463             </listitem>
 464           </varlistentry>
 465           <varlistentry>
 466             <term>Action:</term>
 467               <listitem>
 468                 <para> Introduces the inductive hypothesis. </para>
 469               </listitem>
 470           </varlistentry>
 471           <varlistentry>
 472              <term>New sequents to prove:</term>
 473                  <listitem>
 474                  <para>None.</para>
 475                  </listitem>
 476           </varlistentry>
 477          </variablelist>
 478       </para>
 479     </sect1>
 480
 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>
 485      <para>
 486         <variablelist>
 487            <varlistentry role="tactic.synopsis">
 488              <term>Synopsis:</term>
 489              <listitem>
 490                <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
 491              </listitem>
 492            </varlistentry>
 493            <varlistentry>
 494              <term>Pre-condition:</term>
 495              <listitem>
 496          <para>The provided term <command>t</command> must be convertible with
 497            current sequent.</para>
 498              </listitem>
 499            </varlistentry>
 500            <varlistentry>
 501              <term>Action:</term>
 502              <listitem>
 503                <para>It changes the current goal to the one provided.</para>
 504              </listitem>
 505            </varlistentry>
 506            <varlistentry>
 507              <term>New sequent to prove:</term>
 508              <listitem>
 509                <para>None.</para>
 510              </listitem>
 511            </varlistentry>
 512          </variablelist>
 513        </para>
 514    </sect1>
 515
 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>
 520     <para>
 521       <variablelist>
 522          <varlistentry role="tactic.synopsis">
 523            <term>Synopsis:</term>
 524            <listitem>
 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>
 526            </listitem>
 527          </varlistentry>
 528          <varlistentry>
 529            <term>Pre-condition:</term>
 530              <listitem>
 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>
 534        </listitem>
 535          </varlistentry>
 536          <varlistentry>
 537            <term>Action:</term>
 538            <listitem>
 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>
 542            </listitem>
 543          </varlistentry>
 544          <varlistentry>
 545            <term>New sequent to prove:</term>
 546              <listitem>
 547                 <para>If the chain starts
 548             with <command>obtain H</command> a nre sequent for
 549             <command>t2 = ?</command> is opened.
 550           </para>
 551              </listitem>
 552          </varlistentry>
 553        </variablelist>
 554      </para>
 555    </sect1>
 556
 557
 558
 559
 560
 561
 562
 563 </chapter>