2 <!-- ============ Commands ====================== -->
3 <chapter id="sec_commands">
4 <title>Other commands</title>
5 <sect1 id="command_alias">
7 <para><userinput>alias id "s" = "def"</userinput></para>
8 <para><userinput>alias symbol "s" (instance n) = "def"</userinput></para>
9 <para><userinput>alias num (instance n) = "def"</userinput></para>
13 <term>Synopsis:</term>
15 <para><emphasis role="bold">alias</emphasis>
16 [<emphasis role="bold">id</emphasis> &qstring; <emphasis role="bold">=</emphasis> &qstring;
17 | <emphasis role="bold">symbol</emphasis> &qstring; [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> &qstring;
18 | <emphasis role="bold">num</emphasis> [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> &qstring;
26 <para>Used to give an hint to the disambiguating parser.
27 When the parser is faced to the identifier (or symbol)
28 <command>s</command> or to any number, it will prefer
29 interpretations that "map <command>s</command> (or the
30 number) to <command>def</command>". For identifiers,
31 "def" is the URI of the interpretation.
32 E.g.: <command>cic:/matita/nat/nat.ind#xpointer(1/1/1)</command>
33 for the first constructor of the first inductive type defined
34 in the block of inductive type(s)
35 <command>cic:/matita/nat/nat.ind</command>.
36 For symbols and numbers, "def" is the label used to
38 <link linkend="interpretation">interpretation</link>.
40 <para>When a symbol or a number occurs several times in the
41 term to be parsed, it is possible to give an hint only for the
42 instance <command>n</command>. When the instance is omitted,
43 the hint is valid for every occurrence.
46 Hints are automatically inserted in the script by Matita every
47 time the user is interactively asked a question to disambiguate
48 a term. This way the user won't be posed the same question twice
49 when the script will be executed again.</para>
55 <sect1 id="command_check">
57 <para><userinput>check t</userinput></para>
61 <term>Synopsis:</term>
63 <para><emphasis role="bold">check</emphasis> &sterm;</para>
69 <para>Opens a CIC browser window that shows <command>t</command>
70 together with its type. The command is immediately removed from
78 <sect1 id="command_eval">
80 <para><userinput>eval red on t</userinput></para>
84 <term>Synopsis:</term>
86 <para><emphasis role="bold">eval</emphasis>
88 <emphasis role="bold">on</emphasis>
95 <para>Opens a CIC browser window that shows
98 together with its type.</para>
106 <sect1 id="command_prefer_coercion">
107 <title>prefer coercion</title>
108 <para><userinput>prefer coercion u</userinput></para>
112 <term>Synopsis:</term>
115 <emphasis role="bold">prefer coercion</emphasis>
123 <para>The already declared coercion <command>u</command>
124 is preferred to other coercions with the same source and target.
132 <sect1 id="command_coercion">
133 <title>coercion</title>
136 <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
140 <term>Synopsis:</term>
143 <emphasis role="bold">coercion</emphasis>
144 (&uri; | &term; <emphasis role="bold">with</emphasis>)
146 [ <emphasis role="bold">nocomposites</emphasis> ]
153 <para>Declares <command>u</command> as an implicit coercion.
154 If the type of <command>u</command> is
155 <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
156 <command>T(n - ariety)</command> while its source is
157 <command>T(n - ariety - saturation - 1)</command>.
158 Every time a term <command>x</command>
159 of type source is used with expected type target, Matita
160 automatically replaces <command>x</command> with
161 <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
162 Note that the number of <command>?</command> added after
163 <command>x</command> is saturation.
164 <para>Implicit coercions are not displayed to the user:
165 <command>(u ? … ? x)</command> is rendered simply
166 as <command>x</command>.</para>
167 <para>When a coercion <command>u</command> is declared
168 from source <command>s</command> to target <command>t</command>
169 and there is already a coercion <command>u'</command> of
170 target <command>s</command> or source <command>t</command>,
171 a composite implicit coercion is automatically computed
172 by Matita unless <emphasis role="bold">nocomposites</emphasis>
181 <sect1 id="command_default">
182 <title>default</title>
183 <para><userinput>default "s" u<subscript>1</subscript> … u<subscript>n</subscript></userinput></para>
187 <term>Synopsis:</term>
189 <para><emphasis role="bold">default</emphasis>
190 &qstring; &uri; [&uri;]…
197 <para>It registers a cluster of related definitions and
198 theorems to be used by tactics and the rendering engine.
199 Some functionalities of Matita are not available when some
200 clusters have not been registered. Overloading a cluster
201 registration is possible: the last registration will be the
202 default one, but the previous ones are still in effect.</para>
204 <command>s</command> is an identifier of the cluster and
205 <command>u<subscript>1</subscript> … u<subscript>n</subscript></command>
206 are the URIs of the definitions and theorems of the cluster.
207 The number <command>n</command> of required URIs depends on the
208 cluster. The following clusters are supported.
211 <title>clusters</title>
216 <entry>expected object for 1st URI</entry>
217 <entry>expected object for 2nd URI</entry>
218 <entry>expected object for 3rd URI</entry>
219 <entry>expected object for 4th URI</entry>
220 <entry>expected object for 5th URI</entry>
221 <entry>expected object for 6th URI</entry>
222 <entry>expected object for 7th URI</entry>
223 <entry>expected object for 8th URI</entry>
224 <entry>expected object for 9th URI</entry>
225 <entry>expected object for 10th URI</entry>
226 <entry>expected object for 11th URI</entry>
231 <entry>equality</entry>
232 <entry>an inductive type (say, of type <command>eq</command>) of type ∀A:Type.A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis> with one family parameter and one constructor of type ∀x:A.eq A x</entry>
233 <entry>a theorem of type <emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq A y x</entry>
234 <entry>a theorem of type <emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>x,y,z:A.eq A x y <emphasis role="bold">→</emphasis> eq A y z <emphasis role="bold">→</emphasis> eq A x z</entry>
235 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
236 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
237 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Set</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
238 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Set</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
239 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Type</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
240 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Type</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
241 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>B.<emphasis role="bold">∀</emphasis> f:A <emphasis role="bold">→</emphasis> B.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq B (f x) (f y)</entry>
242 <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>B.<emphasis role="bold">∀</emphasis> f:A <emphasis role="bold">→</emphasis> B.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq B (f y) (f x)</entry>
246 <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> with only one constructor that has no arguments</entry>
254 <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> without constructors</entry>
261 <entry>absurd</entry>
262 <entry>a theorem of type <emphasis role="bold">∀</emphasis>A:Prop.<emphasis role="bold">∀</emphasis>B:Prop.A <emphasis role="bold">→</emphasis> Not A <emphasis role="bold">→</emphasis> B</entry>
278 <sect1 id="command_hint">
280 <para><userinput>hint</userinput></para>
284 <term>Synopsis:</term>
286 <para><emphasis role="bold">hint</emphasis>
293 <para>Displays a list of theorems that can be successfully
294 applied to the current selected sequent. The command is
295 removed from the script, but the window that displays the
296 theorems allow to add to the script the application of the
305 <sect1 id="command_include">
306 <title>include</title>
307 <para><userinput>include "s"</userinput></para>
311 <term>Synopsis:</term>
313 <para><emphasis role="bold">include</emphasis> &qstring;</para>
319 <para>Every <link linkend="command_coercion">coercion</link>,
320 <link linkend="notation">notation</link> and
321 <link linkend="interpretation">interpretation</link> that was active
322 when the file <command>s</command> was compiled last time
323 is made active. The same happens for declarations of
324 <link linkend="command_default">default definitions and
325 theorems</link> and disambiguation
326 hints (<link linkend="command_alias">aliases</link>).
327 On the contrary, theorem and definitions declared in a file can be
328 immediately used without including it.</para>
329 <para>The file <command>s</command> is automatically compiled
330 if it is not compiled yet.
333 If the file <command>s</command> was already included, either
334 directly or recursively, the commands does nothing.
341 <sect1 id="command_include_alias">
342 <title>include alias</title>
343 <para><userinput>include alias "s"</userinput></para>
347 <term>Synopsis:</term>
349 <para><emphasis role="bold">include</emphasis> <emphasis role="bold">alias</emphasis> &qstring;</para>
356 <link linkend="interpretation">interpretation</link>
357 declared in the file <command>s</command> is re-declared
358 so to make it the preferred choice for disambiguation.
366 <sect1 id="command_include_first">
367 <title>include' "s"</title>
368 <para><userinput></userinput></para>
372 <term>Synopsis:</term>
374 <para><emphasis role="bold">include'</emphasis> &qstring;</para>
380 <para>Not documented (&TODO;), do not use it.</para>
388 <sect1 id="command_whelp">
390 <para><userinput>whelp locate "s"</userinput></para>
391 <para><userinput>whelp hint t</userinput></para>
392 <para><userinput>whelp elim t</userinput></para>
393 <para><userinput>whelp match t</userinput></para>
394 <para><userinput>whelp instance t</userinput></para>
398 <term>Synopsis:</term>
400 <para><emphasis role="bold">whelp</emphasis>
401 [<emphasis role="bold">locate</emphasis> &qstring;
402 | <emphasis role="bold">hint</emphasis> &term;
403 | <emphasis role="bold">elim</emphasis> &term;
404 | <emphasis role="bold">match</emphasis> &term;
405 | <emphasis role="bold">instance</emphasis> &term;
413 <para>Performs the corresponding <link linkend="whelp">query</link>,
414 showing the result in the CIC browser. The command is removed
423 <sect1 id="command_qed">
425 <para><userinput>qed</userinput></para>
429 <term>Synopsis:</term>
431 <para><emphasis role="bold">qed</emphasis>
438 <para>Saves and indexes the current interactive theorem or
440 In order to do this, the set of sequents still to be proved
441 must be empty.</para>
447 <sect1 id="command_qed_minus">
449 <para><userinput>qed-</userinput></para>
453 <term>Synopsis:</term>
455 <para><emphasis role="bold">qed-</emphasis>
462 <para>Saves the current interactive theorem or
463 definition without indexing. Therefore automation will ignore
465 In order to do this, the set of sequents still to be proved
466 must be empty.</para>
472 <sect1 id="command_unification_hint">
473 <title>unification hint</title>
476 <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
480 <term>Synopsis:</term>
483 <emphasis role="bold">coercion</emphasis>
484 (&uri; | &term; <emphasis role="bold">with</emphasis>)
486 [ <emphasis role="bold">nocomposites</emphasis> ]
493 <para>Declares <command>u</command> as an implicit coercion.
494 If the type of <command>u</command> is
495 <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
496 <command>T(n - ariety)</command> while its source is
497 <command>T(n - ariety - saturation - 1)</command>.
498 Every time a term <command>x</command>
499 of type source is used with expected type target, Matita
500 automatically replaces <command>x</command> with
501 <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
502 Note that the number of <command>?</command> added after
503 <command>x</command> is saturation.
504 <para>Implicit coercions are not displayed to the user:
505 <command>(u ? … ? x)</command> is rendered simply
506 as <command>x</command>.</para>
507 <para>When a coercion <command>u</command> is declared
508 from source <command>s</command> to target <command>t</command>
509 and there is already a coercion <command>u'</command> of
510 target <command>s</command> or source <command>t</command>,
511 a composite implicit coercion is automatically computed
512 by Matita unless <emphasis role="bold">nocomposites</emphasis>
520 <sect1 id="command_universe_constraints">
521 <title>universe constraint</title>
524 <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
528 <term>Synopsis:</term>
531 <emphasis role="bold">coercion</emphasis>
532 (&uri; | &term; <emphasis role="bold">with</emphasis>)
534 [ <emphasis role="bold">nocomposites</emphasis> ]
541 <para>Declares <command>u</command> as an implicit coercion.
542 If the type of <command>u</command> is
543 <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
544 <command>T(n - ariety)</command> while its source is
545 <command>T(n - ariety - saturation - 1)</command>.
546 Every time a term <command>x</command>
547 of type source is used with expected type target, Matita
548 automatically replaces <command>x</command> with
549 <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
550 Note that the number of <command>?</command> added after
551 <command>x</command> is saturation.
552 <para>Implicit coercions are not displayed to the user:
553 <command>(u ? … ? x)</command> is rendered simply
554 as <command>x</command>.</para>
555 <para>When a coercion <command>u</command> is declared
556 from source <command>s</command> to target <command>t</command>
557 and there is already a coercion <command>u'</command> of
558 target <command>s</command> or source <command>t</command>,
559 a composite implicit coercion is automatically computed
560 by Matita unless <emphasis role="bold">nocomposites</emphasis>
570 <sect1 id="command_inline">
571 <title>inline</title>
572 <para><userinput>inline "s" params</userinput></para>
576 <term>Synopsis:</term>
579 <emphasis role="bold">inline</emphasis> &qstring; &inlineparams;
586 <para>Inlines a representation of the item <command>s</command>,
587 which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
588 URI) or the path of a *.ma source file is provided, all the contained objects
589 are represented in a row.
590 If the inlined object has a proof, this proof is represented in several ways
591 depending on the provided parameters.</para>
597 <sect2 id="inline-params">
598 <title>inline-params</title>
599 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
600 <title>inline-params</title>
604 <entry id="grammar.inlineparams">&inlineparams;</entry>
606 <entry>[&inlineparam; [&inlineparam;] … ]</entry>
611 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
612 <title>inline-param</title>
617 <entry id="grammar.inlineparam">&inlineparam;</entry>
619 <entry><emphasis role="bold">axiom</emphasis></entry>
620 <entry>Try to give an <link linkend="axiom">axiom</link> flavour
621 (bodies are omitted even if present)
628 <entry><emphasis role="bold">definition</emphasis></entry>
629 <entry>Try give a <link linkend="definition">definition</link> flavour
636 <entry><emphasis role="bold">theorem</emphasis></entry>
637 <entry>Try give a <link linkend="theorem">theorem</link> flavour
644 <entry><emphasis role="bold">lemma</emphasis></entry>
645 <entry>Try give a <link linkend="lemma">lemma</link> flavour
652 <entry><emphasis role="bold">remark</emphasis></entry>
653 <entry>Try give a <link linkend="remark">remark</link> flavour
660 <entry><emphasis role="bold">fact</emphasis></entry>
661 <entry>Try give a <link linkend="fact">fact</link> flavour
668 <entry><emphasis role="bold">variant</emphasis></entry>
669 <entry>Try give a <link linkend="variant">variant</link> flavour
670 (implies <emphasis role="bold">plain</emphasis>)
677 <entry><emphasis role="bold">declarative</emphasis></entry>
678 <entry>Represent proofs using
679 <link linkend="sec_declarative_tactics">declarative tactics</link>
680 (this is the dafault and can be omitted)
687 <entry><emphasis role="bold">procedural</emphasis></entry>
688 <entry>Represent proofs using
689 <link linkend="sec_tactics">procedural tactics</link>
696 <entry><emphasis role="bold">plain</emphasis></entry>
697 <entry>Represent proofs using plain
698 <link linkend="tbl_terms">proof terms</link>
705 <entry><emphasis role="bold">nodefaults</emphasis></entry>
707 Do not use the tactics depending on the
708 <link linkend="command_default">default</link> command
709 (<link linkend="tac_rewrite">rewrite</link>
710 in the <emphasis role="bold">procedural</emphasis> mode)
717 <entry><emphasis role="bold">level=&nat;</emphasis></entry>
719 Set the level of the procedural proof representation
720 (the default is the highest level)
723 Tactics used at level 1:
724 <link linkend="tac_exact">exact</link>
727 Additional tactics used at level 2:
728 <link linkend="tac_letin">letin</link>,
729 <link linkend="tac_cut">cut</link>,
730 <link linkend="tac_change">change</link>,
731 <link linkend="tac_intros">intros</link>,
732 <link linkend="tac_apply">apply</link>,
733 <link linkend="tac_elim">elim</link>,
734 <link linkend="tac_cases">cases</link>,
735 <link linkend="tac_rewrite">rewrite</link>
744 <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
745 <entry>&TODO;</entry>