- <sect1 id="tac_suppose">
- <title>suppose</title>
- <titleabbrev>suppose</titleabbrev>
- <para><userinput>suppose t(x) </userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
- <emphasis role="bold">) </emphasis> [ that is equivalent to &term; ]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para> Da Fare </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> Da Fare </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_bydone">
- <title>by done</title>
- <titleabbrev>by done</titleabbrev>
- <para><userinput>by [ t | _ ] done</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold"> done </emphasis></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>The term can be omitted with a "_", the running term will come found automatically. </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It closes the current sequent by applying <command>t</command>, taht it can be one under proof or the main proof.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_weneedtoprove">
- <title> we need to prove</title>
- <titleabbrev>we need to prove</titleabbrev>
- <para><userinput>we need to prove t [(id)] [or equivalent t]</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we need to prove</emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para> Da Fare </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> Da Fare </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_weproceedbyinduction">
- <title> we proceed by induction</title>
- <titleabbrev>we proceed by induction</titleabbrev>
- <para><userinput>we proceed by induction on t to prove th</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>t</command> must inhabit an inductive type and <command>th</command> must be an elimination principle for that inductive type.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It proceed on the values of <command>t</command>.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>It opens one new sequent to demonstrate.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_weproceedbycases">
- <title>we proceed by cases</title>
- <titleabbrev>we proceed by cases</titleabbrev>
- <para><userinput>we proceed by cases on t to prove t</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we proceed by cases on </emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para> Da Fare </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> Da Fare </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-