From 393f6f56c95e12ca7b89181b3868330b0f3292ff Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 11 Jul 2006 17:18:40 +0000 Subject: [PATCH] More documentation. --- matita/help/C/sec_gettingstarted.xml | 4 + matita/help/C/sec_tacticals.xml | 129 ++++++++++++++++++++++++++- 2 files changed, 131 insertions(+), 2 deletions(-) diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml index 8680f4b43..0066449b0 100644 --- a/matita/help/C/sec_gettingstarted.xml +++ b/matita/help/C/sec_gettingstarted.xml @@ -216,6 +216,10 @@ + + The authoring interface + &TODO; + diff --git a/matita/help/C/sec_tacticals.xml b/matita/help/C/sec_tacticals.xml index 981914c9f..bab2ecf64 100644 --- a/matita/help/C/sec_tacticals.xml +++ b/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,6 +242,10 @@ [| &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. @@ -133,6 +253,7 @@ do &nat; &LCFtactical; end + &TODO; @@ -140,6 +261,7 @@ repeat &LCFtactical; end + &TODO; @@ -150,11 +272,13 @@ [| &LCFtactical;]… ] + &TODO; | try &LCFtactical; + &TODO; @@ -165,16 +289,17 @@ [| &LCFtactical;]… ] + &TODO; | (&LCFtactical;) + Used for grouping during parsing.
- &TODO; -- 2.39.2