Tactic arguments

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

intros-spec

Table 4.13. intros-spec

intros-spec::=[nat] [([id]…)] 

The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses.

pattern

Table 4.14. pattern

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

Table 4.15. 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 in 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 ⊢ in 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-kind

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.16. reduction-kind

reduction-kind::=normalizeComputes the βδιζ-normal form
 |simplifyComputes a form supposed to be simpler
 |unfold [sterm]δ-reduces the constant or variable if specified, or that in head position
 |whdComputes the βδιζ-weak-head normal form

auto-params

Table 4.17. auto-params

auto_params::=[simple_auto_param]… [by term [,term]…]  

Table 4.18. simple-auto-param

simple_auto_param::=depth=natGive a bound to the depth of the search tree
 |width=natThe maximal width of the search tree
 |librarySearch everywhere (not only in included files)
 |typeTry to close also goals of sort Type, otherwise only goals living in sort Prop are attacked.
 |paramodulationTry to close the goal performing unit-equality paramodulation
 |size=natThe maximal number of nodes in the proof
 |timeout=natTimeout in seconds

justification

Table 4.19. justification

justification::=using termProof term manually provided
 |auto_paramsCall automation