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