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">
30 <title>qstring</title>
34 <entry id="grammar.qstring">&qstring;</entry>
36 <entry><emphasis role="bold">"</emphasis><emphasis>〈〈any sequence of characters excluded "〉〉</emphasis><emphasis role="bold">"</emphasis></entry>
41 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
46 <entry id="grammar.id">&id;</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>
53 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
58 <entry id="grammar.nat">&nat;</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>
65 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
70 <entry id="grammar.char">&char;</entry>
72 <entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
77 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
78 <title>uri-step</title>
82 <entry id="grammar.uri-step">&uri-step;</entry>
84 <entry>&char;[&char;]…</entry>
89 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
94 <entry id="grammar.uri">&uri;</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>
101 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
102 <title>csymbol</title>
106 <entry id="grammar.csymbol">&csymbol;</entry>
108 <entry><emphasis role="bold">'</emphasis>&id;</entry>
113 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
114 <title>symbol</title>
118 <entry id="grammar.symbol">&symbol;</entry>
120 <entry><emphasis role="bold">〈〈None of the above〉〉</emphasis></entry>
129 <!-- ZACK: Sample EBNF snippet, see:
130 http://www.docbook.org/tdg/en/html/productionset.html -->
134 <production id="grammar.term">
137 <lineannotation></lineannotation>
143 <table id="tbl_terms" frame="topbot" rowsep="0" colsep="0" role="grammar">
148 <entry id="grammar.term">&term;</entry>
150 <entry>&sterm;</entry>
151 <entry>simple or delimited term</entry>
156 <entry>&term; &term;</entry>
157 <entry>application</entry>
162 <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
163 <entry>λ-abstraction</entry>
168 <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
169 <entry>dependent product meant to define a datatype</entry>
174 <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
175 <entry>dependent product meant to define a proposition</entry>
180 <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
181 <entry>non-dependent product (logical implication or function space)</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>
193 <emphasis role="bold">let</emphasis>
194 [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
197 <entry>(co)recursive definitions</entry>
203 [<emphasis role="bold">and</emphasis> &rec_def;]…
211 <emphasis role="bold">in</emphasis> &term;
219 <entry>user provided notation</entry>
222 <entry id="grammar.rec_def">&rec_def;</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>]…
233 [<emphasis role="bold">on</emphasis> &id;]
234 [<emphasis role="bold">:</emphasis> &term;]
235 <emphasis role="bold">≝</emphasis> &term;]
243 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
244 <title>Simple terms</title>
248 <entry id="grammar.sterm">&sterm;</entry>
250 <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></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>]
261 <entry>identifier with optional explicit named substitution</entry>
267 <entry>a qualified reference</entry>
272 <entry><emphasis role="bold">Prop</emphasis></entry>
273 <entry>the impredicative sort of propositions</entry>
278 <entry><emphasis role="bold">Set</emphasis></entry>
279 <entry>the impredicate sort of datatypes</entry>
284 <entry><emphasis role="bold">CProp</emphasis></entry>
285 <entry>one fixed predicative sort of constructive propositions</entry>
290 <entry><emphasis role="bold">Type</emphasis></entry>
291 <entry>one predicative sort of datatypes</entry>
296 <entry><emphasis role="bold">?</emphasis></entry>
297 <entry>implicit argument</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>
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>
316 <entry>case analysis</entry>
322 <emphasis role="bold">[</emphasis>
323 &match_branch;[<emphasis role="bold">|</emphasis>&match_branch;]…
324 <emphasis role="bold">]</emphasis>
331 <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
338 <entry>user provided notation at precedence 90</entry>
344 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
345 <title>Arguments</title>
349 <entry id="grammar.args">&args;</entry>
352 <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
354 <entry>ignored argument</entry>
360 <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
362 <entry>ignored argument</entry>
367 <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
373 <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
377 <entry id="grammar.args2">&args2;</entry>
385 <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
392 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
393 <title>Pattern matching</title>
397 <entry id="grammar.match_branch">&match_branch;</entry>
399 <entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
403 <entry id="grammar.match_pattern">&match_pattern;</entry>
406 <entry>0-ary constructor</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>
417 <entry>&id; &id; [&id;]…</entry>
418 <entry>n-ary constructor (binds the n arguments)</entry>
423 <entry><emphasis role="bold">_</emphasis></entry>
424 <entry>any remaining constructor (ignoring its arguments)</entry>
434 <sect1 id="axiom_definition_declaration">
435 <title>Definitions and declarations</title>
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>
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
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>
457 <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
458 <titleabbrev>&TODO;</titleabbrev>
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;]…]…
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
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
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
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">:></emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></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
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>:></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>
516 <title>Proofs</title>
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
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>
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>
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>
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>
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>
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>
571 <sect1 id="tacticargs">
572 <title>Tactic arguments</title>
573 <para>This section documents the syntax of some recurring arguments for
577 <sect2 id="introsspec">
578 <title>intros-spec</title>
579 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
580 <title>intros-spec</title>
584 <entry id="grammar.intros-spec">&intros-spec;</entry>
586 <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
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>
596 <title>pattern</title>
597 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
598 <title>pattern</title>
602 <entry id="grammar.pattern">&pattern;</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>
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>
621 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
626 <entry id="grammar.path">&path;</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>
633 <para>A <emphasis>path</emphasis> locates zero or more subterms of a given term by mimicking the term structure up to:</para>
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>.
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>
648 <emphasis role="bold">|</emphasis> …
649 <emphasis role="bold">|</emphasis>
650 <emphasis role="bold">_</emphasis>
651 <emphasis role="bold">⇒</emphasis>
653 <emphasis role="bold">]</emphasis>
654 Its semantics is the following: the n-th
655 "<emphasis role="bold">_</emphasis>
656 <emphasis role="bold">⇒</emphasis>
657 &path;" 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.
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>).
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.
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.
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>.
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>.
704 <para>Every tactic that acts on subterms of the selected sequents have
705 a pattern argument for uniformity. To automatically generate a simple
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 "Copy".</para></listitem>
713 <listitem><para>From the "Edit" or the contextual menu select
714 "Paste as pattern"</para></listitem>
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>
728 <entry id="grammar.reduction-kind">&reduction-kind;</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>
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>
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>
753 <entry id="grammar.autoparams">&autoparams;</entry>
755 <entry>[&nat;] [&simpleautoparam;]…
756 [<emphasis role="bold">by</emphasis>
757 [&sterm;… | <emphasis role="bold">_</emphasis>]]
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.
774 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
775 <title>simple-auto-param</title>
779 <entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
781 <entry><emphasis role="bold">width=&nat;</emphasis></entry>
782 <entry>The maximal width of the search tree</entry>
787 <entry><emphasis role="bold">size=&nat;</emphasis></entry>
788 <entry>The maximal number of nodes in the proof</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
801 <entry><emphasis role="bold">paramod</emphasis></entry>
802 <entry>Try to close the goal performing unit-equality paramodulation
808 <entry><emphasis role="bold">fast_paramod</emphasis></entry>
809 <entry>A bounded version of <command>paramod</command> that is granted to terminate quickly
818 <sect2 id="justification">
819 <title>justification</title>
820 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
821 <title>justification</title>
825 <entry id="grammar.justification">&justification;</entry>
827 <entry><emphasis role="bold">using</emphasis> &term;</entry>
828 <entry>Proof term manually provided</entry>
833 <entry>&autoparams;</entry>
834 <entry>Call automation</entry>