mathlib3

588e46c6 - feat(tactic/*,meta/expr): refactor and extend binder matching functions (#3830)

feat(tactic/*,meta/expr): refactor and extend binder matching functions (#3830) This PR deals with meta functions that deconstruct expressions starting with pi or lambda binders. Core defines `mk_local_pis` to deconstruct pi binders and `tactic.core` used to contain some ad-hoc variations of its functionality. This PR unifies all these variations and adds several more, for both pi and lambda binders. Specifically: - We remove `mk_local_pis_whnf`. Use `whnf e md >>= mk_local_pis` instead. Note: we reuse the name for another function with different semantics; see below. - We add `mk_{meta,local}_{pis,lambdas}`, `mk_{meta,local}_{pis,lambdas}n`, `mk_{meta,local}_{pis,lambdas}_whnf`, `mk_{meta,local}_{pis,lambdas}n_whnf`. These can all be used to 'open' a pi or lambda binder. The binder is instantiated with a fresh local for the `local` variants and a fresh metavariable for the `meta` variants. The `whnf` variants normalise the input expression before checking for leading binders. The `{pis,lambdas}n` variants match a given number of leading binders. Some of these functions were already defined, but we now implement them in terms of a new function, `mk_binders`, which abstracts over the common functionality. - We rename `get_pi_binders_dep` to `get_pi_binders_nondep`. This function returns the nondependent binders, so the old name was misleading. - We add `expr.match_<C>` for every constructor `C` of `expr`. `match_pi` and `match_lam` are needed to implement the `mk_*` functions; the other functions are added for completeness. - (Bonus) We add `get_app_fn_args_whnf` and `get_app_fn_whnf`. These are variants of `get_app_fn_args` and `get_app_fn`, respectively, which normalise the input expression as necessary. The refactoring might be a slight performance regression because the new implementation adds some indirection. But the affected functions aren't widely used anyway and I suspect that the performance loss is very minor, so having clearer and more concise code is probably worth it.