matita/help/C/sec_terms.xml

   1
   2 <!-- =========== Terms, declarations and definitions ============ -->
   3
   4 <chapter id="sec_terms">
   5   <title>Terms, axioms, definitions, declarations and proofs</title>
   6
   7   <sect1 id="terms">
   8     <title>Terms</title>
   9     <!--<informaltable>
  10      <tr>
  11       <td>&lt;term&gt;</td>
  12       <td>::=</td>
  13       <td>&lt;id&gt;</td>
  14       <td>identifier</td>
  15      </tr>
  16      <tr><td/><td>|</td><td>&lt;term&gt; &lt;term&gt;</td>
  17       <td>application</td></tr>
  18     </informaltable>-->
  19         <table>
  20           <tgroup>
  21             <thead />
  22             <tbody>
  23               <row>
  24                 <entry>&lt;term&gt;</entry>
  25                 <entry>::=</entry>
  26                 <entry>&lt;id&gt;</entry>
  27                 <entry>identifier</entry>
  28               </row>
  29               <row>
  30                 <entry/>
  31                 <entry>|</entry>
  32                 <entry>&lt;term&gt; &lt;term&gt;</entry>
  33                 <entry>application</entry>
  34               </row>
  35               <row>
  36                 <entry/>
  37                 <entry>|</entry>
  38                 <entry>λ&lt;id&gt;[: &lt;term&gt;].&lt;term&gt;</entry>
  39                 <entry>λ-abstraction</entry>
  40               </row>
  41               <row>
  42                 <entry/>
  43                 <entry>|</entry>
  44                 <entry>Π&lt;id&gt;[: &lt;term&gt;].&lt;term&gt;</entry>
  45                 <entry>dependent product meant to define a datatype</entry>
  46               </row>
  47               <row>
  48                 <entry/>
  49                 <entry>|</entry>
  50                 <entry>∀&lt;id&gt;[: &lt;term&gt;].&lt;term&gt;</entry>
  51                 <entry>dependent product meant to define a proposition</entry>
  52               </row>
  53               <row>
  54                 <entry/>
  55                 <entry>|</entry>
  56                 <entry>&lt;term&gt; → &lt;term&gt;</entry>
  57                 <entry>non-dependent product (logical implication or function space)</entry>
  58               </row>
  59               <row>
  60                 <entry/>
  61                 <entry>|</entry>
  62                 <entry>let [&lt;id&gt;|(&lt;id&gt;: &lt;term&gt;)] ≝ &lt;term&gt; in &lt;term&gt;</entry>
  63                 <entry>local definition</entry>
  64               </row>
  65               <row>
  66                 <entry/>
  67                 <entry>|</entry>
  68                 <entry>let [co]rec &lt;id&gt; ≝ &lt;term&gt; in &lt;term&gt;</entry>
  69                 <entry>local definition</entry>
  70               </row>
  71               <row>
  72                 <entry/>
  73                 <entry>|</entry>
  74                 <entry>...</entry>
  75                 <entry>&TODO;</entry>
  76               </row>
  77             </tbody>
  78           </tgroup>
  79         </table>
  80   </sect1>
  81
  82   <sect1 id="axiom">
  83     <title>axiom &lt;id&gt;: &lt;term&gt;</title>
  84     <titleabbrev>axiom</titleabbrev>
  85     <para><userinput>axiom H: P</userinput></para>
  86     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
  87   </sect1>
  88
  89   <sect1 id="definition">
  90     <title>definition &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
  91     <titleabbrev>definition</titleabbrev>
  92     <para><userinput>definition f: T ≝ t</userinput></para>
  93     <para><command>f</command> is defined as <command>t</command>;
  94      <command>T</command> is its type. An error is raised if the type of
  95      <command>t</command> is not convertible to <command>T</command>.</para>
  96     <para><command>T</command> is inferred from <command>t</command> if
  97       omitted.</para>
  98     <para><command>t</command> can be omitted only if <command>T</command> is
  99      given. In this case Matita enters in interactive mode and
 100      <command>f</command> must be defined by means of tactics.</para>
 101     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 102   </sect1>
 103
 104   <sect1 id="inductive">
 105     <title>[co]inductive &lt;id&gt; (of inductive types)</title>
 106     <titleabbrev>(co)inductive types declaration</titleabbrev>
 107     <para> &TODO; </para>
 108   </sect1>
 109
 110   <sect1 id="proofs">
 111    <title>Proofs</title>
 112    <sect2 id="theorem">
 113     <title>theorem &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
 114     <titleabbrev>theorem</titleabbrev>
 115     <para><userinput>theorem f: P ≝ p</userinput></para>
 116     <para>Proves a new theorem <command>f</command> whose thesis is
 117      <command>P</command>.</para>
 118     <para>If <command>p</command> is provided, it must be a proof term for
 119      <command>P</command>. Otherwise an interactive proof is started.</para>
 120     <para><command>P</command> can be omitted only if the proof is not
 121      interactive.</para>
 122     <para>Proving a theorem already proved in the library is an error.
 123      To provide an alternative name and proof for the same theorem, use
 124      <command>variant f: P ≝ p</command>.</para>
 125     <para>A warning is raised if the name of the theorem cannot be obtained
 126       by mangling the name of the constants in its thesis.</para>
 127     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 128    </sect2>
 129    <sect2 id="variant">
 130     <title>variant &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
 131     <titleabbrev>variant</titleabbrev>
 132     <para><userinput>variant f: T ≝ t</userinput></para>
 133     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 134      complain if the theorem has already been proved. To be used to give
 135      an alternative name or proof to a theorem.</para>
 136    </sect2>
 137    <sect2 id="lemma">
 138     <title>lemma &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
 139     <titleabbrev>lemma</titleabbrev>
 140     <para><userinput>lemma f: T ≝ t</userinput></para>
 141     <para>Same as <command>theorem f: T ≝ t</command></para>
 142    </sect2>
 143    <sect2 id="fact">
 144     <title>fact &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
 145     <titleabbrev>fact</titleabbrev>
 146     <para><userinput>fact f: T ≝ t</userinput></para>
 147     <para>Same as <command>theorem f: T ≝ t</command></para>
 148    </sect2>
 149    <sect2 id="remark">
 150     <title>remark &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
 151     <titleabbrev>remark</titleabbrev>
 152     <para><userinput>remark f: T ≝ t</userinput></para>
 153     <para>Same as <command>theorem f: T ≝ t</command></para>
 154    </sect2>
 155   </sect1>
 156
 157 </chapter>
 158