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>&sterm;</entry>
  69       <entry>simple or delimited term</entry>
  70      </row>
  71      <row>
  72       <entry/>
  73       <entry>|</entry>
  74       <entry>&term; &term;</entry>
  75       <entry>application</entry>
  76      </row>
  77      <row>
  78       <entry/>
  79       <entry>|</entry>
  80       <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
  81       <entry>λ-abstraction</entry>
  82      </row>
  83      <row>
  84       <entry/>
  85       <entry>|</entry>
  86       <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
  87       <entry>dependent product meant to define a datatype</entry>
  88      </row>
  89      <row>
  90       <entry/>
  91       <entry>|</entry>
  92       <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
  93       <entry>dependent product meant to define a proposition</entry>
  94      </row>
  95      <row>
  96       <entry/>
  97       <entry>|</entry>
  98       <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
  99       <entry>non-dependent product (logical implication or function space)</entry>
 100      </row>
 101      <row>
 102       <entry/>
 103       <entry>|</entry>
 104       <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>
 105       <entry>local definition</entry>
 106      </row>
 107      <row>
 108       <entry/>
 109       <entry>|</entry>
 110       <entry><emphasis role="bold">let</emphasis>
 111       [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
 112       &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
 113       [<emphasis role="bold">:</emphasis> &term;]
 114       <emphasis role="bold">≝</emphasis> &term;
 115       </entry>
 116       <entry>(co)recursive definitions</entry>
 117      </row>
 118      <row>
 119       <entry/>
 120       <entry/>
 121       <entry>
 122       [<emphasis role="bold">and</emphasis>
 123       [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
 124       [<emphasis role="bold">:</emphasis> &term;]
 125       <emphasis role="bold">≝</emphasis> &term;]…
 126       </entry>
 127       <entry/>
 128      </row>
 129      <row>
 130       <entry/>
 131       <entry/>
 132       <entry>
 133       <emphasis role="bold">in</emphasis> &term;
 134       </entry>
 135       <entry/>
 136      </row>
 137      <row>
 138       <entry/>
 139       <entry>|</entry>
 140       <entry>…</entry>
 141       <entry>user provided notation</entry>
 142      </row>
 143     </tbody>
 144    </tgroup>
 145   </table>
 146
 147   <table>
 148     <tgroup>
 149      <thead />
 150     <tbody>
 151      <row>
 152       <entry id="sterm">&sterm;</entry>
 153       <entry>::=</entry>
 154       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 155       <entry/>
 156      </row>
 157      <row>
 158       <entry/>
 159       <entry>|</entry>
 160       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
 161        &id;<emphasis role="bold">≝</emphasis>&term;
 162        [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≝</emphasis>&term;]…
 163        <emphasis role="bold">]</emphasis>]
 164       </entry>
 165       <entry>identifier with optional explicit named substitution</entry>
 166      </row>
 167      <row>
 168       <entry/>
 169       <entry>|</entry>
 170       <entry>&uri;</entry>
 171       <entry>a qualified reference</entry>
 172      </row>
 173      <row>
 174       <entry/>
 175       <entry>|</entry>
 176       <entry><emphasis role="bold">Prop</emphasis></entry>
 177       <entry>the impredicative sort of propositions</entry>
 178      </row>
 179      <row>
 180       <entry/>
 181       <entry>|</entry>
 182       <entry><emphasis role="bold">Set</emphasis></entry>
 183       <entry>the impredicate sort of datatypes</entry>
 184      </row>
 185      <row>
 186       <entry/>
 187       <entry>|</entry>
 188       <entry><emphasis role="bold">Type</emphasis></entry>
 189       <entry>one predicative sort of datatypes</entry>
 190      </row>
 191      <row>
 192       <entry/>
 193       <entry>|</entry>
 194       <entry><emphasis role="bold">?</emphasis></entry>
 195       <entry>implicit argument</entry>
 196      </row>
 197      <row>
 198       <entry/>
 199       <entry>|</entry>
 200       <entry><emphasis role="bold">?n</emphasis>
 201       [<emphasis role="bold">[</emphasis>
 202       [<emphasis role="bold">_</emphasis>|&term;]…
 203       <emphasis role="bold">]</emphasis>]</entry>
 204       <entry>metavariable</entry>
 205      </row>
 206      <row>
 207       <entry/>
 208       <entry>|</entry>
 209         <entry><emphasis role="bold">match</emphasis> &term;
 210         [ <emphasis role="bold">in</emphasis> &term; ]
 211         [ <emphasis role="bold">return</emphasis> &term; ]
 212         <emphasis role="bold">with</emphasis>
 213       </entry>
 214       <entry>case analysis</entry>
 215      </row>
 216      <row>
 217       <entry/>
 218       <entry/>
 219       <entry>
 220        <emphasis role="bold">[</emphasis>
 221        &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 222          [
 223          <emphasis role="bold">|</emphasis>
 224          &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 225          ]…<emphasis role="bold">]</emphasis> </entry>
 226       <entry/>
 227      </row>
 228      <row>
 229       <entry/>
 230       <entry>|</entry>
 231       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 232       <entry>cast</entry>
 233      </row>
 234      <row>
 235       <entry/>
 236       <entry>|</entry>
 237       <entry>…</entry>
 238       <entry>user provided notation at precedence 90</entry>
 239      </row>
 240     </tbody>
 241    </tgroup>
 242   </table>
 243
 244   <table>
 245     <tgroup>
 246      <thead />
 247     <tbody>
 248      <row>
 249       <entry id="args">&args;</entry>
 250       <entry>::=</entry>
 251       <entry>
 252        [<emphasis role="bold">(</emphasis>]<emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]
 253       </entry>
 254       <entry>ignored argument</entry>
 255      </row>
 256      <row>
 257       <entry/>
 258       <entry>|</entry>
 259       <entry>[<emphasis role="bold">(</emphasis>]&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]</entry>
 260       <entry></entry>
 261      </row>
 262     </tbody>
 263    </tgroup>
 264   </table>
 265
 266   <table>
 267     <tgroup>
 268      <thead />
 269     <tbody>
 270      <row>
 271       <entry id="match_pattern">&match_pattern;</entry>
 272       <entry>::=</entry>
 273       <entry>&id;</entry>
 274       <entry>0-ary constructor</entry>
 275      </row>
 276      <row>
 277       <entry/>
 278       <entry>|</entry>
 279       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
 280       <entry>n-ary constructor (binds the n arguments)</entry>
 281      </row>
 282     </tbody>
 283    </tgroup>
 284   </table>
 285
 286   </sect2>
 287   </sect1>
 288
 289   <sect1 id="axiom_definition_declaration">
 290    <title>Definitions and declarations</title>
 291    <sect2 id="axiom">
 292     <title>axiom &id;: &term;</title>
 293     <titleabbrev>axiom</titleabbrev>
 294     <para><userinput>axiom H: P</userinput></para>
 295     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
 296   </sect2>
 297   <sect2 id="definition">
 298     <title>definition &id;[: &term;] [≝ &term;]</title>
 299     <titleabbrev>definition</titleabbrev>
 300     <para><userinput>definition f: T ≝ t</userinput></para>
 301     <para><command>f</command> is defined as <command>t</command>;
 302      <command>T</command> is its type. An error is raised if the type of
 303      <command>t</command> is not convertible to <command>T</command>.</para>
 304     <para><command>T</command> is inferred from <command>t</command> if
 305       omitted.</para>
 306     <para><command>t</command> can be omitted only if <command>T</command> is
 307      given. In this case Matita enters in interactive mode and
 308      <command>f</command> must be defined by means of tactics.</para>
 309     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 310   </sect2>
 311   <sect2 id="inductive">
 312     <title>[co]inductive &id; (of inductive types)</title>
 313     <titleabbrev>(co)inductive types declaration</titleabbrev>
 314     <para> &TODO; </para>
 315   </sect2>
 316   </sect1>
 317
 318   <sect1 id="proofs">
 319    <title>Proofs</title>
 320    <sect2 id="theorem">
 321     <title>theorem &id;[: &term;] [≝ &term;]</title>
 322     <titleabbrev>theorem</titleabbrev>
 323     <para><userinput>theorem f: P ≝ p</userinput></para>
 324     <para>Proves a new theorem <command>f</command> whose thesis is
 325      <command>P</command>.</para>
 326     <para>If <command>p</command> is provided, it must be a proof term for
 327      <command>P</command>. Otherwise an interactive proof is started.</para>
 328     <para><command>P</command> can be omitted only if the proof is not
 329      interactive.</para>
 330     <para>Proving a theorem already proved in the library is an error.
 331      To provide an alternative name and proof for the same theorem, use
 332      <command>variant f: P ≝ p</command>.</para>
 333     <para>A warning is raised if the name of the theorem cannot be obtained
 334       by mangling the name of the constants in its thesis.</para>
 335     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 336    </sect2>
 337    <sect2 id="variant">
 338     <title>variant &id;[: &term;] [≝ &term;]</title>
 339     <titleabbrev>variant</titleabbrev>
 340     <para><userinput>variant f: T ≝ t</userinput></para>
 341     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 342      complain if the theorem has already been proved. To be used to give
 343      an alternative name or proof to a theorem.</para>
 344    </sect2>
 345    <sect2 id="lemma">
 346     <title>lemma &id;[: &term;] [≝ &term;]</title>
 347     <titleabbrev>lemma</titleabbrev>
 348     <para><userinput>lemma f: T ≝ t</userinput></para>
 349     <para>Same as <command>theorem f: T ≝ t</command></para>
 350    </sect2>
 351    <sect2 id="fact">
 352     <title>fact &id;[: &term;] [≝ &term;]</title>
 353     <titleabbrev>fact</titleabbrev>
 354     <para><userinput>fact f: T ≝ t</userinput></para>
 355     <para>Same as <command>theorem f: T ≝ t</command></para>
 356    </sect2>
 357    <sect2 id="remark">
 358     <title>remark &id;[: &term;] [≝ &term;]</title>
 359     <titleabbrev>remark</titleabbrev>
 360     <para><userinput>remark f: T ≝ t</userinput></para>
 361     <para>Same as <command>theorem f: T ≝ t</command></para>
 362    </sect2>
 363   </sect1>
 364
 365 </chapter>
 366