mathlib documentation

core.​init.​meta.​match_tactic

core.​init.​meta.​match_tactic

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
}

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.

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.

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

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.

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

Match a subterm in the main goal target.

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