The original semantics is preserved: the execution of the whole sequence
yields the result expected by the original LCF-like tactical.</para>
</sect1>
+ <sect1 id="proofstatus">
+ <title>The proof status</title>
+ <para>
+ During an interactive proof, the proof status is made of
+ the set of sequents to prove and the partial proof built so far.
+ </para>
+ <para>The partial proof can be <link linkend="aboutproof">inspected</link>
+ on demand in the CIC browser. It will be shown in pseudo-natural language
+ produced on the fly from the proof term.</para>
+ <para>The set of sequents to prove is shown in the notebook of the
+ <link linkend="authoringinterface">authoring interface</link>, in the
+ top-right corner of the main window of Matita. Each tab shows a different
+ sequent, named with a question mark followed by a number. The current
+ role of the sequent, according to the following description, is also
+ shown in the tab tag.
+ </para>
+ <orderedlist>
+ <listitem id="selectedsequents">
+ <para>
+ <emphasis role="bold">Selected sequents</emphasis>
+ (name in boldface, e.g. <emphasis role="bold">?3</emphasis>).
+ The next tactic will be applied to every selected sequent, producing
+ new selected sequents. <link linkend="tacticals">Tacticals</link>
+ such as branching ("<emphasis role="bold">[</emphasis>")
+ or "<emphasis role="bold">focus</emphasis>" can be used
+ to change the set of selected sequents.
+ </para>
+ </listitem>
+ <listitem id="siblingsequents">
+ <para>
+ <emphasis role="bold">Sibling sequents</emphasis>
+ (name prefixed by a vertical bar and their position, e.g.
+ |<subscript>3</subscript>?2). When the set of selected sequents
+ has more than one element, the user can decide to focus in turn on each
+ of them. The branching <link linkend="tacticals">tactical</link>
+ ("<emphasis role="bold">[</emphasis>") selects the first
+ sequent only, marking every previously selected sequent as a sibling
+ sequent. Each sibling sequent is given a different position. The
+ tactical "<emphasis role="bold">2,3:</emphasis>" can be used to
+ select one or more sibling sequents, different from the one proposed,
+ according to their position. Once the user starts to work on the
+ selected sibling sequents it becomes impossible to select a new
+ set of siblings until the ("<emphasis role="bold">|</emphasis>")
+ tactical is used to end work on the current one.
+ </para>
+ </listitem>
+ <listitem id="solvedsequents">
+ <para>
+ <emphasis role="bold">Automatically solved sibling sequents</emphasis>
+ (name strokethrough, e.g. |<subscript>3</subscript><emphasis role="strikethrough">?2</emphasis>).
+ Sometimes a tactic can close by side effects a sibling sequent the
+ user has not selected yet. The sequent is left in the automatically
+ solved status in order for the user to explicitly accept
+ (using the "<emphasis role="bold">skip</emphasis>"
+ <link linkend="tacticals">tactical</link>) the automatic
+ instantiation in the proof script. This way the correspondence between
+ the number of branches in the proof script and the number of sequents
+ generated in the proof is preserved.
+ </para>
+ </listitem>
+ </orderedlist>
+ </sect1>
<sect1 id="tacticals">
<title>Tacticals</title>
<table frame="topbot" rowsep="0" colsep="0" role="grammar">
<entry id="grammar.proofstep">&proofstep;</entry>
<entry>::=</entry>
<entry>&LCFtactical;</entry>
+ <entry>The tactical is applied to each
+ <link linkend="selectedsequents">selected sequent</link>.
+ Each new sequent becomes a selected sequent.</entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">.</emphasis></entry>
+ <entry>The first
+ <link linkend="selectedsequents">selected sequent</link> becomes
+ the only one selected. All the remaining previously selected sequents
+ are proposed to the user one at a time when the next
+ "<emphasis role="bold">.</emphasis>" is used.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">;</emphasis></entry>
+ <entry>Nothing changes. Use this proof step as a separator in
+ concrete syntax.</entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">[</emphasis></entry>
+ <entry>Every <link linkend="selectedsequents">selected sequent</link>
+ becomes a <link linkend="siblingsequents">sibling sequent</link>
+ that constitute a branch in the proof.
+ Moreover, the first sequent is also selected.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">|</emphasis></entry>
+ <entry>Stop working on the current branch of the innermost branching
+ proof.
+ The sibling branches become the <link linkend="siblingsequents">sibling
+ sequents</link> and the first one is also selected.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry>&nat;[<emphasis role="bold">,</emphasis>&nat;]…<emphasis role="bold">:</emphasis></entry>
+ <entry>The <link linkend="siblingsequents">sibling sequents</link>
+ specified by the user become the next
+ <link linkend="selectedsequents">selected sequents</link>.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">*:</emphasis></entry>
+ <entry>Every sibling branch not considered yet in the innermost
+ branching proof becomes a
+ <link linkend="selectedsequents">selected sequent</link>.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">skip</emphasis></entry>
+ <entry>Accept the automatically provided instantiation (not shown
+ to the user) for the currently selected
+ <link linkend="solvedsequents">automatically closed sibling sequent</link>.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">]</emphasis></entry>
+ <entry>Stop analyzing branches for the innermost branching proof.
+ Every sequent opened during the branching proof and not closed yet
+ becomes a <link linkend="selectedsequents">selected sequent</link>.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">focus</emphasis> &nat; [&nat;]…</entry>
+ <entry><emphasis role="bold">focus</emphasis> &nat; [&nat;]…</entry>
+ <entry>
+ Selects the sequents specified by the user. The selected sequents
+ must be completely closed (no new sequents left open) before doing an
+ "<emphasis role="bold">unfocus</emphasis> that restores
+ the current set of sibling branches.
+ </entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">unfocus</emphasis></entry>
+ <entry>
+ Used to match the innermost
+ "<emphasis role="bold">focus</emphasis>" tactical
+ when all the sequents selected by it have been closed.
+ Until "<emphasis role="bold">unfocus</emphasis>" is
+ performed, it is not possible to progress in the rest of the
+ proof.
+ </entry>
</row>
</tbody>
</tgroup>
<entry id="grammar.LCFtactical">&LCFtactical;</entry>
<entry>::=</entry>
<entry>&tactic;</entry>
+ <entry>Applies the specified tactic.</entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry>&LCFtactical; <emphasis role="bold">;</emphasis> &LCFtactical;</entry>
+ <entry>Applies the first tactical first and the second tactical
+ to each sequent opened by the first one.</entry>
</row>
<row>
<entry/>
[<emphasis role="bold">|</emphasis> &LCFtactical;]…
<emphasis role="bold">]</emphasis>
</entry>
+ <entry>Applies the first tactical first and each tactical in the
+ list of tacticals to the corresponding sequent opened by the
+ first one. The number of tacticals provided in the list must be
+ equal to the number of sequents opened by the first tactical.</entry>
</row>
<row>
<entry/>
<entry><emphasis role="bold">do</emphasis> &nat;
&LCFtactical; <emphasis role="bold">end</emphasis>
</entry>
+ <entry>&TODO;</entry>
</row>
<row>
<entry/>
<entry><emphasis role="bold">repeat</emphasis>
&LCFtactical; <emphasis role="bold">end</emphasis>
</entry>
+ <entry>&TODO;</entry>
</row>
<row>
<entry/>
[<emphasis role="bold">|</emphasis> &LCFtactical;]…
<emphasis role="bold">]</emphasis>
</entry>
+ <entry>&TODO;</entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">try</emphasis> &LCFtactical;</entry>
+ <entry>&TODO;</entry>
</row>
<row>
<entry/>
[<emphasis role="bold">|</emphasis> &LCFtactical;]…
<emphasis role="bold">]</emphasis>
</entry>
+ <entry>&TODO;</entry>
</row>
<row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">(</emphasis>&LCFtactical;<emphasis role="bold">)</emphasis></entry>
+ <entry>Used for grouping during parsing.</entry>
</row>
</tbody>
</tgroup>
</table>
- <para>&TODO;</para>
</sect1>
</chapter>
projects / helm.git / commitdiff