<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>
<command>P</command>. Otherwise an interactive proof is started.</para>
<para><command>P</command> can be omitted only if the proof is not
interactive.</para>
+ <!--
<para>Proving a theorem already proved in the library is an error.
To provide an alternative name and proof for the same theorem, use
- <command>variant f: P ≝ p</command>.</para>
+ <command>variant f: P ≝ p</command>.</para>-->
<para>A warning is raised if the name of the theorem cannot be obtained
by mangling the name of the constants in its thesis.</para>
<para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
</sect2>
+ <!--
<sect2 id="variant">
<title><emphasis role="bold">variant</emphasis> &id;<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> &term;</title>
<titleabbrev>variant</titleabbrev>
<para>Same as <command>theorem f: T ≝ t</command>, but it does not
complain if the theorem has already been proved. To be used to give
an alternative name or proof to a theorem.</para>
+ </sect2>-->
+ <sect2 id="corollary">
+ <title><emphasis role="bold">corollary</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>corollary</titleabbrev>
+ <para><userinput>corollary f: T ≝ t</userinput></para>
+ <para>Same as <command>theorem f: T ≝ t</command></para>
</sect2>
<sect2 id="lemma">
<title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
<para><userinput>fact f: T ≝ t</userinput></para>
<para>Same as <command>theorem f: T ≝ t</command></para>
</sect2>
- <sect2 id="remark">
- <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
- <titleabbrev>remark</titleabbrev>
- <para><userinput>remark f: T ≝ t</userinput></para>
- <para>Same as <command>theorem f: T ≝ t</command></para>
+ <sect2 id="example">
+ <title><emphasis role="bold">example</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
+ <titleabbrev>example</titleabbrev>
+ <para><userinput>example f: T ≝ t</userinput></para>
+ <para>Same as <command>theorem f: T ≝ t</command>, but the example
+ is not indexed nor used by automation.</para>
</sect2>
</sect1>
<para>This section documents the syntax of some recurring arguments for
tactics.</para>
+ <!--
<sect2 id="introsspec">
<title>intros-spec</title>
<table frame="topbot" rowsep="0" colsep="0" role="grammar">
</table>
<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>
</sect2>
+ -->
<sect2 id="pattern">
<title>pattern</title>
<entry>::=</entry>
<entry><emphasis role="bold">in</emphasis>
[&id;[<emphasis role="bold">:</emphasis> &path;]]…
- [<emphasis role="bold">⊢</emphasis> &path;]]</entry>
+ [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
<entry>simple pattern</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">in 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;]]</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>
</para>
<para>A <emphasis>simple pattern</emphasis> extends paths to locate
subterms in a whole sequent. In particular, the pattern
- <userinput>in H: p K: q ⊢ r</userinput> locates at once all the subterms
+ <userinput>{ H: p K: q ⊢ r }</userinput> locates at once all the subterms
located by the pattern <userinput>r</userinput> in the conclusion of the
sequent and by the patterns <userinput>p</userinput> and
<userinput>q</userinput> in the hypotheses <userinput>H</userinput>
<para>A full pattern can always be replaced by a simple pattern,
often at the cost of increased verbosity or decreased readability.</para>
<para>Example: the pattern
- <userinput>⊢ in match x+y in ∀_,_:?.(? ? % ?)</userinput>
+ <userinput>{ match x+y in ⊢ ∀_,_:?.(? ? % ?) }</userinput>
locates only the first occurrence of <userinput>x+y</userinput>
in the sequent <userinput>x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) =
z * (x+y) + w * (x+y)</userinput>. The corresponding simple pattern
- is <userinput>⊢ ∀_,_:?.(? ? (? % ?) ?)</userinput>.
+ is <userinput>{ ⊢ ∀_,_:?.(? ? (? % ?) ?) }</userinput>.
</para>
<para>Every tactic that acts on subterms of the selected sequents have
a pattern argument for uniformity. To automatically generate a simple
<row>
<entry id="grammar.reduction-kind">&reduction-kind;</entry>
<entry>::=</entry>
- <entry><emphasis role="bold">normalize</emphasis></entry>
- <entry>Computes the βδιζ-normal form</entry>
- </row>
- <row>
- <entry/>
- <entry>|</entry>
- <entry><emphasis role="bold">simplify</emphasis></entry>
- <entry>Computes a form supposed to be simpler</entry>
- </row>
- <row>
- <entry/>
- <entry>|</entry>
- <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
- <entry>δ-reduces the constant or variable if specified, or that
- in head position</entry>
+ <entry><emphasis role="bold">normalize</emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
+ <entry>Computes the βδιζ-normal form. If <userinput>nodelta</userinput>
+ is specified, δ-expansions are not performed.</entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">whd</emphasis></entry>
- <entry>Computes the βδιζ-weak-head normal form</entry>
+ <entry><emphasis role="bold">whd</emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
+ <entry>Computes the βδιζ-weak-head normal form. If <userinput>nodelta</userinput>
+ is specified, δ-expansions are not performed.</entry>
</row>
</tbody>
</tgroup>
<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>
projects / helm.git / blobdiff