<command>f</command> must be defined by means of tactics.</para>
<para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
</sect2>
+ <sect2 id="discriminator">
+ <title><emphasis role="bold">discriminator</emphasis> &id;</title>
+ <titleabbrev>discriminator</titleabbrev>
+ <para><userinput>discriminator i</userinput></para>
+ <para>Defines a new discrimination (injectivity+conflict) principle à la
+ McBride for the inductive type <command>i</command>.</para>
+ <para>The principle will use John
+ Major's equality if such equality is defined, otherwise it will use
+ Leibniz equality; in the former case, it will be called
+ <command>i_jmdiscr</command>, in the latter, <command>i_discr</command>.
+ The command will fail if neither equality is available.</para>
+ <para>Discrimination principles are used by the destruct tactic and are
+ usually automatically generated by Matita during the definition of the
+ corresponding inductive type. This command is thus especially useful
+ when the correct equality was not loaded at the time of that
+ definition.</para>
+ </sect2>
+ <sect2 id="inverter">
+ <title><emphasis role="bold">inverter</emphasis> &id; <emphasis role="bold">for</emphasis> &id; (&path;) [&term;]</title>
+ <titleabbrev>inverter</titleabbrev>
+ <para><userinput>inverter n for i (path) : s</userinput></para>
+ <para>Defines a new induction/inversion principle for the inductive type
+ <command>i</command>, called <command>n</command>.</para>
+ <para><command>(path)</command> must be in the form <command>(# # # ... #)</command>,
+ where each <command>#</command> can be either <command>?</command> or
+ <command>%</command>, and the number of symbols is equal to the number of
+ right parameters (indices) of <command>i</command>. Parentheses are
+ mandatory. If the j-th symbol is
+ <command>%</command>, Matita will generate a principle providing
+ equations for reasoning on the j-th index of <command>i</command>. If the
+ symbol is a <command>?</command>, no corresponding equation will be
+ provided.</para>
+ <para><command>s</command>, which must be a sort, is the target sort of the
+ induction/inversion principle and defaults to <command>Prop</command>.</para>
+ </sect2>
<sect2 id="letrec">
<title><emphasis role="bold">letrec</emphasis> &TODO;</title>
<titleabbrev>&TODO;</titleabbrev>
<row>
<entry id="grammar.pattern">&pattern;</entry>
<entry>::=</entry>
- <entry><emphasis role="bold">{</emphasis>
+ <entry><emphasis role="bold">in</emphasis>
[&id;[<emphasis role="bold">:</emphasis> &path;]]…
- [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+ [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
<entry>simple pattern</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">{match</emphasis> &path;
+ <entry><emphasis role="bold">in</emphasis> <emphasis role="bold">match</emphasis> &path;
[<emphasis role="bold">in</emphasis>
[&id;[<emphasis role="bold">:</emphasis> &path;]]…
- [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+ [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
<entry>full pattern</entry>
</row>
</tbody>
</table>
<table frame="topbot" rowsep="0" colsep="0" role="grammar">
<title>path</title>
- <tgroup cols="4">
+ <tgroup cols="3">
<tbody>
<row>
<entry id="grammar.path">&path;</entry>
<row>
<entry id="grammar.autoparams">&autoparams;</entry>
<entry>::=</entry>
- <entry>[&simpleautoparam;]…
+ <entry>[&nat;] [&simpleautoparam;]…
[<emphasis role="bold">by</emphasis>
- &term; [,&term;]…]
+ [&sterm;… | <emphasis role="bold">_</emphasis>]]
+ </entry>
+ <entry>The natural number, which defaults to 1, gives a bound to
+ the depth of the search tree. The terms listed is the only
+ knowledge base used by automation together with all indexed factual
+ and equational theorems in the included library. If the list of terms
+ is empty, only equational theorems and facts in the library are
+ used. If the list is omitted, it defaults to all indexed theorems
+ in the library. Finally, if the list is <command>_</command>,
+ the automation command becomes a macro that is expanded in a new
+ automation command where <command>_</command> is replaced with the
+ list of theorems required to prove the sequent.
</entry>
</row>
</tbody>
<row>
<entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
<entry>::=</entry>
- <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
- <entry>Give a bound to the depth of the search tree</entry>
- </row>
- <row>
- <entry/>
- <entry>|</entry>
<entry><emphasis role="bold">width=&nat;</emphasis></entry>
<entry>The maximal width of the search tree</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">library</emphasis></entry>
- <entry>Search everywhere (not only in included files)</entry>
+ <entry><emphasis role="bold">size=&nat;</emphasis></entry>
+ <entry>The maximal number of nodes in the proof</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">type</emphasis></entry>
- <entry>Try to close also goals of sort Type, otherwise only goals
- living in sort Prop are attacked.
+ <entry><emphasis role="bold">demod</emphasis></entry>
+ <entry>Simplifies the current sequent using the current set of
+ equations known to automation
</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">paramodulation</emphasis></entry>
+ <entry><emphasis role="bold">paramod</emphasis></entry>
<entry>Try to close the goal performing unit-equality paramodulation
</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">size=&nat;</emphasis></entry>
- <entry>The maximal number of nodes in the proof</entry>
- </row>
- <row>
- <entry/>
- <entry>|</entry>
- <entry><emphasis role="bold">timeout=&nat;</emphasis></entry>
- <entry>Timeout in seconds
+ <entry><emphasis role="bold">fast_paramod</emphasis></entry>
+ <entry>A bounded version of <command>paramod</command> that is granted to terminate quickly
</entry>
</row>
</tbody>
</table>
</sect2>
- <!--
<sect2 id="justification">
<title>justification</title>
<table frame="topbot" rowsep="0" colsep="0" role="grammar">
</tgroup>
</table>
</sect2>
- -->
</sect1>
</chapter>
projects / helm.git / blobdiff