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 |