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   <para>
  30     <table frame="all" rowsep="0" colsep="0">
  31       <title>id</title>
  32       <tgroup cols="4">
  33       <tbody>
  34        <row>
  35         <entry id="id">&id;</entry>
  36         <entry>::=</entry>
  37         <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink 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>
  38        </row>
  39       </tbody>
  40      </tgroup>
  41     </table>
  42     <table frame="all" rowsep="0" colsep="0">
  43       <title>nat</title>
  44       <tgroup cols="4">
  45       <tbody>
  46        <row>
  47         <entry id="nat">&nat;</entry>
  48         <entry>::=</entry>
  49         <entry><emphasis>〈〈any sequence of valid <ulink url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink></emphasis></entry>
  50        </row>
  51       </tbody>
  52      </tgroup>
  53     </table>
  54     <table frame="all" rowsep="0" colsep="0">
  55       <title>char</title>
  56       <tgroup cols="4">
  57       <tbody>
  58        <row>
  59         <entry id="char">&char;</entry>
  60         <entry>::=</entry>
  61         <entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
  62        </row>
  63       </tbody>
  64      </tgroup>
  65     </table>
  66     <table frame="all" rowsep="0" colsep="0">
  67       <title>uri-step</title>
  68       <tgroup cols="4">
  69       <tbody>
  70        <row>
  71         <entry id="uri-step">&uri-step;</entry>
  72         <entry>::=</entry>
  73         <entry>&char;[&char;]…</entry>
  74        </row>
  75       </tbody>
  76      </tgroup>
  77     </table>
  78     <table frame="all" rowsep="0" colsep="0">
  79       <title>uri</title>
  80       <tgroup cols="4">
  81       <tbody>
  82        <row>
  83         <entry id="uri">&uri;</entry>
  84         <entry>::=</entry>
  85         <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>
  86        </row>
  87       </tbody>
  88      </tgroup>
  89     </table>
  90   </para>
  91   </sect2>
  92   <sect2 id="terms">
  93   <title>Terms</title>
  94   <para>
  95   <table frame="all" rowsep="0" colsep="0">
  96     <title>Terms</title>
  97     <tgroup cols="4">
  98     <tbody>
  99      <row>
 100       <entry id="term">&term;</entry>
 101       <entry>::=</entry>
 102       <entry>&sterm;</entry>
 103       <entry>simple or delimited term</entry>
 104      </row>
 105      <row>
 106       <entry/>
 107       <entry>|</entry>
 108       <entry>&term; &term;</entry>
 109       <entry>application</entry>
 110      </row>
 111      <row>
 112       <entry/>
 113       <entry>|</entry>
 114       <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 115       <entry>λ-abstraction</entry>
 116      </row>
 117      <row>
 118       <entry/>
 119       <entry>|</entry>
 120       <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 121       <entry>dependent product meant to define a datatype</entry>
 122      </row>
 123      <row>
 124       <entry/>
 125       <entry>|</entry>
 126       <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 127       <entry>dependent product meant to define a proposition</entry>
 128      </row>
 129      <row>
 130       <entry/>
 131       <entry>|</entry>
 132       <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
 133       <entry>non-dependent product (logical implication or function space)</entry>
 134      </row>
 135      <row>
 136       <entry/>
 137       <entry>|</entry>
 138       <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>
 139       <entry>local definition</entry>
 140      </row>
 141      <row>
 142       <entry/>
 143       <entry>|</entry>
 144       <entry><emphasis role="bold">let</emphasis>
 145       [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
 146       &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
 147       [<emphasis role="bold">:</emphasis> &term;]
 148       <emphasis role="bold">≝</emphasis> &term;
 149       </entry>
 150       <entry>(co)recursive definitions</entry>
 151      </row>
 152      <row>
 153       <entry/>
 154       <entry/>
 155       <entry>
 156       [<emphasis role="bold">and</emphasis>
 157       [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
 158       [<emphasis role="bold">:</emphasis> &term;]
 159       <emphasis role="bold">≝</emphasis> &term;]…
 160       </entry>
 161       <entry/>
 162      </row>
 163      <row>
 164       <entry/>
 165       <entry/>
 166       <entry>
 167       <emphasis role="bold">in</emphasis> &term;
 168       </entry>
 169       <entry/>
 170      </row>
 171      <row>
 172       <entry/>
 173       <entry>|</entry>
 174       <entry>…</entry>
 175       <entry>user provided notation</entry>
 176      </row>
 177     </tbody>
 178    </tgroup>
 179   </table>
 180
 181   <table frame="all" rowsep="0" colsep="0">
 182     <title>Simple terms</title>
 183     <tgroup cols="4">
 184     <tbody>
 185      <row>
 186       <entry id="sterm">&sterm;</entry>
 187       <entry>::=</entry>
 188       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 189       <entry/>
 190      </row>
 191      <row>
 192       <entry/>
 193       <entry>|</entry>
 194       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
 195        &id;<emphasis role="bold">≔</emphasis>&term;
 196        [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
 197        <emphasis role="bold">]</emphasis>]
 198       </entry>
 199       <entry>identifier with optional explicit named substitution</entry>
 200      </row>
 201      <row>
 202       <entry/>
 203       <entry>|</entry>
 204       <entry>&uri;</entry>
 205       <entry>a qualified reference</entry>
 206      </row>
 207      <row>
 208       <entry/>
 209       <entry>|</entry>
 210       <entry><emphasis role="bold">Prop</emphasis></entry>
 211       <entry>the impredicative sort of propositions</entry>
 212      </row>
 213      <row>
 214       <entry/>
 215       <entry>|</entry>
 216       <entry><emphasis role="bold">Set</emphasis></entry>
 217       <entry>the impredicate sort of datatypes</entry>
 218      </row>
 219      <row>
 220       <entry/>
 221       <entry>|</entry>
 222       <entry><emphasis role="bold">Type</emphasis></entry>
 223       <entry>one predicative sort of datatypes</entry>
 224      </row>
 225      <row>
 226       <entry/>
 227       <entry>|</entry>
 228       <entry><emphasis role="bold">?</emphasis></entry>
 229       <entry>implicit argument</entry>
 230      </row>
 231      <row>
 232       <entry/>
 233       <entry>|</entry>
 234       <entry><emphasis role="bold">?n</emphasis>
 235       [<emphasis role="bold">[</emphasis>
 236       [<emphasis role="bold">_</emphasis>|&term;]…
 237       <emphasis role="bold">]</emphasis>]</entry>
 238       <entry>metavariable</entry>
 239      </row>
 240      <row>
 241       <entry/>
 242       <entry>|</entry>
 243         <entry><emphasis role="bold">match</emphasis> &term;
 244         [ <emphasis role="bold">in</emphasis> &term; ]
 245         [ <emphasis role="bold">return</emphasis> &term; ]
 246         <emphasis role="bold">with</emphasis>
 247       </entry>
 248       <entry>case analysis</entry>
 249      </row>
 250      <row>
 251       <entry/>
 252       <entry/>
 253       <entry>
 254        <emphasis role="bold">[</emphasis>
 255        &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 256          [
 257          <emphasis role="bold">|</emphasis>
 258          &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
 259          ]…<emphasis role="bold">]</emphasis> </entry>
 260       <entry/>
 261      </row>
 262      <row>
 263       <entry/>
 264       <entry>|</entry>
 265       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 266       <entry>cast</entry>
 267      </row>
 268      <row>
 269       <entry/>
 270       <entry>|</entry>
 271       <entry>…</entry>
 272       <entry>user provided notation at precedence 90</entry>
 273      </row>
 274     </tbody>
 275    </tgroup>
 276   </table>
 277
 278   <table frame="all" rowsep="0" colsep="0">
 279     <title>Arguments</title>
 280     <tgroup cols="4">
 281     <tbody>
 282      <row>
 283       <entry id="args">&args;</entry>
 284       <entry>::=</entry>
 285       <entry>
 286        <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
 287       </entry>
 288       <entry>ignored argument</entry>
 289      </row>
 290      <row>
 291       <entry/>
 292       <entry>|</entry>
 293       <entry>
 294        <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
 295       </entry>
 296       <entry>ignored argument</entry>
 297      </row>
 298      <row>
 299       <entry/>
 300       <entry>|</entry>
 301       <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
 302       <entry></entry>
 303      </row>
 304      <row>
 305       <entry/>
 306       <entry>|</entry>
 307       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
 308       <entry/>
 309      </row>
 310     </tbody>
 311    </tgroup>
 312   </table>
 313
 314   <table frame="all" rowsep="0" colsep="0">
 315     <title>Miscellaneous arguments</title>
 316     <tgroup cols="4">
 317     <tbody>
 318      <row>
 319       <entry id="args2">&args2;</entry>
 320       <entry>::=</entry>
 321       <entry>&id;</entry>
 322       <entry/>
 323      </row>
 324      <row>
 325       <entry/>
 326       <entry>|</entry>
 327       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
 328       <entry/>
 329      </row>
 330     </tbody>
 331    </tgroup>
 332   </table>
 333
 334   <table frame="all" rowsep="0" colsep="0">
 335     <title>Pattern matching</title>
 336     <tgroup cols="4">
 337     <tbody>
 338      <row>
 339       <entry id="match_pattern">&match_pattern;</entry>
 340       <entry>::=</entry>
 341       <entry>&id;</entry>
 342       <entry>0-ary constructor</entry>
 343      </row>
 344      <row>
 345       <entry/>
 346       <entry>|</entry>
 347       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
 348       <entry>n-ary constructor (binds the n arguments)</entry>
 349      </row>
 350     </tbody>
 351    </tgroup>
 352   </table>
 353   </para>
 354
 355   </sect2>
 356   </sect1>
 357
 358   <sect1 id="axiom_definition_declaration">
 359    <title>Definitions and declarations</title>
 360    <sect2 id="axiom">
 361     <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
 362     <titleabbrev>axiom</titleabbrev>
 363     <para><userinput>axiom H: P</userinput></para>
 364     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
 365   </sect2>
 366   <sect2 id="definition">
 367     <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 368     <titleabbrev>definition</titleabbrev>
 369     <para><userinput>definition f: T ≝ t</userinput></para>
 370     <para><command>f</command> is defined as <command>t</command>;
 371      <command>T</command> is its type. An error is raised if the type of
 372      <command>t</command> is not convertible to <command>T</command>.</para>
 373     <para><command>T</command> is inferred from <command>t</command> if
 374       omitted.</para>
 375     <para><command>t</command> can be omitted only if <command>T</command> is
 376      given. In this case Matita enters in interactive mode and
 377      <command>f</command> must be defined by means of tactics.</para>
 378     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 379   </sect2>
 380   <sect2 id="inductive">
 381     <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;]…
 382 [<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;]…]…
 383 </title>
 384     <titleabbrev>(co)inductive types declaration</titleabbrev>
 385     <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
 386     <para>Declares a family of two mutually inductive types
 387      <command>i</command> and <command>i'</command> whose types are
 388      <command>S</command> and <command>S'</command>, which must be convertible
 389      to sorts.</para>
 390     <para>The constructors <command>ki</command> of type <command>Ti</command>
 391      and <command>ki'</command> of type <command>Ti'</command> are also
 392      simultaneously declared. The declared types <command>i</command> and
 393      <command>i'</command> may occur in the types of the constructors, but
 394      only in strongly positive positions according to the rules of the
 395      calculus.</para>
 396     <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
 397     <para>If the keyword <command>coinductive</command> is used, the declared
 398      types are considered mutually coinductive.</para>
 399     <para>Elimination principles for the record are automatically generated
 400      by Matita, if allowed by the typing rules of the calculus according to
 401      the sort <command>S</command>. If generated,
 402      they are named <command>i_ind</command>, <command>i_rec</command> and
 403      <command>i_rect</command> according to the sort of their induction
 404      predicate.</para>
 405   </sect2>
 406   <sect2 id="record">
 407     <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>
 408     <titleabbrev>record</titleabbrev>
 409     <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
 410     <para>Declares a new record family <command>id</command> parameterized over
 411      <command>x,y,z</command>.</para>
 412     <para><command>S</command> is the type of the record
 413      and it must be convertible to a sort.</para>
 414     <para>Each field <command>fi</command> is declared by giving its type
 415      <command>Ti</command>. A record without any field is admitted.</para>
 416     <para>Elimination principles for the record are automatically generated
 417      by Matita, if allowed by the typing rules of the calculus according to
 418      the sort <command>S</command>. If generated,
 419      they are named <command>i_ind</command>, <command>i_rec</command> and
 420      <command>i_rect</command> according to the sort of their induction
 421      predicate.</para>
 422     <para>For each field <command>fi</command> a record projection
 423      <command>fi</command> is also automatically generated if projection
 424      is allowed by the typing rules of the calculus according to the
 425      sort <command>S</command>, the type <command>T1</command> and
 426      the definability of depending record projections.</para>
 427     <para>If the type of a field is declared with <command>:&gt;</command>,
 428      the corresponding record projection becomes an implicit coercion.
 429      This is just syntactic sugar and it has the same effect of declaring the
 430      record projection as a coercion later on.</para>
 431   </sect2>
 432   </sect1>
 433
 434   <sect1 id="proofs">
 435    <title>Proofs</title>
 436    <sect2 id="theorem">
 437     <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 438     <titleabbrev>theorem</titleabbrev>
 439     <para><userinput>theorem f: P ≝ p</userinput></para>
 440     <para>Proves a new theorem <command>f</command> whose thesis is
 441      <command>P</command>.</para>
 442     <para>If <command>p</command> is provided, it must be a proof term for
 443      <command>P</command>. Otherwise an interactive proof is started.</para>
 444     <para><command>P</command> can be omitted only if the proof is not
 445      interactive.</para>
 446     <para>Proving a theorem already proved in the library is an error.
 447      To provide an alternative name and proof for the same theorem, use
 448      <command>variant f: P ≝ p</command>.</para>
 449     <para>A warning is raised if the name of the theorem cannot be obtained
 450       by mangling the name of the constants in its thesis.</para>
 451     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 452    </sect2>
 453    <sect2 id="variant">
 454     <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 455     <titleabbrev>variant</titleabbrev>
 456     <para><userinput>variant f: T ≝ t</userinput></para>
 457     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 458      complain if the theorem has already been proved. To be used to give
 459      an alternative name or proof to a theorem.</para>
 460    </sect2>
 461    <sect2 id="lemma">
 462     <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 463     <titleabbrev>lemma</titleabbrev>
 464     <para><userinput>lemma f: T ≝ t</userinput></para>
 465     <para>Same as <command>theorem f: T ≝ t</command></para>
 466    </sect2>
 467    <sect2 id="fact">
 468     <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 469     <titleabbrev>fact</titleabbrev>
 470     <para><userinput>fact f: T ≝ t</userinput></para>
 471     <para>Same as <command>theorem f: T ≝ t</command></para>
 472    </sect2>
 473    <sect2 id="remark">
 474     <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 475     <titleabbrev>remark</titleabbrev>
 476     <para><userinput>remark f: T ≝ t</userinput></para>
 477     <para>Same as <command>theorem f: T ≝ t</command></para>
 478    </sect2>
 479   </sect1>
 480
 481   <sect1 id="tacticargs">
 482    <title>Tactic arguments</title>
 483    <para>This section documents the syntax of some recurring arguments for
 484     tactics.</para>
 485
 486     <sect2 id="introsspec">
 487     <title>intros-spec</title>
 488     <table frame="all" rowsep="0" colsep="0">
 489       <title>intros-spec</title>
 490       <tgroup cols="4">
 491       <tbody>
 492        <row>
 493         <entry id="intros-spec">&intros-spec;</entry>
 494         <entry>::=</entry>
 495         <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
 496        </row>
 497       </tbody>
 498      </tgroup>
 499     </table>
 500         <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>
 501     </sect2>
 502
 503     <sect2 id="pattern">
 504     <title>pattern</title>
 505     <table frame="all" rowsep="0" colsep="0">
 506       <title>pattern</title>
 507       <tgroup cols="4">
 508       <tbody>
 509        <row>
 510         <entry id="pattern">&pattern;</entry>
 511         <entry>::=</entry>
 512         <entry>&TODO;</entry>
 513        </row>
 514       </tbody>
 515      </tgroup>
 516     </table>
 517         <para>&TODO;</para>
 518     </sect2>
 519
 520     <sect2 id="reduction-kind">
 521     <title>reduction-kind</title>
 522     <para>Reduction kinds are normalization functions that transform a term
 523      to a convertible but simpler one. Each reduction kind can be used both
 524      as a tactic argument and as a stand-alone tactic.</para>
 525     <table frame="all" rowsep="0" colsep="0">
 526       <title>reduction-kind</title>
 527       <tgroup cols="4">
 528       <tbody>
 529        <row>
 530         <entry id="reduction-kind">&reduction-kind;</entry>
 531         <entry>::=</entry>
 532         <entry><emphasis role="bold">demodulate</emphasis></entry>
 533        </row>
 534        <row>
 535         <entry/>
 536         <entry>|</entry>
 537         <entry><emphasis role="bold">normalize</emphasis></entry>
 538         <entry>Computes the βδιζ-normal form</entry>
 539        </row>
 540        <row>
 541         <entry/>
 542         <entry>|</entry>
 543         <entry><emphasis role="bold">reduce</emphasis></entry>
 544         <entry>Computes the βδιζ-normal form</entry>
 545        </row>
 546        <row>
 547         <entry/>
 548         <entry>|</entry>
 549         <entry><emphasis role="bold">simplify</emphasis></entry>
 550         <entry>Computes a form supposed to be simpler</entry>
 551        </row>
 552        <row>
 553         <entry/>
 554         <entry>|</entry>
 555         <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
 556         <entry>δ-reduces the constant or variable specified, or that
 557          in head position if none is specified</entry>
 558        </row>
 559        <row>
 560         <entry/>
 561         <entry>|</entry>
 562         <entry><emphasis role="bold">whd</emphasis></entry>
 563         <entry>Computes the βδιζ-weak-head normal form</entry>
 564        </row>
 565       </tbody>
 566      </tgroup>
 567     </table>
 568     </sect2>
 569   </sect1>
 570
 571 </chapter>
 572