mathlib documentation

meta.expr

Additional operations on expr and related types #

This file defines basic operations on the types expr, name, declaration, level, environment.

This file is mostly for non-tactics. Tactics should generally be placed in tactic.core.

Tags #

expr, name, declaration, level, environment, meta, metaprogramming, tactic

@[protected, instance]
@[protected, instance]
@[protected, instance]

Declarations about binder_info #

The brackets corresponding to a given binder_info.

Equations

Declarations about name #

def name.map_prefix (f : nameoption name) :

Find the largest prefix n of a name such that f n ≠ none, then replace this prefix with the value of f n.

Equations

If nm is a simple name (having only one string component) starting with _, then deinternalize_field nm removes the underscore. Otherwise, it does nothing.

meta def name.get_nth_prefix  :
namename

get_nth_prefix nm n removes the last n components from nm

meta def name.pop_nth_prefix (nm : name) (n : ) :

Pops the top n prefixes from the given name.

meta def name.pop_prefix (n : name) :

Pop the prefix of a name

Build a name from components. For example from_components ["foo","bar"] becomes `foo.bar

Equations
meta def name.sanitize_name  :

names can contain numeral pieces, which are not legal names when typed/passed directly to the parser. We turn an arbitrary name into a legal identifier name by turning the numbers to strings.

Append a string to the last component of a name.

Equations
def name.update_last (f : stringstring) :

Update the last component of a name.

Equations
def name.append_to_last (nm : name) (s : string) (is_prefix : bool) :

append_to_last nm s is_prefix adds s to the last component of nm, either as prefix or as suffix (specified by is_prefix), separated by _. Used by simps_add_projections.

Equations
meta def name.head  :

The first component of a name, turning a number to a string

meta def name.is_private (n : name) :

Tests whether the first component of a name is "_private"

meta def name.length  :
name

Returns the number of characters used to print all the string components of a name, including periods between name segments. Ignores numerical parts of a name.

def name.has_prefix (P : namebool) :

Checks whether nm has a prefix (including itself) such that P is true

Equations
meta def name.add_prime  :

Appends ' to the end of a name.

last_string n returns the rightmost component of n, ignoring numeral components. For example, last_string `a.b.c.33 will return `c.

Equations
meta def name.append_namespace (ns : name) :

Like ++, except that if the right argument starts with _root_ the namespace will be ignored.

append_namespace `a.b `c.d = `a.b.c.d
append_namespace `a.b `_root_.c.d = `c.d
meta def name.from_string (s : string) :

Constructs a (non-simple) name from a string.

Example: name.from_string "foo.bar" = `foo.bar

In surface Lean, we can write anonymous Π binders (i.e. binders where the argument is not named) using the function arrow notation:

inductive test : Type
| intro : unit  test

After elaboration, however, every binder must have a name, so Lean generates one. In the example, the binder in the type of intro is anonymous, so Lean gives it the name :

test.intro :  ( : unit), test

When there are multiple anonymous binders, they are named ᾰ_1, ᾰ_2 etc.

Thus, when we want to know whether the user named a binder, we can check whether the name follows this scheme. Note, however, that this is not reliable. When the user writes (for whatever reason)

inductive test : Type
| intro :  ( : unit), test

we cannot tell that the binder was, in fact, named.

The function name.is_likely_generated_binder_name checks if a name is of the form , ᾰ_1, etc.

Check whether a simple name was likely generated by Lean to name an anonymous binder. Such names are either or ᾰ_n for some natural n. See note [likely generated binder names].

Check whether a name was likely generated by Lean to name an anonymous binder. Such names are either or ᾰ_n for some natural n. See note [likely generated binder names].

Declarations about level #

meta def level.nonzero  :

Tests whether a universe level is non-zero for all assignments of its variables

meta def level.fold_mvar {α : Sort u_1} :
level(nameα → α)α → α

