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> &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_byinduction">
  55       <title>by induction hypothesis we know</title>
  56       <titleabbrev>by induction hypothesis we know</titleabbrev>
  57       <para><userinput>by induction hypothesis we know t (id)</userinput></para>
  58       <para>
  59         <variablelist>
  60           <varlistentry role="tactic.synopsis">
  61             <term>Synopsis:</term>
  62             <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
  63             </listitem>
  64           </varlistentry>
  65           <varlistentry>
  66             <term>Pre-condition:</term>
  67             <listitem>
  68         <para>To be used in a proof by induction to state the inductive
  69           hypothesis.</para>
  70             </listitem>
  71           </varlistentry>
  72           <varlistentry>
  73             <term>Action:</term>
  74               <listitem>
  75                 <para> Introduces the inductive hypothesis. </para>
  76               </listitem>
  77           </varlistentry>
  78           <varlistentry>
  79              <term>New sequents to prove:</term>
  80                  <listitem>
  81                  <para>None.</para>
  82                  </listitem>
  83           </varlistentry>
  84          </variablelist>
  85       </para>
  86     </sect1>
  87
  88    <sect1 id="tac_case">
  89      <title>case</title>
  90      <titleabbrev>case</titleabbrev>
  91      <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
  92      <para>
  93        <variablelist>
  94          <varlistentry role="tactic.synopsis">
  95            <term>Synopsis:</term>
  96            <listitem>
  97              <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term;  <emphasis role="bold">)</emphasis>] … </para>
  98            </listitem>
  99          </varlistentry>
 100          <varlistentry>
 101             <term>Pre-condition:</term>
 102             <listitem>
 103         <para>To be used in a proof by induction or by cases to start
 104           a new case</para>
 105             </listitem>
 106          </varlistentry>
 107          <varlistentry>
 108             <term>Action:</term>
 109             <listitem>
 110               <para>Starts the new case <command>id</command> declaring
 111                 the local parameters <command>(id1:t1) … (idn:tn)</command></para>
 112             </listitem>
 113          </varlistentry>
 114          <varlistentry>
 115            <term>New sequents to prove:</term>
 116            <listitem>
 117                <para>None</para>
 118            </listitem>
 119          </varlistentry>
 120        </variablelist>
 121      </para>
 122   </sect1>
 123
 124  <sect1 id="tac_bydone">
 125    <title>done</title>
 126    <titleabbrev>done</titleabbrev>
 127    <para><userinput>justification done</userinput></para>
 128    <para>
 129      <variablelist>
 130        <varlistentry role="tactic.synopsis">
 131          <term>Synopsis:</term>
 132          <listitem>
 133            <para>&justification; <emphasis role="bold">done</emphasis></para>
 134          </listitem>
 135        </varlistentry>
 136        <varlistentry>
 137          <term>Pre-condition:</term>
 138          <listitem>
 139            <para></para>
 140          </listitem>
 141        </varlistentry>
 142        <varlistentry>
 143          <term>Action:</term>
 144            <listitem>
 145              <para>It closes the current sequent given the justification.</para>
 146            </listitem>
 147        </varlistentry>
 148        <varlistentry>
 149            <term>New sequents to prove:</term>
 150            <listitem>
 151                <para>None.</para>
 152            </listitem>
 153        </varlistentry>
 154    </variablelist>
 155      </para>
 156   </sect1>
 157
 158
 159   <sect1 id="tac_exitselim">
 160     <title>let such that</title>
 161     <titleabbrev>let such that</titleabbrev>
 162     <para><userinput>justification let x:t such that p (id)</userinput>
 163     </para>
 164     <para>
 165       <variablelist>
 166         <varlistentry role="tactic.synopsis">
 167           <term>Synopsis:</term>
 168           <listitem>
 169             <para>&justification; <emphasis role="bold">let</emphasis> &id;
 170                     <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term;
 171                      <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
 172           </listitem>
 173         </varlistentry>
 174         <varlistentry>
 175           <term>Pre-condition:</term>
 176           <listitem>
 177       <para>
 178             </para>
 179           </listitem>
 180         </varlistentry>
 181         <varlistentry>
 182           <term>Action:</term>
 183           <listitem>
 184       <para>It derives <command>∃x:t.p</command> using the
 185         <command>justification</command> and then it introduces in the context
 186         <command>x</command> and the hypothesis
 187         <command>p</command> labelled with
 188         <command>id</command>.
 189       </para>
 190           </listitem>
 191         </varlistentry>
 192         <varlistentry>
 193           <term>New sequent to prove:</term>
 194           <listitem>
 195       <para>None.</para>
 196           </listitem>
 197         </varlistentry>
 198      </variablelist>
 199     </para>
 200   </sect1>
 201
 202   <sect1 id="tac_obtain">
 203     <title>obtain</title>
 204     <titleabbrev>obtain</titleabbrev>
 205     <para><userinput>obtain H t1 = t2 justification</userinput></para>
 206     <para>
 207       <variablelist>
 208          <varlistentry role="tactic.synopsis">
 209            <term>Synopsis:</term>
 210            <listitem>
 211              <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>
 212            </listitem>
 213          </varlistentry>
 214          <varlistentry>
 215            <term>Pre-condition:</term>
 216              <listitem>
 217          <para><command>conclude</command> can be used only if the current
 218            sequent is stating an equality. The left hand side must be omitted
 219            in an equality chain.</para>
 220        </listitem>
 221          </varlistentry>
 222          <varlistentry>
 223            <term>Action:</term>
 224            <listitem>
 225        <para>Starts or continues an equality chain. If the chain starts
 226          with <command>obtain H</command> a new subproof named
 227          <command>H</command> is started.</para>
 228            </listitem>
 229          </varlistentry>
 230          <varlistentry>
 231            <term>New sequent to prove:</term>
 232              <listitem>
 233                 <para>If the chain starts
 234             with <command>obtain H</command> a nre sequent for
 235             <command>t2 = ?</command> is opened.
 236           </para>
 237              </listitem>
 238          </varlistentry>
 239        </variablelist>
 240      </para>
 241    </sect1>
 242
 243   <sect1 id="tac_suppose">
 244     <title>suppose</title>
 245     <titleabbrev>suppose</titleabbrev>
 246     <para><userinput>suppose t1 (x) that is equivalent to t2</userinput></para>
 247   <para>
 248      <variablelist>
 249        <varlistentry role="tactic.synopsis">
 250          <term>Synopsis:</term>
 251          <listitem>
 252            <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
 253              <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis>  &term; ]</para>
 254          </listitem>
 255        </varlistentry>
 256       <varlistentry>
 257          <term>Pre-condition:</term>
 258          <listitem>
 259            <para>The conclusion of the current proof must be
 260            <command>∀x:T.P</command> or
 261            <command>T→P</command> where <command>T</command> is
 262            a proposition (i.e. <command>T</command> has type
 263            <command>Prop</command> or <command>CProp</command>).</para>
 264          </listitem>
 265       </varlistentry>
 266       <varlistentry>
 267         <term>Action:</term>
 268           <listitem>
 269             <para>It adds to the context of the current sequent to prove a new
 270            declaration <command>x : T </command>. The new conclusion becomes
 271            <command>P</command>.</para>
 272           </listitem>
 273       </varlistentry>
 274       <varlistentry>
 275         <term>New sequents to prove:</term>
 276         <listitem>
 277             <para>None.</para>
 278         </listitem>
 279       </varlistentry>
 280     </variablelist>
 281    </para>
 282   </sect1>
 283
 284    <sect1 id="tac_thesisbecomes">
 285      <title>the thesis becomes</title>
 286      <titleabbrev>the thesis becomes</titleabbrev>
 287      <para><userinput>the thesis becomes t</userinput></para>
 288      <para>
 289         <variablelist>
 290            <varlistentry role="tactic.synopsis">
 291              <term>Synopsis:</term>
 292              <listitem>
 293                <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
 294              </listitem>
 295            </varlistentry>
 296            <varlistentry>
 297              <term>Pre-condition:</term>
 298              <listitem>
 299          <para>The provided term <command>t</command> must be convertible with
 300            current sequent.</para>
 301              </listitem>
 302            </varlistentry>
 303            <varlistentry>
 304              <term>Action:</term>
 305              <listitem>
 306                <para>It changes the current goal to the one provided.</para>
 307              </listitem>
 308            </varlistentry>
 309            <varlistentry>
 310              <term>New sequent to prove:</term>
 311              <listitem>
 312                <para>None.</para>
 313              </listitem>
 314            </varlistentry>
 315          </variablelist>
 316        </para>
 317    </sect1>
 318
 319   <sect1 id="tac_weneedtoprove">
 320     <title>we need to prove</title>
 321     <titleabbrev>we need to prove</titleabbrev>
 322     <para><userinput>we need to prove t1 (id) or equivalently t2</userinput></para>
 323     <para>
 324       <variablelist>
 325         <varlistentry role="tactic.synopsis">
 326           <term>Synopsis:</term>
 327           <listitem>
 328       <para><emphasis role="bold">we need to prove</emphasis> &term;
 329         [<emphasis role="bold">(</emphasis>&id;
 330         <emphasis role="bold">)</emphasis>]
 331         [ <emphasis role="bold">or equivalently</emphasis> &term;]</para>
 332           </listitem>
 333         </varlistentry>
 334         <varlistentry>
 335           <term>Pre-condition:</term>
 336           <listitem>
 337             <para></para>
 338           </listitem>
 339         </varlistentry>
 340         <varlistentry>
 341           <term>Action:</term>
 342             <listitem>
 343         <para>If <command>id</command> is provided, starts a subproof that once concluded
 344               will be named <command>id</command>. Otherwise states what needs to be proved.
 345               If <command>t2</command> is provided, the new goal is
 346               immediately changed to <command>t2</command> wich must
 347               be equivalent to <command>t1</command>.
 348             </para>
 349             </listitem>
 350         </varlistentry>
 351         <varlistentry>
 352            <term>New sequents to prove:</term>
 353            <listitem>
 354              <para>The stated one if <command>id</command> is provided</para>
 355            </listitem>
 356         </varlistentry>
 357      </variablelist>
 358     </para>
 359   </sect1>
 360
 361
 362   <sect1 id="tac_andelim">
 363     <title>we have</title>
 364     <titleabbrev>we have</titleabbrev>
 365     <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
 366     </para>
 367     <para>
 368       <variablelist>
 369         <varlistentry role="tactic_synopsis">
 370           <term>Synopsis:</term>
 371           <listitem>
 372             <para>&justification; <emphasis role="bold">we have</emphasis> &term;
 373                     <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
 374                       <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
 375           </listitem>
 376         </varlistentry>
 377         <varlistentry>
 378           <term>Pre-condition:</term>
 379           <listitem>
 380             <para></para>
 381           </listitem>
 382         </varlistentry>
 383         <varlistentry>
 384           <term>Action:</term>
 385           <listitem>
 386       <para>It derives <command>t1∧t2</command> using the
 387         <command>justification</command> then it introduces in the context
 388         <command>t1</command>   labelled with <command>id1</command> and
 389         <command>t2</command>   labelled with <command>id2</command>.
 390       </para>
 391           </listitem>
 392         </varlistentry>
 393         <varlistentry>
 394           <term>New sequent to prove:</term>
 395           <listitem>
 396              <para>None.</para>
 397           </listitem>
 398         </varlistentry>
 399       </variablelist>
 400     </para>
 401   </sect1>
 402
 403   <sect1 id="tac_weproceedbycases">
 404     <title>we proceed by cases on</title>
 405       <titleabbrev>we proceed by cases on</titleabbrev>
 406       <para><userinput>we proceed by cases on t to prove th</userinput></para>
 407       <para>
 408         <variablelist>
 409           <varlistentry role="tactic.synopsis">
 410             <term>Synopsis:</term>
 411             <listitem>
 412               <para><emphasis role="bold">we proceed by cases on</emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
 413              </listitem>
 414           </varlistentry>
 415           <varlistentry>
 416             <term>Pre-condition:</term>
 417             <listitem>
 418         <para><command>t</command> must inhabitant of an inductive type and
 419           <command>th</command> must be the conclusion to be proved by
 420           cases.</para>
 421             </listitem>
 422           </varlistentry>
 423           <varlistentry>
 424             <term>Action:</term>
 425               <listitem>
 426           <para> It proceeds by cases on <command>t</command> </para>
 427               </listitem>
 428           </varlistentry>
 429           <varlistentry>
 430             <term>New sequents to prove:</term>
 431             <listitem>
 432                <para>It opens one new sequent for each constructor of the
 433                 type of <command>t</command>.</para>
 434             </listitem>
 435           </varlistentry>
 436          </variablelist>
 437        </para>
 438     </sect1>
 439
 440     <sect1 id="tac_weproceedbyinduction">
 441     <title>we proceed by induction on</title>
 442     <titleabbrev>we proceed by induction on</titleabbrev>
 443     <para><userinput>we proceed by induction on t to prove th</userinput></para>
 444     <para>
 445       <variablelist>
 446         <varlistentry role="tactic.synopsis">
 447           <term>Synopsis:</term>
 448           <listitem>
 449             <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
 450           </listitem>
 451         </varlistentry>
 452         <varlistentry>
 453           <term>Pre-condition:</term>
 454           <listitem>
 455       <para><command>t</command> must inhabitant of an inductive type and
 456         <command>th</command> must be the conclusion to be proved by induction.
 457         </para>
 458           </listitem>
 459         </varlistentry>
 460         <varlistentry>
 461           <term>Action:</term>
 462             <listitem>
 463               <para>It proceed by induction on <command>t</command>.</para>
 464             </listitem>
 465         </varlistentry>
 466         <varlistentry>
 467             <term>New sequents to prove:</term>
 468             <listitem>
 469               <para>It opens one new sequent for each constructor of the
 470                 type of <command>t</command>.</para>
 471             </listitem>
 472         </varlistentry>
 473       </variablelist>
 474     </para>
 475   </sect1>
 476
 477
 478  <sect1 id="tac_bytermweproved">
 479    <title>we proved</title>
 480      <titleabbrev>we proved</titleabbrev>
 481      <para><userinput>justification we proved t (id)</userinput></para>
 482      <para>
 483        <variablelist>
 484          <varlistentry role="tactic.synopsis">
 485            <term>Synopsis:</term>
 486            <listitem>
 487              <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
 488          <emphasis role="bold">(</emphasis> &id;
 489          <emphasis role="bold">)</emphasis></para>
 490            </listitem>
 491            </varlistentry>
 492            <varlistentry>
 493              <term>Pre-condition:</term>
 494              <listitem>
 495                <para><command>t</command>must have type <command>Prop</command>.
 496          </para>
 497              </listitem>
 498            </varlistentry>
 499            <varlistentry>
 500              <term>Action:</term>
 501              <listitem>
 502          <para>It derives <command>t</command>
 503            using the justification and labels the conclusion with
 504            <command>id</command>.
 505          </para>
 506              </listitem>
 507            </varlistentry>
 508            <varlistentry>
 509              <term>New sequent to prove:</term>
 510              <listitem>
 511                <para>None.</para>
 512              </listitem>
 513            </varlistentry>
 514          </variablelist>
 515        </para>
 516     </sect1>
 517
 518 </chapter>