matita/help/C/sec_tactics.xml

   1
   2 <!-- ============ Tactics ====================== -->
   3 <sect1 id="tactics">
   4  <title>Tactics</title>
   5
   6   <sect2 id="tac_absurd">
   7     <title>absurd &lt;term&gt;</title>
   8     <para>The tactic <command>absurd</command> </para>
   9 <para>
  10 </para>
  11   </sect2>
  12   <sect2 id="tac_apply">
  13     <title>apply &lt;term&gt;</title>
  14     <para>The tactic <command>apply</command> </para>
  15   </sect2>
  16   <sect2 id="tac_assumption">
  17     <title>assumption</title>
  18     <para>The tactic <command>assumption</command> </para>
  19   </sect2>
  20   <sect2 id="tac_auto">
  21     <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
  22     <para>The tactic <command>auto</command> </para>
  23   </sect2>
  24   <sect2 id="tac_clear">
  25     <title>clear &lt;id&gt;</title>
  26     <para>The tactic <command>clear</command> </para>
  27   </sect2>
  28   <sect2 id="tac_clearbody">
  29     <title>clearbody &lt;id&gt;</title>
  30     <para>The tactic <command>clearbody</command> </para>
  31   </sect2>
  32   <sect2 id="tac_change">
  33     <title>change &lt;pattern&gt; with &lt;term&gt;</title>
  34     <para>The tactic <command>change</command> </para>
  35   </sect2>
  36   <sect2 id="tac_compare">
  37     <title>compare &lt;term&gt;</title>
  38     <para>The tactic <command>compare</command> </para>
  39   </sect2>
  40   <sect2 id="tac_constructor">
  41     <title>constructor &lt;int&gt;</title>
  42     <para>The tactic <command>constructor</command> </para>
  43   </sect2>
  44   <sect2 id="tac_contradiction">
  45     <title>contradiction</title>
  46     <para>The tactic <command>contradiction</command> </para>
  47   </sect2>
  48   <sect2 id="tac_cut">
  49     <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
  50     <para>The tactic <command>cut</command> </para>
  51   </sect2>
  52   <sect2 id="tac_decide_equality">
  53     <title>decide</title>
  54     <para>The tactic <command>decide equality</command> </para>
  55   </sect2>
  56   <sect2 id="tac_decompose">
  57     <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
  58     <para>The tactic <command>decompose</command> </para>
  59   </sect2>
  60   <sect2 id="tac_discriminate">
  61     <title>discriminate &lt;term&gt;</title>
  62     <para>The tactic <command>discriminate</command> </para>
  63   </sect2>
  64   <sect2 id="tac_elim">
  65     <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
  66     <para>The tactic <command>elim</command> </para>
  67   </sect2>
  68   <sect2 id="tac_elimType">
  69     <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
  70     <para>The tactic <command>elimType</command> </para>
  71   </sect2>
  72   <sect2 id="tac_exact">
  73     <title>exact &lt;term&gt;</title>
  74     <para>The tactic <command>exact</command> </para>
  75   </sect2>
  76   <sect2 id="tac_exists">
  77     <title>exists</title>
  78     <para>The tactic <command>exists</command> </para>
  79   </sect2>
  80   <sect2 id="tac_fail">
  81     <title>fail</title>
  82     <para>The tactic <command>fail</command> </para>
  83   </sect2>
  84   <sect2 id="tac_fold">
  85     <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
  86     <para>The tactic <command>fold</command> </para>
  87   </sect2>
  88   <sect2 id="tac_fourier">
  89     <title>fourier</title>
  90     <para>The tactic <command>fourier</command> </para>
  91   </sect2>
  92   <sect2 id="tac_fwd">
  93     <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
  94     <para>The tactic <command>fwd</command> </para>
  95   </sect2>
  96   <sect2 id="tac_generalize">
  97     <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
  98     <para>The tactic <command>generalize</command> </para>
  99   </sect2>
 100   <sect2 id="tac_id">
 101     <title>id</title>
 102     <para>The tactic <command>id</command> </para>
 103   </sect2>
 104   <sect2 id="tac_injection">
 105     <title>injection &lt;term&gt;</title>
 106     <para>The tactic <command>injection</command> </para>
 107   </sect2>
 108   <sect2 id="tac_intro">
 109     <title>intro [&lt;ident&gt;]</title>
 110     <para>The tactic <command>intro</command> </para>
 111   </sect2>
 112   <sect2 id="tac_intros">
 113     <title>intros &lt;intros_spec&gt;</title>
 114     <para>The tactic <command>intros</command> </para>
 115   </sect2>
 116   <sect2 id="tac_inversion">
 117     <title>intros &lt;term&gt;</title>
 118     <para>The tactic <command>intros</command> </para>
 119   </sect2>
 120   <sect2 id="tac_lapply">
 121     <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
 122     <para>The tactic <command>lapply</command> </para>
 123   </sect2>
 124   <sect2 id="tac_left">
 125     <title>left</title>
 126     <para>The tactic <command>left</command> </para>
 127   </sect2>
 128   <sect2 id="tac_letin">
 129     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
 130     <para>The tactic <command>letin</command> </para>
 131   </sect2>
 132   <sect2 id="tac_normalize">
 133     <title>normalize &lt;pattern&gt;</title>
 134     <para>The tactic <command>normalize</command> </para>
 135   </sect2>
 136   <sect2 id="tac_paramodulation">
 137     <title>paramodulation &lt;pattern&gt;</title>
 138     <para>The tactic <command>paramodulation</command> </para>
 139   </sect2>
 140   <sect2 id="tac_reduce">
 141     <title>reduce &lt;pattern&gt;</title>
 142     <para>The tactic <command>reduce</command> </para>
 143   </sect2>
 144   <sect2 id="tac_reflexivity">
 145     <title>reflexivity</title>
 146     <para>The tactic <command>reflexivity</command> </para>
 147   </sect2>
 148   <sect2 id="tac_replace">
 149     <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
 150     <para>The tactic <command>replace</command> </para>
 151   </sect2>
 152   <sect2 id="tac_rewrite">
 153     <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
 154     <para>The tactic <command>rewrite</command> </para>
 155   </sect2>
 156   <sect2 id="tac_right">
 157     <title>right</title>
 158     <para>The tactic <command>right</command> </para>
 159   </sect2>
 160   <sect2 id="tac_ring">
 161     <title>ring</title>
 162     <para>The tactic <command>ring</command> </para>
 163   </sect2>
 164   <sect2 id="tac_simplify">
 165     <title>simplify &lt;pattern&gt;</title>
 166     <para>The tactic <command>simplify</command> </para>
 167   </sect2>
 168   <sect2 id="tac_split">
 169     <title>split</title>
 170     <para>The tactic <command>split</command> </para>
 171   </sect2>
 172   <sect2 id="tac_symmetry">
 173     <title>symmetry</title>
 174     <para>The tactic <command>symmetry</command> </para>
 175   </sect2>
 176   <sect2 id="tac_transitivity">
 177     <title>transitivity &lt;term&gt;</title>
 178     <para>The tactic <command>transitivity</command> </para>
 179   </sect2>
 180   <sect2 id="tac_unfold">
 181     <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
 182     <para>The tactic <command>unfold</command> </para>
 183   </sect2>
 184   <sect2 id="tac_whd">
 185     <title>whd &lt;pattern&gt;</title>
 186     <para>The tactic <command>whd</command> </para>
 187   </sect2>
 188
 189 </sect1>