l.fold_mvar f folds a function f : name → α → α over each n : name appearing in a level.mvar n in l.

@[protected]
meta def level.params (u : level) :

l.params is the set of parameters occuring in l. For example if l = max 1 (max (u+1) (max v w)) then l.params = {u, v, w}.

Declarations about binder #

@[protected, instance]
meta structure binder  :
Type

The type of binders containing a name, the binding info and the binding type

Instances for binder
@[protected, instance]
@[protected]
meta def binder.to_string (b : binder) :

Turn a binder into a string. Uses expr.to_string for the type.

@[protected, instance]
@[protected, instance]
@[protected, instance]

Converting between expressions and numerals #

There are a number of ways to convert between expressions and numerals, depending on the input and output types and whether you want to infer the necessary type classes.

See also the tactics expr.of_nat, expr.of_int, expr.of_rat.

meta def nat.mk_numeral (type has_zero has_one has_add : expr) :
expr

nat.mk_numeral n embeds n as a numeral expression inside a type with 0, 1, and +. type: an expression representing the target type. This must live in Type 0. has_zero, has_one, has_add: expressions of the type has_zero %%type, etc.

meta def int.mk_numeral (type has_zero has_one has_add has_neg : expr) :
expr

int.mk_numeral z embeds z as a numeral expression inside a type with 0, 1, +, and -. type: an expression representing the target type. This must live in Type 0. has_zero, has_one, has_add, has_neg: expressions of the type has_zero %%type, etc.

meta def nat.to_pexpr  :

nat.to_pexpr n creates a pexpr that will evaluate to n. The pexpr does not hold any typing information: to_expr ``((%%(nat.to_pexpr 5) : ℤ)) will create a native integer numeral (5 : ℤ).

meta def int.to_pexpr  :

int.to_pexpr n creates a pexpr that will evaluate to n. The pexpr does not hold any typing information: to_expr ``((%%(int.to_pexpr (-5)) : ℚ)) will create a native numeral (-5 : ℚ).

@[protected]
meta def expr.to_nat  :

Turns an expression into a natural number, assuming it is only built up from has_one.one, bit0, bit1, has_zero.zero, nat.zero, and nat.succ.

@[protected]
meta def expr.to_int  :

Turns an expression into a integer, assuming it is only built up from has_one.one, bit0, bit1, has_zero.zero and a optionally a single has_neg.neg as head.

@[protected]
meta def expr.to_list {α : Type u_1} (f : exproption α) :
exproption (list α)

Turns an expression into a list, assuming it is only built up from list.nil and list.cons.

meta def expr.is_num_eq  :
exprexprbool

is_num_eq n1 n2 returns true if n1 and n2 are both numerals with the same numeral structure, ignoring differences in type and type class arguments.

Declarations about pexpr #

meta def pexpr.get_frozen_name (e : pexpr) :

If e is an annotation of frozen_name to expr.const n, e.get_frozen_name returns n. Otherwise, returns name.anonymous.

If e : pexpr is a sequence of applications f e₁ e₂ ... eₙ, e.get_app_fn_args returns (f, [e₁, ... eₙ]). See also expr.get_app_fn_args.

meta def pexpr.get_app_fn  :

If e : pexpr is a sequence of applications f e₁ e₂ ... eₙ, e.get_app_fn returns f. See also expr.get_app_fn.

meta def pexpr.get_app_args  :

If e : pexpr is a sequence of applications f e₁ e₂ ... eₙ, e.get_app_args returns [e₁, ... eₙ]. See also expr.get_app_args.

Declarations about expr #

meta def expr.clean_ids  :

List of names removed by clean. All these names must resolve to functions defeq id.

meta def expr.clean (e : expr) :

Clean an expression by removing ids listed in clean_ids.

