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
implemented by tactic.open_binders and tactic.open_n_binders.
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 core'sopen_pis.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.1and_fresh.2are fresh local constants (with typesXandY, respectively). The second component of the pair is the lambda body withxreplaced by_fresh.1andyreplaced by_fresh.2.open_pis_metasopens all leading Π binders and replaces them with fresh metavariables (instead of local constants).open_n_pisopens only the firstnleading Π binders and fails if there are not at leastnleading 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.
open_n_lambdas_metas_whnfto opennλ binders up to normalisation, replacing them with fresh metavariables.
The open_* functions are commonly used like this:
- Open (some of) the binders of an expression
e, producing local constantslcsand the 'body'e'ofe. - Process
e'in some way. - Reconstruct the binders using
tactic.pisortactic.lambdas, which Π/λ-bind thelcsine'. This reverts the effect ofopen_*.
get_binder do_whnf pi_or_lambda e matches e of the form λ x, e' or
Π x, e. Returns information about the leading binder (its name, binder_info,
type and body), or none if e does not start with a binder.
If do_whnf = some (md, unfold_ginductive), then e is weak head normalised
with transparency md before matching on it. unfold_ginductive controls
whether constructors of generalised inductive data types are unfolded during
normalisation.
If pi_or_lambda is tt, we match a leading Π binder; otherwise a leading λ
binder.
mk_binder_replacement local_or_meta b creates an expression that can be used
to replace the binder b. If local_or_meta is true, we create a fresh local
constant with b's display name, binder_info and type; otherwise a fresh
metavariable with b's type.
open_binders is a generalisation of functions like open_pis,
mk_meta_lambdas etc. open_binders do_whnf pis_or_lamdas local_or_metas e
proceeds as follows:
- Match a leading λ or Π binder using
get_binder do_whnf pis_or_lambdas. Seeget_binderfor details. Returneunchanged (and an empty list) ifedoes not start with a λ/Π. - Construct a replacement for the bound variable using
mk_binder_replacement locals_or_metas. Seemk_binder_replacementfor details. Replace the bound variable with this replacement in the binder body. - Recurse into the binder body.
Returns the constructed replacement expressions and e without its leading
binders.
open_n_binders do_whnf pis_or_lambdas local_or_metas e n is like
open_binders do_whnf pis_or_lambdas local_or_metas e, but it matches exactly n
leading Π/λ binders of e. If e does not start with at least n Π/λ binders,
(after normalisation, if do_whnf is given), the tactic fails.
open_pis e instantiates all leading Π binders of e with fresh local
constants. Returns the local constants and the remainder of e. This is an
alias for tactic.mk_local_pis.
open_pis_whnf e md unfold_ginductive instantiates all leading Π binders of e
with fresh local constants. The leading Π binders of e are matched up to
normalisation with transparency md. unfold_ginductive determines whether
constructors of generalised inductive types are unfolded during normalisation.
This is open_pis up to normalisation.
open_pis_metas_whnf e md unfold_ginductive instantiates all leading Π binders
of e with fresh metavariables. The leading Π binders of e are matched up to
normalisation with transparency md. unfold_ginductive determines whether
constructors of generalised inductive types are unfolded during normalisation.
This is open_pis_metas up to normalisation.
open_n_pis_whnf e n md unfold_ginductive instantiates the first n Π binders
of e with fresh local constants. The leading Π binders of e are matched up
to normalisation with transparency md. unfold_ginductive determines whether
constructors of generalised inductive types are unfolded during normalisation.
This is open_pis_whnf but restricted to n binders.
open_n_pis_metas_whnf e n md unfold_ginductive instantiates the first n Π
binders of e with fresh metavariables. The leading Π binders of e are
matched up to normalisation with transparency md. unfold_ginductive
determines whether constructors of generalised inductive types are unfolded
during normalisation. This is open_pis_metas_whnf but restricted to n
binders.
get_pi_binders e instantiates all leading Π binders of e with fresh local
constants (like open_pis). Returns the remainder of e and information about
the binders that were instantiated (but not the new local constants). See also
expr.pi_binders (which produces open terms).
get_pi_binders_nondep e instantiates all leading Π binders of e with fresh
local constants (like open_pis). Returns the remainder of e and information
about the nondependent binders that were instantiated (but not the new local
constants). A nondependent binder is one that does not appear later in the
expression. Also returns the index of each returned binder (starting at 0).
open_n_lambdas e n instantiates the first n λ binders of e with fresh
local constants. Returns the new local constants and the remainder of e. Fails
if e does not start with at least n λ binders. This is open_lambdas but
restricted to the first n binders.
open_n_lambdas_metas e n instantiates the first n λ binders of e with
fresh metavariables. Returns the new metavariables and the remainder of e.
Fails if e does not start with at least n λ binders. This is
open_lambdas_metas but restricted to the first n binders.
open_lambdas_whnf e md unfold_ginductive instantiates all leading λ binders of
e with fresh local constants. The leading λ binders of e are matched up to
normalisation with transparency md. unfold_ginductive determines whether
constructors of generalised inductive types are unfolded during normalisation.
This is open_lambdas up to normalisation.
open_lambdas_metas_whnf e md unfold_ginductive instantiates all leading λ
binders of e with fresh metavariables. The leading λ binders of e are
matched up to normalisation with transparency md. unfold_ginductive
determines whether constructors of generalised inductive types are unfolded
during normalisation. This is open_lambdas_metas up to normalisation.
open_n_lambdas_whnf e md unfold_ginductive instantiates the first n λ
binders of e with fresh local constants. The λ binders are matched up to
normalisation with transparency md. unfold_ginductive determines whether
constructors of generalised inductive types are unfolded during normalisation.
Fails if e does not start with n λ binders (after normalisation). This is
open_n_lambdas up to normalisation.
open_n_lambdas_metas_whnf e md unfold_ginductive instantiates the first n λ
binders of e with fresh metavariables. The λ binders are matched up to
normalisation with transparency md. unfold_ginductive determines whether
constructors of generalised inductive types are unfolded during normalisation.
Fails if e does not start with n λ binders (after normalisation). This is
open_n_lambdas_metas up to normalisation.