Tactic arguments

This section documents the syntax of some recurring arguments for tactics.


Table 4.13. pattern

pattern::=in [id[: path]]… [ path]];simple pattern
 |in match path [in [id[: path]]… [ path]];full pattern

Table 4.14. path

path::=〈〈any sterm without occurrences of Set, Prop, CProp, Type, id, uri and user provided notation; however, % is now an additional production for sterm〉〉

A path locates zero or more subterms of a given term by mimicking the term structure up to:

  1. Occurrences of the subterms to locate that are represented by %.

  2. Subterms without any occurrence of subterms to locate that can be represented by ?.

Warning: the format for a path for a matchwith 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:

  1. 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.

  2. From the contextual menu select "Copy".

  3. 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=natThe maximal width of the search tree
 |size=natThe maximal number of nodes in the proof
 |demodSimplifies the current sequent using the current set of equations known to automation
 |paramodTry to close the goal performing unit-equality paramodulation
 |fast_paramodA bounded version of paramod that is granted to terminate quickly