helm/software/matita/help/C/sec_commands.xml

   1
   2 <!-- ============ Commands ====================== -->
   3 <chapter id="sec_commands">
   4  <title>Other commands</title>
   5  <sect1 id="command_alias">
   6    <title>alias</title>
   7    <para><userinput>alias id &quot;s&quot; = &quot;def&quot;</userinput></para>
   8    <para><userinput>alias symbol &quot;s&quot; (instance n) = &quot;def&quot;</userinput></para>
   9    <para><userinput>alias num (instance n) = &quot;def&quot;</userinput></para>
  10    <para>
  11      <variablelist>
  12        <varlistentry>
  13          <term>Synopsis:</term>
  14          <listitem>
  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;
  19             ]
  20            </para>
  21          </listitem>
  22        </varlistentry>
  23        <varlistentry>
  24          <term>Action:</term>
  25          <listitem>
  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 &quot;map <command>s</command> (or the
  30             number) to <command>def</command>&quot;. For identifiers,
  31             &quot;def&quot; 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, &quot;def&quot; is the label used to
  37             mark the wanted
  38             <link linkend="interpretation">interpretation</link>.
  39            </para>
  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.
  44           </para>
  45           <para>
  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>
  50          </listitem>
  51        </varlistentry>
  52      </variablelist>
  53    </para>
  54  </sect1>
  55  <sect1 id="command_check">
  56    <title>check</title>
  57    <para><userinput>check t</userinput></para>
  58    <para>
  59      <variablelist>
  60        <varlistentry>
  61          <term>Synopsis:</term>
  62          <listitem>
  63            <para><emphasis role="bold">check</emphasis> &term;</para>
  64          </listitem>
  65        </varlistentry>
  66        <varlistentry>
  67          <term>Action:</term>
  68          <listitem>
  69            <para>Opens a CIC browser window that shows <command>t</command>
  70             together with its type. The command is immediately removed from
  71             the script.</para>
  72          </listitem>
  73        </varlistentry>
  74      </variablelist>
  75    </para>
  76  </sect1>
  77  <sect1 id="command_eval">
  78    <title>eval</title>
  79    <para><userinput>eval red on t</userinput></para>
  80    <para>
  81      <variablelist>
  82        <varlistentry>
  83          <term>Synopsis:</term>
  84          <listitem>
  85            <para><emphasis role="bold">eval</emphasis>
  86             &reduction-kind;
  87              <emphasis role="bold">on</emphasis>
  88              &term;</para>
  89          </listitem>
  90        </varlistentry>
  91        <varlistentry>
  92          <term>Action:</term>
  93          <listitem>
  94            <para>Opens a CIC browser window that shows
  95              the reduct of
  96              <command>t</command>
  97              together with its type.</para>
  98          </listitem>
  99        </varlistentry>
 100      </variablelist>
 101    </para>
 102  </sect1>
 103  <sect1 id="command_prefer_coercion">
 104    <title>prefer coercion</title>
 105    <para><userinput>prefer coercion u</userinput></para>
 106    <para>
 107      <variablelist>
 108        <varlistentry>
 109          <term>Synopsis:</term>
 110          <listitem>
 111                  <para>
 112                          <emphasis role="bold">prefer coercion</emphasis>
 113        (&uri; | &term;)
 114                  </para>
 115          </listitem>
 116        </varlistentry>
 117        <varlistentry>
 118          <term>Action:</term>
 119          <listitem>
 120            <para>The already declared coercion <command>u</command>
 121              is preferred to other coercions with the same source and target.
 122            </para>
 123          </listitem>
 124        </varlistentry>
 125      </variablelist>
 126    </para>
 127  </sect1>
 128  <sect1 id="command_coercion">
 129    <title>coercion</title>
 130    <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
 131    <para>
 132      <variablelist>
 133        <varlistentry>
 134          <term>Synopsis:</term>
 135          <listitem>
 136                  <para>
 137                          <emphasis role="bold">coercion</emphasis>
 138                          (&uri; | &term; <emphasis role="bold">with</emphasis>)
 139                          [ &nat; [&nat;]]
 140                          [ <emphasis role="bold">nocomposites</emphasis> ]
 141                  </para>
 142          </listitem>
 143        </varlistentry>
 144        <varlistentry>
 145          <term>Action:</term>
 146          <listitem>
 147                  <para>Declares <command>u</command> as an implicit coercion.
 148                  If the type of <command>u</command> is
 149                  <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
 150                  <command>T(n - ariety)</command> while its source is
 151                  <command>T(n - ariety - saturation - 1)</command>.
 152             Every time a term <command>x</command>
 153             of type source is used with expected type target, Matita
 154             automatically replaces <command>x</command> with
 155             <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
 156             Note that the number of <command>?</command> added after
 157             <command>x</command> is saturation.
 158            <para>Implicit coercions are not displayed to the user:
 159             <command>(u ? … ? x)</command> is rendered simply
 160             as <command>x</command>.</para>
 161            <para>When a coercion <command>u</command> is declared
 162             from source <command>s</command> to target <command>t</command>
 163             and there is already a coercion <command>u'</command> of
 164             target <command>s</command> or source <command>t</command>,
 165             a composite implicit coercion is automatically computed
 166             by Matita unless <emphasis role="bold">nocomposites</emphasis>
 167             is specified.</para>
 168          </listitem>
 169        </varlistentry>
 170      </variablelist>
 171    </para>
 172  </sect1>
 173  <sect1 id="command_default">
 174    <title>default</title>
 175    <para><userinput>default &quot;s&quot; u<subscript>1</subscript> … u<subscript>n</subscript></userinput></para>
 176    <para>
 177      <variablelist>
 178        <varlistentry>
 179          <term>Synopsis:</term>
 180          <listitem>
 181            <para><emphasis role="bold">default</emphasis>
 182             &qstring; &uri; [&uri;]…
 183            </para>
 184          </listitem>
 185        </varlistentry>
 186        <varlistentry>
 187          <term>Action:</term>
 188          <listitem>
 189            <para>It registers a cluster of related definitions and
 190             theorems to be used by tactics and the rendering engine.
 191             Some functionalities of Matita are not available when some
 192             clusters have not been registered. Overloading a cluster
 193             registration is possible: the last registration will be the
 194             default one, but the previous ones are still in effect.</para>
 195            <para>
 196             <command>s</command> is an identifier of the cluster and
 197             <command>u<subscript>1</subscript> … u<subscript>n</subscript></command>
 198             are the URIs of the definitions and theorems of the cluster.
 199             The number <command>n</command> of required URIs depends on the
 200             cluster. The following clusters are supported.
 201            </para>
 202            <table>
 203             <title>clusters</title>
 204             <tgroup cols="6">
 205             <thead>
 206              <row>
 207               <entry>name</entry>
 208               <entry>expected object for 1st URI</entry>
 209               <entry>expected object for 2nd URI</entry>
 210               <entry>expected object for 3rd URI</entry>
 211               <entry>expected object for 4th URI</entry>
 212               <entry>expected object for 5th URI</entry>
 213               <entry>expected object for 6th URI</entry>
 214               <entry>expected object for 7th URI</entry>
 215               <entry>expected object for 8th URI</entry>
 216               <entry>expected object for 9th URI</entry>
 217               <entry>expected object for 10th URI</entry>
 218               <entry>expected object for 11th URI</entry>
 219              </row>
 220             </thead>
 221             <tbody>
 222              <row>
 223               <entry>equality</entry>
 224               <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>
 225               <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>
 226               <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>
 227               <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>
 228               <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>
 229               <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>
 230               <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>
 231               <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>
 232               <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>
 233               <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>
 234               <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>
 235              </row>
 236              <row>
 237               <entry>true</entry>
 238               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> with only one constructor that has no arguments</entry>
 239               <entry/>
 240               <entry/>
 241               <entry/>
 242               <entry/>
 243              </row>
 244              <row>
 245               <entry>false</entry>
 246               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> without constructors</entry>
 247               <entry/>
 248               <entry/>
 249               <entry/>
 250               <entry/>
 251              </row>
 252              <row>
 253               <entry>absurd</entry>
 254               <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>
 255               <entry/>
 256               <entry/>
 257               <entry/>
 258               <entry/>
 259              </row>
 260             </tbody>
 261             </tgroup>
 262            </table>
 263          </listitem>
 264        </varlistentry>
 265      </variablelist>
 266    </para>
 267  </sect1>
 268  <sect1 id="command_hint">
 269    <title>hint</title>
 270    <para><userinput>hint</userinput></para>
 271    <para>
 272      <variablelist>
 273        <varlistentry>
 274          <term>Synopsis:</term>
 275          <listitem>
 276            <para><emphasis role="bold">hint</emphasis>
 277            </para>
 278          </listitem>
 279        </varlistentry>
 280        <varlistentry>
 281          <term>Action:</term>
 282          <listitem>
 283            <para>Displays a list of theorems that can be successfully
 284             applied to the current selected sequent. The command is
 285             removed from the script, but the window that displays the
 286             theorems allow to add to the script the application of the
 287             selected theorem.
 288            </para>
 289          </listitem>
 290        </varlistentry>
 291      </variablelist>
 292    </para>
 293  </sect1>
 294  <sect1 id="command_include">
 295    <title>include</title>
 296    <para><userinput>include &quot;s&quot;</userinput></para>
 297    <para>
 298      <variablelist>
 299        <varlistentry>
 300          <term>Synopsis:</term>
 301          <listitem>
 302            <para><emphasis role="bold">include</emphasis> &qstring;</para>
 303          </listitem>
 304        </varlistentry>
 305        <varlistentry>
 306          <term>Action:</term>
 307          <listitem>
 308            <para>Every <link linkend="command_coercion">coercion</link>,
 309             <link linkend="notation">notation</link> and
 310             <link linkend="interpretation">interpretation</link> that was active
 311             when the file <command>s</command> was compiled last time
 312             is made active. The same happens for declarations of
 313             <link linkend="command_default">default definitions and
 314             theorems</link> and disambiguation
 315             hints (<link linkend="command_alias">aliases</link>).
 316             On the contrary, theorem and definitions declared in a file can be
 317            immediately used without including it.</para>
 318           <para>The file <command>s</command> is automatically compiled
 319           if it is not compiled yet.
 320           </para>
 321          </listitem>
 322        </varlistentry>
 323      </variablelist>
 324    </para>
 325  </sect1>
 326  <sect1 id="command_include_first">
 327    <title>include' &quot;s&quot;</title>
 328    <para><userinput></userinput></para>
 329    <para>
 330      <variablelist>
 331        <varlistentry>
 332          <term>Synopsis:</term>
 333          <listitem>
 334            <para><emphasis role="bold">include'</emphasis> &qstring;</para>
 335          </listitem>
 336        </varlistentry>
 337        <varlistentry>
 338          <term>Action:</term>
 339          <listitem>
 340            <para>Not documented (&TODO;), do not use it.</para>
 341          </listitem>
 342        </varlistentry>
 343      </variablelist>
 344    </para>
 345  </sect1>
 346  <sect1 id="command_whelp">
 347    <title>whelp</title>
 348    <para><userinput>whelp locate &quot;s&quot;</userinput></para>
 349    <para><userinput>whelp hint t</userinput></para>
 350    <para><userinput>whelp elim t</userinput></para>
 351    <para><userinput>whelp match t</userinput></para>
 352    <para><userinput>whelp instance t</userinput></para>
 353    <para>
 354      <variablelist>
 355        <varlistentry>
 356          <term>Synopsis:</term>
 357          <listitem>
 358            <para><emphasis role="bold">whelp</emphasis>
 359             [<emphasis role="bold">locate</emphasis> &qstring;
 360             | <emphasis role="bold">hint</emphasis> &term;
 361             | <emphasis role="bold">elim</emphasis> &term;
 362             | <emphasis role="bold">match</emphasis> &term;
 363             | <emphasis role="bold">instance</emphasis> &term;
 364             ]
 365            </para>
 366          </listitem>
 367        </varlistentry>
 368        <varlistentry>
 369          <term>Action:</term>
 370          <listitem>
 371            <para>Performs the corresponding <link linkend="whelp">query</link>,
 372             showing the result in the CIC browser. The command is removed
 373             from the script.
 374            </para>
 375          </listitem>
 376        </varlistentry>
 377      </variablelist>
 378    </para>
 379  </sect1>
 380  <sect1 id="command_qed">
 381    <title>qed</title>
 382    <para><userinput></userinput></para>
 383    <para>
 384      <variablelist>
 385        <varlistentry>
 386          <term>Synopsis:</term>
 387          <listitem>
 388            <para><emphasis role="bold">qed</emphasis>
 389            </para>
 390          </listitem>
 391        </varlistentry>
 392        <varlistentry>
 393          <term>Action:</term>
 394          <listitem>
 395            <para>Saves and indexes the current interactive theorem or
 396             definition.
 397             In order to do this, the set of sequents still to be proved
 398             must be empty.</para>
 399          </listitem>
 400        </varlistentry>
 401      </variablelist>
 402    </para>
 403  </sect1>
 404 </chapter>
 405