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="letrec">
 457     <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
 458     <titleabbrev>&TODO;</titleabbrev>
 459     <para>&TODO;</para>
 460   </sect2>
 461   <sect2 id="inductive">
 462     <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;]…
 463 [<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;]…]…
 464 </title>
 465     <titleabbrev>(co)inductive types declaration</titleabbrev>
 466     <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
 467     <para>Declares a family of two mutually inductive types
 468      <command>i</command> and <command>i'</command> whose types are
 469      <command>S</command> and <command>S'</command>, which must be convertible
 470      to sorts.</para>
 471     <para>The constructors <command>ki</command> of type <command>Ti</command>
 472      and <command>ki'</command> of type <command>Ti'</command> are also
 473      simultaneously declared. The declared types <command>i</command> and
 474      <command>i'</command> may occur in the types of the constructors, but
 475      only in strongly positive positions according to the rules of the
 476      calculus.</para>
 477     <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
 478     <para>If the keyword <command>coinductive</command> is used, the declared
 479      types are considered mutually coinductive.</para>
 480     <para>Elimination principles for the record are automatically generated
 481      by Matita, if allowed by the typing rules of the calculus according to
 482      the sort <command>S</command>. If generated,
 483      they are named <command>i_ind</command>, <command>i_rec</command> and
 484      <command>i_rect</command> according to the sort of their induction
 485      predicate.</para>
 486   </sect2>
 487   <sect2 id="record">
 488     <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>
 489     <titleabbrev>record</titleabbrev>
 490     <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
 491     <para>Declares a new record family <command>id</command> parameterized over
 492      <command>x,y,z</command>.</para>
 493     <para><command>S</command> is the type of the record
 494      and it must be convertible to a sort.</para>
 495     <para>Each field <command>fi</command> is declared by giving its type
 496      <command>Ti</command>. A record without any field is admitted.</para>
 497     <para>Elimination principles for the record are automatically generated
 498      by Matita, if allowed by the typing rules of the calculus according to
 499      the sort <command>S</command>. If generated,
 500      they are named <command>i_ind</command>, <command>i_rec</command> and
 501      <command>i_rect</command> according to the sort of their induction
 502      predicate.</para>
 503     <para>For each field <command>fi</command> a record projection
 504      <command>fi</command> is also automatically generated if projection
 505      is allowed by the typing rules of the calculus according to the
 506      sort <command>S</command>, the type <command>T1</command> and
 507      the definability of depending record projections.</para>
 508     <para>If the type of a field is declared with <command>:&gt;</command>,
 509      the corresponding record projection becomes an implicit coercion.
 510      This is just syntactic sugar and it has the same effect of declaring the
 511      record projection as a coercion later on.</para>
 512   </sect2>
 513   </sect1>
 514
 515   <sect1 id="proofs">
 516    <title>Proofs</title>
 517    <sect2 id="theorem">
 518     <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 519     <titleabbrev>theorem</titleabbrev>
 520     <para><userinput>theorem f: P ≝ p</userinput></para>
 521     <para>Proves a new theorem <command>f</command> whose thesis is
 522      <command>P</command>.</para>
 523     <para>If <command>p</command> is provided, it must be a proof term for
 524      <command>P</command>. Otherwise an interactive proof is started.</para>
 525     <para><command>P</command> can be omitted only if the proof is not
 526      interactive.</para>
 527      <!--
 528     <para>Proving a theorem already proved in the library is an error.
 529      To provide an alternative name and proof for the same theorem, use
 530      <command>variant f: P ≝ p</command>.</para>-->
 531     <para>A warning is raised if the name of the theorem cannot be obtained
 532       by mangling the name of the constants in its thesis.</para>
 533     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 534    </sect2>
 535    <!--
 536    <sect2 id="variant">
 537     <title><emphasis role="bold">variant</emphasis> &id;<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> &term;</title>
 538     <titleabbrev>variant</titleabbrev>
 539     <para><userinput>variant f: T ≝ t</userinput></para>
 540     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 541      complain if the theorem has already been proved. To be used to give
 542      an alternative name or proof to a theorem.</para>
 543    </sect2>-->
 544    <sect2 id="corollary">
 545     <title><emphasis role="bold">corollary</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 546     <titleabbrev>corollary</titleabbrev>
 547     <para><userinput>corollary f: T ≝ t</userinput></para>
 548     <para>Same as <command>theorem f: T ≝ t</command></para>
 549    </sect2>
 550    <sect2 id="lemma">
 551     <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 552     <titleabbrev>lemma</titleabbrev>
 553     <para><userinput>lemma f: T ≝ t</userinput></para>
 554     <para>Same as <command>theorem f: T ≝ t</command></para>
 555    </sect2>
 556    <sect2 id="fact">
 557     <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 558     <titleabbrev>fact</titleabbrev>
 559     <para><userinput>fact f: T ≝ t</userinput></para>
 560     <para>Same as <command>theorem f: T ≝ t</command></para>
 561    </sect2>
 562    <sect2 id="example">
 563     <title><emphasis role="bold">example</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 564     <titleabbrev>example</titleabbrev>
 565     <para><userinput>example f: T ≝ t</userinput></para>
 566     <para>Same as <command>theorem f: T ≝ t</command>, but the example
 567      is not indexed nor used by automation.</para>
 568    </sect2>
 569   </sect1>
 570
 571   <sect1 id="tacticargs">
 572    <title>Tactic arguments</title>
 573    <para>This section documents the syntax of some recurring arguments for
 574     tactics.</para>
 575
 576     <!--
 577     <sect2 id="introsspec">
 578     <title>intros-spec</title>
 579     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 580       <title>intros-spec</title>
 581       <tgroup cols="4">
 582       <tbody>
 583        <row>
 584         <entry id="grammar.intros-spec">&intros-spec;</entry>
 585         <entry>::=</entry>
 586         <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
 587        </row>
 588       </tbody>
 589      </tgroup>
 590     </table>
 591         <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>
 592     </sect2>
 593     -->
 594
 595     <sect2 id="pattern">
 596     <title>pattern</title>
 597     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 598       <title>pattern</title>
 599       <tgroup cols="4">
 600       <tbody>
 601        <row>
 602         <entry id="grammar.pattern">&pattern;</entry>
 603         <entry>::=</entry>
 604         <entry><emphasis role="bold">{</emphasis>
 605           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
 606           [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
 607         <entry>simple pattern</entry>
 608        </row>
 609        <row>
 610         <entry/>
 611         <entry>|</entry>
 612         <entry><emphasis role="bold">{match</emphasis> &path;
 613           [<emphasis role="bold">in</emphasis>
 614           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
 615           [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
 616         <entry>full pattern</entry>
 617        </row>
 618       </tbody>
 619      </tgroup>
 620     </table>
 621     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 622       <title>path</title>
 623       <tgroup cols="4">
 624       <tbody>
 625        <row>
 626         <entry id="grammar.path">&path;</entry>
 627         <entry>::=</entry>
 628         <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>
 629        </row>
 630       </tbody>
 631      </tgroup>
 632     </table>
 633     <para>A <emphasis>path</emphasis> locates zero or more subterms of a given term by mimicking the term structure up to:</para>
 634     <orderedlist>
 635       <listitem><para>Occurrences of the subterms to locate that are
 636        represented by <emphasis role="bold">%</emphasis>.</para></listitem>
 637       <listitem><para>Subterms without any occurrence of subterms to locate
 638        that can be represented by <emphasis role="bold">?</emphasis>.
 639        </para></listitem>
 640     </orderedlist>
 641     <para>Warning: the format for a path for a <emphasis role="bold">match</emphasis> … <emphasis role="bold">with</emphasis>
 642      expression is restricted to: <emphasis role="bold">match</emphasis> &path;
 643      <emphasis role="bold">with</emphasis>
 644      <emphasis role="bold">[</emphasis>
 645      <emphasis role="bold">_</emphasis>
 646      <emphasis role="bold">⇒</emphasis>
 647      &path;
 648      <emphasis role="bold">|</emphasis> …
 649      <emphasis role="bold">|</emphasis>
 650      <emphasis role="bold">_</emphasis>
 651      <emphasis role="bold">⇒</emphasis>
 652      &path;
 653      <emphasis role="bold">]</emphasis>
 654      Its semantics is the following: the n-th
 655      &quot;<emphasis role="bold">_</emphasis>
 656      <emphasis role="bold">⇒</emphasis>
 657      &path;&quot; branch is matched against the n-th constructor of the
 658      inductive data type. The head λ-abstractions of &path; are matched
 659      against the corresponding constructor arguments.
 660     </para>
 661     <para>For instance, the path
 662       <userinput>∀_,_:?.(? ? % ?)→(? ? ? %)</userinput>
 663        locates at once the subterms
 664       <userinput>x+y</userinput> and <userinput>x*y</userinput> in the
 665       term <userinput>∀x,y:nat.x+y=1→0=x*y</userinput>
 666       (where the notation <userinput>A=B</userinput> hides the term
 667       <userinput>(eq T A B)</userinput> for some type <userinput>T</userinput>).
 668     </para>
 669     <para>A <emphasis>simple pattern</emphasis> extends paths to locate
 670      subterms in a whole sequent. In particular, the pattern
 671      <userinput>{ H: p  K: q ⊢ r }</userinput> locates at once all the subterms
 672      located by the pattern <userinput>r</userinput> in the conclusion of the
 673      sequent and by the patterns <userinput>p</userinput> and
 674      <userinput>q</userinput> in the hypotheses <userinput>H</userinput>
 675      and <userinput>K</userinput> of the sequent.
 676     </para>
 677     <para>If no list of hypotheses is provided in a simple pattern, no subterm
 678      is selected in the hypothesis. If the <userinput>⊢ p</userinput>
 679      part of the pattern is not provided, no subterm will be matched in the
 680      conclusion if at least one hypothesis is provided; otherwise the whole
 681      conclusion is selected.
 682     </para>
 683     <para>Finally, a <emphasis>full pattern</emphasis> is interpreted in three
 684      steps. In the first step the <userinput>match T in</userinput>
 685      part is ignored and a set <emphasis>S</emphasis> of subterms is
 686      located as for the case of
 687      simple patterns. In the second step the term <userinput>T</userinput>
 688      is parsed and interpreted in the context of each subterm
 689      <emphasis>s ∈ S</emphasis>. In the last term for each
 690      <emphasis>s ∈ S</emphasis> the interpreted term <userinput>T</userinput>
 691      computed in the previous step is looked for. The final set of subterms
 692      located by the full pattern is the set of occurrences of
 693      the interpreted <userinput>T</userinput> in the subterms <emphasis>s</emphasis>.
 694     </para>
 695     <para>A full pattern can always be replaced by a simple pattern,
 696       often at the cost of increased verbosity or decreased readability.</para>
 697     <para>Example: the pattern
 698       <userinput>{ match x+y in ⊢ ∀_,_:?.(? ? % ?) }</userinput>
 699       locates only the first occurrence of <userinput>x+y</userinput>
 700       in the sequent <userinput>x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) =
 701       z * (x+y) + w * (x+y)</userinput>. The corresponding simple pattern
 702       is <userinput>{ ⊢ ∀_,_:?.(? ? (? % ?) ?) }</userinput>.
 703     </para>
 704     <para>Every tactic that acts on subterms of the selected sequents have
 705      a pattern argument for uniformity. To automatically generate a simple
 706      pattern:</para>
 707     <orderedlist>
 708      <listitem><para>Select in the current goal the subterms to pass to the
 709       tactic by using the mouse. In order to perform a multiple selection of
 710       subterms, hold the Ctrl key while selecting every subterm after the
 711       first one.</para></listitem>
 712      <listitem><para>From the contextual menu select &quot;Copy&quot;.</para></listitem>
 713      <listitem><para>From the &quot;Edit&quot; or the contextual menu select
 714       &quot;Paste as pattern&quot;</para></listitem>
 715     </orderedlist>
 716     </sect2>
 717
 718     <sect2 id="reduction-kind">
 719     <title>reduction-kind</title>
 720     <para>Reduction kinds are normalization functions that transform a term
 721      to a convertible but simpler one. Each reduction kind can be used both
 722      as a tactic argument and as a stand-alone tactic.</para>
 723     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 724       <title>reduction-kind</title>
 725       <tgroup cols="4">
 726       <tbody>
 727        <row>
 728         <entry id="grammar.reduction-kind">&reduction-kind;</entry>
 729         <entry>::=</entry>
 730         <entry><emphasis role="bold">normalize</emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
 731         <entry>Computes the βδιζ-normal form. If <userinput>nodelta</userinput>
 732          is specified, δ-expansions are not performed.</entry>
 733        </row>
 734        <row>
 735         <entry/>
 736         <entry>|</entry>
 737         <entry><emphasis role="bold">whd</emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
 738         <entry>Computes the βδιζ-weak-head normal form. If <userinput>nodelta</userinput>
 739          is specified, δ-expansions are not performed.</entry>
 740        </row>
 741       </tbody>
 742      </tgroup>
 743     </table>
 744     </sect2>
 745
 746     <sect2 id="auto-params">
 747     <title>auto-params</title>
 748     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 749       <title>auto-params</title>
 750       <tgroup cols="4">
 751       <tbody>
 752        <row>
 753         <entry id="grammar.autoparams">&autoparams;</entry>
 754         <entry>::=</entry>
 755         <entry>[&nat;] [&simpleautoparam;]…
 756                [<emphasis role="bold">by</emphasis>
 757                 [&sterm;… | <emphasis role="bold">_</emphasis>]]
 758         </entry>
 759         <entry>The natural number, which defaults to 1, gives a bound to
 760         the depth of the search tree. The terms listed is the only
 761         knowledge base used by automation together with all indexed factual
 762         and equational theorems in the included library. If the list of terms
 763         is empty, only equational theorems and facts in the library are
 764         used. If the list is omitted, it defaults to all indexed theorems
 765         in the library. Finally, if the list is <command>_</command>,
 766         the automation command becomes a macro that is expanded in a new
 767         automation command where <command>_</command> is replaced with the
 768         list of theorems required to prove the sequent.
 769         </entry>
 770        </row>
 771       </tbody>
 772      </tgroup>
 773     </table>
 774     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 775       <title>simple-auto-param</title>
 776       <tgroup cols="4">
 777       <tbody>
 778        <row>
 779         <entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
 780         <entry>::=</entry>
 781         <entry><emphasis role="bold">width=&nat;</emphasis></entry>
 782         <entry>The maximal width of the search tree</entry>
 783        </row>
 784        <row>
 785         <entry/>
 786         <entry>|</entry>
 787         <entry><emphasis role="bold">size=&nat;</emphasis></entry>
 788         <entry>The maximal number of nodes in the proof</entry>
 789        </row>
 790        <row>
 791         <entry/>
 792         <entry>|</entry>
 793         <entry><emphasis role="bold">demod</emphasis></entry>
 794         <entry>Simplifies the current sequent using the current set of
 795          equations known to automation
 796         </entry>
 797        </row>
 798        <row>
 799         <entry/>
 800         <entry>|</entry>
 801         <entry><emphasis role="bold">paramod</emphasis></entry>
 802         <entry>Try to close the goal performing unit-equality paramodulation
 803         </entry>
 804        </row>
 805        <row>
 806         <entry/>
 807         <entry>|</entry>
 808         <entry><emphasis role="bold">fast_paramod</emphasis></entry>
 809         <entry>A bounded version of <command>paramod</command> that is granted to terminate quickly
 810         </entry>
 811        </row>
 812       </tbody>
 813      </tgroup>
 814     </table>
 815     </sect2>
 816
 817     <!--
 818     <sect2 id="justification">
 819     <title>justification</title>
 820     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 821       <title>justification</title>
 822       <tgroup cols="4">
 823       <tbody>
 824        <row>
 825         <entry id="grammar.justification">&justification;</entry>
 826   <entry>::=</entry>
 827         <entry><emphasis role="bold">using</emphasis> &term;</entry>
 828         <entry>Proof term manually provided</entry>
 829        </row>
 830        <row>
 831         <entry/>
 832         <entry>|</entry>
 833         <entry>&autoparams;</entry>
 834         <entry>Call automation</entry>
 835        </row>
 836       </tbody>
 837      </tgroup>
 838     </table>
 839     </sect2>
 840     -->
 841   </sect1>
 842
 843 </chapter>
 844