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><link linkend="tac_assume"><emphasis role="bold">assume</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold"> : </emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
   9       </row>
  10       <row>
  11         <entry/>
  12         <entry>|</entry>
  13         <entry><link linkend="tac_by induction hypothesis we know"><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>
  14       </row>
  15       <row>
  16         <entry/>
  17         <entry>|</entry>
  18         <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>] … </entry>
  19       </row>
  20       <row>
  21         <entry/>
  22         <entry>|</entry>
  23         <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_done"><emphasis role="bold">done</emphasis></link></entry>
  24       </row>
  25       <row>
  26         <entry/>
  27         <entry>|</entry>
  28         <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <emphasis role="bold">let</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
  29                     <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>
  30                      <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
  31       </row>
  32       <row>
  33         <entry/>
  34         <entry>|</entry>
  35         <entry>[<link linkend="tac_obtain"><emphasis role="bold">obtain</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> | <emphasis role="bold">conclude</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>] <emphasis role="bold">=</emphasis> <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>]</entry>
  36       </row>
  37       <row>
  38         <entry/>
  39         <entry>|</entry>
  40         <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>
  41              <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis>  <emphasis><link linkend="grammar.term">term</link></emphasis> ]</entry>
  42       </row>
  43       <row>
  44         <entry/>
  45         <entry>|</entry>
  46         <entry><link linkend="tac_the thesis becomes"><emphasis role="bold">the thesis becomes</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
  47       </row>
  48       <row>
  49         <entry/>
  50         <entry>|</entry>
  51         <entry><link linkend="tac_we need to prove"><emphasis role="bold">we need to prove</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
  52         [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
  53         <emphasis role="bold">)</emphasis>]
  54         [ <emphasis role="bold">or equivalently</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>]</entry>
  55       </row>
  56       <row>
  57         <entry/>
  58         <entry>|</entry>
  59         <entry><link linkend="tac_we proceed by cases on"><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>
  60       </row>
  61       <row>
  62         <entry/>
  63         <entry>|</entry>
  64         <entry><link linkend="tac_we proceed by induction on"><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>
  65       </row>
  66       <row>
  67         <entry/>
  68         <entry>|</entry>
  69         <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_we proved"><emphasis role="bold">we proved</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
  70          <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>
  71          <emphasis role="bold">)</emphasis></entry>
  72       </row>
  73     </tbody>
  74   </tgroup>
  75 </table>