helm/www/matita/docs/manual-0.5.9/sec_tactics.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 7. Tactics</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="prev" href="tacticals.html" title="Tacticals" /><link rel="next" href="tac_absurd.html" title="absurd" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 7. Tactics</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tacticals.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="tac_absurd.html">Next</a></td></tr></table><hr /></div><div class="chapter"><div class="titlepage"><div><div><h1 class="title"><a id="sec_tactics"></a>Chapter 7. Tactics</h1></div></div></div><div class="toc"><p><strong>Table of Contents</strong></p><dl class="toc"><dt><span class="sect1"><a href="sec_tactics.html#tactics_quickref">Quick reference card</a></span></dt><dt><span class="sect1"><a href="tac_absurd.html">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</a></span></dt><dt><span class="sect1"><a href="tac_applyS.html">applyS</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">auto</a></span></dt><dt><span class="sect1"><a href="tac_cases.html">cases</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">clear</a></span></dt><dt><span class="sect1"><a href="tac_clearbody.html">clearbody</a></span></dt><dt><span class="sect1"><a href="tac_compose.html">compose</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">constructor</a></span></dt><dt><span class="sect1"><a href="tac_contradiction.html">contradiction</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">decompose</a></span></dt><dt><span class="sect1"><a href="tac_demodulate.html">demodulate</a></span></dt><dt><span class="sect1"><a href="tac_destruct.html">destruct</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_elimType.html">elimType</a></span></dt><dt><span class="sect1"><a href="tac_exact.html">exact</a></span></dt><dt><span class="sect1"><a href="tac_exists.html">exists</a></span></dt><dt><span class="sect1"><a href="tac_fail.html">fail</a></span></dt><dt><span class="sect1"><a href="tac_fold.html">fold</a></span></dt><dt><span class="sect1"><a href="tac_fourier.html">fourier</a></span></dt><dt><span class="sect1"><a href="tac_fwd.html">fwd</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_id.html">id</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">intro</a></span></dt><dt><span class="sect1"><a href="tac_intros.html">intros</a></span></dt><dt><span class="sect1"><a href="tac_inversion.html">inversion</a></span></dt><dt><span class="sect1"><a href="tac_lapply.html">lapply</a></span></dt><dt><span class="sect1"><a href="tac_left.html">left</a></span></dt><dt><span class="sect1"><a href="tac_letin.html">letin</a></span></dt><dt><span class="sect1"><a href="tac_normalize.html">normalize</a></span></dt><dt><span class="sect1"><a href="tac_reflexivity.html">reflexivity</a></span></dt><dt><span class="sect1"><a href="tac_replace.html">change</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">rewrite</a></span></dt><dt><span class="sect1"><a href="tac_right.html">right</a></span></dt><dt><span class="sect1"><a href="tac_ring.html">ring</a></span></dt><dt><span class="sect1"><a href="tac_simplify.html">simplify</a></span></dt><dt><span class="sect1"><a href="tac_split.html">split</a></span></dt><dt><span class="sect1"><a href="tac_subst.html">subst</a></span></dt><dt><span class="sect1"><a href="tac_symmetry.html">symmetry</a></span></dt><dt><span class="sect1"><a href="tac_transitivity.html">transitivity</a></span></dt><dt><span class="sect1"><a href="tac_unfold.html">unfold</a></span></dt><dt><span class="sect1"><a href="tac_whd.html">whd</a></span></dt></dl></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tactics_quickref"></a>Quick reference card</h2></div></div></div><p>
   3       </p><div class="table"><a id="idp71070096"></a><p class="title"><strong>Table 7.1. tactics</strong></p><div class="table-contents"><table summary="tactics" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.tactic"></a><span class="emphasis"><em><a class="link" href="sec_tactics.html#grammar.tactic">tactic</a></em></span></td><td style="">::=</td><td style=""><a class="link" href="tac_absurd.html" title="absurd"><span class="bold"><strong>absurd</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_apply.html" title="apply"><span class="bold"><strong>apply</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_applyS.html" title="applyS"><span class="bold"><strong>applyS</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.autoparams">auto_params</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
   4           <a class="link" href="tac_assumption.html" title="assumption">
   5             <span class="bold"><strong>assumption</strong></span>
   6           </a>
   7         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_auto.html" title="auto"><span class="bold"><strong>auto</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.autoparams">auto_params</a></em></span>. <span class="bold"><strong>autobatch</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.autoparams">auto_params</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
   8              <a class="link" href="tac_cases.html" title="cases"><span class="bold"><strong>cases</strong></span></a>
   9              <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span> [<span class="bold"><strong>(</strong></span>[<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]…<span class="bold"><strong>)</strong></span>]
  10             </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_change.html" title="change"><span class="bold"><strong>change</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span> <span class="bold"><strong>with</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  11              <a class="link" href="tac_clear.html" title="clear"><span class="bold"><strong>clear</strong></span></a>
  12              <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>…]
  13             </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_clearbody.html" title="clearbody"><span class="bold"><strong>clearbody</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_compose.html" title="compose"><span class="bold"><strong>compose</strong></span></a> [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>] <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> [<span class="bold"><strong>with</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>] [<span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.intros-spec">intros-spec</a></em></span>]</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_constructor.html" title="constructor"><span class="bold"><strong>constructor</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  14           <a class="link" href="tac_contradiction.html" title="contradiction">
  15             <span class="bold"><strong>contradiction</strong></span>
  16           </a>
  17         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_cut.html" title="cut"><span class="bold"><strong>cut</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> [<span class="bold"><strong>as</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]</td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  18              <a class="link" href="tac_decompose.html" title="decompose"><span class="bold"><strong>decompose</strong></span></a>
  19              [<span class="bold"><strong>as</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>…]
  20             </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_demodulate.html" title="demodulate"><span class="bold"><strong>demodulate</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.autoparams">auto_params</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_destruct.html" title="destruct"><span class="bold"><strong>destruct</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_elim.html" title="elim"><span class="bold"><strong>elim</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span> [<span class="bold"><strong>using</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>] <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.intros-spec">intros-spec</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_elimType.html" title="elimType"><span class="bold"><strong>elimType</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> [<span class="bold"><strong>using</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>] <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.intros-spec">intros-spec</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_exact.html" title="exact"><span class="bold"><strong>exact</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  21           <a class="link" href="tac_exists.html" title="exists">
  22             <span class="bold"><strong>exists</strong></span>
  23           </a>
  24         </td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  25           <a class="link" href="tac_fail.html" title="fail">
  26             <span class="bold"><strong>fail</strong></span>
  27           </a>
  28         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_fold.html" title="fold"><span class="bold"><strong>fold</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.reduction-kind">reduction-kind</a></em></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  29           <a class="link" href="tac_fourier.html" title="fourier">
  30             <span class="bold"><strong>fourier</strong></span>
  31           </a>
  32         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_fwd.html" title="fwd"><span class="bold"><strong>fwd</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> [<span class="bold"><strong>as</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]…]</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_generalize.html" title="generalize"><span class="bold"><strong>generalize</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span> [<span class="bold"><strong>as</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]</td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  33           <a class="link" href="tac_id.html" title="id">
  34             <span class="bold"><strong>id</strong></span>
  35           </a>
  36         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_intro.html" title="intro"><span class="bold"><strong>intro</strong></span></a> [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_intros.html" title="intros"><span class="bold"><strong>intros</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.intros-spec">intros-spec</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_inversion.html" title="inversion"><span class="bold"><strong>inversion</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  37              <a class="link" href="tac_lapply.html" title="lapply"><span class="bold"><strong>lapply</strong></span></a>
  38              [<span class="bold"><strong>linear</strong></span>]
  39              [<span class="bold"><strong>depth=</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>]
  40              <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>
  41              [<span class="bold"><strong>to</strong></span>
  42               <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>
  43               [<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>…]
  44              ]
  45              [<span class="bold"><strong>as</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]
  46             </td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  47           <a class="link" href="tac_left.html" title="left">
  48             <span class="bold"><strong>left</strong></span>
  49           </a>
  50         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_letin.html" title="letin"><span class="bold"><strong>letin</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> <span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_normalize.html" title="normalize"><span class="bold"><strong>normalize</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  51           <a class="link" href="tac_reflexivity.html" title="reflexivity">
  52             <span class="bold"><strong>reflexivity</strong></span>
  53           </a>
  54         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_replace.html" title="replace"><span class="bold"><strong>replace</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span> <span class="bold"><strong>with</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_rewrite.html" title="rewrite"><span class="bold"><strong>rewrite</strong></span></a> [<span class="bold"><strong>&lt;</strong></span>|<span class="bold"><strong>&gt;</strong></span>] <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  55           <a class="link" href="tac_right.html" title="right">
  56             <span class="bold"><strong>right</strong></span>
  57           </a>
  58         </td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  59           <a class="link" href="tac_ring.html" title="ring">
  60             <span class="bold"><strong>ring</strong></span>
  61           </a>
  62         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_simplify.html" title="simplify"><span class="bold"><strong>simplify</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  63           <a class="link" href="tac_split.html" title="split">
  64             <span class="bold"><strong>split</strong></span>
  65           </a>
  66         </td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  67           <a class="link" href="tac_subst.html" title="subst">
  68             <span class="bold"><strong>subst</strong></span>
  69           </a>
  70         </td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  71           <a class="link" href="tac_symmetry.html" title="symmetry">
  72             <span class="bold"><strong>symmetry</strong></span>
  73           </a>
  74         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_transitivity.html" title="transitivity"><span class="bold"><strong>transitivity</strong></span></a> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_unfold.html" title="unfold"><span class="bold"><strong>unfold</strong></span></a> [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>] <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><a class="link" href="tac_whd.html" title="whd"><span class="bold"><strong>whd</strong></span></a> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.pattern">pattern</a></em></span></td></tr></tbody></table></div></div><p><br class="table-break" />
  75
  76     </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tacticals.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="tac_absurd.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Tacticals </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> absurd</td></tr></table></div></body></html>