matita/matita/help/C/html/tac_inversion.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>inversion</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><link rel="up" href="sec_tactics.html" title="Chapter 7. Tactics" /><link rel="prev" href="tac_generalize.html" title="generalize" /><link rel="next" href="tac_lapply.html" title="lapply" /></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">inversion</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_generalize.html">Prev</a> </td><th width="60%" align="center">Chapter 7. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_lapply.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_inversion"></a>inversion</h2></div></div></div><p><strong class="userinput"><code>inversion t</code></strong></p><p>
   3       </p><div class="variablelist"><dl class="variablelist"><dt><span class="term">Synopsis:</span></dt><dd><p><span class="bold"><strong>inversion</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span></p></dd><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of the term <span class="command"><strong>t</strong></span> must be an inductive
   4              type or the application of an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It proceeds by cases on <span class="command"><strong>t</strong></span> paying attention
   5              to the constraints imposed by the actual "right arguments"
   6              of the inductive type.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens one new sequent to prove for each case in the
   7              definition of the type of <span class="command"><strong>t</strong></span>. With respect to
   8              a simple elimination, each new sequent has additional hypotheses
   9              that states the equalities of the "right parameters"
  10              of the inductive type with terms originally present in the
  11              sequent to prove. It uses either Leibniz or John Major equality
  12              for the new hypotheses, according to the included files.</p></dd></dl></div><p>
  13     </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_generalize.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_lapply.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">generalize </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> lapply</td></tr></table></div></body></html>