From: Claudio Sacerdoti Coen Date: Fri, 30 Jun 2006 16:39:28 +0000 (+0000) Subject: Documentation of tinycals started. X-Git-Tag: make_still_working~7115 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=398fc6acced3d63a7dfa706fb11e7e8177576c7b;p=helm.git Documentation of tinycals started. --- diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index a20663fec..98d6489f3 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -8,8 +8,8 @@ - + @@ -42,6 +42,10 @@ pattern"> reduction-kind"> path"> + proof-script"> + proof-step"> + tactic"> + LCF-tactical"> ]> @@ -118,8 +122,8 @@ &gettingstarted; &terms; &usernotation; -&tactics; &tacticals; +&tactics; &othercommands; &license; diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml index b4a6c8007..243960cf9 100644 --- a/helm/software/matita/help/C/sec_commands.xml +++ b/helm/software/matita/help/C/sec_commands.xml @@ -8,5 +8,9 @@ &TODO; + + Qed + &TODO; + diff --git a/helm/software/matita/help/C/sec_tacticals.xml b/helm/software/matita/help/C/sec_tacticals.xml index ea863605f..981914c9f 100644 --- a/helm/software/matita/help/C/sec_tacticals.xml +++ b/helm/software/matita/help/C/sec_tacticals.xml @@ -3,10 +3,178 @@ Tacticals - Introduction + Interactive proofs and definitions - &TODO; + 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. + + + Tacticals + + proof script + + + + &proofscript; + ::= + &proofstep; [&proofstep;]… + + + +
+ Every proof step can be immediately executed. + + proof steps + + + + &proofstep; + ::= + &LCFtactical; + + + + | + . + + + + | + ; + + + + | + [ + + + + | + | + + + + | + &nat;[,&nat;]…: + + + + | + *: + + + + | + skip + + + + | + ] + + + + | + focus &nat; [&nat;]… + + + + | + unfocus + + + +
+ + tactics and LCF tacticals + + + + &LCFtactical; + ::= + &tactic; + + + + | + &LCFtactical; ; &LCFtactical; + + + + | + &LCFtactical; + [ + [&LCFtactical;] + [| &LCFtactical;]… + ] + + + + + | + do &nat; + &LCFtactical; end + + + + + | + repeat + &LCFtactical; end + + + + + | + + first [ + [&LCFtactical;] + [| &LCFtactical;]… + ] + + + + + | + try &LCFtactical; + + + + | + + solve [ + [&LCFtactical;] + [| &LCFtactical;]… + ] + + + + + | + (&LCFtactical;) + + + +
+ &TODO; diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml index 58fd32afd..b41ae79eb 100644 --- a/helm/software/matita/help/C/tactic_quickref.xml +++ b/helm/software/matita/help/C/tactic_quickref.xml @@ -1,125 +1,184 @@ - - - absurd sterm - - - apply sterm - - - - - assumption - - - - - auto [depth=nat] [width=nat] [paramodulation] [full] - - - change pattern with sterm - - - + + tactics + + + + &tactic; + ::= + absurd sterm + + + + | + apply sterm + + + + | + + + assumption + + + + + + | + auto [depth=nat] [width=nat] [paramodulation] [full] + + + + | + change pattern with sterm + + + + | + clear id [id…] - - - - clearbody id - - - constructor nat - - - - - contradiction - - - - - cut sterm [as id] - - - + + + + + | + clearbody id + + + + | + constructor nat + + + + | + + + contradiction + + + + + + | + cut sterm [as id] + + + + | + decompose [( id… )] [id] [as id…] - - - - - - demodulate - - - - - discriminate sterm - - - elim sterm [using sterm] intros-spec - - - elimType sterm [using sterm] intros-spec - - - exact sterm - - - - - exists - - - - - - - fail - - - - - fold reduction-kind sterm pattern - - - - - fourier - - - - - fwd id [as id [id]…] - - - generalize pattern [as id] - - - - - id - - - - - injection sterm - - - intro [id] - - - intros intros-spec - - - inversion sterm - - - + + + + + | + + + demodulate + + + + + + | + discriminate sterm + + + + | + elim sterm [using sterm] intros-spec + + + + | + elimType sterm [using sterm] intros-spec + + + + | + exact sterm + + + + | + + + exists + + + + + + | + + + fail + + + + + + | + fold reduction-kind sterm pattern + + + + | + + + fourier + + + + + + | + fwd id [as id [id]…] + + + + | + generalize pattern [as id] + + + + | + + + id + + + + + + | + injection sterm + + + + | + intro [id] + + + + | + intros intros-spec + + + + | + inversion sterm + + + + | + lapply [linear] [depth=nat] @@ -129,78 +188,112 @@ [,sterm…] ] [as id] - - - - - - left - - - - - letin id ≝ sterm - - - normalize pattern - - - paramodulation pattern - - - reduce pattern - - - - - reflexivity - - - - - replace pattern with sterm - - - rewrite [<|>] sterm pattern - - - - - right - - - - - - - ring - - - - - simplify pattern - - - - - split - - - - - - - symmetry - - - - - transitivity sterm - - - unfold [sterm] pattern - - - whd pattern - - + + + + + | + + + left + + + + + + | + letin id ≝ sterm + + + + | + normalize pattern + + + + | + paramodulation pattern + + + + | + reduce pattern + + + + | + + + reflexivity + + + + + + | + replace pattern with sterm + + + + | + rewrite [<|>] sterm pattern + + + + | + + + right + + + + + + | + + + ring + + + + + + | + simplify pattern + + + + | + + + split + + + + + + | + + + symmetry + + + + + + | + transitivity sterm + + + + | + unfold [sterm] pattern + + + + | + whd pattern + + + +
diff --git a/helm/software/matita/help/C/xsl/tactic_quickref.xsl b/helm/software/matita/help/C/xsl/tactic_quickref.xsl index fa9c034fc..42e435740 100644 --- a/helm/software/matita/help/C/xsl/tactic_quickref.xsl +++ b/helm/software/matita/help/C/xsl/tactic_quickref.xsl @@ -8,11 +8,16 @@ /> - - - - - + + tactics + + + + + + + +
@@ -21,8 +26,26 @@ - - + + + + + grammar.tactic + &tactic; + + + + + + + ::= + + + | + + + + @@ -42,8 +65,8 @@ - - + +