Matching expressions with leading binders #
This module defines a family of tactics for matching expressions with leading Π
or λ binders, similar to Core's
mk_local_pis. They all iterate over an
expression, processing one leading binder at a time. The bound variable is
replaced by either a fresh local constant or a fresh metavariable in the binder
body, 'opening' the binder. We then recurse into this new body. This scheme is
Based on these general tactics, we define many variations of this recipe:
open_pisopens all leading Π binders and replaces them with fresh local constants. This is defined in core.
open_lambdasopens leading λ binders instead. Example:
open_lambdas `(λ (x : X) (y : Y), f x y) = ([`(_fresh.1), `(_fresh.2)], `(f _fresh.1 _fresh.2))
_fresh.2are fresh local constants (with types
Y, respectively). The second component of the pair is the lambda body with
open_pis_metasopens all leading Π binders and replaces them with fresh metavariables (instead of local constants).
open_n_pisopens only the first
nleading Π binders and fails if there are not at least
nleading binders. Example:
open_n_pis `(Π (x : X) (y : Y), P x y) 1 = ([`(_fresh.1)], `(Π (y : Y), P _fresh.1 y))
open_lambdas_whnfnormalises the input expression each time before trying to match a binder. Example:
open_lambdas_whnf `(let f := λ (x : X), g x y in f) = ([`(_fresh.1)], `(g _fresh.1 y))
Any combination of these features is also provided, e.g.
nλ binders up to normalisation, replacing them with fresh metavariables.
open_* functions are commonly used like this:
Special-purpose tactics #
The following tactics are variations of the 'opening binders' theme that do not quite fit in the above scheme.