- <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>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_contradiction">
- <title>contradiction</title>
- <titleabbrev>contradiction</titleabbrev>
- <para><userinput>contradiction </userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">contradiction</emphasis></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <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
- type <command>False</command>.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_cut">
- <title>cut</title>
- <titleabbrev>cut</titleabbrev>
- <para><userinput>cut P as H</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">cut</emphasis> &sterm; [<emphasis role="bold">as</emphasis> &id;]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para><command>P</command> must have type <command>Prop</command>.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <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
- 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
- hypotheses the hypotheses of the current sequent to prove.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_decompose">
- <title>decompose</title>
- <titleabbrev>decompose</titleabbrev>
- <para><userinput>
- decompose as H<subscript>1</subscript> ... H<subscript>m</subscript>
- </userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para>
- <emphasis role="bold">decompose</emphasis>
- [<emphasis role="bold">as</emphasis> &id;…]
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>
- For each each premise <command>H</command> of type
- <command>T</command> in the current context where
- <command>T</command> is a non-recursive inductive type without
- right parameters and of sort Prop or CProp, the tactic runs
- <command>
- elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
- </command>, clears <command>H</command> and runs itself
- recursively on each new premise introduced by
- <command>elim</command> in the opened sequents.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>
- The ones generated by all the <command>elim</command> tactics run.
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_demodulate">
- <title>demodulate</title>
- <titleabbrev>demodulate</titleabbrev>
- <para><userinput>demodulate auto_params</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">demodulate</emphasis> &autoparams;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>&TODO;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_destruct">
- <title>destruct</title>
- <titleabbrev>destruct</titleabbrev>
- <para><userinput>destruct p</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">destruct</emphasis> &sterm;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para><command>p</command> must have type <command>E<subscript>1</subscript> = E<subscript>2</subscript></command> where the two sides of the equality are possibly applied constructors of an inductive type.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>The tactic recursively compare the two sides of the equality
- looking for different constructors in corresponding position.
- If two of them are found, the tactic closes the current sequent
- by proving the absurdity of <command>p</command>. Otherwise
- it adds a new hypothesis for each leaf of the formula that
- states the equality of the subformulae in the corresponding
- positions on the two sides of the equality.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_elim">
- <title>elim</title>
- <titleabbrev>elim</titleabbrev>
- <para><userinput>elim t pattern using th hyps</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">elim</emphasis> &sterm; &pattern; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para><command>t</command> must inhabit an inductive type and
- <command>th</command> must be an elimination principle for that
- inductive type. If <command>th</command> is omitted the appropriate
- standard elimination principle is chosen.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It proceeds by cases on the values of <command>t</command>,
- according to the elimination principle <command>th</command>.
- The induction predicate is restricted by
- <command>pattern</command>. In particular, if some hypothesis
- is listed in <command>pattern</command>, the hypothesis is
- generalized and cleared before eliminating <command>t</command>
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>It opens one new sequent for each case. The names of
- the new hypotheses are picked by <command>hyps</command>, if
- 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</title>
- <titleabbrev>elimType</titleabbrev>
- <para><userinput>elimType T using th hyps</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para><command>T</command> must be an inductive type.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>TODO (severely bugged now).</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>TODO</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_exact">
- <title>exact</title>
- <titleabbrev>exact</titleabbrev>
- <para><userinput>exact p</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">exact</emphasis> &sterm;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <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>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_exists">
- <title>exists</title>
- <titleabbrev>exists</titleabbrev>
- <para><userinput>exists </userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">exists</emphasis></para>
- </listitem>
- </varlistentry>
- <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>fail</titleabbrev>
- <para><userinput>fail</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">fail</emphasis></para>
- </listitem>
- </varlistentry>
- <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</title>
- <titleabbrev>fold</titleabbrev>
- <para><userinput>fold red t patt</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern;</para>
- </listitem>
- </varlistentry>
- <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 role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">fourier</emphasis></para>
- </listitem>
- </varlistentry>
- <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</title>
- <titleabbrev>fwd</titleabbrev>
- <para><userinput>fwd H as H<subscript>0</subscript> ... H<subscript>n</subscript></userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">as</emphasis> &id; [&id;]…]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para>
- The type of <command>H</command> must be the premise of a
- forward simplification theorem.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>
- This tactic is under development.
- It simplifies the current context by removing
- <command>H</command> using the following methods:
- forward application (by <command>lapply</command>) of a suitable
- simplification theorem, chosen automatically, of which the type
- of <command>H</command> is a premise,
- decomposition (by <command>decompose</command>),
- rewriting (by <command>rewrite</command>).
- <command>H<subscript>0</subscript> ... H<subscript>n</subscript></command>
- are passed to the tactics <command>fwd</command> invokes, as
- names for the premise they introduce.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>
- The ones opened by the tactics <command>fwd</command> invokes.
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
- <sect1 id="tac_generalize">
- <title>generalize</title>
- <titleabbrev>generalize</titleabbrev>
- <para><userinput>generalize patt as H</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;]</para>
- </listitem>
- </varlistentry>
- <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 role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">id</emphasis></para>
- </listitem>
- </varlistentry>
- <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_intro">
- <title>intro</title>
- <titleabbrev>intro</titleabbrev>
- <para><userinput>intro H</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">intro</emphasis> [&id;]</para>
- </listitem>
- </varlistentry>
- <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</title>
- <titleabbrev>intros</titleabbrev>
- <para><userinput>intros hyps</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">intros</emphasis> &intros-spec;</para>
- </listitem>
- </varlistentry>
- <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>