mathlib docs: core.init.meta.match

meta structure tactic.pattern :

Type

target : expr
uoutput : list level
moutput : list expr
nuvars : ℕ
nmvars : ℕ

A pattern is an expression target containing temporary metavariables. A pattern also contains a list of outputs which also depend on these temporary metavariables. When we run match p e, the system will match p.target with e and assign the temporary metavariables. It then returns the outputs with the assigned variables.

Fields

target Term to match. Contains temporary metavariables.
uoutput List of universes that are returned on a successful match.
moutput List of expressions that are returned on a successful match.
nuvars Number of (temporary) universe metavariables in this pattern.
nmvars Number of (temporary) metavariables in this pattern.

Example

The pattern for list.cons h t returning h and t would be

{ target  := `(@list.cons ?x_0 ?x_1 ?x_2),
  uoutput := [],
  moutput := [?x_1,?x_2],
  nuvars  := 0,
  nmvars  := 3
}

source

meta constant tactic.mk_pattern :

list level → list expr → expr → list level → list expr → tactic tactic.pattern

mk_pattern umetas emetas target uoutput eoutput creates a new pattern. The arguments are

umetas a list of level params to be replaced with temporary universe metavariables.
emetas a list of local constants to be replaced with temporary metavariables.
target the expression to be matched.
uoutput a list of levels to return upon matching. Fails if this depends on metavariables.
eoutput a list of expressions to return upon matching. Fails if this depends on metavariables.

The procedure is as follows:

Convert all metavariables in target to temporary metavariables.
For each item in umetas amd emetas, create a temporary metavariable and replace each instance of the item in target with a temporary metavariable
Replace these instances in uoutput and eoutput too.
Return these replaced versions as a pattern.

Example

Let h,t be exprs with types α and list α respectively. Then mk_pattern [] [α,h,t](@list.cons α h t) [] [h,t]wouldmatch_pattern` against any expr which is a list.cons constructor and return the head and tail arguments.

source

meta constant tactic.match_pattern :

tactic.pattern → expr → (tactic.transparency := tactic.transparency.reducible) → tactic (list level × list expr)

mk_pattern p e m matches (pattern.target p) and e using transparency m. If the matching is successful, then return the instantiation of pattern.output p. The tactic fails if not all (temporary) meta-variables are assigned.

source

meta def tactic.pexpr_to_pattern :

pexpr → tactic tactic.pattern

Given a pre-term of the form λ x₁ ... xₙ, t[x₁, ..., xₙ], converts it into the pattern t[?x₁, ..., ?xₙ] with outputs [?x₁, ..., ?xₙ]

source

meta def tactic.match_expr :

pexpr → expr → (tactic.transparency := tactic.transparency.reducible) → tactic (list expr)

Convert pre-term into a pattern and try to match e. Given p of the form λ x₁ ... xₙ, t[x₁, ..., xₙ], a successful match will produce a list of length n.

source

meta def tactic.match_subexpr :

pexpr → expr → (tactic.transparency := tactic.transparency.reducible) → tactic (list expr)

Similar to match_expr, but it tries to match a subexpression of e. Remark: the procedure does not go inside binders.

source

meta def tactic.match_target :

pexpr → (tactic.transparency := tactic.transparency.reducible) → tactic (list expr)

Match the main goal target.

source

meta def tactic.match_target_subexpr :

pexpr → (tactic.transparency := tactic.transparency.reducible) → tactic (list expr)

Match a subterm in the main goal target.