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   <table>
  10     <tgroup>
  11      <thead />
  12     <tbody>
  13      <row>
  14       <entry id="id">&id;</entry>
  15       <entry>::=</entry>
  16       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
  17      </row>
  18     </tbody>
  19    </tgroup>
  20   </table>
  21   <table>
  22     <tgroup>
  23      <thead />
  24     <tbody>
  25      <row>
  26       <entry id="nat">&nat;</entry>
  27       <entry>::=</entry>
  28       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
  29      </row>
  30     </tbody>
  31    </tgroup>
  32   </table>
  33   <table>
  34     <tgroup>
  35      <thead />
  36     <tbody>
  37      <row>
  38       <entry id="uri">&uri;</entry>
  39       <entry>::=</entry>
  40       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
  41      </row>
  42     </tbody>
  43    </tgroup>
  44   </table>
  45   <table>
  46     <tgroup>
  47      <thead />
  48     <tbody>
  49      <row>
  50       <entry id="term">&term;</entry>
  51       <entry>::=</entry>
  52       <entry>&id;</entry>
  53       <entry>identifier</entry>
  54      </row>
  55      <row>
  56       <entry/>
  57       <entry>|</entry>
  58       <entry>&uri;</entry>
  59       <entry>a qualified reference</entry>
  60      </row>
  61      <row>
  62       <entry/>
  63       <entry>|</entry>
  64       <entry><emphasis role="bold">Prop</emphasis></entry>
  65       <entry>the impredicative sort of propositions</entry>
  66      </row>
  67      <row>
  68       <entry/>
  69       <entry>|</entry>
  70       <entry><emphasis role="bold">Set</emphasis></entry>
  71       <entry>the impredicate sort of datatypes</entry>
  72      </row>
  73      <row>
  74       <entry/>
  75       <entry>|</entry>
  76       <entry><emphasis role="bold">Type</emphasis></entry>
  77       <entry>one predicatie sort of datatypes</entry>
  78      </row>
  79      <row>
  80       <entry/>
  81       <entry>|</entry>
  82       <entry>&term; &term;</entry>
  83       <entry>application</entry>
  84      </row>
  85      <row>
  86       <entry/>
  87       <entry>|</entry>
  88       <entry><emphasis role="bold">λ</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
  89       <entry>λ-abstraction</entry>
  90      </row>
  91      <row>
  92       <entry/>
  93       <entry>|</entry>
  94       <entry><emphasis role="bold">Π</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
  95       <entry>dependent product meant to define a datatype</entry>
  96      </row>
  97      <row>
  98       <entry/>
  99       <entry>|</entry>
 100       <entry><emphasis role="bold">∀</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
 101       <entry>dependent product meant to define a proposition</entry>
 102      </row>
 103      <row>
 104       <entry/>
 105       <entry>|</entry>
 106       <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
 107       <entry>non-dependent product (logical implication or function space)</entry>
 108      </row>
 109      <row>
 110       <entry/>
 111       <entry>|</entry>
 112       <entry><emphasis role="bold">let</emphasis> [&id;|(&id;<emphasis role="bold">:</emphasis> &term;)] <emphasis role="bold">≝</emphasis> &term; <emphasis role="bold">in</emphasis> &term;</entry>
 113       <entry>local definition</entry>
 114      </row>
 115      <row>
 116       <entry/>
 117       <entry>|</entry>
 118         <entry><emphasis role="bold">match</emphasis> &term;
 119         [ <emphasis role="bold">in</emphasis> &term; ]
 120         [ <emphasis role="bold">return</emphasis> &term; ]
 121         <emphasis role="bold">with</emphasis>
 122       </entry>
 123       <entry>case analysis</entry>
 124      </row>
 125      <row>
 126       <entry/>
 127       <entry/>
 128       <entry>
 129        <emphasis role="bold">[</emphasis>
 130        &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 131          [
 132          <emphasis role="bold">|</emphasis>
 133          &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 134          ]…<emphasis role="bold">]</emphasis> </entry>
 135       <entry/>
 136      </row>
 137      <row>
 138       <entry/>
 139       <entry>|</entry>
 140       <entry><emphasis role="bold">let</emphasis>
 141       [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
 142       &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
 143       [<emphasis role="bold">:</emphasis> &term;]
 144       <emphasis role="bold">≝</emphasis> &term;
 145       </entry>
 146       <entry>(co)recursive definitions</entry>
 147      </row>
 148      <row>
 149       <entry/>
 150       <entry/>
 151       <entry>
 152       [<emphasis role="bold">and</emphasis>
 153       &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
 154       [<emphasis role="bold">:</emphasis> &term;]
 155       <emphasis role="bold">≝</emphasis> &term;]…
 156       </entry>
 157       <entry/>
 158      </row>
 159      <row>
 160       <entry/>
 161       <entry/>
 162       <entry>
 163       <emphasis role="bold">in</emphasis> &term;
 164       </entry>
 165       <entry/>
 166      </row>
 167     </tbody>
 168    </tgroup>
 169   </table>
 170
 171   <table>
 172     <tgroup>
 173      <thead />
 174     <tbody>
 175      <row>
 176       <entry id="term_pattern">&term_pattern;</entry>
 177       <entry>::=</entry>
 178       <entry>&id;</entry>
 179       <entry>0-ary constructor</entry>
 180      </row>
 181      <row>
 182       <entry/>
 183       <entry>|</entry>
 184       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
 185       <entry>n-ary constructor (binds the n arguments)</entry>
 186      </row>
 187     </tbody>
 188    </tgroup>
 189   </table>
 190   </sect1>
 191
 192   <sect1 id="axiom">
 193     <title>axiom &id;: &term;</title>
 194     <titleabbrev>axiom</titleabbrev>
 195     <para><userinput>axiom H: P</userinput></para>
 196     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
 197   </sect1>
 198
 199   <sect1 id="definition">
 200     <title>definition &id;[: &term;] [≝ &term;]</title>
 201     <titleabbrev>definition</titleabbrev>
 202     <para><userinput>definition f: T ≝ t</userinput></para>
 203     <para><command>f</command> is defined as <command>t</command>;
 204      <command>T</command> is its type. An error is raised if the type of
 205      <command>t</command> is not convertible to <command>T</command>.</para>
 206     <para><command>T</command> is inferred from <command>t</command> if
 207       omitted.</para>
 208     <para><command>t</command> can be omitted only if <command>T</command> is
 209      given. In this case Matita enters in interactive mode and
 210      <command>f</command> must be defined by means of tactics.</para>
 211     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 212   </sect1>
 213
 214   <sect1 id="inductive">
 215     <title>[co]inductive &id; (of inductive types)</title>
 216     <titleabbrev>(co)inductive types declaration</titleabbrev>
 217     <para> &TODO; </para>
 218   </sect1>
 219
 220   <sect1 id="proofs">
 221    <title>Proofs</title>
 222    <sect2 id="theorem">
 223     <title>theorem &id;[: &term;] [≝ &term;]</title>
 224     <titleabbrev>theorem</titleabbrev>
 225     <para><userinput>theorem f: P ≝ p</userinput></para>
 226     <para>Proves a new theorem <command>f</command> whose thesis is
 227      <command>P</command>.</para>
 228     <para>If <command>p</command> is provided, it must be a proof term for
 229      <command>P</command>. Otherwise an interactive proof is started.</para>
 230     <para><command>P</command> can be omitted only if the proof is not
 231      interactive.</para>
 232     <para>Proving a theorem already proved in the library is an error.
 233      To provide an alternative name and proof for the same theorem, use
 234      <command>variant f: P ≝ p</command>.</para>
 235     <para>A warning is raised if the name of the theorem cannot be obtained
 236       by mangling the name of the constants in its thesis.</para>
 237     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 238    </sect2>
 239    <sect2 id="variant">
 240     <title>variant &id;[: &term;] [≝ &term;]</title>
 241     <titleabbrev>variant</titleabbrev>
 242     <para><userinput>variant f: T ≝ t</userinput></para>
 243     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 244      complain if the theorem has already been proved. To be used to give
 245      an alternative name or proof to a theorem.</para>
 246    </sect2>
 247    <sect2 id="lemma">
 248     <title>lemma &id;[: &term;] [≝ &term;]</title>
 249     <titleabbrev>lemma</titleabbrev>
 250     <para><userinput>lemma f: T ≝ t</userinput></para>
 251     <para>Same as <command>theorem f: T ≝ t</command></para>
 252    </sect2>
 253    <sect2 id="fact">
 254     <title>fact &id;[: &term;] [≝ &term;]</title>
 255     <titleabbrev>fact</titleabbrev>
 256     <para><userinput>fact f: T ≝ t</userinput></para>
 257     <para>Same as <command>theorem f: T ≝ t</command></para>
 258    </sect2>
 259    <sect2 id="remark">
 260     <title>remark &id;[: &term;] [≝ &term;]</title>
 261     <titleabbrev>remark</titleabbrev>
 262     <para><userinput>remark f: T ≝ t</userinput></para>
 263     <para>Same as <command>theorem f: T ≝ t</command></para>
 264    </sect2>
 265   </sect1>
 266
 267 </chapter>
 268