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><para>Non terminal symbols are emphasized and have a link to their
   9         definition. E.g.: &term;</para></listitem>
  10     <listitem><para>Terminal symbols are in bold. E.g.:
  11         <emphasis role="bold">theorem</emphasis></para></listitem>
  12     <listitem><para>Optional sequences of elements are put in square brackets.
  13         E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
  14     <listitem><para>Alternatives are put in square brakets and they are
  15         separated by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</para></listitem>
  16     <listitem><para>Repetitions of a sequence of elements are given by putting the
  17     sequence in square brackets, that are followed by three dots. The empty
  18     sequence is a valid repetition.
  19     E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
  20   </orderedlist>
  21   <sect1 id="terms_and_co">
  22   <title>Terms &amp; co.</title>
  23   <sect2 id="lexical">
  24   <title>Lexical conventions</title>
  25   <para>
  26     <table frame="all" rowsep="0" colsep="0">
  27       <title>id</title>
  28       <tgroup cols="4">
  29       <tbody>
  30        <row>
  31         <entry id="id">&id;</entry>
  32         <entry>::=</entry>
  33         <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink> prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉</emphasis></entry>
  34        </row>
  35       </tbody>
  36      </tgroup>
  37     </table>
  38     <table frame="all" rowsep="0" colsep="0">
  39       <title>nat</title>
  40       <tgroup cols="4">
  41       <tbody>
  42        <row>
  43         <entry id="nat">&nat;</entry>
  44         <entry>::=</entry>
  45         <entry><emphasis>〈〈any sequence of valid <ulink url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink></emphasis></entry>
  46        </row>
  47       </tbody>
  48      </tgroup>
  49     </table>
  50     <table frame="all" rowsep="0" colsep="0">
  51       <title>char</title>
  52       <tgroup cols="4">
  53       <tbody>
  54        <row>
  55         <entry id="char">&char;</entry>
  56         <entry>::=</entry>
  57         <entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
  58        </row>
  59       </tbody>
  60      </tgroup>
  61     </table>
  62     <table frame="all" rowsep="0" colsep="0">
  63       <title>uri-step</title>
  64       <tgroup cols="4">
  65       <tbody>
  66        <row>
  67         <entry id="uri-step">&uri-step;</entry>
  68         <entry>::=</entry>
  69         <entry>&char;[&char;]…</entry>
  70        </row>
  71       </tbody>
  72      </tgroup>
  73     </table>
  74     <table frame="all" rowsep="0" colsep="0">
  75       <title>uri</title>
  76       <tgroup cols="4">
  77       <tbody>
  78        <row>
  79         <entry id="uri">&uri;</entry>
  80         <entry>::=</entry>
  81         <entry>[<emphasis role="bold">cic:/</emphasis>|<emphasis role="bold">theory:/</emphasis>]&uri-step;[<emphasis role="bold">/</emphasis>&uri-step;]…<emphasis role="bold">.</emphasis>&id;[<emphasis role="bold">.</emphasis>&id;]…[<emphasis role="bold">#xpointer(</emphasis>&nat;<emphasis role="bold">/</emphasis>&nat;[<emphasis role="bold">/</emphasis>&nat;]…<emphasis role="bold">)</emphasis>]</entry>
  82        </row>
  83       </tbody>
  84      </tgroup>
  85     </table>
  86   </para>
  87   </sect2>
  88   <sect2 id="terms">
  89   <title>Terms</title>
  90   <para>
  91   <table frame="all" rowsep="0" colsep="0">
  92     <title>Terms</title>
  93     <tgroup cols="4">
  94     <tbody>
  95      <row>
  96       <entry id="term">&term;</entry>
  97       <entry>::=</entry>
  98       <entry>&sterm;</entry>
  99       <entry>simple or delimited term</entry>
 100      </row>
 101      <row>
 102       <entry/>
 103       <entry>|</entry>
 104       <entry>&term; &term;</entry>
 105       <entry>application</entry>
 106      </row>
 107      <row>
 108       <entry/>
 109       <entry>|</entry>
 110       <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 111       <entry>λ-abstraction</entry>
 112      </row>
 113      <row>
 114       <entry/>
 115       <entry>|</entry>
 116       <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 117       <entry>dependent product meant to define a datatype</entry>
 118      </row>
 119      <row>
 120       <entry/>
 121       <entry>|</entry>
 122       <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 123       <entry>dependent product meant to define a proposition</entry>
 124      </row>
 125      <row>
 126       <entry/>
 127       <entry>|</entry>
 128       <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
 129       <entry>non-dependent product (logical implication or function space)</entry>
 130      </row>
 131      <row>
 132       <entry/>
 133       <entry>|</entry>
 134       <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>
 135       <entry>local definition</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">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<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;|<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;]
 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      <row>
 168       <entry/>
 169       <entry>|</entry>
 170       <entry>…</entry>
 171       <entry>user provided notation</entry>
 172      </row>
 173     </tbody>
 174    </tgroup>
 175   </table>
 176
 177   <table frame="all" rowsep="0" colsep="0">
 178     <title>Simple terms</title>
 179     <tgroup cols="4">
 180     <tbody>
 181      <row>
 182       <entry id="sterm">&sterm;</entry>
 183       <entry>::=</entry>
 184       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 185       <entry/>
 186      </row>
 187      <row>
 188       <entry/>
 189       <entry>|</entry>
 190       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
 191        &id;<emphasis role="bold">≔</emphasis>&term;
 192        [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
 193        <emphasis role="bold">]</emphasis>]
 194       </entry>
 195       <entry>identifier with optional explicit named substitution</entry>
 196      </row>
 197      <row>
 198       <entry/>
 199       <entry>|</entry>
 200       <entry>&uri;</entry>
 201       <entry>a qualified reference</entry>
 202      </row>
 203      <row>
 204       <entry/>
 205       <entry>|</entry>
 206       <entry><emphasis role="bold">Prop</emphasis></entry>
 207       <entry>the impredicative sort of propositions</entry>
 208      </row>
 209      <row>
 210       <entry/>
 211       <entry>|</entry>
 212       <entry><emphasis role="bold">Set</emphasis></entry>
 213       <entry>the impredicate sort of datatypes</entry>
 214      </row>
 215      <row>
 216       <entry/>
 217       <entry>|</entry>
 218       <entry><emphasis role="bold">Type</emphasis></entry>
 219       <entry>one predicative sort of datatypes</entry>
 220      </row>
 221      <row>
 222       <entry/>
 223       <entry>|</entry>
 224       <entry><emphasis role="bold">?</emphasis></entry>
 225       <entry>implicit argument</entry>
 226      </row>
 227      <row>
 228       <entry/>
 229       <entry>|</entry>
 230       <entry><emphasis role="bold">?n</emphasis>
 231       [<emphasis role="bold">[</emphasis>
 232       [<emphasis role="bold">_</emphasis>|&term;]…
 233       <emphasis role="bold">]</emphasis>]</entry>
 234       <entry>metavariable</entry>
 235      </row>
 236      <row>
 237       <entry/>
 238       <entry>|</entry>
 239         <entry><emphasis role="bold">match</emphasis> &term;
 240         [ <emphasis role="bold">in</emphasis> &term; ]
 241         [ <emphasis role="bold">return</emphasis> &term; ]
 242         <emphasis role="bold">with</emphasis>
 243       </entry>
 244       <entry>case analysis</entry>
 245      </row>
 246      <row>
 247       <entry/>
 248       <entry/>
 249       <entry>
 250        <emphasis role="bold">[</emphasis>
 251        &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 252          [
 253          <emphasis role="bold">|</emphasis>
 254          &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 255          ]…<emphasis role="bold">]</emphasis> </entry>
 256       <entry/>
 257      </row>
 258      <row>
 259       <entry/>
 260       <entry>|</entry>
 261       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 262       <entry>cast</entry>
 263      </row>
 264      <row>
 265       <entry/>
 266       <entry>|</entry>
 267       <entry>…</entry>
 268       <entry>user provided notation at precedence 90</entry>
 269      </row>
 270     </tbody>
 271    </tgroup>
 272   </table>
 273
 274   <table frame="all" rowsep="0" colsep="0">
 275     <title>Arguments</title>
 276     <tgroup cols="4">
 277     <tbody>
 278      <row>
 279       <entry id="args">&args;</entry>
 280       <entry>::=</entry>
 281       <entry>
 282        <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
 283       </entry>
 284       <entry>ignored argument</entry>
 285      </row>
 286      <row>
 287       <entry/>
 288       <entry>|</entry>
 289       <entry>
 290        <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
 291       </entry>
 292       <entry>ignored argument</entry>
 293      </row>
 294      <row>
 295       <entry/>
 296       <entry>|</entry>
 297       <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
 298       <entry></entry>
 299      </row>
 300      <row>
 301       <entry/>
 302       <entry>|</entry>
 303       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
 304       <entry/>
 305      </row>
 306     </tbody>
 307    </tgroup>
 308   </table>
 309
 310   <table frame="all" rowsep="0" colsep="0">
 311     <title>Miscellaneous arguments</title>
 312     <tgroup cols="4">
 313     <tbody>
 314      <row>
 315       <entry id="args2">&args2;</entry>
 316       <entry>::=</entry>
 317       <entry>&id;</entry>
 318       <entry/>
 319      </row>
 320      <row>
 321       <entry/>
 322       <entry>|</entry>
 323       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
 324       <entry/>
 325      </row>
 326     </tbody>
 327    </tgroup>
 328   </table>
 329
 330   <table frame="all" rowsep="0" colsep="0">
 331     <title>Pattern matching</title>
 332     <tgroup cols="4">
 333     <tbody>
 334      <row>
 335       <entry id="match_pattern">&match_pattern;</entry>
 336       <entry>::=</entry>
 337       <entry>&id;</entry>
 338       <entry>0-ary constructor</entry>
 339      </row>
 340      <row>
 341       <entry/>
 342       <entry>|</entry>
 343       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
 344       <entry>n-ary constructor (binds the n arguments)</entry>
 345      </row>
 346     </tbody>
 347    </tgroup>
 348   </table>
 349   </para>
 350
 351   </sect2>
 352   </sect1>
 353
 354   <sect1 id="axiom_definition_declaration">
 355    <title>Definitions and declarations</title>
 356    <sect2 id="axiom">
 357     <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
 358     <titleabbrev>axiom</titleabbrev>
 359     <para><userinput>axiom H: P</userinput></para>
 360     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
 361   </sect2>
 362   <sect2 id="definition">
 363     <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 364     <titleabbrev>definition</titleabbrev>
 365     <para><userinput>definition f: T ≝ t</userinput></para>
 366     <para><command>f</command> is defined as <command>t</command>;
 367      <command>T</command> is its type. An error is raised if the type of
 368      <command>t</command> is not convertible to <command>T</command>.</para>
 369     <para><command>T</command> is inferred from <command>t</command> if
 370       omitted.</para>
 371     <para><command>t</command> can be omitted only if <command>T</command> is
 372      given. In this case Matita enters in interactive mode and
 373      <command>f</command> must be defined by means of tactics.</para>
 374     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 375   </sect2>
 376   <sect2 id="inductive">
 377     <title>[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…
 378 [<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]…
 379 </title>
 380     <titleabbrev>(co)inductive types declaration</titleabbrev>
 381     <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
 382     <para>Declares a family of two mutually inductive types
 383      <command>i</command> and <command>i'</command> whose types are
 384      <command>S</command> and <command>S'</command>, which must be convertible
 385      to sorts.</para>
 386     <para>The constructors <command>ki</command> of type <command>Ti</command>
 387      and <command>ki'</command> of type <command>Ti'</command> are also
 388      simultaneously declared. The declared types <command>i</command> and
 389      <command>i'</command> may occur in the types of the constructors, but
 390      only in strongly positive positions according to the rules of the
 391      calculus.</para>
 392     <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
 393     <para>If the keyword <command>coinductive</command> is used, the declared
 394      types are considered mutually coinductive.</para>
 395     <para>Elimination principles for the record are automatically generated
 396      by Matita, if allowed by the typing rules of the calculus according to
 397      the sort <command>S</command>. If generated,
 398      they are named <command>i_ind</command>, <command>i_rec</command> and
 399      <command>i_rect</command> according to the sort of their induction
 400      predicate.</para>
 401   </sect2>
 402   <sect2 id="record">
 403     <title><emphasis role="bold">record</emphasis> &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis><emphasis role="bold">{</emphasis>[&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:&gt;</emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:&gt;</emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>
 404     <titleabbrev>record</titleabbrev>
 405     <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
 406     <para>Declares a new record family <command>id</command> parameterized over
 407      <command>x,y,z</command>.</para>
 408     <para><command>S</command> is the type of the record
 409      and it must be convertible to a sort.</para>
 410     <para>Each field <command>fi</command> is declared by giving its type
 411      <command>Ti</command>. A record without any field is admitted.</para>
 412     <para>Elimination principles for the record are automatically generated
 413      by Matita, if allowed by the typing rules of the calculus according to
 414      the sort <command>S</command>. If generated,
 415      they are named <command>i_ind</command>, <command>i_rec</command> and
 416      <command>i_rect</command> according to the sort of their induction
 417      predicate.</para>
 418     <para>For each field <command>fi</command> a record projection
 419      <command>fi</command> is also automatically generated if projection
 420      is allowed by the typing rules of the calculus according to the
 421      sort <command>S</command>, the type <command>T1</command> and
 422      the definability of depending record projections.</para>
 423     <para>If the type of a field is declared with <command>:&gt;</command>,
 424      the corresponding record projection becomes an implicit coercion.
 425      This is just syntactic sugar and it has the same effect of declaring the
 426      record projection as a coercion later on.</para>
 427   </sect2>
 428   </sect1>
 429
 430   <sect1 id="proofs">
 431    <title>Proofs</title>
 432    <sect2 id="theorem">
 433     <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 434     <titleabbrev>theorem</titleabbrev>
 435     <para><userinput>theorem f: P ≝ p</userinput></para>
 436     <para>Proves a new theorem <command>f</command> whose thesis is
 437      <command>P</command>.</para>
 438     <para>If <command>p</command> is provided, it must be a proof term for
 439      <command>P</command>. Otherwise an interactive proof is started.</para>
 440     <para><command>P</command> can be omitted only if the proof is not
 441      interactive.</para>
 442     <para>Proving a theorem already proved in the library is an error.
 443      To provide an alternative name and proof for the same theorem, use
 444      <command>variant f: P ≝ p</command>.</para>
 445     <para>A warning is raised if the name of the theorem cannot be obtained
 446       by mangling the name of the constants in its thesis.</para>
 447     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 448    </sect2>
 449    <sect2 id="variant">
 450     <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 451     <titleabbrev>variant</titleabbrev>
 452     <para><userinput>variant f: T ≝ t</userinput></para>
 453     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 454      complain if the theorem has already been proved. To be used to give
 455      an alternative name or proof to a theorem.</para>
 456    </sect2>
 457    <sect2 id="lemma">
 458     <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 459     <titleabbrev>lemma</titleabbrev>
 460     <para><userinput>lemma f: T ≝ t</userinput></para>
 461     <para>Same as <command>theorem f: T ≝ t</command></para>
 462    </sect2>
 463    <sect2 id="fact">
 464     <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 465     <titleabbrev>fact</titleabbrev>
 466     <para><userinput>fact f: T ≝ t</userinput></para>
 467     <para>Same as <command>theorem f: T ≝ t</command></para>
 468    </sect2>
 469    <sect2 id="remark">
 470     <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 471     <titleabbrev>remark</titleabbrev>
 472     <para><userinput>remark f: T ≝ t</userinput></para>
 473     <para>Same as <command>theorem f: T ≝ t</command></para>
 474    </sect2>
 475   </sect1>
 476
 477 </chapter>
 478