mathlib documentation

core / init.meta.match_tactic

source
meta structure tactic.pattern  :
Type

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 (umetas : list level) (emetas : list expr) (target : expr) (uoutput : list level) (eoutput : 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:

  1. Convert all metavariables in target to temporary metavariables.
  2. For each item in umetas amd emetas, create a temporary metavariable and replace each instance of the item in target with a temporary metavariable
  3. Replace these instances in uoutput and eoutput too.
  4. 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 (p : tactic.pattern) (e : expr) (m : 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 (p : 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 (p : pexpr) (e : expr) (m : 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 (p : pexpr) (e : expr) (m : 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 (p : pexpr) (m : tactic.transparency := reducible) :
tactic (list expr)

Match the main goal target.

source
meta def tactic.match_target_subexpr (p : pexpr) (m : tactic.transparency := reducible) :
tactic (list expr)

Match a subterm in the main goal target.

source
meta def tactic.match_hypothesis (p : pexpr) (m : tactic.transparency := reducible) :
tactic (expr × list expr)

Match hypothesis in the main goal target. The result is pair (hypothesis, substitution).

source
@[protected, instance]
meta def tactic.pattern.has_to_tactic_format  :
has_to_tactic_format tactic.pattern