2 <!-- =========== Terms, declarations and definitions ============ -->
4 <chapter id="sec_terms">
6 <para>To describe syntax in this manual we use the following conventions:</para>
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"><</emphasis>|<emphasis role="bold">></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>
25 <sect1 id="terms_and_co">
26 <title>Terms & co.</title>
28 <title>Lexical conventions</title>
29 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
34 <entry id="grammar.id">&id;</entry>
36 <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>
41 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
46 <entry id="grammar.nat">&nat;</entry>
48 <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>
53 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
58 <entry id="grammar.char">&char;</entry>
60 <entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
65 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
66 <title>uri-step</title>
70 <entry id="grammar.uri-step">&uri-step;</entry>
72 <entry>&char;[&char;]…</entry>
77 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
82 <entry id="grammar.uri">&uri;</entry>
84 <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>
93 <!-- ZACK: Sample EBNF snippet, see:
94 http://www.docbook.org/tdg/en/html/productionset.html -->
98 <production id="grammar.term">
101 <lineannotation></lineannotation>
107 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
112 <entry id="grammar.term">&term;</entry>
114 <entry>&sterm;</entry>
115 <entry>simple or delimited term</entry>
120 <entry>&term; &term;</entry>
121 <entry>application</entry>
126 <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
127 <entry>λ-abstraction</entry>
132 <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
133 <entry>dependent product meant to define a datatype</entry>
138 <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
139 <entry>dependent product meant to define a proposition</entry>
144 <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
145 <entry>non-dependent product (logical implication or function space)</entry>
150 <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>
151 <entry>local definition</entry>
157 <emphasis role="bold">let</emphasis>
158 [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
161 <entry>(co)recursive definitions</entry>
167 [<emphasis role="bold">and</emphasis> &rec_def;]…
175 <emphasis role="bold">in</emphasis> &term;
183 <entry>user provided notation</entry>
186 <entry id="grammar.rec_def">&rec_def;</entry>
189 &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
197 [<emphasis role="bold">on</emphasis> &nat;]
198 [<emphasis role="bold">:</emphasis> &term;]
199 <emphasis role="bold">≝</emphasis> &term;]
207 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
208 <title>Simple terms</title>
212 <entry id="grammar.sterm">&sterm;</entry>
214 <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
220 <entry>&id;[<emphasis role="bold">\subst[</emphasis>
221 &id;<emphasis role="bold">≔</emphasis>&term;
222 [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
223 <emphasis role="bold">]</emphasis>]
225 <entry>identifier with optional explicit named substitution</entry>
231 <entry>a qualified reference</entry>
236 <entry><emphasis role="bold">Prop</emphasis></entry>
237 <entry>the impredicative sort of propositions</entry>
242 <entry><emphasis role="bold">Set</emphasis></entry>
243 <entry>the impredicate sort of datatypes</entry>
248 <entry><emphasis role="bold">Type</emphasis></entry>
249 <entry>one predicative sort of datatypes</entry>
254 <entry><emphasis role="bold">?</emphasis></entry>
255 <entry>implicit argument</entry>
260 <entry><emphasis role="bold">?n</emphasis>
261 [<emphasis role="bold">[</emphasis>
262 [<emphasis role="bold">_</emphasis>|&term;]…
263 <emphasis role="bold">]</emphasis>]</entry>
264 <entry>metavariable</entry>
269 <entry><emphasis role="bold">match</emphasis> &term;
270 [ <emphasis role="bold">in</emphasis> &term; ]
271 [ <emphasis role="bold">return</emphasis> &term; ]
272 <emphasis role="bold">with</emphasis>
274 <entry>case analysis</entry>
280 <emphasis role="bold">[</emphasis>
281 &match_branch;[<emphasis role="bold">|</emphasis>&match_branch;]…
282 <emphasis role="bold">]</emphasis>
289 <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
296 <entry>user provided notation at precedence 90</entry>
302 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
303 <title>Arguments</title>
307 <entry id="grammar.args">&args;</entry>
310 <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
312 <entry>ignored argument</entry>
318 <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
320 <entry>ignored argument</entry>
325 <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
331 <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
335 <entry id="grammar.args2">&args2;</entry>
343 <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
350 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
351 <title>Pattern matching</title>
355 <entry id="grammar.match_branch">&match_branch;</entry>
357 <entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
361 <entry id="grammar.match_pattern">&match_pattern;</entry>
364 <entry>0-ary constructor</entry>
369 <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
370 <entry>n-ary constructor (binds the n arguments)</entry>
380 <sect1 id="axiom_definition_declaration">
381 <title>Definitions and declarations</title>
383 <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
384 <titleabbrev>axiom</titleabbrev>
385 <para><userinput>axiom H: P</userinput></para>
386 <para><command>H</command> is declared as an axiom that states <command>P</command></para>
388 <sect2 id="definition">
389 <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
390 <titleabbrev>definition</titleabbrev>
391 <para><userinput>definition f: T ≝ t</userinput></para>
392 <para><command>f</command> is defined as <command>t</command>;
393 <command>T</command> is its type. An error is raised if the type of
394 <command>t</command> is not convertible to <command>T</command>.</para>
395 <para><command>T</command> is inferred from <command>t</command> if
397 <para><command>t</command> can be omitted only if <command>T</command> is
398 given. In this case Matita enters in interactive mode and
399 <command>f</command> must be defined by means of tactics.</para>
400 <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
402 <sect2 id="inductive">
403 <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;]…
404 [<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;]…]…
406 <titleabbrev>(co)inductive types declaration</titleabbrev>
407 <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
408 <para>Declares a family of two mutually inductive types
409 <command>i</command> and <command>i'</command> whose types are
410 <command>S</command> and <command>S'</command>, which must be convertible
412 <para>The constructors <command>ki</command> of type <command>Ti</command>
413 and <command>ki'</command> of type <command>Ti'</command> are also
414 simultaneously declared. The declared types <command>i</command> and
415 <command>i'</command> may occur in the types of the constructors, but
416 only in strongly positive positions according to the rules of the
418 <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
419 <para>If the keyword <command>coinductive</command> is used, the declared
420 types are considered mutually coinductive.</para>
421 <para>Elimination principles for the record are automatically generated
422 by Matita, if allowed by the typing rules of the calculus according to
423 the sort <command>S</command>. If generated,
424 they are named <command>i_ind</command>, <command>i_rec</command> and
425 <command>i_rect</command> according to the sort of their induction
429 <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">:></emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>
430 <titleabbrev>record</titleabbrev>
431 <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
432 <para>Declares a new record family <command>id</command> parameterized over
433 <command>x,y,z</command>.</para>
434 <para><command>S</command> is the type of the record
435 and it must be convertible to a sort.</para>
436 <para>Each field <command>fi</command> is declared by giving its type
437 <command>Ti</command>. A record without any field is admitted.</para>
438 <para>Elimination principles for the record are automatically generated
439 by Matita, if allowed by the typing rules of the calculus according to
440 the sort <command>S</command>. If generated,
441 they are named <command>i_ind</command>, <command>i_rec</command> and
442 <command>i_rect</command> according to the sort of their induction
444 <para>For each field <command>fi</command> a record projection
445 <command>fi</command> is also automatically generated if projection
446 is allowed by the typing rules of the calculus according to the
447 sort <command>S</command>, the type <command>T1</command> and
448 the definability of depending record projections.</para>
449 <para>If the type of a field is declared with <command>:></command>,
450 the corresponding record projection becomes an implicit coercion.
451 This is just syntactic sugar and it has the same effect of declaring the
452 record projection as a coercion later on.</para>
457 <title>Proofs</title>
459 <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
460 <titleabbrev>theorem</titleabbrev>
461 <para><userinput>theorem f: P ≝ p</userinput></para>
462 <para>Proves a new theorem <command>f</command> whose thesis is
463 <command>P</command>.</para>
464 <para>If <command>p</command> is provided, it must be a proof term for
465 <command>P</command>. Otherwise an interactive proof is started.</para>
466 <para><command>P</command> can be omitted only if the proof is not
468 <para>Proving a theorem already proved in the library is an error.
469 To provide an alternative name and proof for the same theorem, use
470 <command>variant f: P ≝ p</command>.</para>
471 <para>A warning is raised if the name of the theorem cannot be obtained
472 by mangling the name of the constants in its thesis.</para>
473 <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
476 <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
477 <titleabbrev>variant</titleabbrev>
478 <para><userinput>variant f: T ≝ t</userinput></para>
479 <para>Same as <command>theorem f: T ≝ t</command>, but it does not
480 complain if the theorem has already been proved. To be used to give
481 an alternative name or proof to a theorem.</para>
484 <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
485 <titleabbrev>lemma</titleabbrev>
486 <para><userinput>lemma f: T ≝ t</userinput></para>
487 <para>Same as <command>theorem f: T ≝ t</command></para>
490 <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
491 <titleabbrev>fact</titleabbrev>
492 <para><userinput>fact f: T ≝ t</userinput></para>
493 <para>Same as <command>theorem f: T ≝ t</command></para>
496 <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
497 <titleabbrev>remark</titleabbrev>
498 <para><userinput>remark f: T ≝ t</userinput></para>
499 <para>Same as <command>theorem f: T ≝ t</command></para>
503 <sect1 id="tacticargs">
504 <title>Tactic arguments</title>
505 <para>This section documents the syntax of some recurring arguments for
508 <sect2 id="introsspec">
509 <title>intros-spec</title>
510 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
511 <title>intros-spec</title>
515 <entry id="grammar.intros-spec">&intros-spec;</entry>
517 <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
522 <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>
526 <title>pattern</title>
527 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
528 <title>pattern</title>
532 <entry id="grammar.pattern">&pattern;</entry>
534 <entry>&TODO;</entry>
542 <sect2 id="reduction-kind">
543 <title>reduction-kind</title>
544 <para>Reduction kinds are normalization functions that transform a term
545 to a convertible but simpler one. Each reduction kind can be used both
546 as a tactic argument and as a stand-alone tactic.</para>
547 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
548 <title>reduction-kind</title>
552 <entry id="grammar.reduction-kind">&reduction-kind;</entry>
554 <entry><emphasis role="bold">demodulate</emphasis></entry>
559 <entry><emphasis role="bold">normalize</emphasis></entry>
560 <entry>Computes the βδιζ-normal form</entry>
565 <entry><emphasis role="bold">reduce</emphasis></entry>
566 <entry>Computes the βδιζ-normal form</entry>
571 <entry><emphasis role="bold">simplify</emphasis></entry>
572 <entry>Computes a form supposed to be simpler</entry>
577 <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
578 <entry>δ-reduces the constant or variable if specified, or that
579 in head position</entry>
584 <entry><emphasis role="bold">whd</emphasis></entry>
585 <entry>Computes the βδιζ-weak-head normal form</entry>