matita/help/C/sec_tactics.xml

   1
   2 <!-- ============ Tactics ====================== -->
   3 <sect1 id="sec_tactics">
   4  <title>Tactics</title>
   5
   6   <sect2 id="tac_absurd">
   7     <title>absurd &lt;term&gt;</title>
   8     <para><userinput>absurd P</userinput></para>
   9     <para>
  10         <varlistentry>
  11           <term>Pre-conditions:</term>
  12           <listitem>
  13             <para><command>P</command> must have type <command>Type</command>.</para>
  14           </listitem>
  15         </varlistentry>
  16       <variablelist>
  17         <varlistentry>
  18           <term>Action:</term>
  19           <listitem>
  20             <para>it closes the current goal by eliminating an
  21              absurd term.</para>
  22           </listitem>
  23         </varlistentry>
  24         <varlistentry>
  25           <term>New sequents to prove:</term>
  26           <listitem>
  27             <para>it opens two new sequents of conclusion <command>P</command>
  28              and <command>¬P</command>.</para>
  29           </listitem>
  30         </varlistentry>
  31       </variablelist>
  32     </para>
  33   </sect2>
  34   <sect2 id="tac_apply">
  35     <title>apply &lt;term&gt;</title>
  36     <para><userinput>apply t</userinput></para>
  37     <para>
  38       <variablelist>
  39         <varlistentry>
  40           <term>Pre-conditions:</term>
  41           <listitem>
  42             <para><command>t</command> must have type
  43              <command>T<subscript>1</subscript> → ... →
  44               T<subscript>n</subscript> → G</command>
  45              where <command>G</command> can be unified with the conclusion
  46              of the current sequent.</para>
  47           </listitem>
  48         </varlistentry>
  49         <varlistentry>
  50           <term>Action:</term>
  51           <listitem>
  52             <para>it closes the current goal by applying <command>t</command>.</para>
  53           </listitem>
  54         </varlistentry>
  55         <varlistentry>
  56           <term>New sequents to prove:</term>
  57           <listitem>
  58             <para>it opens a new goal for each premise
  59              <command>T<subscript>i</subscript></command> that is not
  60              instantiated by unification.</para>
  61           </listitem>
  62         </varlistentry>
  63       </variablelist>
  64     </para>
  65   </sect2>
  66   <sect2 id="tac_assumption">
  67     <title>assumption</title>
  68     <para>The tactic <command>assumption</command> </para>
  69   </sect2>
  70   <sect2 id="tac_auto">
  71     <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
  72     <para>The tactic <command>auto</command> </para>
  73   </sect2>
  74   <sect2 id="tac_clear">
  75     <title>clear &lt;id&gt;</title>
  76     <para>The tactic <command>clear</command> </para>
  77   </sect2>
  78   <sect2 id="tac_clearbody">
  79     <title>clearbody &lt;id&gt;</title>
  80     <para>The tactic <command>clearbody</command> </para>
  81   </sect2>
  82   <sect2 id="tac_change">
  83     <title>change &lt;pattern&gt; with &lt;term&gt;</title>
  84     <para>The tactic <command>change</command> </para>
  85   </sect2>
  86   <sect2 id="tac_compare">
  87     <title>compare &lt;term&gt;</title>
  88     <para>The tactic <command>compare</command> </para>
  89   </sect2>
  90   <sect2 id="tac_constructor">
  91     <title>constructor &lt;int&gt;</title>
  92     <para>The tactic <command>constructor</command> </para>
  93   </sect2>
  94   <sect2 id="tac_contradiction">
  95     <title>contradiction</title>
  96     <para>The tactic <command>contradiction</command> </para>
  97   </sect2>
  98   <sect2 id="tac_cut">
  99     <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
 100     <para>The tactic <command>cut</command> </para>
 101   </sect2>
 102   <sect2 id="tac_decide_equality">
 103     <title>decide</title>
 104     <para>The tactic <command>decide equality</command> </para>
 105   </sect2>
 106   <sect2 id="tac_decompose">
 107     <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
 108     <para>The tactic <command>decompose</command> </para>
 109   </sect2>
 110   <sect2 id="tac_discriminate">
 111     <title>discriminate &lt;term&gt;</title>
 112     <para>The tactic <command>discriminate</command> </para>
 113   </sect2>
 114   <sect2 id="tac_elim">
 115     <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
 116     <para>The tactic <command>elim</command> </para>
 117   </sect2>
 118   <sect2 id="tac_elimType">
 119     <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
 120     <para>The tactic <command>elimType</command> </para>
 121   </sect2>
 122   <sect2 id="tac_exact">
 123     <title>exact &lt;term&gt;</title>
 124     <para>The tactic <command>exact</command> </para>
 125   </sect2>
 126   <sect2 id="tac_exists">
 127     <title>exists</title>
 128     <para>The tactic <command>exists</command> </para>
 129   </sect2>
 130   <sect2 id="tac_fail">
 131     <title>fail</title>
 132     <para>The tactic <command>fail</command> </para>
 133   </sect2>
 134   <sect2 id="tac_fold">
 135     <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
 136     <para>The tactic <command>fold</command> </para>
 137   </sect2>
 138   <sect2 id="tac_fourier">
 139     <title>fourier</title>
 140     <para>The tactic <command>fourier</command> </para>
 141   </sect2>
 142   <sect2 id="tac_fwd">
 143     <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
 144     <para>The tactic <command>fwd</command> </para>
 145   </sect2>
 146   <sect2 id="tac_generalize">
 147     <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
 148     <para>The tactic <command>generalize</command> </para>
 149   </sect2>
 150   <sect2 id="tac_id">
 151     <title>id</title>
 152     <para>The tactic <command>id</command> </para>
 153   </sect2>
 154   <sect2 id="tac_injection">
 155     <title>injection &lt;term&gt;</title>
 156     <para>The tactic <command>injection</command> </para>
 157   </sect2>
 158   <sect2 id="tac_intro">
 159     <title>intro [&lt;ident&gt;]</title>
 160     <para>The tactic <command>intro</command> </para>
 161   </sect2>
 162   <sect2 id="tac_intros">
 163     <title>intros &lt;intros_spec&gt;</title>
 164     <para>The tactic <command>intros</command> </para>
 165   </sect2>
 166   <sect2 id="tac_inversion">
 167     <title>intros &lt;term&gt;</title>
 168     <para>The tactic <command>intros</command> </para>
 169   </sect2>
 170   <sect2 id="tac_lapply">
 171     <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
 172     <para>The tactic <command>lapply</command> </para>
 173   </sect2>
 174   <sect2 id="tac_left">
 175     <title>left</title>
 176     <para>The tactic <command>left</command> </para>
 177   </sect2>
 178   <sect2 id="tac_letin">
 179     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
 180     <para>The tactic <command>letin</command> </para>
 181   </sect2>
 182   <sect2 id="tac_normalize">
 183     <title>normalize &lt;pattern&gt;</title>
 184     <para>The tactic <command>normalize</command> </para>
 185   </sect2>
 186   <sect2 id="tac_paramodulation">
 187     <title>paramodulation &lt;pattern&gt;</title>
 188     <para>The tactic <command>paramodulation</command> </para>
 189   </sect2>
 190   <sect2 id="tac_reduce">
 191     <title>reduce &lt;pattern&gt;</title>
 192     <para>The tactic <command>reduce</command> </para>
 193   </sect2>
 194   <sect2 id="tac_reflexivity">
 195     <title>reflexivity</title>
 196     <para>The tactic <command>reflexivity</command> </para>
 197   </sect2>
 198   <sect2 id="tac_replace">
 199     <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
 200     <para>The tactic <command>replace</command> </para>
 201   </sect2>
 202   <sect2 id="tac_rewrite">
 203     <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
 204     <para>The tactic <command>rewrite</command> </para>
 205   </sect2>
 206   <sect2 id="tac_right">
 207     <title>right</title>
 208     <para>The tactic <command>right</command> </para>
 209   </sect2>
 210   <sect2 id="tac_ring">
 211     <title>ring</title>
 212     <para>The tactic <command>ring</command> </para>
 213   </sect2>
 214   <sect2 id="tac_simplify">
 215     <title>simplify &lt;pattern&gt;</title>
 216     <para>The tactic <command>simplify</command> </para>
 217   </sect2>
 218   <sect2 id="tac_split">
 219     <title>split</title>
 220     <para>The tactic <command>split</command> </para>
 221   </sect2>
 222   <sect2 id="tac_symmetry">
 223     <title>symmetry</title>
 224     <para>The tactic <command>symmetry</command> </para>
 225   </sect2>
 226   <sect2 id="tac_transitivity">
 227     <title>transitivity &lt;term&gt;</title>
 228     <para>The tactic <command>transitivity</command> </para>
 229   </sect2>
 230   <sect2 id="tac_unfold">
 231     <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
 232     <para>The tactic <command>unfold</command> </para>
 233   </sect2>
 234   <sect2 id="tac_whd">
 235     <title>whd &lt;pattern&gt;</title>
 236     <para>The tactic <command>whd</command> </para>
 237   </sect2>
 238
 239 </sect1>
 240