Matita Home

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

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

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`

`x*y`

`∀x,y:nat.x+y=1→0=x*y`

`A=B`

`(eq T A B)`

`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`

`p`

`q`

`H`

`K`

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

`T`

`T`

`T`

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`

```
x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) =
z * (x+y) + w * (x+y)
```

`⊢ ∀_,_:?.(? ? (? % ?) ?)`

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

reduction-kind | ::= | normalize | Computes the βδιζ-normal form |

| | simplify | Computes a form supposed to be simpler | |

| | unfold [sterm] | δ-reduces the constant or variable if specified, or that in head position | |

| | whd | Computes the βδιζ-weak-head normal form |

**Table 4.18. simple-auto-param**

simple_auto_param | ::= | depth=nat | Give a bound to the depth of the search tree |

| | width=nat | The maximal width of the search tree | |

| | library | Search everywhere (not only in included files) | |

| | type | Try to close also goals of sort Type, otherwise only goals living in sort Prop are attacked. | |

| | paramodulation | Try to close the goal performing unit-equality paramodulation | |

| | size=nat | The maximal number of nodes in the proof | |

| | timeout=nat | Timeout in seconds |

**Table 4.19. justification**

justification | ::= | using term | Proof term manually provided |

| | auto_params | Call automation |