matita/help/C/sec_terms.xml

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