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</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; </para>
  25        </listitem>
  26       </varlistentry>
  27       <varlistentry>
  28         <term>Pre-conditions:</term>
  29         <listitem>
  30         <para>
  31             The conclusion of the sequent to prove must be a universal quantification.
  32        </para>
  33         </listitem>
  34       </varlistentry>
  35       <varlistentry>
  36         <term>Action:</term>
  37         <listitem>
  38         <para>
  39             It applies the right introduction rule for the universal quantifier, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the quantifier).
  40         </para>
  41         </listitem>
  42       </varlistentry>
  43       <varlistentry>
  44         <term>New sequents to prove:</term>
  45         <listitem>
  46         <para>
  47             It opens a new sequent to prove the quantified subformula adding <command>x : T</command> to the hypotheses.
  48         </para>
  49         </listitem>
  50       </varlistentry>
  51     </variablelist>
  52    </para>
  53   </sect1>
  54
  55   <sect1 id="tac_suppose">
  56     <title>suppose</title>
  57     <titleabbrev>suppose</titleabbrev>
  58     <para><userinput>suppose A (H)</userinput></para>
  59   <para>
  60      <variablelist>
  61        <varlistentry role="tactic.synopsis">
  62          <term>Synopsis:</term>
  63          <listitem>
  64            <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
  65              <emphasis role="bold">) </emphasis></para>
  66          </listitem>
  67        </varlistentry>
  68       <varlistentry>
  69          <term>Pre-condition:</term>
  70         <listitem>
  71         <para>
  72             The conclusion of the sequent to prove must be an implication.
  73        </para>
  74         </listitem>
  75     </varlistentry>
  76       <varlistentry>
  77          <term>Action:</term>
  78         <listitem>
  79         <para>
  80             It applies the right introduction rule for the implication, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the implication).
  81         </para>
  82         </listitem>
  83       </varlistentry>
  84       <varlistentry>
  85         <term>New sequents to prove:</term>
  86         <listitem>
  87         <para>
  88                 It opens a new sequent to prove the consequent of the implication adding the antecedent <command>A</command> to the hypotheses. The name of the new hypothesis is <command>H</command>.
  89         </para>
  90         </listitem>
  91       </varlistentry>
  92     </variablelist>
  93    </para>
  94   </sect1>
  95
  96 <sect1 id="tac_let">
  97     <title>letin</title>
  98     <titleabbrev>letin</titleabbrev>
  99     <para><userinput>let x := T </userinput></para>
 100   <para>
 101      <variablelist>
 102        <varlistentry role="tactic.synopsis">
 103          <term>Synopsis:</term>
 104          <listitem>
 105          <para><emphasis role="bold">let</emphasis> &id; <emphasis role="bold"> = </emphasis> &term;</para>
 106          </listitem>
 107        </varlistentry>
 108       <varlistentry>
 109          <term>Pre-condition:</term>
 110          <listitem>
 111            <para>None</para>
 112         </listitem>
 113       </varlistentry>
 114       <varlistentry>
 115         <term>Action:</term>
 116         <listitem>
 117         <para>It adds a new local definition <command>x := T</command> to the context of the sequent to prove.</para>
 118         </listitem>
 119       </varlistentry>
 120       <varlistentry>
 121         <term>New sequents to prove:</term>
 122         <listitem>
 123           <para>None.</para>
 124         </listitem>
 125       </varlistentry>
 126     </variablelist>
 127    </para>
 128   </sect1>
 129
 130   <sect1 id="tac_thatisequivalentto">
 131       <title>that is equivalent to</title>
 132       <titleabbrev>that is equivalent to</titleabbrev>
 133       <para><userinput>that is equivalent to t</userinput></para>
 134     <para>
 135       <variablelist>
 136          <varlistentry role="tactic.synopsis">
 137            <term>Synopsis:</term>
 138            <listitem>
 139            <para>
 140                <emphasis role="bold">that is equivalent to</emphasis> &term;
 141            </para>
 142            </listitem>
 143          </varlistentry>
 144          <varlistentry>
 145            <term>Pre-condition:</term>
 146              <listitem>
 147              <para>
 148                  The user must have applied one of the following tactics immediately before applying this tactic: <emphasis role="bold">assume</emphasis>, <emphasis role="bold">suppose</emphasis>, <emphasis role="bold">we need to prove</emphasis>, <emphasis role="bold">by just we proved</emphasis>,<emphasis role="bold">the thesis becomes</emphasis>, <emphasis role="bold">that is equivalent to</emphasis>.
 149              </para>
 150        </listitem>
 151          </varlistentry>
 152          <varlistentry>
 153            <term>Action:</term>
 154            <listitem>
 155            <para>
 156                    If the tactic that was applied before this introduced a new hypothesis in the context, this tactic works on this hypothesis; otherwise, it works on the conclusion. Either way, if the term <command>t</command> is beta-equivalent to the term <command>t1</command> on which this tactic is working (i.e. they can be reduced to a common term), <command>t1</command> is changed with <command>t</command>.
 157
 158                        If the tactic that was applied before this tactic was <emphasis role="bold">that is equivalent to</emphasis>, and that tactic was working on a term <command>t1</command>, this tactic keeps working on <command>t1</command>.
 159            </para>
 160            </listitem>
 161          </varlistentry>
 162          <varlistentry>
 163            <term>New sequent to prove:</term>
 164              <listitem>
 165              <para>
 166                      If this tactic is working on the conclusion, a new sequent with the same hypotheses and the conclusion changed to <command>t</command> is opened. If this tactic is working on the last introduced hypotesis, a new sequent with the same conclusion is opened. The hypotheses of this sequent are the same, except for the one on which the tactic is working on, which is changed with <command>t</command>.
 167              </para>
 168              </listitem>
 169          </varlistentry>
 170        </variablelist>
 171      </para>
 172    </sect1>
 173
 174    <sect1 id="tac_thesisbecomes">
 175      <title>the thesis becomes</title>
 176      <titleabbrev>the thesis becomes</titleabbrev>
 177      <para><userinput>the thesis becomes P</userinput></para>
 178      <para>
 179         <variablelist>
 180            <varlistentry role="tactic.synopsis">
 181              <term>Synopsis:</term>
 182              <listitem>
 183                <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
 184              </listitem>
 185            </varlistentry>
 186            <varlistentry>
 187              <term>Pre-condition:</term>
 188              <listitem>
 189          <para>The provided term <command>P</command> must be identical to the current conclusion.</para>
 190              </listitem>
 191            </varlistentry>
 192            <varlistentry>
 193              <term>Action:</term>
 194              <listitem>
 195                <para>It allows the user to start a chain of reductions on the conclusion with the tactic <emphasis role="bold">that is equivalent to</emphasis>, after stating the current conclusion.</para>
 196              </listitem>
 197            </varlistentry>
 198            <varlistentry>
 199              <term>New sequent to prove:</term>
 200              <listitem>
 201                <para>None.</para>
 202              </listitem>
 203            </varlistentry>
 204          </variablelist>
 205        </para>
 206    </sect1>
 207
 208   <sect1 id="tac_weneedtoprove">
 209     <title>we need to prove</title>
 210     <titleabbrev>we need to prove</titleabbrev>
 211     <para><userinput>we need to prove T [(H)]</userinput></para>
 212     <para>
 213       <variablelist>
 214         <varlistentry role="tactic.synopsis">
 215           <term>Synopsis:</term>
 216           <listitem>
 217       <para><emphasis role="bold">we need to prove</emphasis> &term;
 218         [<emphasis role="bold">(</emphasis>&id;
 219         <emphasis role="bold">)</emphasis>]
 220         </para>
 221           </listitem>
 222         </varlistentry>
 223         <varlistentry>
 224           <term>Pre-condition:</term>
 225           <listitem>
 226             <para>None.</para>
 227           </listitem>
 228         </varlistentry>
 229         <varlistentry>
 230           <term>Action:</term>
 231             <listitem>
 232             <para>If <command>id</command> is provided, it applies a logical cut on <command>T</command>. Otherwise, it allows the user to start a chain of reductions on the conclusion with the tactic <emphasis role="bold">that is equivalent to</emphasis>.
 233             </para>
 234             </listitem>
 235         </varlistentry>
 236         <varlistentry>
 237            <term>New sequents to prove:</term>
 238            <listitem>
 239            <para>If <command>id</command> is supplied, a new sequent with <command>T</command> as the conclusion is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with <command>H:T</command> added to the hypotheses.</para>
 240            </listitem>
 241         </varlistentry>
 242      </variablelist>
 243     </para>
 244   </sect1>
 245
 246  <sect1 id="tac_bytermweproved">
 247    <title>we proved</title>
 248      <titleabbrev>we proved</titleabbrev>
 249          <para><userinput>justification we proved T [(id)]</userinput></para>
 250      <para>
 251        <variablelist>
 252          <varlistentry role="tactic.synopsis">
 253            <term>Synopsis:</term>
 254            <listitem>
 255              <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
 256          [<emphasis role="bold">(</emphasis> &id;
 257          <emphasis role="bold">)</emphasis>]
 258      </para>
 259            </listitem>
 260            </varlistentry>
 261            <varlistentry>
 262              <term>Pre-condition:</term>
 263              <listitem>
 264              <para>
 265                  None.
 266              </para>
 267              </listitem>
 268            </varlistentry>
 269            <varlistentry>
 270              <term>Action:</term>
 271              <listitem>
 272              <para>
 273                      If <command>id</command> is supplied, a logical cut on <command>T</command> is made. Otherwise, if <command>T</command> is identical to the current conclusion, it allows the user to start a chain of reductions on the conclusion with the tactic <emphasis role="bold">that is equivalent to</emphasis>.
 274              </para>
 275              </listitem>
 276            </varlistentry>
 277            <varlistentry>
 278              <term>New sequent to prove:</term>
 279              <listitem>
 280              <para>
 281                      If <command>id</command> is supplied, a new sequent with <command>T</command> as the conclusion is opened and then immediately closed using the supplied justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and a new hypotesis <command>T</command> is added to the context, with name <command>id</command>.
 282                          If <command>id</command> is not supplied, no new sequents are opened.
 283              </para>
 284              </listitem>
 285            </varlistentry>
 286          </variablelist>
 287        </para>
 288     </sect1>
 289
 290
 291   <sect1 id="tac_existselim">
 292     <title>let such that</title>
 293     <titleabbrev>let such that</titleabbrev>
 294     <para><userinput>justification let x:T such that P (H)</userinput>
 295     </para>
 296     <para>
 297       <variablelist>
 298         <varlistentry role="tactic.synopsis">
 299           <term>Synopsis:</term>
 300           <listitem>
 301             <para>&justification; <emphasis role="bold">let</emphasis> &id;
 302                     <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term;
 303                      <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
 304           </listitem>
 305         </varlistentry>
 306         <varlistentry>
 307           <term>Pre-condition:</term>
 308           <listitem>
 309       <para>
 310           None.
 311             </para>
 312           </listitem>
 313         </varlistentry>
 314         <varlistentry>
 315           <term>Action:</term>
 316           <listitem>
 317           <para>
 318               It applies the left introduction rule of the existential quantifier on the formula <command>∃ x. P(x)</command> (in Natural Deduction this corresponds to the elimination rule for the quantifier).
 319           </para>
 320           </listitem>
 321         </varlistentry>
 322         <varlistentry>
 323           <term>New sequent to prove:</term>
 324           <listitem>
 325       <para>A new sequent with <command>∃ x. P(x)</command> as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses <command>x : T</command> and <command>H : P</command> are added to the context.</para>
 326           </listitem>
 327         </varlistentry>
 328      </variablelist>
 329     </para>
 330   </sect1>
 331
 332   <sect1 id="tac_andelim">
 333     <title>we have</title>
 334     <titleabbrev>we have</titleabbrev>
 335     <para><userinput>justification we have A (H1) and B (H2)</userinput>
 336     </para>
 337     <para>
 338       <variablelist>
 339         <varlistentry role="tactic_synopsis">
 340           <term>Synopsis:</term>
 341           <listitem>
 342             <para>&justification; <emphasis role="bold">we have</emphasis> &term;
 343                     <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
 344                       <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
 345           </listitem>
 346         </varlistentry>
 347         <varlistentry>
 348           <term>Pre-condition:</term>
 349           <listitem>
 350           <para>
 351               None.
 352           </para>
 353           </listitem>
 354         </varlistentry>
 355         <varlistentry>
 356           <term>Action:</term>
 357           <listitem>
 358           <para>
 359                   It applies the left multiplicative introduction rule for the conjunction on the formula <command>A ∧ B</command> (in Natural Deduction this corresponds to the elimination rule for the conjunction).
 360           </para>
 361           </listitem>
 362         </varlistentry>
 363         <varlistentry>
 364           <term>New sequent to prove:</term>
 365           <listitem>
 366       <para>A new sequent with <command>A ∧ B</command> as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses <command>H1 : A</command> and <command>H2 : B</command> are added to the context.</para>
 367           </listitem>
 368         </varlistentry>
 369       </variablelist>
 370     </para>
 371   </sect1>
 372
 373
 374     <sect1 id="tac_weproceedbyinduction">
 375     <title>we proceed by induction on</title>
 376     <titleabbrev>we proceed by induction on</titleabbrev>
 377     <para><userinput>we proceed by induction on t to prove P</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 induction 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>The type of <command>t</command> must be an inductive type and <command>P</command> must be identical to the current conclusion.
 390         </para>
 391           </listitem>
 392         </varlistentry>
 393         <varlistentry>
 394           <term>Action:</term>
 395             <listitem>
 396             <para>It applies the induction principle on <command>t</command> to prove <command>P</command>.</para>
 397             </listitem>
 398         </varlistentry>
 399         <varlistentry>
 400             <term>New sequents to prove:</term>
 401             <listitem>
 402                 <para>It opens a new sequent for each constructor of the type of <command>t</command>, each with the conclusion <command>P</command> instantiated for the constructor. For the inductive constructors (i.e. if the inductive type is <command>T</command>, constructors with an argument of type <command>T</command>), the conclusion is a logical implication, where the antecedent is the inductive hypothesis for the constructor, and the consequent is <command>P</command>.</para>
 403             </listitem>
 404         </varlistentry>
 405       </variablelist>
 406     </para>
 407   </sect1>
 408
 409   <sect1 id="tac_weproceedbycases">
 410     <title>we proceed by cases on</title>
 411       <titleabbrev>we proceed by cases on</titleabbrev>
 412       <para><userinput>we proceed by cases on t to prove P</userinput></para>
 413       <para>
 414         <variablelist>
 415           <varlistentry role="tactic.synopsis">
 416             <term>Synopsis:</term>
 417             <listitem>
 418               <para><emphasis role="bold">we proceed by cases on</emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
 419              </listitem>
 420           </varlistentry>
 421           <varlistentry>
 422             <term>Pre-condition:</term>
 423             <listitem>
 424       <para>The type of <command>t</command> must be an inductive type and <command>P</command> must be identical to the current conclusion.
 425         </para>
 426         <!--para><command>t</command> must inhabitant of an inductive type and
 427           <command>th</command> must be the conclusion to be proved by
 428           cases.</para-->
 429             </listitem>
 430           </varlistentry>
 431           <varlistentry>
 432             <term>Action:</term>
 433               <listitem>
 434           <para> It proceeds by case-analysis on <command>t</command> </para>
 435               </listitem>
 436           </varlistentry>
 437           <varlistentry>
 438             <term>New sequents to prove:</term>
 439             <listitem>
 440                <para>It opens one new sequent for each constructor of the
 441                 type of <command>t</command>, each with the conclusion <command>P</command> instantiated for the constructor.</para>
 442             </listitem>
 443           </varlistentry>
 444          </variablelist>
 445        </para>
 446     </sect1>
 447
 448    <sect1 id="tac_case">
 449      <title>case</title>
 450      <titleabbrev>case</titleabbrev>
 451      <para><userinput>case id (id1:T1) … (idn:Tn)</userinput></para>
 452      <para>
 453        <variablelist>
 454          <varlistentry role="tactic.synopsis">
 455            <term>Synopsis:</term>
 456            <listitem>
 457              <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term;  <emphasis role="bold">)</emphasis>] … [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term;  <emphasis role="bold">)</emphasis>]</para>
 458            </listitem>
 459          </varlistentry>
 460          <varlistentry>
 461             <term>Pre-condition:</term>
 462             <listitem>
 463             <para>The user must have started a proof by induction/cases that has not been concluded yet, <command>id</command> must be a constructor for the inductive type of the term under induction/case-analysis, and the case must not have already been proved.</para>
 464             </listitem>
 465          </varlistentry>
 466          <varlistentry>
 467             <term>Action:</term>
 468             <listitem>
 469                 <para>It starts the proof for the case <command>id</command>, where <command>id1:T1</command>,…,<command>idn:Tn</command> are the arguments of the constructor, each declared with its type.</para>
 470             </listitem>
 471          </varlistentry>
 472          <varlistentry>
 473            <term>New sequents to prove:</term>
 474            <listitem>
 475                <para>The sequent for the case <command>id</command>.</para>
 476            </listitem>
 477          </varlistentry>
 478        </variablelist>
 479      </para>
 480   </sect1>
 481
 482     <sect1 id="tac_byinduction">
 483       <title>by induction hypothesis we know</title>
 484       <titleabbrev>by induction hypothesis we know</titleabbrev>
 485       <para><userinput>by induction hypothesis we know P (id)</userinput></para>
 486       <para>
 487         <variablelist>
 488           <varlistentry role="tactic.synopsis">
 489             <term>Synopsis:</term>
 490             <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
 491             </listitem>
 492           </varlistentry>
 493           <varlistentry>
 494             <term>Pre-condition:</term>
 495             <listitem>
 496             <para>The user must have started proving a case for a proof by induction/case-analysis.</para>
 497             </listitem>
 498           </varlistentry>
 499           <varlistentry>
 500             <term>Action:</term>
 501               <listitem>
 502                 <para> It introduces the inductive hypothesis. </para>
 503               </listitem>
 504           </varlistentry>
 505           <varlistentry>
 506              <term>New sequents to prove:</term>
 507                  <listitem>
 508                  <para>None.</para>
 509                  </listitem>
 510           </varlistentry>
 511          </variablelist>
 512       </para>
 513     </sect1>
 514
 515   <sect1 id="tac_conclude">
 516       <title>conclude</title>
 517       <titleabbrev>conclude</titleabbrev>
 518       <para><userinput>conclude t1 </userinput></para>
 519     <para>
 520       <variablelist>
 521          <varlistentry role="tactic.synopsis">
 522            <term>Synopsis:</term>
 523            <listitem>
 524              <para><emphasis role="bold">conclude</emphasis> &term;</para>
 525            </listitem>
 526          </varlistentry>
 527          <varlistentry>
 528            <term>Pre-condition:</term>
 529              <listitem>
 530              <para>
 531                  The current conclusion must be an equality <command>t1 = tk</command>
 532              </para>
 533        </listitem>
 534          </varlistentry>
 535          <varlistentry>
 536            <term>Action:</term>
 537            <listitem>
 538            <para>It starts an equality chain on the conclusion. It allows the user to apply the tactic <emphasis role="bold">=</emphasis> to continue the chain.</para>
 539            </listitem>
 540          </varlistentry>
 541          <varlistentry>
 542            <term>New sequent to prove:</term>
 543              <listitem>
 544                 <para>None.</para>
 545              </listitem>
 546          </varlistentry>
 547        </variablelist>
 548      </para>
 549    </sect1>
 550   <sect1 id="tac_obtain">
 551       <title>obtain</title>
 552       <titleabbrev>obtain</titleabbrev>
 553       <para><userinput>obtain H t1 </userinput></para>
 554     <para>
 555       <variablelist>
 556          <varlistentry role="tactic.synopsis">
 557            <term>Synopsis:</term>
 558            <listitem>
 559            <para><emphasis role="bold">obtain</emphasis> &id; &term;</para>
 560            </listitem>
 561          </varlistentry>
 562          <varlistentry>
 563            <term>Pre-condition:</term>
 564              <listitem>
 565              <para>
 566                  None.
 567              </para>
 568        </listitem>
 569          </varlistentry>
 570          <varlistentry>
 571            <term>Action:</term>
 572            <listitem>
 573            <para>It starts an equality chain <command>t1 = ?</command>, which, when concluded, will be added to hypoteses of the current sequent. It allows the user to apply the tactic <emphasis role="bold">=</emphasis> to continue the chain.</para>
 574            </listitem>
 575          </varlistentry>
 576          <varlistentry>
 577            <term>New sequent to prove:</term>
 578              <listitem>
 579              <para>A new sequent for <command>t1 = ?</command> is opened, a new sequent for <command>?</command> is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with <command>H: t1 = ?</command> added to its hypotheses. This hypotesis will be changed when the equality chain is concluded with <command>H: t1 = tk</command>, where <command>tk</command> is the last term of the equality chain. The goal for <command>?</command> can be safely ignored, as it will be automatically closed when the equality chain is concluded.</para>
 580              </listitem>
 581          </varlistentry>
 582        </variablelist>
 583      </para>
 584    </sect1>
 585   <sect1 id="tac_rewrite">
 586       <title>=</title>
 587       <titleabbrev>=</titleabbrev>
 588       <para><userinput>= t2 justification</userinput></para>
 589     <para>
 590       <variablelist>
 591          <varlistentry role="tactic.synopsis">
 592            <term>Synopsis:</term>
 593            <listitem>
 594            <para>
 595                <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>]
 596            </para>
 597            </listitem>
 598          </varlistentry>
 599          <varlistentry>
 600            <term>Pre-condition:</term>
 601              <listitem>
 602              <para>
 603                  The user must have started an equality chain with <emphasis role="bold">conclude</emphasis> or <emphasis role="bold">obtain</emphasis> that has not been concluded yet.
 604              </para>
 605        </listitem>
 606          </varlistentry>
 607          <varlistentry>
 608            <term>Action:</term>
 609            <listitem>
 610            <para>
 611                    It applies the transitivity of <command>=</command> on the left-hand-side of the current conclusion, <command>t2</command>, and the right-hand-side of the current conclusion, using the given justification. If <emphasis role="bold">done</emphasis> is supplied, this represents the last step in the equality chain.
 612            </para>
 613            </listitem>
 614          </varlistentry>
 615          <varlistentry>
 616            <term>New sequent to prove:</term>
 617              <listitem>
 618              <para>
 619                  A new sequent for <command>lhs = t2</command> is opened and then immediately closed using the given justification. A new sequent with the conclusion <command>t2 = rhs</command> is opened.
 620              </para>
 621              </listitem>
 622          </varlistentry>
 623        </variablelist>
 624      </para>
 625    </sect1>
 626
 627  <sect1 id="tac_bydone">
 628    <title>done</title>
 629    <titleabbrev>done</titleabbrev>
 630    <para><userinput>justification done</userinput></para>
 631    <para>
 632      <variablelist>
 633        <varlistentry role="tactic.synopsis">
 634          <term>Synopsis:</term>
 635          <listitem>
 636            <para>&justification; <emphasis role="bold">done</emphasis></para>
 637          </listitem>
 638        </varlistentry>
 639        <varlistentry>
 640          <term>Pre-condition:</term>
 641          <listitem>
 642          <para>The user is proving a sequent which was opened with the tactic <emphasis role="bold">we need to prove</emphasis>, or the user is proving a sequent which was opened with the tactic <emphasis role="bold">we proceed by induction/cases on</emphasis>, or the user is proving a chain of equalities that was started with either the tactic <emphasis role="bold">conclude</emphasis> or <emphasis role="bold">obtain</emphasis>.</para>
 643          </listitem>
 644        </varlistentry>
 645        <varlistentry>
 646          <term>Action:</term>
 647            <listitem>
 648              <para>It closes the current sequent with the given justification.</para>
 649            </listitem>
 650        </varlistentry>
 651        <varlistentry>
 652            <term>New sequents to prove:</term>
 653            <listitem>
 654                <para>None.</para>
 655            </listitem>
 656        </varlistentry>
 657    </variablelist>
 658      </para>
 659   </sect1>
 660
 661 </chapter>