X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Ftacticargs.html;fp=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Ftacticargs.html;h=4896638be1d84cf1e8e0ae4b46fcf91f1e2cc6f3;hb=9d5a0d55e331b348d44b6d50d3d67e62b60a0e18;hp=0000000000000000000000000000000000000000;hpb=7b6ca76a0ed511b288b654729c9758277dbcd352;p=helm.git diff --git a/matita/matita/help/C/html/tacticargs.html b/matita/matita/help/C/html/tacticargs.html new file mode 100644 index 000000000..4896638be --- /dev/null +++ b/matita/matita/help/C/html/tacticargs.html @@ -0,0 +1,94 @@ + +
This section documents the syntax of some recurring arguments for + tactics.
A path locates zero or more subterms of a given term by mimicking the term structure up to:
Occurrences of the subterms to locate that are + represented by %.
Subterms without any occurrence of subterms to locate + that can be represented by ?. +
Warning: the format for a path for a match ⦠with + expression is restricted to: match path + with + [ + _ + â + path + | ⦠+ | + _ + â + path + ] + Its semantics is the following: the n-th + "_ + â + path" branch is matched against the n-th constructor of the + inductive data type. The head λ-abstractions of path are matched + against the corresponding constructor arguments. +
For instance, the path
+ â_,_:?.(? ? % ?)â(? ? ? %)
+ locates at once the subterms
+ x+y
and x*y
in the
+ term âx,y:nat.x+y=1â0=x*y
+ (where the notation A=B
hides the term
+ (eq T A B)
for some type T
).
+
A simple pattern extends paths to locate
+ subterms in a whole sequent. In particular, the pattern
+ { H: p K: q ⢠r }
locates at once all the subterms
+ located by the pattern r
in the conclusion of the
+ sequent and by the patterns p
and
+ q
in the hypotheses H
+ and K
of the sequent.
+
If no list of hypotheses is provided in a simple pattern, no subterm
+ is selected in the hypothesis. If the ⢠p
+ part of the pattern is not provided, no subterm will be matched in the
+ conclusion if at least one hypothesis is provided; otherwise the whole
+ conclusion is selected.
+
Finally, a full pattern is interpreted in three
+ steps. In the first step the match T in
+ part is ignored and a set S of subterms is
+ located as for the case of
+ simple patterns. In the second step the term T
+ is parsed and interpreted in the context of each subterm
+ s â S. In the last term for each
+ s â S the interpreted term T
+ computed in the previous step is looked for. The final set of subterms
+ located by the full pattern is the set of occurrences of
+ the interpreted T
in the subterms s.
+
A full pattern can always be replaced by a simple pattern, + often at the cost of increased verbosity or decreased readability.
Example: the pattern
+ { match x+y in ⢠â_,_:?.(? ? % ?) }
+ locates only the first occurrence of x+y
+ in the sequent x,y: nat ⢠âz,w:nat. (x+y) * (z+w) =
+ z * (x+y) + w * (x+y)
. The corresponding simple pattern
+ is { ⢠â_,_:?.(? ? (? % ?) ?) }
.
+
Every tactic that acts on subterms of the selected sequents have + a pattern argument for uniformity. To automatically generate a simple + pattern:
Select in the current goal the subterms to pass to the + tactic by using the mouse. In order to perform a multiple selection of + subterms, hold the Ctrl key while selecting every subterm after the + first one.
From the contextual menu select "Copy".
From the "Edit" or the contextual menu select + "Paste as pattern"
Reduction kinds are normalization functions that transform a term + to a convertible but simpler one. Each reduction kind can be used both + as a tactic argument and as a stand-alone tactic.
Table 4.15. reduction-kind
reduction-kind | ::= | normalize [nodelta] | Computes the βδιζ-normal form. If nodelta
+ is specified, δ-expansions are not performed. |
 | | | whd [nodelta] | Computes the βδιζ-weak-head normal form. If nodelta
+ is specified, δ-expansions are not performed. |
Table 4.16. auto-params
auto_params | ::= | [nat] [simple_auto_param]⦠+ [by + [sterm⦠| _]] + | The natural number, which defaults to 1, gives a bound to + the depth of the search tree. The terms listed is the only + knowledge base used by automation together with all indexed factual + and equational theorems in the included library. If the list of terms + is empty, only equational theorems and facts in the library are + used. If the list is omitted, it defaults to all indexed theorems + in the library. Finally, if the list is _, + the automation command becomes a macro that is expanded in a new + automation command where _ is replaced with the + list of theorems required to prove the sequent. + |
Table 4.17. simple-auto-param
simple_auto_param | ::= | width=nat | The maximal width of the search tree |
 | | | size=nat | The maximal number of nodes in the proof |
 | | | demod | Simplifies the current sequent using the current set of + equations known to automation + |
 | | | paramod | Try to close the goal performing unit-equality paramodulation + |
 | | | fast_paramod | A bounded version of paramod that is granted to terminate quickly + |
Table 4.18. justification
justification | ::= | using term | Proof term manually provided |
 | | | auto_params | Call automation |