X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tacticals.xml;fp=matita%2Fhelp%2FC%2Fsec_tacticals.xml;h=2f84ae73690c88b25e1b8f073c405d81f8262035;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/help/C/sec_tacticals.xml b/matita/help/C/sec_tacticals.xml new file mode 100644 index 000000000..2f84ae736 --- /dev/null +++ b/matita/help/C/sec_tacticals.xml @@ -0,0 +1,305 @@ + + + + Tacticals + + Interactive proofs and definitions + + An interactive definition is started by giving a + definition command omitting + the definiens. + An interactive proof is started by using one of the + proof commands omitting + an explicit proof term. + + An interactive proof or definition can and must be terminated by + a qed command when no more sequents are + left to prove. Between the command that starts the interactive session and + the qed command the user must provide a procedural proof script made + of tactics structured by means of + tacticals. + In the tradition of the LCF system, tacticals can be considered + higher order tactics. Their syntax is structured and they are executed + atomically. On the contrary, in Matita the syntax of several tacticals is + destructured into a sequence of tokens and tactics in such a way that is + is possible to stop execution after every single token or tactic. + 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 + + proof script + + + + &proofscript; + ::= + &proofstep; [&proofstep;]… + + + +
+ Every proof step can be immediately executed. + + proof steps + + + + &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;]… + + 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. + + + + +
+ + tactics and LCF tacticals + + + + &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. + + + + | + &LCFtactical; + [ + [&LCFtactical;] + [| &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; + + &TODO; + + + + | + repeat + &LCFtactical; + + &TODO; + + + + | + + first [ + [&LCFtactical;] + [| &LCFtactical;]… + ] + + &TODO; + + + + | + try &LCFtactical; + &TODO; + + + + | + + solve [ + [&LCFtactical;] + [| &LCFtactical;]… + ] + + &TODO; + + + + | + (&LCFtactical;) + Used for grouping during parsing. + + + +
+ + +