X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tacticals.xml;h=2f84ae73690c88b25e1b8f073c405d81f8262035;hb=5978b976f9e1a2679e2b4ecc3c9984afdf2d5e11;hp=981914c9fc073fe8b2ef4eb7dbc296ec097f590f;hpb=398fc6acced3d63a7dfa706fb11e7e8177576c7b;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tacticals.xml b/helm/software/matita/help/C/sec_tacticals.xml
index 981914c9f..2f84ae736 100644
--- a/helm/software/matita/help/C/sec_tacticals.xml
+++ b/helm/software/matita/help/C/sec_tacticals.xml
@@ -26,6 +26,68 @@
The original semantics is preserved: the execution of the whole sequence
yields the result expected by the original LCF-like tactical.
+
+ The proof status
+
+ During an interactive proof, the proof status is made of
+ the set of sequents to prove and the partial proof built so far.
+
+ The partial proof can be inspected
+ on demand in the CIC browser. It will be shown in pseudo-natural language
+ produced on the fly from the proof term.
+ The set of sequents to prove is shown in the notebook of the
+ authoring interface, 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.
+
+
+
+
+ Selected sequents
+ (name in boldface, e.g. ?3).
+ The next tactic will be applied to every selected sequent, producing
+ new selected sequents. Tacticals
+ such as branching ("[")
+ or "focus" can be used
+ to change the set of selected sequents.
+
+
+
+
+ Sibling sequents
+ (name prefixed by a vertical bar and their position, e.g.
+ |3?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 tactical
+ ("[") selects the first
+ sequent only, marking every previously selected sequent as a sibling
+ sequent. Each sibling sequent is given a different position. The
+ tactical "2,3:" 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 ("|")
+ tactical is used to end work on the current one.
+
+
+
+
+ Automatically solved sibling sequents
+ (name strokethrough, e.g. |3?2).
+ 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 "skip"
+ tactical) 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.
+
+
+
+ Tacticals
@@ -49,56 +111,107 @@
&proofstep;::=&LCFtactical;
+ The tactical is applied to each
+ selected sequent.
+ Each new sequent becomes a selected sequent.|.
+ The first
+ selected sequent becomes
+ the only one selected. All the remaining previously selected sequents
+ are proposed to the user one at a time when the next
+ "." is used.
+ |;
+ Nothing changes. Use this proof step as a separator in
+ concrete syntax.|[
+ Every selected sequent
+ becomes a sibling sequent
+ that constitute a branch in the proof.
+ Moreover, the first sequent is also selected.
+ ||
+ Stop working on the current branch of the innermost branching
+ proof.
+ The sibling branches become the sibling
+ sequents and the first one is also selected.
+ |&nat;[,&nat;]â¦:
+ The sibling sequents
+ specified by the user become the next
+ selected sequents.
+ |*:
+ Every sibling branch not considered yet in the innermost
+ branching proof becomes a
+ selected sequent.
+ |skip
+ Accept the automatically provided instantiation (not shown
+ to the user) for the currently selected
+ automatically closed sibling sequent.
+ |]
+ Stop analyzing branches for the innermost branching proof.
+ Every sequent opened during the branching proof and not closed yet
+ becomes a selected sequent.
+ |
- focus &nat; [&nat;]â¦
+ focus &nat; [&nat;]â¦
+
+ Selects the sequents specified by the user. The selected sequents
+ must be completely closed (no new sequents left open) before doing an
+ "unfocus that restores
+ the current set of sibling branches.
+ |unfocus
+
+ Used to match the innermost
+ "focus" tactical
+ when all the sequents selected by it have been closed.
+ Until "unfocus" is
+ performed, it is not possible to progress in the rest of the
+ proof.
+
@@ -111,11 +224,14 @@
&LCFtactical;::=&tactic;
+ Applies the specified tactic.|&LCFtactical; ; &LCFtactical;
+ Applies the first tactical first and the second tactical
+ to each sequent opened by the first one.
@@ -126,20 +242,26 @@
[| &LCFtactical;]â¦
]
+ 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.|do &nat;
- &LCFtactical; end
+ &LCFtactical;
+ &TODO;|repeat
- &LCFtactical; end
+ &LCFtactical;
+ &TODO;
@@ -150,11 +272,13 @@
[| &LCFtactical;]â¦
]
+ &TODO;|try &LCFtactical;
+ &TODO;
@@ -165,16 +289,17 @@
[| &LCFtactical;]â¦
]
+ &TODO;|(&LCFtactical;)
+ Used for grouping during parsing.