matita/matita/help/C/axiom_definition_declaration.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>Definitions and declarations</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_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="next" href="proofs.html" title="Proofs" /></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">Definitions and declarations</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_terms.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="proofs.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="axiom_definition_declaration"></a>Definitions and declarations</h2></div></div></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="axiom"></a><span class="bold"><strong>axiom</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> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span></h3></div></div></div><p><strong class="userinput"><code>axiom H: P</code></strong></p><p><span class="command"><strong>H</strong></span> is declared as an axiom that states <span class="command"><strong>P</strong></span></p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="definition"></a><span class="bold"><strong>definition</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> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>definition f: T ≝ t</code></strong></p><p><span class="command"><strong>f</strong></span> is defined as <span class="command"><strong>t</strong></span>;
   3      <span class="command"><strong>T</strong></span> is its type. An error is raised if the type of
   4      <span class="command"><strong>t</strong></span> is not convertible to <span class="command"><strong>T</strong></span>.</p><p><span class="command"><strong>T</strong></span> is inferred from <span class="command"><strong>t</strong></span> if
   5       omitted.</p><p><span class="command"><strong>t</strong></span> can be omitted only if <span class="command"><strong>T</strong></span> is
   6      given. In this case Matita enters in interactive mode and
   7      <span class="command"><strong>f</strong></span> must be defined by means of tactics.</p><p>Notice that the command is equivalent to <span class="command"><strong>theorem f: T ≝ t</strong></span>.</p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="discriminator"></a><span class="bold"><strong>discriminator</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></h3></div></div></div><p><strong class="userinput"><code>discriminator i</code></strong></p><p>Defines a new discrimination (injectivity+conflict) principle à la
   8      McBride for the inductive type <span class="command"><strong>i</strong></span>.</p><p>The principle will use John
   9      Major's equality if such equality is defined, otherwise it will use
  10      Leibniz equality; in the former case, it will be called
  11      <span class="command"><strong>i_jmdiscr</strong></span>, in the latter, <span class="command"><strong>i_discr</strong></span>.
  12      The command will fail if neither equality is available.</p><p>Discrimination principles are used by the destruct tactic and are
  13      usually automatically generated by Matita during the definition of the
  14      corresponding inductive type. This command is thus especially useful
  15      when the correct equality was not loaded at the time of that
  16      definition.</p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="inverter"></a><span class="bold"><strong>inverter</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> <span class="bold"><strong>for</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="tacticargs.html#grammar.path">path</a></em></span>) [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>inverter n for i (path) : s</code></strong></p><p>Defines a new induction/inversion principle for the inductive type
  17      <span class="command"><strong>i</strong></span>, called <span class="command"><strong>n</strong></span>.</p><p><span class="command"><strong>(path)</strong></span> must be in the form <span class="command"><strong>(# # # ... #)</strong></span>,
  18      where each <span class="command"><strong>#</strong></span> can be either <span class="command"><strong>?</strong></span> or
  19      <span class="command"><strong>%</strong></span>, and the number of symbols is equal to the number of
  20      right parameters (indices) of <span class="command"><strong>i</strong></span>. Parentheses are
  21      mandatory. If the j-th symbol is
  22      <span class="command"><strong>%</strong></span>, Matita will generate a principle providing
  23      equations for reasoning on the j-th index of <span class="command"><strong>i</strong></span>. If the
  24      symbol is a <span class="command"><strong>?</strong></span>, no corresponding equation will be
  25      provided.</p><p><span class="command"><strong>s</strong></span>, which must be a sort, is the target sort of the
  26      induction/inversion principle and defaults to <span class="command"><strong>Prop</strong></span>.</p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="letrec"></a><span class="bold"><strong>letrec</strong></span> <span class="emphasis"><em>TODO</em></span></h3></div></div></div><p><span class="emphasis"><em>TODO</em></span></p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="inductive"></a>[<span class="bold"><strong>inductive</strong></span>|<span class="bold"><strong>coinductive</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.args2">args2</a></em></span>]… <span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span> <span class="bold"><strong>≝</strong></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><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</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><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>]…
  27 [<span class="bold"><strong>with</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> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span> <span class="bold"><strong>≝</strong></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><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</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><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>]…]…
  28 </h3></div></div></div><p><strong class="userinput"><code>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</code></strong></p><p>Declares a family of two mutually inductive types
  29      <span class="command"><strong>i</strong></span> and <span class="command"><strong>i'</strong></span> whose types are
  30      <span class="command"><strong>S</strong></span> and <span class="command"><strong>S'</strong></span>, which must be convertible
  31      to sorts.</p><p>The constructors <span class="command"><strong>ki</strong></span> of type <span class="command"><strong>Ti</strong></span>
  32      and <span class="command"><strong>ki'</strong></span> of type <span class="command"><strong>Ti'</strong></span> are also
  33      simultaneously declared. The declared types <span class="command"><strong>i</strong></span> and
  34      <span class="command"><strong>i'</strong></span> may occur in the types of the constructors, but
  35      only in strongly positive positions according to the rules of the
  36      calculus.</p><p>The whole family is parameterized over the arguments <span class="command"><strong>x,y,z</strong></span>.</p><p>If the keyword <span class="command"><strong>coinductive</strong></span> is used, the declared
  37      types are considered mutually coinductive.</p><p>Elimination principles for the record are automatically generated
  38      by Matita, if allowed by the typing rules of the calculus according to
  39      the sort <span class="command"><strong>S</strong></span>. If generated,
  40      they are named <span class="command"><strong>i_ind</strong></span>, <span class="command"><strong>i_rec</strong></span> and
  41      <span class="command"><strong>i_rect</strong></span> according to the sort of their induction
  42      predicate.</p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="record"></a><span class="bold"><strong>record</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.args2">args2</a></em></span>]… <span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span> <span class="bold"><strong>≝</strong></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>|<span class="bold"><strong>:&gt;</strong></span>] <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</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>|<span class="bold"><strong>:&gt;</strong></span>] <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>]…<span class="bold"><strong>}</strong></span></h3></div></div></div><p><strong class="userinput"><code>record id x y z: S ≝ { f1: T1; …; fn:Tn }</code></strong></p><p>Declares a new record family <span class="command"><strong>id</strong></span> parameterized over
  43      <span class="command"><strong>x,y,z</strong></span>.</p><p><span class="command"><strong>S</strong></span> is the type of the record
  44      and it must be convertible to a sort.</p><p>Each field <span class="command"><strong>fi</strong></span> is declared by giving its type
  45      <span class="command"><strong>Ti</strong></span>. A record without any field is admitted.</p><p>Elimination principles for the record are automatically generated
  46      by Matita, if allowed by the typing rules of the calculus according to
  47      the sort <span class="command"><strong>S</strong></span>. If generated,
  48      they are named <span class="command"><strong>i_ind</strong></span>, <span class="command"><strong>i_rec</strong></span> and
  49      <span class="command"><strong>i_rect</strong></span> according to the sort of their induction
  50      predicate.</p><p>For each field <span class="command"><strong>fi</strong></span> a record projection
  51      <span class="command"><strong>fi</strong></span> is also automatically generated if projection
  52      is allowed by the typing rules of the calculus according to the
  53      sort <span class="command"><strong>S</strong></span>, the type <span class="command"><strong>T1</strong></span> and
  54      the definability of depending record projections.</p><p>If the type of a field is declared with <span class="command"><strong>:&gt;</strong></span>,
  55      the corresponding record projection becomes an implicit coercion.
  56      This is just syntactic sugar and it has the same effect of declaring the
  57      record projection as a coercion later on.</p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_terms.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_terms.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="proofs.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 4. Syntax </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Proofs</td></tr></table></div></body></html>