- <para>The tactic <command>exists</command> </para>
- </sect2>
- <sect2 id="tac_fail">
- <title>fail</title>
- <para>The tactic <command>fail</command> </para>
- </sect2>
- <sect2 id="tac_fold">
- <title>fold <reduction_kind> <term> <pattern></title>
- <para>The tactic <command>fold</command> </para>
- </sect2>
- <sect2 id="tac_fourier">
- <title>fourier</title>
- <para>The tactic <command>fourier</command> </para>
- </sect2>
- <sect2 id="tac_fwd">
- <title>fwd <ident> [<ident list>]</title>
- <para>The tactic <command>fwd</command> </para>
- </sect2>
- <sect2 id="tac_generalize">
- <title>generalize <pattern> [as <id>]</title>
- <para>The tactic <command>generalize</command> </para>
- </sect2>
- <sect2 id="tac_id">
- <title>id</title>
- <para>The tactic <command>id</command> </para>
- </sect2>
- <sect2 id="tac_injection">
- <title>injection <term></title>
- <para>The tactic <command>injection</command> </para>
- </sect2>
- <sect2 id="tac_intro">
- <title>intro [<ident>]</title>
- <para>The tactic <command>intro</command> </para>
- </sect2>
- <sect2 id="tac_intros">
- <title>intros <intros_spec></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_inversion">
- <title>intros <term></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_lapply">
- <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
- <para>The tactic <command>lapply</command> </para>
- </sect2>
- <sect2 id="tac_left">
- <title>left</title>
- <para>The tactic <command>left</command> </para>
- </sect2>
- <sect2 id="tac_letin">
- <title>letin <ident> ≝ <term></title>
- <para>The tactic <command>letin</command> </para>
- </sect2>
- <sect2 id="tac_normalize">
- <title>normalize <pattern></title>
- <para>The tactic <command>normalize</command> </para>
- </sect2>
- <sect2 id="tac_paramodulation">
+ <titleabbrev>exists</titleabbrev>
+ <para><userinput>exists </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_fail">
+ <title>fail </title>
+ <titleabbrev>failt</titleabbrev>
+ <para><userinput>fail</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>This tactic always fail.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>N.A.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_fold">
+ <title>fold <reduction_kind> &sterm; <pattern></title>
+ <titleabbrev>fold</titleabbrev>
+ <para><userinput>fold red t patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <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
+ <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
+ <command>t</command> every occurrence of the normal form in the
+ matched subterm.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_fourier">
+ <title>fourier</title>
+ <titleabbrev>fourier</titleabbrev>
+ <para><userinput>fourier </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <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>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <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>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_fwd">
+ <title>fwd &id; [<ident list>]</title>
+ <titleabbrev>fwd</titleabbrev>
+ <para><userinput>fwd ...TODO</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_generalize">
+ <title>generalize <pattern> [as &id;]</title>
+ <titleabbrev>generalize</titleabbrev>
+ <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><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 &sterm;</title>
+ <titleabbrev>injection</titleabbrev>
+ <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 [&id;]</title>
+ <titleabbrev>intro</titleabbrev>
+ <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><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 &sterm;</title>
+ <titleabbrev>inversion</titleabbrev>
+ <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=&nat;] &sterm; [to <term list>] [using &id;]</title>
+ <titleabbrev>lapply</titleabbrev>
+ <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><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 &id; ≝ &sterm;</title>
+ <titleabbrev>letin</titleabbrev>
+ <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><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">