matita/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     <listitem><para>Characters belonging to a set of characters are given
  21      by listing the set elements in square brackets. Hyphens are used to
  22      specify ranges of characters in the set.
  23      E.g.: [<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</para></listitem>
  24   </orderedlist>
  25   <sect1 id="terms_and_co">
  26   <title>Terms &amp; co.</title>
  27   <sect2 id="lexical">
  28   <title>Lexical conventions</title>
  29     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  30       <title>qstring</title>
  31       <tgroup cols="4">
  32       <tbody>
  33        <row>
  34         <entry id="grammar.qstring">&qstring;</entry>
  35         <entry>::=</entry>
  36         <entry><emphasis role="bold">&quot;</emphasis><emphasis>〈〈any sequence of characters excluded &quot;〉〉</emphasis><emphasis role="bold">&quot;</emphasis></entry>
  37        </row>
  38       </tbody>
  39      </tgroup>
  40     </table>
  41     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  42       <title>id</title>
  43       <tgroup cols="4">
  44       <tbody>
  45        <row>
  46         <entry id="grammar.id">&id;</entry>
  47         <entry>::=</entry>
  48         <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink type="http" 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>
  49        </row>
  50       </tbody>
  51      </tgroup>
  52     </table>
  53     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  54       <title>nat</title>
  55       <tgroup cols="4">
  56       <tbody>
  57        <row>
  58         <entry id="grammar.nat">&nat;</entry>
  59         <entry>::=</entry>
  60         <entry><emphasis>〈〈any sequence of valid <ulink type="http" url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink>〉〉</emphasis></entry>
  61        </row>
  62       </tbody>
  63      </tgroup>
  64     </table>
  65     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  66       <title>char</title>
  67       <tgroup cols="4">
  68       <tbody>
  69        <row>
  70         <entry id="grammar.char">&char;</entry>
  71         <entry>::=</entry>
  72         <entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
  73        </row>
  74       </tbody>
  75      </tgroup>
  76     </table>
  77     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  78       <title>uri-step</title>
  79       <tgroup cols="4">
  80       <tbody>
  81        <row>
  82         <entry id="grammar.uri-step">&uri-step;</entry>
  83         <entry>::=</entry>
  84         <entry>&char;[&char;]…</entry>
  85        </row>
  86       </tbody>
  87      </tgroup>
  88     </table>
  89     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  90       <title>uri</title>
  91       <tgroup cols="4">
  92       <tbody>
  93        <row>
  94         <entry id="grammar.uri">&uri;</entry>
  95         <entry>::=</entry>
  96         <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>
  97        </row>
  98       </tbody>
  99      </tgroup>
 100     </table>
 101     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 102       <title>csymbol</title>
 103       <tgroup cols="4">
 104       <tbody>
 105        <row>
 106         <entry id="grammar.csymbol">&csymbol;</entry>
 107         <entry>::=</entry>
 108         <entry><emphasis role="bold">'</emphasis>&id;</entry>
 109        </row>
 110       </tbody>
 111       </tgroup>
 112     </table>
 113     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 114       <title>symbol</title>
 115       <tgroup cols="4">
 116       <tbody>
 117        <row>
 118         <entry id="grammar.symbol">&symbol;</entry>
 119         <entry>::=</entry>
 120         <entry><emphasis role="bold">〈〈None of the above〉〉</emphasis></entry>
 121        </row>
 122       </tbody>
 123       </tgroup>
 124     </table>
 125   </sect2>
 126   <sect2 id="terms">
 127   <title>Terms</title>
 128
 129   <!-- ZACK: Sample EBNF snippet, see:
 130   http://www.docbook.org/tdg/en/html/productionset.html -->
 131   <!--
 132   <productionset>
 133     <title>Terms</title>
 134     <production id="grammar.term">
 135       <lhs>&term;</lhs>
 136       <rhs>&sterm;</rhs>
 137       <lineannotation></lineannotation>
 138     </production>
 139   </productionset>
 140   -->
 141
 142   <para>
 143   <table id="tbl_terms" frame="topbot" rowsep="0" colsep="0" role="grammar">
 144     <title>Terms</title>
 145     <tgroup cols="4">
 146     <tbody>
 147      <row>
 148       <entry id="grammar.term">&term;</entry>
 149       <entry>::=</entry>
 150       <entry>&sterm;</entry>
 151       <entry>simple or delimited term</entry>
 152      </row>
 153      <row>
 154       <entry/>
 155       <entry>|</entry>
 156       <entry>&term; &term;</entry>
 157       <entry>application</entry>
 158      </row>
 159      <row>
 160       <entry/>
 161       <entry>|</entry>
 162       <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 163       <entry>λ-abstraction</entry>
 164      </row>
 165      <row>
 166       <entry/>
 167       <entry>|</entry>
 168       <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 169       <entry>dependent product meant to define a datatype</entry>
 170      </row>
 171      <row>
 172       <entry/>
 173       <entry>|</entry>
 174       <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 175       <entry>dependent product meant to define a proposition</entry>
 176      </row>
 177      <row>
 178       <entry/>
 179       <entry>|</entry>
 180       <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
 181       <entry>non-dependent product (logical implication or function space)</entry>
 182      </row>
 183      <row>
 184       <entry/>
 185       <entry>|</entry>
 186       <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>
 187       <entry>local definition</entry>
 188      </row>
 189      <row>
 190       <entry/>
 191       <entry>|</entry>
 192       <entry>
 193         <emphasis role="bold">let</emphasis>
 194         [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
 195         &rec_def;
 196       </entry>
 197       <entry>(co)recursive definitions</entry>
 198      </row>
 199      <row>
 200       <entry/>
 201       <entry/>
 202       <entry>
 203       [<emphasis role="bold">and</emphasis> &rec_def;]…
 204       </entry>
 205       <entry/>
 206      </row>
 207      <row>
 208       <entry/>
 209       <entry/>
 210       <entry>
 211       <emphasis role="bold">in</emphasis> &term;
 212       </entry>
 213       <entry/>
 214      </row>
 215      <row>
 216       <entry/>
 217       <entry>|</entry>
 218       <entry>…</entry>
 219       <entry>user provided notation</entry>
 220      </row>
 221       <row>
 222         <entry id="grammar.rec_def">&rec_def;</entry>
 223         <entry>::=</entry>
 224         <entry>
 225           &id; [&id;|<emphasis role="bold">_</emphasis>|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
 226         </entry>
 227         <entry />
 228       </row>
 229       <row>
 230         <entry />
 231         <entry />
 232         <entry>
 233           [<emphasis role="bold">on</emphasis> &id;]
 234           [<emphasis role="bold">:</emphasis> &term;]
 235           <emphasis role="bold">≝</emphasis> &term;]
 236         </entry>
 237         <entry />
 238       </row>
 239     </tbody>
 240    </tgroup>
 241   </table>
 242
 243   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 244     <title>Simple terms</title>
 245     <tgroup cols="4">
 246     <tbody>
 247      <row>
 248       <entry id="grammar.sterm">&sterm;</entry>
 249       <entry>::=</entry>
 250       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 251       <entry/>
 252      </row>
 253      <row>
 254       <entry/>
 255       <entry>|</entry>
 256       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
 257        &id;<emphasis role="bold">≔</emphasis>&term;
 258        [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
 259        <emphasis role="bold">]</emphasis>]
 260       </entry>
 261       <entry>identifier with optional explicit named substitution</entry>
 262      </row>
 263      <row>
 264       <entry/>
 265       <entry>|</entry>
 266       <entry>&uri;</entry>
 267       <entry>a qualified reference</entry>
 268      </row>
 269      <row>
 270       <entry/>
 271       <entry>|</entry>
 272       <entry><emphasis role="bold">Prop</emphasis></entry>
 273       <entry>the impredicative sort of propositions</entry>
 274      </row>
 275      <row>
 276       <entry/>
 277       <entry>|</entry>
 278       <entry><emphasis role="bold">Set</emphasis></entry>
 279       <entry>the impredicate sort of datatypes</entry>
 280      </row>
 281      <row>
 282       <entry/>
 283       <entry>|</entry>
 284       <entry><emphasis role="bold">CProp</emphasis></entry>
 285       <entry>one fixed predicative sort of constructive propositions</entry>
 286      </row>
 287      <row>
 288       <entry/>
 289       <entry>|</entry>
 290       <entry><emphasis role="bold">Type</emphasis></entry>
 291       <entry>one predicative sort of datatypes</entry>
 292      </row>
 293      <row>
 294       <entry/>
 295       <entry>|</entry>
 296       <entry><emphasis role="bold">?</emphasis></entry>
 297       <entry>implicit argument</entry>
 298      </row>
 299      <row>
 300       <entry/>
 301       <entry>|</entry>
 302       <entry><emphasis role="bold">?n</emphasis>
 303       [<emphasis role="bold">[</emphasis>
 304       [<emphasis role="bold">_</emphasis>|&term;]…
 305       <emphasis role="bold">]</emphasis>]</entry>
 306       <entry>metavariable</entry>
 307      </row>
 308      <row>
 309       <entry/>
 310       <entry>|</entry>
 311         <entry><emphasis role="bold">match</emphasis> &term;
 312         [ <emphasis role="bold">in</emphasis> &id; ]
 313         [ <emphasis role="bold">return</emphasis> &term; ]
 314         <emphasis role="bold">with</emphasis>
 315       </entry>
 316       <entry>case analysis</entry>
 317      </row>
 318      <row>
 319       <entry/>
 320       <entry/>
 321       <entry>
 322        <emphasis role="bold">[</emphasis>
 323        &match_branch;[<emphasis role="bold">|</emphasis>&match_branch;]…
 324        <emphasis role="bold">]</emphasis>
 325       </entry>
 326       <entry/>
 327      </row>
 328      <row>
 329       <entry/>
 330       <entry>|</entry>
 331       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 332       <entry>cast</entry>
 333      </row>
 334      <row>
 335       <entry/>
 336       <entry>|</entry>
 337       <entry>…</entry>
 338       <entry>user provided notation at precedence 90</entry>
 339      </row>
 340     </tbody>
 341    </tgroup>
 342   </table>
 343
 344   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 345     <title>Arguments</title>
 346     <tgroup cols="4">
 347     <tbody>
 348      <row>
 349       <entry id="grammar.args">&args;</entry>
 350       <entry>::=</entry>
 351       <entry>
 352        <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
 353       </entry>
 354       <entry>ignored argument</entry>
 355      </row>
 356      <row>
 357       <entry/>
 358       <entry>|</entry>
 359       <entry>
 360        <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
 361       </entry>
 362       <entry>ignored argument</entry>
 363      </row>
 364      <row>
 365       <entry/>
 366       <entry>|</entry>
 367       <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
 368       <entry></entry>
 369      </row>
 370      <row>
 371       <entry/>
 372       <entry>|</entry>
 373       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
 374       <entry/>
 375      </row>
 376      <row>
 377       <entry id="grammar.args2">&args2;</entry>
 378       <entry>::=</entry>
 379       <entry>&id;</entry>
 380       <entry/>
 381      </row>
 382      <row>
 383       <entry/>
 384       <entry>|</entry>
 385       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
 386       <entry/>
 387      </row>
 388     </tbody>
 389    </tgroup>
 390   </table>
 391
 392   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 393     <title>Pattern matching</title>
 394     <tgroup cols="4">
 395     <tbody>
 396       <row>
 397         <entry id="grammar.match_branch">&match_branch;</entry>
 398         <entry>::=</entry>
 399         <entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
 400         <entry />
 401       </row>
 402      <row>
 403       <entry id="grammar.match_pattern">&match_pattern;</entry>
 404       <entry>::=</entry>
 405       <entry>&id;</entry>
 406       <entry>0-ary constructor</entry>
 407      </row>
 408      <row>
 409       <entry/>
 410       <entry>|</entry>
 411       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
 412       <entry>n-ary constructor (binds the n arguments)</entry>
 413      </row>
 414      <row>
 415       <entry/>
 416       <entry>|</entry>
 417       <entry>&id; &id; [&id;]…</entry>
 418       <entry>n-ary constructor (binds the n arguments)</entry>
 419      </row>
 420      <row>
 421       <entry/>
 422       <entry>|</entry>
 423       <entry><emphasis role="bold">_</emphasis></entry>
 424       <entry>any remaining constructor (ignoring its arguments)</entry>
 425      </row>
 426     </tbody>
 427    </tgroup>
 428   </table>
 429   </para>
 430
 431   </sect2>
 432   </sect1>
 433
 434   <sect1 id="axiom_definition_declaration">
 435    <title>Definitions and declarations</title>
 436    <sect2 id="axiom">
 437     <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
 438     <titleabbrev>axiom</titleabbrev>
 439     <para><userinput>axiom H: P</userinput></para>
 440     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
 441   </sect2>
 442   <sect2 id="definition">
 443     <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 444     <titleabbrev>definition</titleabbrev>
 445     <para><userinput>definition f: T ≝ t</userinput></para>
 446     <para><command>f</command> is defined as <command>t</command>;
 447      <command>T</command> is its type. An error is raised if the type of
 448      <command>t</command> is not convertible to <command>T</command>.</para>
 449     <para><command>T</command> is inferred from <command>t</command> if
 450       omitted.</para>
 451     <para><command>t</command> can be omitted only if <command>T</command> is
 452      given. In this case Matita enters in interactive mode and
 453      <command>f</command> must be defined by means of tactics.</para>
 454     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 455   </sect2>
 456   <sect2 id="discriminator">
 457     <title><emphasis role="bold">discriminator</emphasis> &id;</title>
 458     <titleabbrev>discriminator</titleabbrev>
 459     <para><userinput>discriminator i</userinput></para>
 460     <para>Defines a new discrimination (injectivity+conflict) principle à la
 461      McBride for the inductive type <command>i</command>.</para>
 462     <para>The principle will use John
 463      Major's equality if such equality is defined, otherwise it will use
 464      Leibniz equality; in the former case, it will be called
 465      <command>i_jmdiscr</command>, in the latter, <command>i_discr</command>.
 466      The command will fail if neither equality is available.</para>
 467     <para>Discrimination principles are used by the destruct tactic and are
 468      usually automatically generated by Matita during the definition of the
 469      corresponding inductive type. This command is thus especially useful
 470      when the correct equality was not loaded at the time of that
 471      definition.</para>
 472   </sect2>
 473   <sect2 id="inverter">
 474     <title><emphasis role="bold">inverter</emphasis> &id; <emphasis role="bold">for</emphasis> &id; (&path;) [&term;]</title>
 475     <titleabbrev>inverter</titleabbrev>
 476     <para><userinput>inverter n for i (path) : s</userinput></para>
 477     <para>Defines a new induction/inversion principle for the inductive type
 478      <command>i</command>, called <command>n</command>.</para>
 479     <para><command>(path)</command> must be in the form <command>(# # # ... #)</command>,
 480      where each <command>#</command> can be either <command>?</command> or
 481      <command>%</command>, and the number of symbols is equal to the number of
 482      right parameters (indices) of <command>i</command>. Parentheses are
 483      mandatory. If the j-th symbol is
 484      <command>%</command>, Matita will generate a principle providing
 485      equations for reasoning on the j-th index of <command>i</command>. If the
 486      symbol is a <command>?</command>, no corresponding equation will be
 487      provided.</para>
 488     <para><command>s</command>, which must be a sort, is the target sort of the
 489      induction/inversion principle and defaults to <command>Prop</command>.</para>
 490   </sect2>
 491   <sect2 id="letrec">
 492     <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
 493     <titleabbrev>&TODO;</titleabbrev>
 494     <para>&TODO;</para>
 495   </sect2>
 496   <sect2 id="inductive">
 497     <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;]…
 498 [<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;]…]…
 499 </title>
 500     <titleabbrev>(co)inductive types declaration</titleabbrev>
 501     <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
 502     <para>Declares a family of two mutually inductive types
 503      <command>i</command> and <command>i'</command> whose types are
 504      <command>S</command> and <command>S'</command>, which must be convertible
 505      to sorts.</para>
 506     <para>The constructors <command>ki</command> of type <command>Ti</command>
 507      and <command>ki'</command> of type <command>Ti'</command> are also
 508      simultaneously declared. The declared types <command>i</command> and
 509      <command>i'</command> may occur in the types of the constructors, but
 510      only in strongly positive positions according to the rules of the
 511      calculus.</para>
 512     <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
 513     <para>If the keyword <command>coinductive</command> is used, the declared
 514      types are considered mutually coinductive.</para>
 515     <para>Elimination principles for the record are automatically generated
 516      by Matita, if allowed by the typing rules of the calculus according to
 517      the sort <command>S</command>. If generated,
 518      they are named <command>i_ind</command>, <command>i_rec</command> and
 519      <command>i_rect</command> according to the sort of their induction
 520      predicate.</para>
 521   </sect2>
 522   <sect2 id="record">
 523     <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>
 524     <titleabbrev>record</titleabbrev>
 525     <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
 526     <para>Declares a new record family <command>id</command> parameterized over
 527      <command>x,y,z</command>.</para>
 528     <para><command>S</command> is the type of the record
 529      and it must be convertible to a sort.</para>
 530     <para>Each field <command>fi</command> is declared by giving its type
 531      <command>Ti</command>. A record without any field is admitted.</para>
 532     <para>Elimination principles for the record are automatically generated
 533      by Matita, if allowed by the typing rules of the calculus according to
 534      the sort <command>S</command>. If generated,
 535      they are named <command>i_ind</command>, <command>i_rec</command> and
 536      <command>i_rect</command> according to the sort of their induction
 537      predicate.</para>
 538     <para>For each field <command>fi</command> a record projection
 539      <command>fi</command> is also automatically generated if projection
 540      is allowed by the typing rules of the calculus according to the
 541      sort <command>S</command>, the type <command>T1</command> and
 542      the definability of depending record projections.</para>
 543     <para>If the type of a field is declared with <command>:&gt;</command>,
 544      the corresponding record projection becomes an implicit coercion.
 545      This is just syntactic sugar and it has the same effect of declaring the
 546      record projection as a coercion later on.</para>
 547   </sect2>
 548   </sect1>
 549
 550   <sect1 id="proofs">
 551    <title>Proofs</title>
 552    <sect2 id="theorem">
 553     <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 554     <titleabbrev>theorem</titleabbrev>
 555     <para><userinput>theorem f: P ≝ p</userinput></para>
 556     <para>Proves a new theorem <command>f</command> whose thesis is
 557      <command>P</command>.</para>
 558     <para>If <command>p</command> is provided, it must be a proof term for
 559      <command>P</command>. Otherwise an interactive proof is started.</para>
 560     <para><command>P</command> can be omitted only if the proof is not
 561      interactive.</para>
 562      <!--
 563     <para>Proving a theorem already proved in the library is an error.
 564      To provide an alternative name and proof for the same theorem, use
 565      <command>variant f: P ≝ p</command>.</para>-->
 566     <para>A warning is raised if the name of the theorem cannot be obtained
 567       by mangling the name of the constants in its thesis.</para>
 568     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 569    </sect2>
 570    <!--
 571    <sect2 id="variant">
 572     <title><emphasis role="bold">variant</emphasis> &id;<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> &term;</title>
 573     <titleabbrev>variant</titleabbrev>
 574     <para><userinput>variant f: T ≝ t</userinput></para>
 575     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 576      complain if the theorem has already been proved. To be used to give
 577      an alternative name or proof to a theorem.</para>
 578    </sect2>-->
 579    <sect2 id="corollary">
 580     <title><emphasis role="bold">corollary</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 581     <titleabbrev>corollary</titleabbrev>
 582     <para><userinput>corollary f: T ≝ t</userinput></para>
 583     <para>Same as <command>theorem f: T ≝ t</command></para>
 584    </sect2>
 585    <sect2 id="lemma">
 586     <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 587     <titleabbrev>lemma</titleabbrev>
 588     <para><userinput>lemma f: T ≝ t</userinput></para>
 589     <para>Same as <command>theorem f: T ≝ t</command></para>
 590    </sect2>
 591    <sect2 id="fact">
 592     <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 593     <titleabbrev>fact</titleabbrev>
 594     <para><userinput>fact f: T ≝ t</userinput></para>
 595     <para>Same as <command>theorem f: T ≝ t</command></para>
 596    </sect2>
 597    <sect2 id="example">
 598     <title><emphasis role="bold">example</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 599     <titleabbrev>example</titleabbrev>
 600     <para><userinput>example f: T ≝ t</userinput></para>
 601     <para>Same as <command>theorem f: T ≝ t</command>, but the example
 602      is not indexed nor used by automation.</para>
 603    </sect2>
 604   </sect1>
 605
 606   <sect1 id="tacticargs">
 607    <title>Tactic arguments</title>
 608    <para>This section documents the syntax of some recurring arguments for
 609     tactics.</para>
 610
 611     <!--
 612     <sect2 id="introsspec">
 613     <title>intros-spec</title>
 614     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 615       <title>intros-spec</title>
 616       <tgroup cols="4">
 617       <tbody>
 618        <row>
 619         <entry id="grammar.intros-spec">&intros-spec;</entry>
 620         <entry>::=</entry>
 621         <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
 622        </row>
 623       </tbody>
 624      </tgroup>
 625     </table>
 626         <para>The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses.</para>
 627     </sect2>
 628     -->
 629
 630     <sect2 id="pattern">
 631     <title>pattern</title>
 632     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 633       <title>pattern</title>
 634       <tgroup cols="4">
 635       <tbody>
 636        <row>
 637         <entry id="grammar.pattern">&pattern;</entry>
 638         <entry>::=</entry>
 639         <entry><emphasis role="bold">in</emphasis>
 640           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
 641           [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
 642         <entry>simple pattern</entry>
 643        </row>
 644        <row>
 645         <entry/>
 646         <entry>|</entry>
 647         <entry><emphasis role="bold">in</emphasis> <emphasis role="bold">match</emphasis> &path;
 648           [<emphasis role="bold">in</emphasis>
 649           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
 650           [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
 651         <entry>full pattern</entry>
 652        </row>
 653       </tbody>
 654      </tgroup>
 655     </table>
 656     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 657       <title>path</title>
 658       <tgroup cols="3">
 659       <tbody>
 660        <row>
 661         <entry id="grammar.path">&path;</entry>
 662         <entry>::=</entry>
 663         <entry><emphasis>〈〈any &sterm; without occurrences of <emphasis role="bold">Set</emphasis>, <emphasis role="bold">Prop</emphasis>, <emphasis role="bold">CProp</emphasis>, <emphasis role="bold">Type</emphasis>, &id;, &uri; and user provided notation; however, <emphasis role="bold">%</emphasis> is now an additional production for &sterm;〉〉</emphasis></entry>
 664        </row>
 665       </tbody>
 666      </tgroup>
 667     </table>
 668     <para>A <emphasis>path</emphasis> locates zero or more subterms of a given term by mimicking the term structure up to:</para>
 669     <orderedlist>
 670       <listitem><para>Occurrences of the subterms to locate that are
 671        represented by <emphasis role="bold">%</emphasis>.</para></listitem>
 672       <listitem><para>Subterms without any occurrence of subterms to locate
 673        that can be represented by <emphasis role="bold">?</emphasis>.
 674        </para></listitem>
 675     </orderedlist>
 676     <para>Warning: the format for a path for a <emphasis role="bold">match</emphasis> … <emphasis role="bold">with</emphasis>
 677      expression is restricted to: <emphasis role="bold">match</emphasis> &path;
 678      <emphasis role="bold">with</emphasis>
 679      <emphasis role="bold">[</emphasis>
 680      <emphasis role="bold">_</emphasis>
 681      <emphasis role="bold">⇒</emphasis>
 682      &path;
 683      <emphasis role="bold">|</emphasis> …
 684      <emphasis role="bold">|</emphasis>
 685      <emphasis role="bold">_</emphasis>
 686      <emphasis role="bold">⇒</emphasis>
 687      &path;
 688      <emphasis role="bold">]</emphasis>
 689      Its semantics is the following: the n-th
 690      &quot;<emphasis role="bold">_</emphasis>
 691      <emphasis role="bold">⇒</emphasis>
 692      &path;&quot; branch is matched against the n-th constructor of the
 693      inductive data type. The head λ-abstractions of &path; are matched
 694      against the corresponding constructor arguments.
 695     </para>
 696     <para>For instance, the path
 697       <userinput>∀_,_:?.(? ? % ?)→(? ? ? %)</userinput>
 698        locates at once the subterms
 699       <userinput>x+y</userinput> and <userinput>x*y</userinput> in the
 700       term <userinput>∀x,y:nat.x+y=1→0=x*y</userinput>
 701       (where the notation <userinput>A=B</userinput> hides the term
 702       <userinput>(eq T A B)</userinput> for some type <userinput>T</userinput>).
 703     </para>
 704     <para>A <emphasis>simple pattern</emphasis> extends paths to locate
 705      subterms in a whole sequent. In particular, the pattern
 706      <userinput>{ H: p  K: q ⊢ r }</userinput> locates at once all the subterms
 707      located by the pattern <userinput>r</userinput> in the conclusion of the
 708      sequent and by the patterns <userinput>p</userinput> and
 709      <userinput>q</userinput> in the hypotheses <userinput>H</userinput>
 710      and <userinput>K</userinput> of the sequent.
 711     </para>
 712     <para>If no list of hypotheses is provided in a simple pattern, no subterm
 713      is selected in the hypothesis. If the <userinput>⊢ p</userinput>
 714      part of the pattern is not provided, no subterm will be matched in the
 715      conclusion if at least one hypothesis is provided; otherwise the whole
 716      conclusion is selected.
 717     </para>
 718     <para>Finally, a <emphasis>full pattern</emphasis> is interpreted in three
 719      steps. In the first step the <userinput>match T in</userinput>
 720      part is ignored and a set <emphasis>S</emphasis> of subterms is
 721      located as for the case of
 722      simple patterns. In the second step the term <userinput>T</userinput>
 723      is parsed and interpreted in the context of each subterm
 724      <emphasis>s ∈ S</emphasis>. In the last term for each
 725      <emphasis>s ∈ S</emphasis> the interpreted term <userinput>T</userinput>
 726      computed in the previous step is looked for. The final set of subterms
 727      located by the full pattern is the set of occurrences of
 728      the interpreted <userinput>T</userinput> in the subterms <emphasis>s</emphasis>.
 729     </para>
 730     <para>A full pattern can always be replaced by a simple pattern,
 731       often at the cost of increased verbosity or decreased readability.</para>
 732     <para>Example: the pattern
 733       <userinput>{ match x+y in ⊢ ∀_,_:?.(? ? % ?) }</userinput>
 734       locates only the first occurrence of <userinput>x+y</userinput>
 735       in the sequent <userinput>x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) =
 736       z * (x+y) + w * (x+y)</userinput>. The corresponding simple pattern
 737       is <userinput>{ ⊢ ∀_,_:?.(? ? (? % ?) ?) }</userinput>.
 738     </para>
 739     <para>Every tactic that acts on subterms of the selected sequents have
 740      a pattern argument for uniformity. To automatically generate a simple
 741      pattern:</para>
 742     <orderedlist>
 743      <listitem><para>Select in the current goal the subterms to pass to the
 744       tactic by using the mouse. In order to perform a multiple selection of
 745       subterms, hold the Ctrl key while selecting every subterm after the
 746       first one.</para></listitem>
 747      <listitem><para>From the contextual menu select &quot;Copy&quot;.</para></listitem>
 748      <listitem><para>From the &quot;Edit&quot; or the contextual menu select
 749       &quot;Paste as pattern&quot;</para></listitem>
 750     </orderedlist>
 751     </sect2>
 752
 753     <sect2 id="reduction-kind">
 754     <title>reduction-kind</title>
 755     <para>Reduction kinds are normalization functions that transform a term
 756      to a convertible but simpler one. Each reduction kind can be used both
 757      as a tactic argument and as a stand-alone tactic.</para>
 758     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 759       <title>reduction-kind</title>
 760       <tgroup cols="4">
 761       <tbody>
 762        <row>
 763         <entry id="grammar.reduction-kind">&reduction-kind;</entry>
 764         <entry>::=</entry>
 765         <entry><emphasis role="bold">normalize</emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
 766         <entry>Computes the βδιζ-normal form. If <userinput>nodelta</userinput>
 767          is specified, δ-expansions are not performed.</entry>
 768        </row>
 769        <row>
 770         <entry/>
 771         <entry>|</entry>
 772         <entry><emphasis role="bold">whd</emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
 773         <entry>Computes the βδιζ-weak-head normal form. If <userinput>nodelta</userinput>
 774          is specified, δ-expansions are not performed.</entry>
 775        </row>
 776       </tbody>
 777      </tgroup>
 778     </table>
 779     </sect2>
 780
 781     <sect2 id="auto-params">
 782     <title>auto-params</title>
 783     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 784       <title>auto-params</title>
 785       <tgroup cols="4">
 786       <tbody>
 787        <row>
 788         <entry id="grammar.autoparams">&autoparams;</entry>
 789         <entry>::=</entry>
 790         <entry>[&nat;] [&simpleautoparam;]…
 791                [<emphasis role="bold">by</emphasis>
 792                 [&sterm;… | <emphasis role="bold">_</emphasis>]]
 793         </entry>
 794         <entry>The natural number, which defaults to 1, gives a bound to
 795         the depth of the search tree. The terms listed is the only
 796         knowledge base used by automation together with all indexed factual
 797         and equational theorems in the included library. If the list of terms
 798         is empty, only equational theorems and facts in the library are
 799         used. If the list is omitted, it defaults to all indexed theorems
 800         in the library. Finally, if the list is <command>_</command>,
 801         the automation command becomes a macro that is expanded in a new
 802         automation command where <command>_</command> is replaced with the
 803         list of theorems required to prove the sequent.
 804         </entry>
 805        </row>
 806       </tbody>
 807      </tgroup>
 808     </table>
 809     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 810       <title>simple-auto-param</title>
 811       <tgroup cols="4">
 812       <tbody>
 813        <row>
 814         <entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
 815         <entry>::=</entry>
 816         <entry><emphasis role="bold">width=&nat;</emphasis></entry>
 817         <entry>The maximal width of the search tree</entry>
 818        </row>
 819        <row>
 820         <entry/>
 821         <entry>|</entry>
 822         <entry><emphasis role="bold">size=&nat;</emphasis></entry>
 823         <entry>The maximal number of nodes in the proof</entry>
 824        </row>
 825        <row>
 826         <entry/>
 827         <entry>|</entry>
 828         <entry><emphasis role="bold">demod</emphasis></entry>
 829         <entry>Simplifies the current sequent using the current set of
 830          equations known to automation
 831         </entry>
 832        </row>
 833        <row>
 834         <entry/>
 835         <entry>|</entry>
 836         <entry><emphasis role="bold">paramod</emphasis></entry>
 837         <entry>Try to close the goal performing unit-equality paramodulation
 838         </entry>
 839        </row>
 840        <row>
 841         <entry/>
 842         <entry>|</entry>
 843         <entry><emphasis role="bold">fast_paramod</emphasis></entry>
 844         <entry>A bounded version of <command>paramod</command> that is granted to terminate quickly
 845         </entry>
 846        </row>
 847       </tbody>
 848      </tgroup>
 849     </table>
 850     </sect2>
 851
 852     <sect2 id="justification">
 853     <title>justification</title>
 854     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 855       <title>justification</title>
 856       <tgroup cols="4">
 857       <tbody>
 858        <row>
 859         <entry id="grammar.justification">&justification;</entry>
 860   <entry>::=</entry>
 861         <entry><emphasis role="bold">using</emphasis> &term;</entry>
 862         <entry>Proof term manually provided</entry>
 863        </row>
 864        <row>
 865         <entry/>
 866         <entry>|</entry>
 867         <entry>&autoparams;</entry>
 868         <entry>Call automation</entry>
 869        </row>
 870       </tbody>
 871      </tgroup>
 872     </table>
 873     </sect2>
 874   </sect1>
 875
 876 </chapter>
 877