meta def expr.replace_with (e s s' : expr) :

replace_with e s s' replaces ocurrences of s with s' in e.

meta def expr.mreplace_aux {m : Type → Type u_1} [monad m] (R : exprm (option expr)) :
exprm expr

Implementation of expr.mreplace.

meta def expr.mreplace {m : Type → Type u_1} [monad m] (R : exprm (option expr)) (e : expr) :

Monadic analogue of expr.replace.

The mreplace R e visits each subexpression s of e, and is called with R s n, where n is the number of binders above e. If R s n fails, the whole replacement fails. If R s n returns some t, s is replaced with t (and mreplace does not visit its subexpressions). If R s n return none, then mreplace continues visiting subexpressions of s.

WARNING: This function performs exponentially worse on large terms than expr.replace, if a subexpression occurs more than once in an expression, expr.replace visits them only once, but this function will visit every occurence of it. Do not use this on large expressions.

meta def expr.match_var {elab : bool := bool.tt} :
expr elaboption

Match a variable.

meta def expr.match_sort {elab : bool := bool.tt} :
expr elaboption level

Match a sort.

meta def expr.match_const {elab : bool := bool.tt} :

Match a constant.

meta def expr.match_mvar {elab : bool := bool.tt} :
expr elaboption (name × name × expr elab)

Match a metavariable.

meta def expr.match_local_const {elab : bool := bool.tt} :

Match a local constant.

meta def expr.match_app {elab : bool := bool.tt} :
expr elaboption (expr elab × expr elab)

Match an application.

Match an application of coe_fn.

meta def expr.match_lam {elab : bool := bool.tt} :
expr elaboption (name × binder_info × expr elab × expr elab)

Match an abstraction.

meta def expr.match_pi {elab : bool := bool.tt} :
expr elaboption (name × binder_info × expr elab × expr elab)

Match a Π type.

meta def expr.match_elet {elab : bool := bool.tt} :
expr elaboption (name × expr elab × expr elab × expr elab)

Match a let.

meta def expr.match_macro {elab : bool := bool.tt} :
expr elaboption (macro_def × list (expr elab))

Match a macro.

meta def expr.is_mvar  :

Tests whether an expression is a meta-variable.

meta def expr.is_sort  :

Tests whether an expression is a sort.

meta def expr.univ_levels  :

Get the universe levels of a const expression

meta def expr.replace_mvars (e : expr) :

Replace any metavariables in the expression with underscores, in preparation for printing refine ... statements.

If e is a local constant, to_implicit_local_const e changes the binder info of e to implicit. See also to_implicit_binder, which also changes lambdas and pis.

meta def expr.to_implicit_binder  :

If e is a local constant, lamda, or pi expression, to_implicit_binder e changes the binder info of e to implicit. See also to_implicit_local_const, which only changes local constants.

meta def expr.list_local_consts (e : expr) :

Returns a list of all local constants in an expression (without duplicates).

Returns the set of all local constants in an expression.

Returns the unique names of all local constants in an expression.

meta def expr.list_constant (e : expr) :

Returns a name_set of all constants in an expression.

meta def expr.list_constant' (e : expr) :

Returns a list name containing the constant names of an expr in the same order that expr.fold traverses it.

meta def expr.list_meta_vars (e : expr) :

Returns a list of all meta-variables in an expression (without duplicates).

meta def expr.list_meta_vars' (e : expr) :

Returns the set of all meta-variables in an expression.

Returns a list of all universe meta-variables in an expression (without duplicates).

meta def expr.contains_expr_or_mvar (t e : expr) :

Test t contains the specified subexpression e, or a metavariable. This represents the notion that e "may occur" in t, possibly after subsequent unification.

meta def expr.list_names_with_prefix (pre : name) (e : expr) :

Returns a name_set of all constants in an expression starting with a certain prefix.

meta def expr.contains_constant (e : expr) (p : name → Prop) [decidable_pred p] :

Returns true if e contains a name n where p n is true. Returns true if p name.anonymous is true.

meta def expr.contains_sorry (e : expr) :

Returns true if e contains a sorry. See also name.contains_sorry.

meta def expr.app_symbol_in (e : expr) (l : list name) :

app_symbol_in e l returns true iff e is an application of a constant whose name is in l.

meta def expr.get_simp_args (e : expr) :

get_simp_args e returns the arguments of e that simp can reach via congruence lemmas.

Simplifies the expression t with the specified options. The result is (new_e, pr) with the new expression new_e and a proof pr : e = new_e.

Definitionally simplifies the expression t with the specified options. The result is the simplified expression.

meta def expr.binding_names  :

Get the names of the bound variables by a sequence of pis or lambdas.

meta def expr.reduce_let  :

head-reduce a single let expression

meta def expr.reduce_lets  :

head-reduce all let expressions

meta def expr.instantiate_lambdas  :
list exprexprexpr

Instantiate lambdas in the second argument by expressions from the first.

meta def expr.substs  :
exprlist exprexpr

Repeatedly apply expr.subst.

instantiate_lambdas_or_apps es e instantiates lambdas in e by expressions from es. If the length of es is larger than the number of lambdas in e, then the term is applied to the remaining terms. Also reduces head let-expressions in e, including those after instantiating all lambdas.

This is very similar to expr.substs, but this also reduces head let-expressions.

Some declarations work with open expressions, i.e. an expr that has free variables. Terms will free variables are not well-typed, and one should not use them in tactics like infer_type or unify. You can still do syntactic analysis/manipulation on them. The reason for working with open types is for performance: instantiating variables requires iterating through the expression. In one performance test pi_binders was more than 6x quicker than mk_local_pis (when applied to the type of all imported declarations 100x).

meta def expr.pi_codomain  :

Get the codomain/target of a pi-type. This definition doesn't instantiate bound variables, and therefore produces a term that is open. See note [open expressions].

meta def expr.lambda_body  :

Get the body/value of a lambda-expression. This definition doesn't instantiate bound variables, and therefore produces a term that is open. See note [open expressions].

Auxiliary defintion for pi_binders. See note [open expressions].

meta def expr.pi_binders (e : expr) :

Get the binders and codomain of a pi-type. This definition doesn't instantiate bound variables, and therefore produces a term that is open. The.tactic get_pi_binders in tactic.core does the same, but also instantiates the free variables. See note [open expressions].

Auxiliary defintion for get_app_fn_args.

A combination of get_app_fn and get_app_args: lists both the function and its arguments of an application

meta def expr.drop_pis  :

drop_pis es e instantiates the pis in e with the expressions from es.

meta def expr.instantiate_pis  :
list exprexprexpr

instantiate_pis es e instantiates the pis in e with the expressions from es. Does not check whether the result remains type-correct.

meta def expr.mk_op_lst (op empty : expr) :

mk_op_lst op empty [x1, x2, ...] is defined as op x1 (op x2 ...). Returns empty if the list is empty.

meta def expr.mk_and_lst  :

mk_and_lst [x1, x2, ...] is defined as x1 ∧ (x2 ∧ ...), or true if the list is empty.

meta def expr.mk_or_lst  :

mk_or_lst [x1, x2, ...] is defined as x1 ∨ (x2 ∨ ...), or false if the list is empty.

local_binding_info e returns the binding info of e if e is a local constant. Otherwise returns binder_info.default.

meta def expr.is_default_local  :

is_default_local e tests whether e is a local constant with binder info binder_info.default

meta def expr.has_local_constant (e l : expr) :

has_local_constant e l checks whether local constant l occurs in expression e

meta def expr.to_binder  :

Turns a local constant into a binder

Strip-away the context-dependent unique id for the given local const and return: its friendly name, its binder_info, and its type : expr.

meta def expr.local_const_set_type {elab : bool} :
expr elabexpr elabexpr elab

local_const_set_type e t sets the type of e to t, if e is a local_const.

meta def expr.unsafe_cast {elab₁ elab₂ : bool} :
expr elab₁expr elab₂

unsafe_cast e freely changes the elab : bool parameter of the passed expr. Mainly used to access core expr manipulation functions for pexpr-based use, but which are restricted to expr tt at the site of definition unnecessarily.

DANGER: Unless you know exactly what you are doing, this is probably not the function you are looking for. For pexprexpr see tactic.to_expr. For exprpexpr see to_pexpr.

meta def expr.replace_subexprs {elab : bool} (e : expr elab) (mappings : list (expr × expr)) :
expr elab

replace_subexprs e mappings takes an e : expr and interprets a list (expr × expr) as a collection of rules for variable replacements. A pair (f, t) encodes a rule which says "whenever f is encountered in e verbatim, replace it with t".

is_implicitly_included_variable e vs accepts e, an expr.local_const, and a list vs of other expr.local_consts. It determines whether e should be considered "available in context" as a variable by virtue of the fact that the variables vs have been deemed such.

For example, given variables (n : ℕ) [prime n] [ih : even n], a reference to n implies that the typeclass instance prime n should be included, but ih : even n should not.

DANGER: It is possible that for f : expr another expr.local_const, we have is_implicitly_included_variable f vs = ff but is_implicitly_included_variable f (e :: vs) = tt. This means that one usually wants to iteratively add a list of local constants (usually, the variables declared in the local scope) which satisfy is_implicitly_included_variable to an initial vs, repeating if any variables were added in a particular iteration. The function all_implicitly_included_variables below implements this behaviour.

Note that if e ∈ vs then is_implicitly_included_variable e vs = tt.

all_implicitly_included_variables es vs accepts es, a list of expr.local_const, and vs, another such list. It returns a list of all variables e in es or vs for which an inclusion of the variables in vs into the local context implies that e should also be included. See is_implicitly_included_variable e vs for the details.

In particular, those elements of vs are included automatically.

Get the list of explicit arguments of a function.

meta def expr.replace_explicit_args (f : expr) (parg : list expr) :

replace_explicit_args f parg assumes that f is an expression corresponding to a function application. It replaces the explicit arguments of f, in succession, by the elements of parg. The implicit arguments of f remain unchanged.

@[protected]

Infer the type of an application of the form f x1 x2 ... xn, where f is an identifier. This also works if x1, ... xn contain free variables.

meta def expr.head_eta_expand_aux  :
exprexprexpr

Auxilliary function for head_eta_expand.

meta def expr.head_eta_expand (n : ) (e t : expr) :

head_eta_expand n e t eta-expands e n times, with the binders info and domains obtained by its type t.

@[protected]
meta def expr.eta_expand (env : environment) (dict : name_map (list )) :

e.eta_expand env dict eta-expands all expressions that have as head a constant n in dict. They are expanded until they are applied to one more argument than the maximum in dict.find n.

@[protected]
meta def expr.apply_replacement_fun (f : namename) (test : exprbool) (relevant : name_map ) (reorder : name_map (list )) :

e.apply_replacement_fun f test applies f to each identifier (inductive type, defined function etc) in an expression, unless

  • The identifier occurs in an application with first argument arg; and
  • test arg is false. However, if f is in the dictionary relevant, then the argument relevant.find f is tested, instead of the first argument.

Reorder contains the information about what arguments to reorder: e.g. g x₁ x₂ x₃ ... xₙ becomes g x₂ x₁ x₃ ... xₙ if reorder.find g = some [1]. We assume that all functions where we want to reorder arguments are fully applied. This can be done by applying expr.eta_expand first.

Declarations about environment #

meta def environment.is_structure (env : environment) (n : name) :

Tests whether n is a structure.

Get the full names of all projections of the structure n. Returns none if n is not a structure.

meta def environment.is_ginductive' (e : environment) (nm : name) :

Tests whether nm is a generalized inductive type that is not a normal inductive type. Note that is_ginductive returns tt even on regular inductive types. This returns tt if nm is (part of a) mutually defined inductive type or a nested inductive type.

meta def environment.decl_filter_map {α : Type} (e : environment) (f : declarationoption α) :
list α

For all declarations d where f d = some x this adds x to the returned list.

meta def environment.decl_map {α : Type} (e : environment) (f : declaration → α) :
list α

Maps f to all declarations in the environment.

Lists all declarations in the environment

Lists all trusted (non-meta) declarations in the environment

Lists the name of all declarations in the environment

meta def environment.mfold {α : Type} {m : Type → Type} [monad m] (e : environment) (x : α) (fn : declarationα → m α) :
m α

Fold a monad over all declarations in the environment.

Filters all declarations in the environment.

Filters all declarations in the environment.

meta def environment.is_prefix_of_file (e : environment) (s : string) (n : name) :

Checks whether s is a prefix of the file where n is declared. This is used to check whether n is declared in mathlib, where s is the mathlib directory.

is_eta_expansion #

In this section we define the tactic is_eta_expansion which checks whether an expression is an eta-expansion of a structure. (not to be confused with eta-expanion for λ).

meta def expr.is_eta_expansion_of (args : list expr) (univs : list level) (l : list (name × expr)) :

is_eta_expansion_of args univs l checks whether for all elements (nm, pr) in l we have pr = nm.{univs} args. Used in is_eta_expansion, where l consists of the projections and the fields of the value we want to eta-reduce.

is_eta_expansion_test l checks whether there is a list of expresions args such that for all elements (nm, pr) in l we have pr = nm args. If so, returns the last element of args. Used in is_eta_expansion, where l consists of the projections and the fields of the value we want to eta-reduce.

meta def expr.is_eta_expansion_aux (val : expr) (l : list (name × expr)) :

is_eta_expansion_aux val l checks whether val can be eta-reduced to an expression e. Here l is intended to consists of the projections and the fields of val. This tactic calls is_eta_expansion_test l, but first removes all proofs from the list l and afterward checks whether the resulting expression e unifies with val. This last check is necessary, because val and e might have different types.

meta def expr.is_eta_expansion (val : expr) :

is_eta_expansion val checks whether there is an expression e such that val is the eta-expansion of e. With eta-expansion we here mean the eta-expansion of a structure, not of a function. For example, the eta-expansion of x : α × β is ⟨x.1, x.2⟩. This assumes that val is a fully-applied application of the constructor of a structure.

This is useful to reduce expressions generated by the notation { field_1 := _, ..other_structure } If other_structure is itself a field of the structure, then the elaborator will insert an eta-expanded version of other_structure.

Declarations about declaration #

@[protected]
meta def declaration.update_with_fun (env : environment) (f : namename) (test : exprbool) (relevant : name_map ) (reorder : name_map (list )) (tgt : name) (decl : declaration) :

declaration.update_with_fun f test tgt decl sets the name of the given decl : declaration to tgt, and applies both expr.eta_expand and expr.apply_replacement_fun to the value and type of decl.

Checks whether the declaration is declared in the current file. This is a simple wrapper around environment.in_current_file Use environment.in_current_file instead if performance matters.

Checks whether a declaration is a theorem

Checks whether a declaration is a constant

Checks whether a declaration is a axiom

Checks whether a declaration is automatically generated in the environment. There is no cheap way to check whether a declaration in the namespace of a generalized inductive type is automatically generated, so for now we say that all of them are automatically generated.

Returns true iff d is an automatically-generated or internal declaration.

Returns the list of universe levels of a declaration.

@[protected]

Returns the reducibility_hints field of a defn, and reducibility_hints.opaque otherwise

pretty-prints a declaration object.

@[protected, instance]
meta def pexpr.decidable_eq {elab : bool := bool.tt} :
@[protected, instance]
meta def thunk.has_reflect {α : Type u_1} [has_reflect α] :