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

@[instance]
meta def has_reflect.has_to_pexpr {α : Sort u_1} [has_reflect α] :

Declarations about binder_info

The brackets corresponding to a given binder_info.

Equations

Declarations about name

def name.map_prefix  :
(nameoption name)namename

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  :
namename

Pops the top n prefixes from the given name.

meta def name.pop_prefix  :

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
meta def name.head  :

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

meta def name.is_private  :

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

meta def name.last  :

Get the last component of a name, and convert it to a string.

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  :
(namebool)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.from_string  :

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

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

Check whether a simple name was likely generated by Lean to name an anonymous binder. Such names are either a or a_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 a or a_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.

Declarations about binder

@[instance]

meta structure binder  :
Type

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

@[instance]

meta def binder.to_string  :

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

@[instance]

@[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  :
exprexprexprexprexpr

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  :
exprexprexprexprexprexpr

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 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.

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.

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 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  :

Clean an expression by removing ids listed in clean_ids.

meta def expr.replace_with  :
exprexprexprexpr

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

meta def expr.apply_replacement_fun  :
(namename)exprexpr

Apply a function to each constant (inductive type, defined function etc) in an expression.

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

Match a variable.

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

Match a sort.

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

Match a constant.

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

Match a metavariable.

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

Match a local constant.

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

Match an application.

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

Match an abstraction.

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

Match a Π type.

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

Match a let.

meta def expr.match_macro {elab : 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  :

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.

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  :

Returns a name_set of all constants in an expression.

meta def expr.list_meta_vars  :

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

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  :
exprexprbool

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

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  :

Returns true if e contains a sorry.

meta def expr.app_symbol_in  :
exprlist namebool

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  :

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.

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].

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

meta def expr.pi_binders  :

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].

Auxilliary 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.mk_op_lst  :
exprexprlist exprexpr

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  :
exprexprbool

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} :
expr elablist (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.

Declarations about environment

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.

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} :
environment(declarationoption α)list α

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

meta def environment.decl_map {α : Type} :
environment(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] :
environmentα → (declarationα → m α)m α

Fold a monad over all declarations in the environment.

Filters all declarations in the environment.

Filters all declarations in the environment.

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 λ).

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.

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.

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

declaration.update_with_fun f tgt decl sets the name of the given decl : declaration to tgt, and applies f to the names of all expr.consts which appear in the value or 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.

pretty-prints a declaration object.

@[instance]
meta def pexpr.decidable_eq {elab : bool := tt} :