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 cols="4">
  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 cols="4">
  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 cols="4">
  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 cols="4">
  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 cols="4">
 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 cols="4">
 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> &term;]
 253       </entry>
 254       <entry>ignored argument</entry>
 255      </row>
 256      <row>
 257       <entry/>
 258       <entry>|</entry>
 259       <entry>
 260        <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
 261       </entry>
 262       <entry>ignored argument</entry>
 263      </row>
 264      <row>
 265       <entry/>
 266       <entry>|</entry>
 267       <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
 268       <entry></entry>
 269      </row>
 270      <row>
 271       <entry/>
 272       <entry>|</entry>
 273       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
 274       <entry/>
 275      </row>
 276     </tbody>
 277    </tgroup>
 278   </table>
 279
 280   <table>
 281     <tgroup cols="4">
 282      <thead />
 283     <tbody>
 284      <row>
 285       <entry id="args2">&args2;</entry>
 286       <entry>::=</entry>
 287       <entry>&id;</entry>
 288       <entry/>
 289      </row>
 290      <row>
 291       <entry/>
 292       <entry>|</entry>
 293       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
 294       <entry/>
 295      </row>
 296     </tbody>
 297    </tgroup>
 298   </table>
 299
 300   <table>
 301     <tgroup cols="4">
 302      <thead />
 303     <tbody>
 304      <row>
 305       <entry id="match_pattern">&match_pattern;</entry>
 306       <entry>::=</entry>
 307       <entry>&id;</entry>
 308       <entry>0-ary constructor</entry>
 309      </row>
 310      <row>
 311       <entry/>
 312       <entry>|</entry>
 313       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
 314       <entry>n-ary constructor (binds the n arguments)</entry>
 315      </row>
 316     </tbody>
 317    </tgroup>
 318   </table>
 319
 320   </sect2>
 321   </sect1>
 322
 323   <sect1 id="axiom_definition_declaration">
 324    <title>Definitions and declarations</title>
 325    <sect2 id="axiom">
 326     <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
 327     <titleabbrev>axiom</titleabbrev>
 328     <para><userinput>axiom H: P</userinput></para>
 329     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
 330   </sect2>
 331   <sect2 id="definition">
 332     <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 333     <titleabbrev>definition</titleabbrev>
 334     <para><userinput>definition f: T ≝ t</userinput></para>
 335     <para><command>f</command> is defined as <command>t</command>;
 336      <command>T</command> is its type. An error is raised if the type of
 337      <command>t</command> is not convertible to <command>T</command>.</para>
 338     <para><command>T</command> is inferred from <command>t</command> if
 339       omitted.</para>
 340     <para><command>t</command> can be omitted only if <command>T</command> is
 341      given. In this case Matita enters in interactive mode and
 342      <command>f</command> must be defined by means of tactics.</para>
 343     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 344   </sect2>
 345   <sect2 id="inductive">
 346     <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;]…
 347 [<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;]…]…
 348 </title>
 349     <titleabbrev>(co)inductive types declaration</titleabbrev>
 350     <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
 351     <para>Declares a family of two mutually inductive types
 352      <command>i</command> and <command>i'</command> whose types are
 353      <command>S</command> and <command>S'</command>, which must be convertible
 354      to sorts.</para>
 355     <para>The constructors <command>ki</command> of type <command>Ti</command>
 356      and <command>ki'</command> of type <command>Ti'</command> are also
 357      simultaneously declared. The declared types <command>i</command> and
 358      <command>i'</command> may occur in the types of the constructors, but
 359      only in strongly positive positions according to the rules of the
 360      calculus.</para>
 361     <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
 362     <para>If the keyword <command>coinductive</command> is used, the declared
 363      types are considered mutually coinductive.</para>
 364     <para>Elimination principles for the record are automatically generated
 365      by Matita, if allowed by the typing rules of the calculus according to
 366      the sort <command>S</command>. If generated,
 367      they are named <command>i_ind</command>, <command>i_rec</command> and
 368      <command>i_rect</command> according to the sort of their induction
 369      predicate.</para>
 370   </sect2>
 371   <sect2 id="record">
 372     <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>
 373     <titleabbrev>record</titleabbrev>
 374     <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
 375     <para>Declares a new record family <command>id</command> parameterized over
 376      <command>x,y,z</command>.</para>
 377     <para><command>S</command> is the type of the record
 378      and it must be convertible to a sort.</para>
 379     <para>Each field <command>fi</command> is declared by giving its type
 380      <command>Ti</command>. A record without any field is admitted.</para>
 381     <para>Elimination principles for the record are automatically generated
 382      by Matita, if allowed by the typing rules of the calculus according to
 383      the sort <command>S</command>. If generated,
 384      they are named <command>i_ind</command>, <command>i_rec</command> and
 385      <command>i_rect</command> according to the sort of their induction
 386      predicate.</para>
 387     <para>For each field <command>fi</command> a record projection
 388      <command>fi</command> is also automatically generated if projection
 389      is allowed by the typing rules of the calculus according to the
 390      sort <command>S</command>, the type <command>T1</command> and
 391      the definability of depending record projections.</para>
 392     <para>If the type of a field is declared with <command>:&gt;</command>,
 393      the corresponding record projection becomes an implicit coercion.
 394      This is just syntactic sugar and it has the same effect of declaring the
 395      record projection as a coercion later on.</para>
 396   </sect2>
 397   </sect1>
 398
 399   <sect1 id="proofs">
 400    <title>Proofs</title>
 401    <sect2 id="theorem">
 402     <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 403     <titleabbrev>theorem</titleabbrev>
 404     <para><userinput>theorem f: P ≝ p</userinput></para>
 405     <para>Proves a new theorem <command>f</command> whose thesis is
 406      <command>P</command>.</para>
 407     <para>If <command>p</command> is provided, it must be a proof term for
 408      <command>P</command>. Otherwise an interactive proof is started.</para>
 409     <para><command>P</command> can be omitted only if the proof is not
 410      interactive.</para>
 411     <para>Proving a theorem already proved in the library is an error.
 412      To provide an alternative name and proof for the same theorem, use
 413      <command>variant f: P ≝ p</command>.</para>
 414     <para>A warning is raised if the name of the theorem cannot be obtained
 415       by mangling the name of the constants in its thesis.</para>
 416     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 417    </sect2>
 418    <sect2 id="variant">
 419     <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 420     <titleabbrev>variant</titleabbrev>
 421     <para><userinput>variant f: T ≝ t</userinput></para>
 422     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 423      complain if the theorem has already been proved. To be used to give
 424      an alternative name or proof to a theorem.</para>
 425    </sect2>
 426    <sect2 id="lemma">
 427     <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 428     <titleabbrev>lemma</titleabbrev>
 429     <para><userinput>lemma f: T ≝ t</userinput></para>
 430     <para>Same as <command>theorem f: T ≝ t</command></para>
 431    </sect2>
 432    <sect2 id="fact">
 433     <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 434     <titleabbrev>fact</titleabbrev>
 435     <para><userinput>fact f: T ≝ t</userinput></para>
 436     <para>Same as <command>theorem f: T ≝ t</command></para>
 437    </sect2>
 438    <sect2 id="remark">
 439     <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 440     <titleabbrev>remark</titleabbrev>
 441     <para><userinput>remark f: T ≝ t</userinput></para>
 442     <para>Same as <command>theorem f: T ≝ t</command></para>
 443    </sect2>
 444   </sect1>
 445
 446 </chapter>
 447