helm/software/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     <para>Proving a theorem already proved in the library is an error.
 528      To provide an alternative name and proof for the same theorem, use
 529      <command>variant f: P ≝ p</command>.</para>
 530     <para>A warning is raised if the name of the theorem cannot be obtained
 531       by mangling the name of the constants in its thesis.</para>
 532     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 533    </sect2>
 534    <sect2 id="variant">
 535     <title><emphasis role="bold">variant</emphasis> &id;<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> &term;</title>
 536     <titleabbrev>variant</titleabbrev>
 537     <para><userinput>variant f: T ≝ t</userinput></para>
 538     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 539      complain if the theorem has already been proved. To be used to give
 540      an alternative name or proof to a theorem.</para>
 541    </sect2>
 542    <sect2 id="lemma">
 543     <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 544     <titleabbrev>lemma</titleabbrev>
 545     <para><userinput>lemma f: T ≝ t</userinput></para>
 546     <para>Same as <command>theorem f: T ≝ t</command></para>
 547    </sect2>
 548    <sect2 id="fact">
 549     <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 550     <titleabbrev>fact</titleabbrev>
 551     <para><userinput>fact f: T ≝ t</userinput></para>
 552     <para>Same as <command>theorem f: T ≝ t</command></para>
 553    </sect2>
 554    <sect2 id="remark">
 555     <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 556     <titleabbrev>remark</titleabbrev>
 557     <para><userinput>remark f: T ≝ t</userinput></para>
 558     <para>Same as <command>theorem f: T ≝ t</command></para>
 559    </sect2>
 560   </sect1>
 561
 562   <sect1 id="tacticargs">
 563    <title>Tactic arguments</title>
 564    <para>This section documents the syntax of some recurring arguments for
 565     tactics.</para>
 566
 567     <sect2 id="introsspec">
 568     <title>intros-spec</title>
 569     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 570       <title>intros-spec</title>
 571       <tgroup cols="4">
 572       <tbody>
 573        <row>
 574         <entry id="grammar.intros-spec">&intros-spec;</entry>
 575         <entry>::=</entry>
 576         <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
 577        </row>
 578       </tbody>
 579      </tgroup>
 580     </table>
 581         <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>
 582     </sect2>
 583
 584     <sect2 id="pattern">
 585     <title>pattern</title>
 586     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 587       <title>pattern</title>
 588       <tgroup cols="4">
 589       <tbody>
 590        <row>
 591         <entry id="grammar.pattern">&pattern;</entry>
 592         <entry>::=</entry>
 593         <entry><emphasis role="bold">in</emphasis>
 594           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
 595           [<emphasis role="bold">⊢</emphasis> &path;]]</entry>
 596         <entry>simple pattern</entry>
 597        </row>
 598        <row>
 599         <entry/>
 600         <entry>|</entry>
 601         <entry><emphasis role="bold">in match</emphasis> &path;
 602           [<emphasis role="bold">in</emphasis>
 603           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
 604           [<emphasis role="bold">⊢</emphasis> &path;]]</entry>
 605         <entry>full pattern</entry>
 606        </row>
 607       </tbody>
 608      </tgroup>
 609     </table>
 610     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 611       <title>path</title>
 612       <tgroup cols="4">
 613       <tbody>
 614        <row>
 615         <entry id="grammar.path">&path;</entry>
 616         <entry>::=</entry>
 617         <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>
 618        </row>
 619       </tbody>
 620      </tgroup>
 621     </table>
 622     <para>A <emphasis>path</emphasis> locates zero or more subterms of a given term by mimicking the term structure up to:</para>
 623     <orderedlist>
 624       <listitem><para>Occurrences of the subterms to locate that are
 625        represented by <emphasis role="bold">%</emphasis>.</para></listitem>
 626       <listitem><para>Subterms without any occurrence of subterms to locate
 627        that can be represented by <emphasis role="bold">?</emphasis>.
 628        </para></listitem>
 629     </orderedlist>
 630     <para>Warning: the format for a path for a <emphasis role="bold">match</emphasis> … <emphasis role="bold">with</emphasis>
 631      expression is restricted to: <emphasis role="bold">match</emphasis> &path;
 632      <emphasis role="bold">with</emphasis>
 633      <emphasis role="bold">[</emphasis>
 634      <emphasis role="bold">_</emphasis>
 635      <emphasis role="bold">⇒</emphasis>
 636      &path;
 637      <emphasis role="bold">|</emphasis> …
 638      <emphasis role="bold">|</emphasis>
 639      <emphasis role="bold">_</emphasis>
 640      <emphasis role="bold">⇒</emphasis>
 641      &path;
 642      <emphasis role="bold">]</emphasis>
 643      Its semantics is the following: the n-th
 644      &quot;<emphasis role="bold">_</emphasis>
 645      <emphasis role="bold">⇒</emphasis>
 646      &path;&quot; branch is matched against the n-th constructor of the
 647      inductive data type. The head λ-abstractions of &path; are matched
 648      against the corresponding constructor arguments.
 649     </para>
 650     <para>For instance, the path
 651       <userinput>∀_,_:?.(? ? % ?)→(? ? ? %)</userinput>
 652        locates at once the subterms
 653       <userinput>x+y</userinput> and <userinput>x*y</userinput> in the
 654       term <userinput>∀x,y:nat.x+y=1→0=x*y</userinput>
 655       (where the notation <userinput>A=B</userinput> hides the term
 656       <userinput>(eq T A B)</userinput> for some type <userinput>T</userinput>).
 657     </para>
 658     <para>A <emphasis>simple pattern</emphasis> extends paths to locate
 659      subterms in a whole sequent. In particular, the pattern
 660      <userinput>in H: p  K: q ⊢ r</userinput> locates at once all the subterms
 661      located by the pattern <userinput>r</userinput> in the conclusion of the
 662      sequent and by the patterns <userinput>p</userinput> and
 663      <userinput>q</userinput> in the hypotheses <userinput>H</userinput>
 664      and <userinput>K</userinput> of the sequent.
 665     </para>
 666     <para>If no list of hypotheses is provided in a simple pattern, no subterm
 667      is selected in the hypothesis. If the <userinput>⊢ p</userinput>
 668      part of the pattern is not provided, no subterm will be matched in the
 669      conclusion if at least one hypothesis is provided; otherwise the whole
 670      conclusion is selected.
 671     </para>
 672     <para>Finally, a <emphasis>full pattern</emphasis> is interpreted in three
 673      steps. In the first step the <userinput>match T in</userinput>
 674      part is ignored and a set <emphasis>S</emphasis> of subterms is
 675      located as for the case of
 676      simple patterns. In the second step the term <userinput>T</userinput>
 677      is parsed and interpreted in the context of each subterm
 678      <emphasis>s ∈ S</emphasis>. In the last term for each
 679      <emphasis>s ∈ S</emphasis> the interpreted term <userinput>T</userinput>
 680      computed in the previous step is looked for. The final set of subterms
 681      located by the full pattern is the set of occurrences of
 682      the interpreted <userinput>T</userinput> in the subterms <emphasis>s</emphasis>.
 683     </para>
 684     <para>A full pattern can always be replaced by a simple pattern,
 685       often at the cost of increased verbosity or decreased readability.</para>
 686     <para>Example: the pattern
 687       <userinput>⊢ in match x+y in ∀_,_:?.(? ? % ?)</userinput>
 688       locates only the first occurrence of <userinput>x+y</userinput>
 689       in the sequent <userinput>x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) =
 690       z * (x+y) + w * (x+y)</userinput>. The corresponding simple pattern
 691       is <userinput>⊢ ∀_,_:?.(? ? (? % ?) ?)</userinput>.
 692     </para>
 693     <para>Every tactic that acts on subterms of the selected sequents have
 694      a pattern argument for uniformity. To automatically generate a simple
 695      pattern:</para>
 696     <orderedlist>
 697      <listitem><para>Select in the current goal the subterms to pass to the
 698       tactic by using the mouse. In order to perform a multiple selection of
 699       subterms, hold the Ctrl key while selecting every subterm after the
 700       first one.</para></listitem>
 701      <listitem><para>From the contextual menu select &quot;Copy&quot;.</para></listitem>
 702      <listitem><para>From the &quot;Edit&quot; or the contextual menu select
 703       &quot;Paste as pattern&quot;</para></listitem>
 704     </orderedlist>
 705     </sect2>
 706
 707     <sect2 id="reduction-kind">
 708     <title>reduction-kind</title>
 709     <para>Reduction kinds are normalization functions that transform a term
 710      to a convertible but simpler one. Each reduction kind can be used both
 711      as a tactic argument and as a stand-alone tactic.</para>
 712     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 713       <title>reduction-kind</title>
 714       <tgroup cols="4">
 715       <tbody>
 716        <row>
 717         <entry id="grammar.reduction-kind">&reduction-kind;</entry>
 718         <entry>::=</entry>
 719         <entry><emphasis role="bold">normalize</emphasis></entry>
 720         <entry>Computes the βδιζ-normal form</entry>
 721        </row>
 722        <row>
 723         <entry/>
 724         <entry>|</entry>
 725         <entry><emphasis role="bold">simplify</emphasis></entry>
 726         <entry>Computes a form supposed to be simpler</entry>
 727        </row>
 728        <row>
 729         <entry/>
 730         <entry>|</entry>
 731         <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
 732         <entry>δ-reduces the constant or variable if specified, or that
 733          in head position</entry>
 734        </row>
 735        <row>
 736         <entry/>
 737         <entry>|</entry>
 738         <entry><emphasis role="bold">whd</emphasis></entry>
 739         <entry>Computes the βδιζ-weak-head normal form</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>[&simpleautoparam;]…
 756                [<emphasis role="bold">by</emphasis>
 757                 &term; [,&term;]…]
 758         </entry>
 759        </row>
 760       </tbody>
 761      </tgroup>
 762     </table>
 763     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 764       <title>simple-auto-param</title>
 765       <tgroup cols="4">
 766       <tbody>
 767        <row>
 768         <entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
 769         <entry>::=</entry>
 770         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
 771         <entry>Give a bound to the depth of the search tree</entry>
 772        </row>
 773        <row>
 774         <entry/>
 775         <entry>|</entry>
 776         <entry><emphasis role="bold">width=&nat;</emphasis></entry>
 777         <entry>The maximal width of the search tree</entry>
 778        </row>
 779        <row>
 780         <entry/>
 781         <entry>|</entry>
 782         <entry><emphasis role="bold">library</emphasis></entry>
 783         <entry>Search everywhere (not only in included files)</entry>
 784        </row>
 785        <row>
 786         <entry/>
 787         <entry>|</entry>
 788         <entry><emphasis role="bold">type</emphasis></entry>
 789         <entry>Try to close also goals of sort Type, otherwise only goals
 790                living in sort Prop are attacked.
 791         </entry>
 792        </row>
 793        <row>
 794         <entry/>
 795         <entry>|</entry>
 796         <entry><emphasis role="bold">paramodulation</emphasis></entry>
 797         <entry>Try to close the goal performing unit-equality paramodulation
 798         </entry>
 799        </row>
 800        <row>
 801         <entry/>
 802         <entry>|</entry>
 803         <entry><emphasis role="bold">size=&nat;</emphasis></entry>
 804         <entry>The maximal number of nodes in the proof</entry>
 805        </row>
 806        <row>
 807         <entry/>
 808         <entry>|</entry>
 809         <entry><emphasis role="bold">timeout=&nat;</emphasis></entry>
 810         <entry>Timeout in seconds
 811         </entry>
 812        </row>
 813       </tbody>
 814      </tgroup>
 815     </table>
 816     </sect2>
 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   </sect1>
 841
 842 </chapter>
 843