matita/matita/help/C/declarative_tactics_quickref.xml

   1 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
   2   <title>tactics</title>
   3   <tgroup cols="3">
   4     <tbody>
   5       <row>
   6         <entry id="grammar.declarative_tactic">&tactic;</entry>
   7         <entry>::=</entry>
   8         <entry>
   9                <link linkend="tac_rewrite_step"><emphasis role="bold">=</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> [<emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis> | <emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">using once</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]
  10            </entry>
  11       </row>
  12       <row>
  13         <entry/>
  14         <entry>|</entry>
  15         <entry><link linkend="tac_assume"><emphasis role="bold">assume</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold"> : </emphasis>
  16              <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> </entry>
  17       </row>
  18       <row>
  19         <entry/>
  20         <entry>|</entry>
  21         <entry><link linkend="tac_byinduction"><emphasis role="bold">by induction hypothesis we know</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
  22       </row>
  23       <row>
  24         <entry/>
  25         <entry>|</entry>
  26         <entry><link linkend="tac_case"><emphasis role="bold">case</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>  <emphasis role="bold">)</emphasis>] … [<emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>  <emphasis role="bold">)</emphasis>]</entry>
  27       </row>
  28       <row>
  29         <entry/>
  30         <entry>|</entry>
  31         <entry><link linkend="tac_conclude"><emphasis role="bold">conclude</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis></entry>
  32       </row>
  33       <row>
  34         <entry/>
  35         <entry>|</entry>
  36         <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_bydone"><emphasis role="bold">done</emphasis></link></entry>
  37       </row>
  38       <row>
  39         <entry/>
  40         <entry>|</entry>
  41         <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <emphasis role="bold">let</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
  42                     <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">such that</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>
  43                      <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
  44       </row>
  45       <row>
  46         <entry/>
  47         <entry>|</entry>
  48         <entry><emphasis role="bold">let</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold"> = </emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis></entry>
  49       </row>
  50       <row>
  51         <entry/>
  52         <entry>|</entry>
  53         <entry><link linkend="tac_obtain"><emphasis role="bold">obtain</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis></entry>
  54       </row>
  55       <row>
  56         <entry/>
  57         <entry>|</entry>
  58         <entry><link linkend="tac_suppose"><emphasis role="bold">suppose</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
  59              <emphasis role="bold">) </emphasis></entry>
  60       </row>
  61       <row>
  62         <entry/>
  63         <entry>|</entry>
  64         <entry>
  65                <link linkend="tac_thatisequivalentto"><emphasis role="bold">that is equivalent to</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
  66            </entry>
  67       </row>
  68       <row>
  69         <entry/>
  70         <entry>|</entry>
  71         <entry><link linkend="tac_thesisbecomes"><emphasis role="bold">the thesis becomes</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
  72       </row>
  73       <row>
  74         <entry/>
  75         <entry>|</entry>
  76         <entry><link linkend="tac_weneedtoprove"><emphasis role="bold">we need to prove</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
  77         [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
  78         <emphasis role="bold">)</emphasis>]
  79         </entry>
  80       </row>
  81       <row>
  82         <entry/>
  83         <entry>|</entry>
  84         <entry><link linkend="tac_weproceedbycases"><emphasis role="bold">we proceed by cases on</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">to prove</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
  85       </row>
  86       <row>
  87         <entry/>
  88         <entry>|</entry>
  89         <entry><link linkend="tac_weproceedbyinduction"><emphasis role="bold">we proceed by induction on</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> to prove </emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
  90       </row>
  91       <row>
  92         <entry/>
  93         <entry>|</entry>
  94         <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_bytermweproved"><emphasis role="bold">we proved</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
  95          [<emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
  96          <emphasis role="bold">)</emphasis>]
  97      </entry>
  98       </row>
  99     </tbody>
 100   </tgroup>
 101 </table>