+ <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 (T<subscript>1</subscript> ... T<subscript>n</subscript>)
+ H 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">(</emphasis>
+ &id;…
+ <emphasis role="bold">)</emphasis>]
+ [&id;]
+ [<emphasis role="bold">as</emphasis> &id;…]
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>
+ <command>H</command> must inhabit one inductive type among
+ <command>
+ T<subscript>1</subscript> ... T<subscript>n</subscript>
+ </command>
+ and the types of a predefined list.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>
+ Runs <command>
+ elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
+ </command>, clears <command>H</command> and tries to run itself
+ recursively on each new identifier introduced by
+ <command>elim</command> in the opened sequents.
+ If <command>H</command> is not provided tries this operation on
+ each premise in the current context.
+ </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</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">demodulate</emphasis></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 using th hyps</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">elim</emphasis> &sterm; [<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>.
+ </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">