<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent by eliminating an
+ <para>It closes the current sequent by eliminating an
absurd term.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>it opens two new sequents of conclusion <command>P</command>
+ <para>It opens two new sequents of conclusion <command>P</command>
and <command>¬P</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
+ <para>It closes the current sequent by applying <command>t</command> to <command>n</command> implicit arguments (that become new sequents).</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>it opens a new sequent for each premise
+ <para>It opens a new sequent for each premise
<command>T<subscript>i</subscript></command> that is not
instantiated by unification. <command>T<subscript>i</subscript></command> is
the conclusion of the <command>i</command>-th new sequent to
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>there must exist an hypothesis whose type can be unified with
+ <para>There must exist an hypothesis whose type can be unified with
the conclusion of the current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent exploiting an hypothesis.</para>
+ <para>It closes the current sequent exploiting an hypothesis.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none</para>
+ <para>None</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>none, but the tactic may fail finding a proof if every
+ <para>None, but the tactic may fail finding a proof if every
proof is in the search space that is pruned away. Pruning is
controlled by <command>d</command> and <command>w</command>.
Moreover, only lemmas whose type signature is a subset of the
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent by repeated application of
+ <para>It closes the current sequent by repeated application of
rewriting steps (unless <command>paramodulation</command> is
omitted), hypothesis and lemmas in the library.</para>
</listitem>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none</para>
+ <para>None</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it hides the hypothesis <command>H</command> from the
+ <para>It hides the hypothesis <command>H</command> from the
current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none</para>
+ <para>None</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it hides the definiens of a definition in the current
+ <para>It hides the definiens of a definition in the current
sequent context. Thus the definition becomes an hypothesis.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none.</para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>each subterm matched by the pattern must be convertible
+ <para>Each subterm matched by the pattern must be convertible
with the term <command>t</command> disambiguated in the context
of the matched subterm.</para>
</listitem>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it replaces the subterms of the current sequent matched by
+ <para>It replaces the subterms of the current sequent matched by
<command>patt</command> with the new term <command>t</command>.
For each subterm matched by the pattern, <command>t</command> is
disambiguated in the context of the subterm.</para>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none.</para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>the conclusion of the current sequent must be
- an inductive type or the application of an inductive type.</para>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least <command>n</command> constructors.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it applies the <command>n</command>-th constructor of the
+ <para>It applies the <command>n</command>-th constructor of the
inductive type of the conclusion of the current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>it opens a new sequent for each premise of the constructor
+ <para>It opens a new sequent for each premise of the constructor
that can not be inferred by unification. For more details,
see the <command>apply</command> tactic.</para>
</listitem>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>there must be in the current context an hypothesis of type
+ <para>There must be in the current context an hypothesis of type
<command>False</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent by applying an hypothesis of
+ <para>It closes the current sequent by applying an hypothesis of
type <command>False</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none</para>
+ <para>None</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent.</para>
+ <para>It closes the current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>it opens two new sequents. The first one has an extra
+ <para>It opens two new sequents. The first one has an extra
hypothesis <command>H:P</command>. If <command>H</command> is
omitted, the name of the hypothesis is automatically generated.
The second sequent has conclusion <command>P</command> and
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para><command>p</command> must have type <command>K<subscript>1</subscript> t<subscript>1</subscript> ... t<subscript>n</subscript> = K'<subscript>1</subscript> t'<subscript>1</subscript> ... t'<subscript>m</subscript></command> where <command>K</command> and <command>K'</command> must be different constructors of the same inductive type and each argument list can be empty if
+ <para><command>p</command> must have type <command>K t<subscript>1</subscript> ... t<subscript>n</subscript> = K' t'<subscript>1</subscript> ... t'<subscript>m</subscript></command> where <command>K</command> and <command>K'</command> must be different constructors of the same inductive type and each argument list can be empty if
its constructor takes no arguments.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent by proving the absurdity of
+ <para>It closes the current sequent by proving the absurdity of
<command>p</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none.</para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it proceeds by cases on the values of <command>t</command>,
+ <para>It proceeds by cases on the values of <command>t</command>,
according to the elimination principle <command>th</command>.
</para>
</listitem>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>it opens one new sequent for each case. The names of
+ <para>It opens one new sequent for each case. The names of
the new hypotheses are picked by <command>hyps</command>, if
- provided.</para>
+ provided. If hyps specifies also a number of hypotheses that
+ is less than the number of new hypotheses for a new sequent,
+ then the exceeding hypothesis will be kept as implications in
+ the conclusion of the sequent.</para>
</listitem>
</varlistentry>
</variablelist>
</para>
</sect1>
<sect1 id="tac_elimType">
- <title>elimType <term> [using <term>]</title>
+ <title>elimType <term> [using <term>] [<intros_spec>]</title>
<titleabbrev>elimType</titleabbrev>
- <para><userinput>elimType T using th</userinput></para>
+ <para><userinput>elimType T using th hyps</userinput></para>
<para>
<variablelist>
<varlistentry>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>the type of <command>p</command> must be convertible
+ <para>The type of <command>p</command> must be convertible
with the conclusion of the current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent using <command>p</command>.</para>
+ <para>It closes the current sequent using <command>p</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none.</para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>the conclusion of the current sequent must be
- an inductive type or the application of an inductive type.</para>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type
+ with at least one constructor.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>equivalent to <command>constructor 1</command>.</para>
+ <para>Equivalent to <command>constructor 1</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>it opens a new sequent for each premise of the first
+ <para>It opens a new sequent for each premise of the first
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>none.</para>
+ <para>None.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>this tactic always fail.</para>
+ <para>This tactic always fail.</para>
</listitem>
</varlistentry>
<varlistentry>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>the pattern must not specify the wanted term.</para>
+ <para>The pattern must not specify the wanted term.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>first of all it locates all the subterms matched by
+ <para>First of all it locates all the subterms matched by
<command>patt</command>. In the context of each matched subterm
it disambiguates the term <command>t</command> and reduces it
to its <command>red</command> normal form; then it replaces with
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none.</para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para>the conclusion of the current sequent must be a linear
+ <para>The conclusion of the current sequent must be a linear
inequation over real numbers taken from standard library of
Coq. Moreover the inequations in the hypotheses must imply the
inequation in the conclusion of the current sequent.</para>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>it closes the current sequent by applying the Fourier method.</para>
+ <para>It closes the current sequent by applying the Fourier method.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
- <para>none.</para>
+ <para>None.</para>
</listitem>
</varlistentry>
</variablelist>
<sect1 id="tac_generalize">
<title>generalize <pattern> [as <id>]</title>
<titleabbrev>generalize</titleabbrev>
- <para>The tactic <command>generalize</command> </para>
+ <para><userinput>generalize patt as H</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>All the terms matched by <command>patt</command> must be
+ convertible and close in the context of the current sequent.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent by applying a stronger
+ lemma that is proved using the new generated sequent.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent where the current sequent conclusion
+ <command>G</command> is generalized to
+ <command>∀x.G{x/t}</command> where <command>{x/t}</command>
+ is a notation for the replacement with <command>x</command> of all
+ the occurrences of the term <command>t</command> matched by
+ <command>patt</command>. If <command>patt</command> matches no
+ subterm then <command>t</command> is defined as the
+ <command>wanted</command> part of the pattern.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_id">
<title>id</title>
<titleabbrev>id</titleabbrev>
- <para>The tactic <command>id</command> </para>
+ <para><userinput>id </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>This identity tactic does nothing without failing.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_injection">
<title>injection <term></title>
<titleabbrev>injection</titleabbrev>
- <para>The tactic <command>injection</command> </para>
+ <para><userinput>injection p</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para><command>p</command> must have type <command>K t<subscript>1</subscript> ... t<subscript>n</subscript> = K t'<subscript>1</subscript> ... t'<subscript>n</subscript></command> where both argument lists are empty if
+<command>K</command> takes no arguments.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It derives new hypotheses by injectivity of
+ <command>K</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>The new sequent to prove is equal to the current sequent
+ with the additional hypotheses
+ <command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_intro">
<title>intro [<ident>]</title>
<titleabbrev>intro</titleabbrev>
- <para>The tactic <command>intro</command> </para>
+ <para><userinput>intro H</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the sequent to prove must be an implication
+ or a universal quantification.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It applies the right introduction rule for implication,
+ closing the current sequent.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent to prove adding to the hypothesis
+ the antecedent of the implication and setting the conclusion
+ to the consequent of the implicaiton. The name of the new
+ hypothesis is <command>H</command> if provided; otherwise it
+ is automatically generated.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_intros">
<title>intros <intros_spec></title>
<titleabbrev>intros</titleabbrev>
- <para>The tactic <command>intros</command> </para>
+ <para><userinput>intros hyps</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>If <command>hyps</command> specifies a number of hypotheses
+ to introduce, then the conclusion of the current sequent must
+ be formed by at least that number of imbricated implications
+ or universal quantifications.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It applies several times the right introduction rule for
+ implication, closing the current sequent.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent to prove adding a number of new
+ hypotheses equal to the number of new hypotheses requested.
+ If the user does not request a precise number of new hypotheses,
+ it adds as many hypotheses as possible.
+ The name of each new hypothesis is either popped from the
+ user provided list of names, or it is automatically generated when
+ the list is (or becomes) empty.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_inversion">
<title>inversion <term></title>
<titleabbrev>inversion</titleabbrev>
- <para>The tactic <command>inversion</command> </para>
+ <para><userinput>inversion t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The type of the term <command>t</command> must be an inductive
+ type or the application of an inductive type.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It proceeds by cases on <command>t</command> paying attention
+ to the constraints imposed by the actual "right arguments"
+ of the inductive type.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent to prove for each case in the
+ definition of the type of <command>t</command>. With respect to
+ a simple elimination, each new sequent has additional hypotheses
+ that states the equalities of the "right parameters"
+ of the inductive type with terms originally present in the
+ sequent to prove.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_lapply">
<title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
<titleabbrev>lapply</titleabbrev>
- <para>The tactic <command>lapply</command> </para>
+ <para><userinput>lapply ???</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>TODO.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>TODO.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>TODO.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_left">
<title>left</title>
<titleabbrev>left</titleabbrev>
- <para>The tactic <command>left</command> </para>
+ <para><userinput>left </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type
+ with at least one constructor.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Equivalent to <command>constructor 1</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <command>constructor</command> tactic.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_letin">
<title>letin <ident> ≝ <term></title>
<titleabbrev>letin</titleabbrev>
- <para>The tactic <command>letin</command> </para>
+ <para><userinput>letin x ≝ t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It adds to the context of the current sequent to prove a new
+ definition <command>x ≝ t</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_normalize">
<title>normalize <pattern></title>
<titleabbrev>normalize</titleabbrev>
- <para>The tactic <command>normalize</command> </para>
+ <para><userinput>normalize patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces all the terms matched by <command>patt</command>
+ with their βδιζ-normal form.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_paramodulation">
<title>paramodulation <pattern></title>
<titleabbrev>paramodulation</titleabbrev>
- <para>The tactic <command>paramodulation</command> </para>
+ <para><userinput>paramodulation patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>TODO.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>TODO.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>TODO.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_reduce">
<title>reduce <pattern></title>
<titleabbrev>reduce</titleabbrev>
- <para>The tactic <command>reduce</command> </para>
+ <para><userinput>reduce patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces all the terms matched by <command>patt</command>
+ with their βδιζ-normal form.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_reflexivity">
<title>reflexivity</title>
<titleabbrev>reflexivity</titleabbrev>
- <para>The tactic <command>reflexivity</command> </para>
+ <para><userinput>reflexivity </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ <command>t=t</command> for some term <command>t</command></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent by reflexivity
+ of equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_replace">
<title>replace <pattern> with <term></title>
- <titleabbrev>replace</titleabbrev>
- <para>The tactic <command>replace</command> </para>
+ <titleabbrev>change</titleabbrev>
+ <para><userinput>change patt with t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces the subterms of the current sequent matched by
+ <command>patt</command> with the new term <command>t</command>.
+ For each subterm matched by the pattern, <command>t</command> is
+ disambiguated in the context of the subterm.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>For each matched term <command>t'</command> it opens
+ a new sequent to prove whose conclusion is
+ <command>t'=t</command>.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_rewrite">
<title>rewrite {<|>} <term> <pattern></title>
<titleabbrev>rewrite</titleabbrev>
- <para>The tactic <command>rewrite</command> </para>
+ <para><userinput>rewrite dir p patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para><command>p</command> must be the proof of an equality,
+ possibly under some hypotheses.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It looks in every term matched by <command>patt</command>
+ for all the occurrences of the
+ left hand side of the equality that <command>p</command> proves
+ (resp. the right hand side if <command>dir</command> is
+ <command><</command>). Every occurence found is replaced with
+ the opposite side of the equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent for each hypothesis of the
+ equality proved by <command>p</command> that is not closed
+ by unification.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_right">
<title>right</title>
<titleabbrev>right</titleabbrev>
- <para>The tactic <command>right</command> </para>
+ <para><userinput>right </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least two constructors.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Equivalent to <command>constructor 2</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent for each premise of the second
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <command>constructor</command> tactic.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_ring">
<title>ring</title>
<titleabbrev>ring</titleabbrev>
- <para>The tactic <command>ring</command> </para>
+ <para><userinput>ring </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be an
+ equality over Coq's real numbers that can be proved using
+ the ring properties of the real numbers only.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent veryfying the equality by
+ means of computation (i.e. this is a reflexive tactic, implemented
+ exploiting the "two level reasoning" technique).</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_simplify">
<title>simplify <pattern></title>
<titleabbrev>simplify</titleabbrev>
- <para>The tactic <command>simplify</command> </para>
+ <para><userinput>simplify patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces all the terms matched by <command>patt</command>
+ with other convertible terms that are supposed to be simpler.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_split">
<title>split</title>
<titleabbrev>split</titleabbrev>
- <para>The tactic <command>split</command> </para>
+ <para><userinput>split </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least one constructor.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Equivalent to <command>constructor 1</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <command>constructor</command> tactic.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_symmetry">
<title>symmetry</title>
<titleabbrev>symmetry</titleabbrev>
<para>The tactic <command>symmetry</command> </para>
+ <para><userinput>symmetry </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current proof must be an equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It swaps the two sides of the equalityusing the symmetric
+ property.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_transitivity">
<title>transitivity <term></title>
<titleabbrev>transitivity</titleabbrev>
- <para>The tactic <command>transitivity</command> </para>
+ <para><userinput>transitivity t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current proof must be an equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent by transitivity of the equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens two new sequents <command>l=t</command> and
+ <command>t=r</command> where <command>l</command> and <command>r</command> are the left and right hand side of the equality in the conclusion of
+the current sequent to prove.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_unfold">
<title>unfold [<term>] <pattern></title>
<titleabbrev>unfold</titleabbrev>
- <para>The tactic <command>unfold</command> </para>
+ <para><userinput>unfold t patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It finds all the occurrences of <command>t</command>
+ (possibly applied to arguments) in the subterms matched by
+ <command>patt</command>. Then it δ-expands each occurrence,
+ also performing β-reduction of the obtained term. If
+ <command>t</command> is omitted it defaults to each
+ subterm matched by <command>patt</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
<sect1 id="tac_whd">
<title>whd <pattern></title>
<titleabbrev>whd</titleabbrev>
- <para>The tactic <command>whd</command> </para>
+ <para><userinput>whd patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces all the terms matched by <command>patt</command>
+ with their βδιζ-weak-head normal form.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
</chapter>