core / init.meta.tactic

source

meta constant tactic_state :

Type

source

meta constant tactic_state.env :

tactic_state → environment

source

meta constant tactic_state.to_format (s : tactic_state) (target_lhs_only : bool := ff) :

format

Format the given tactic state. If target_lhs_only is true and the target is of the form lhs ~ rhs, where ~ is a simplification relation, then only the lhs is displayed.

Remark: the parameter target_lhs_only is a temporary hack used to implement the conv monad. It will be removed in the future.

source

meta constant tactic_state.format_expr :

tactic_state → expr → format

Format expression with respect to the main goal in the tactic state. If the tactic state does not contain any goals, then format expression using an empty local context.

source

meta constant tactic_state.get_options :

tactic_state → options

source

meta constant tactic_state.set_options :

tactic_state → options → tactic_state

source

@[protected, instance]

meta def tactic_state.has_to_format :

has_to_format tactic_state

source

@[protected, instance]

meta def tactic_state.has_to_string :

has_to_string tactic_state

source

meta def tactic (α : Type u_1) :

Type u_1

tactic is the monad for building tactics. You use this to:

View and modify the local goals and hypotheses in the prover's state.
Invoke type checking and elaboration of terms.
View and modify the environment.
Build new tactics out of existing ones such as simp and rewrite.

source

meta def tactic_result (α : Type u_1) :

Type u_1

source

meta def tactic.failed {α : Type} :

tactic α

Cause the tactic to fail with no error message.

source

meta def tactic.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) :

tactic α

source

@[protected, instance]

meta def tactic.alternative :

alternative tactic

source

meta def tactic.up {α : Type u₂} (t : tactic α) :

tactic (ulift α)

source

meta def tactic.down {α : Type u₂} (t : tactic (ulift α)) :

tactic α

source

@[class]

meta structure interactive.executor (m : Type → Type u) [monad m] :

Type (max 1 u)

config_type : Type
inhabited : inhabited (interactive.executor.config_type m)
execute_with : interactive.executor.config_type m → m unit → tactic unit

Typeclass for custom interaction monads, which provides the information required to convert an interactive-mode construction to a tactic which can actually be executed.

Given a [monad m], execute_with explains how to turn a begin ... end block, or a by ... statement into a tactic α which can actually be executed. The inhabited first argument facilitates the passing of an optional configuration parameter config, using the syntax:

begin [custom_monad] with config,
    ...
end

Instances

source

meta def interactive.executor.execute_explicit (m : Type → Type u) [monad m] [e : interactive.executor m] :

m unit → tactic unit

source

meta def interactive.executor.execute_with_explicit (m : Type → Type u) [monad m] [interactive.executor m] :

interactive.executor.config_type m → m unit → tactic unit

source

@[protected, instance]

meta def interactive.executor_tactic :

interactive.executor tactic

Default executor instance for tactics themselves

source

meta def tactic.skip :

tactic unit

Does nothing.

source

meta def tactic.try_core {α : Type u} (t : tactic α) :

tactic (option α)

try_core t acts like t, but succeeds even if t fails. It returns the result of t if t succeeded and none otherwise.

source

meta def tactic.try {α : Type u} (t : tactic α) :

tactic unit

try t acts like t, but succeeds even if t fails.

source

meta def tactic.try_lst :

list (tactic unit) → tactic unit

source

meta def tactic.fail_if_success {α : Type u} (t : tactic α) :

tactic unit

fail_if_success t acts like t, but succeeds if t fails and fails if t succeeds. Changes made by t to the tactic_state are preserved only if t succeeds.

source

meta def tactic.success_if_fail {α : Type u} (t : tactic α) :

tactic unit

success_if_fail t acts like t, but succeeds if t fails and fails if t succeeds. Changes made by t to the tactic_state are preserved only if t succeeds.

source

meta def tactic.iterate_at_most {α : Type u} :

ℕ → tactic α → tactic (list α)

iterate_at_most n t iterates t n times or until t fails, returning the result of each successful iteration.

source

meta def tactic.iterate_at_most' :

ℕ → tactic unit → tactic unit

iterate_at_most' n t repeats t n times or until t fails.

source

meta def tactic.iterate_exactly {α : Type u} :

ℕ → tactic α → tactic (list α)

iterate_exactly n t iterates t n times, returning the result of each iteration. If any iteration fails, the whole tactic fails.

source

meta def tactic.iterate_exactly' :

ℕ → tactic unit → tactic unit

iterate_exactly' n t executes t n times. If any iteration fails, the whole tactic fails.

source

meta def tactic.iterate {α : Type u} :

tactic α → tactic (list α)

iterate t repeats t 100.000 times or until t fails, returning the result of each iteration.

source

meta def tactic.iterate' :

tactic unit → tactic unit

iterate' t repeats t 100.000 times or until t fails.

source

meta def tactic.returnopt {α : Type u} (e : option α) :

tactic α

source

@[protected, instance]

meta def tactic.opt_to_tac {α : Type u} :

has_coe (option α) (tactic α)

source

meta def tactic.decorate_ex {α : Type u} (msg : format) (t : tactic α) :

tactic α

Decorate t's exceptions with msg.

source

meta def tactic.write (s' : tactic_state) :

tactic unit

Set the tactic_state.

source

meta def tactic.read :

tactic tactic_state

Get the tactic_state.

source

meta def tactic.capture {α : Type u} (t : tactic α) :

tactic (tactic_result α)

capture t acts like t, but succeeds with a result containing either the returned value or the exception. Changes made by t to the tactic_state are preserved in both cases.

The result can be used to inspect the error message, or passed to unwrap to rethrow the failure later.

source

meta def tactic.unwrap {α : Type u_1} (t : tactic_result α) :

tactic α

unwrap r unwraps a result previously obtained using capture.

If the previous result was a success, this produces its wrapped value. If the previous result was an exception, this "rethrows" the exception as if it came from where it originated.

do r ← capture t, unwrap r is identical to t, but allows for intermediate tactics to be inserted.

source

meta def tactic.resume {α : Type u_1} (t : tactic_result α) :

tactic α

resume r continues execution from a result previously obtained using capture.

This is like unwrap, but the tactic_state is rolled back to point of capture even upon success.

source

meta def tactic.get_options :

tactic options

source

meta def tactic.set_options (o : options) :

tactic unit

source

meta def tactic.save_options {α : Type} (t : tactic α) :

tactic α

source

meta def tactic.returnex {α : Type} (e : exceptional α) :

tactic α

source

@[protected, instance]

meta def tactic.ex_to_tac {α : Type} :

has_coe (exceptional α) (tactic α)

source

meta def tactic_format_expr (e : expr) :

tactic format

source

@[class]

meta structure has_to_tactic_format (α : Type u) :

Type u

to_tactic_format : α → tactic format

Instances

source

@[protected, instance]

meta def expr.has_to_tactic_format :

has_to_tactic_format expr

source

meta def tactic.pp {α : Type u} [has_to_tactic_format α] :

α → tactic format

source

@[protected, instance]

meta def list.has_to_tactic_format {α : Type u} [has_to_tactic_format α] :

has_to_tactic_format (list α)

source

@[protected, instance]

meta def prod.has_to_tactic_format (α : Type u) (β : Type v) [has_to_tactic_format α] [has_to_tactic_format β] :

has_to_tactic_format (α × β)

source

meta def option_to_tactic_format {α : Type u} [has_to_tactic_format α] :

option α → tactic format

source

@[protected, instance]

meta def option.has_to_tactic_format {α : Type u} [has_to_tactic_format α] :

has_to_tactic_format (option α)

source

@[protected, instance]

meta def reflected.has_to_tactic_format {α : Sort u_1} (a : α) :

has_to_tactic_format (reflected a)

source

@[protected, instance]

meta def has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] :

has_to_tactic_format α

source

meta def tactic.get_env :

tactic environment

source

meta def tactic.get_decl (n : name) :

tactic declaration

source

meta constant tactic.get_trace_msg_pos :

tactic pos

source

meta def tactic.trace {α : Type u} [has_to_tactic_format α] (a : α) :

tactic unit

source

meta def tactic.trace_call_stack :

tactic unit

source

meta def tactic.timetac {α : Type u} (desc : string) (t : thunk (tactic α)) :

tactic α

source

meta def tactic.trace_state :

tactic unit

source

inductive tactic.transparency :

Type

A parameter representing how aggressively definitions should be unfolded when trying to decide if two terms match, unify or are definitionally equal. By default, theorem declarations are never unfolded.

all will unfold everything, including macros and theorems. Except projection macros.
semireducible will unfold everything except theorems and definitions tagged as irreducible.
instances will unfold all class instance definitions and definitions tagged with reducible.
reducible will only unfold definitions tagged with the reducible attribute.
none will never unfold anything. [NOTE] You are not allowed to tag a definition with more than one of reducible, irreducible, semireducible attributes. [NOTE] there is a config flag m_unfold_lemmasthat will make it unfold theorems.

source

meta constant tactic.eval_expr (α : Type u) [reflected α] :

expr → tactic α

(eval_expr α e) evaluates 'e' IF 'e' has type 'α'.

source

meta constant tactic.result :

tactic expr

Return the partial term/proof constructed so far. Note that the resultant expression may contain variables that are not declarate in the current main goal.

source

meta constant tactic.format_result :

tactic format

Display the partial term/proof constructed so far. This tactic is not equivalent to do { r ← result, s ← read, return (format_expr s r) } because this one will format the result with respect to the current goal, and trace_result will do it with respect to the initial goal.

source

meta constant tactic.target :

tactic expr

Return target type of the main goal. Fail if tactic_state does not have any goal left.

source

meta constant tactic.intro_core :

name → tactic expr

source

meta constant tactic.intron :

ℕ → tactic unit

source

meta constant tactic.clear :

expr → tactic unit

Clear the given local constant. The tactic fails if the given expression is not a local constant.

source

meta constant tactic.revert_lst :

list expr → tactic ℕ

revert_lst : list expr → tactic nat is the reverse of intron. It takes a local constant c and puts it back as bound by a pi or elet of the main target. If there are other local constants that depend on c, these are also reverted. Because of this, the nat that is returned is the actual number of reverted local constants. Example: with x : ℕ, h : P(x) ⊢ T(x), revert_lst [x] returns 2 and produces the state ⊢ Π x, P(x) → T(x).

source

meta constant tactic.whnf (e : expr) (md : tactic.transparency := semireducible) (unfold_ginductive : bool := tt) :

tactic expr

Return e in weak head normal form with respect to the given transparency setting. If unfold_ginductive is tt, then nested and/or mutually recursive inductive datatype constructors and types are unfolded. Recall that nested and mutually recursive inductive datatype declarations are compiled into primitive datatypes accepted by the Kernel.

source

meta constant tactic.head_eta_expand :

expr → tactic expr

(head) eta expand the given expression. f : α → β head-eta-expands to λ a, f a. If f isn't a function then it just returns f.

source

meta constant tactic.head_beta :

expr → tactic expr

(head) beta reduction. (λ x, B) c reduces to B[x/c].

source

meta constant tactic.head_zeta :

expr → tactic expr

(head) zeta reduction. Reduction of let bindings at the head of the expression. let x : a := b in c reduces to c[x/b].

source

meta constant tactic.zeta :

expr → tactic expr

Zeta reduction. Reduction of let bindings. let x : a := b in c reduces to c[x/b].

source

meta constant tactic.head_eta :

expr → tactic expr

(head) eta reduction. (λ x, f x) reduces to f.

source

meta constant tactic.unify (t s : expr) (md : tactic.transparency := semireducible) (approx : bool := ff) :

tactic unit

Succeeds if t and s can be unified using the given transparency setting.

source

meta constant tactic.is_def_eq (t s : expr) (md : tactic.transparency := semireducible) (approx : bool := ff) :

tactic unit

Similar to unify, but it treats metavariables as constants.

source

meta constant tactic.infer_type :

expr → tactic expr

Infer the type of the given expression. Remark: transparency does not affect type inference

source

meta constant tactic.get_local :

name → tactic expr

Get the local_const expr for the given name.

source

meta constant tactic.resolve_name :

name → tactic pexpr

Resolve a name using the current local context, environment, aliases, etc.

source

meta constant tactic.local_context :

tactic (list expr)

Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left.

source

meta constant tactic.get_unused_name (n : name := name.mk_string "_x" name.anonymous) (i : option ℕ := none) :

tactic name

Get a fresh name that is guaranteed to not be in use in the local context. If n is provided and n is not in use, then n is returned. Otherwise a number i is appended to give "n_i".

source

meta constant tactic.mk_app (fn : name) (args : list expr) (md : tactic.transparency := semireducible) :

tactic expr

Helper tactic for creating simple applications where some arguments are inferred using type inference.

Example, given

    rel.{l_1 l_2} : Pi (α : Type.{l_1}) (β : α -> Type.{l_2}), (Pi x : α, β x) -> (Pi x : α, β x) -> , Prop
    nat     : Type
    real    : Type
    vec.{l} : Pi (α : Type l) (n : nat), Type.{l1}
    f g     : Pi (n : nat), vec real n

then

mk_app_core semireducible "rel" [f, g]

returns the application

rel.{1 2} nat (fun n : nat, vec real n) f g

The unification constraints due to type inference are solved using the transparency md.

source

meta constant tactic.mk_mapp (fn : name) (args : list (option expr)) (md : tactic.transparency := semireducible) :

tactic expr

Similar to mk_app, but allows to specify which arguments are explicit/implicit. Example, given (a b : nat) then

mk_mapp "ite" [some (a > b), none, none, some a, some b]

returns the application

@ite.{1} nat (a > b) (nat.decidable_gt a b) a b

source

meta constant tactic.mk_congr_arg :

expr → expr → tactic expr

(mk_congr_arg h₁ h₂) is a more efficient version of (mk_app `congr_arg [h₁, h₂])

source

meta constant tactic.mk_congr_fun :

expr → expr → tactic expr

(mk_congr_fun h₁ h₂) is a more efficient version of (mk_app `congr_fun [h₁, h₂])

source

meta constant tactic.mk_congr :

expr → expr → tactic expr

(mk_congr h₁ h₂) is a more efficient version of (mk_app `congr [h₁, h₂])

source

meta constant tactic.mk_eq_refl :

expr → tactic expr

(mk_eq_refl h) is a more efficient version of (mk_app `eq.refl [h])

source

meta constant tactic.mk_eq_symm :

expr → tactic expr

(mk_eq_symm h) is a more efficient version of (mk_app `eq.symm [h])

source

meta constant tactic.mk_eq_trans :

expr → expr → tactic expr

(mk_eq_trans h₁ h₂) is a more efficient version of (mk_app `eq.trans [h₁, h₂])

source

meta constant tactic.mk_eq_mp :

expr → expr → tactic expr

(mk_eq_mp h₁ h₂) is a more efficient version of (mk_app `eq.mp [h₁, h₂])

source

meta constant tactic.mk_eq_mpr :

expr → expr → tactic expr

(mk_eq_mpr h₁ h₂) is a more efficient version of (mk_app `eq.mpr [h₁, h₂])

source

meta constant tactic.subst_core :

expr → tactic unit

Given a local constant t, if t has type (lhs = rhs) apply substitution. Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t). The tactic fails if the given expression is not a local constant.

source

meta constant tactic.exact (e : expr) (md : tactic.transparency := semireducible) :

tactic unit

Close the current goal using e. Fail if the type of e is not definitionally equal to the target type.

source

meta constant tactic.to_expr (q : pexpr) (allow_mvars subgoals : bool := tt) :

tactic expr

Elaborate the given quoted expression with respect to the current main goal. Note that this means that any implicit arguments for the given pexpr will be applied with fresh metavariables. If allow_mvars is tt, then metavariables are tolerated and become new goals if subgoals is tt.

source

meta constant tactic.is_class :

expr → tactic bool

Return true if the given expression is a type class.

source

meta constant tactic.mk_instance :

expr → tactic expr

Try to create an instance of the given type class.

source

meta constant tactic.change (e : expr) (check : bool := tt) :

tactic unit

Change the target of the main goal. The input expression must be definitionally equal to the current target. If check is ff, then the tactic does not check whether e is definitionally equal to the current target. If it is not, then the error will only be detected by the kernel type checker.

source

meta constant tactic.assert_core :

name → expr → tactic unit

assert_core H T, adds a new goal for T, and change target to T -> target.

source

meta constant tactic.assertv_core :

name → expr → expr → tactic unit

assertv_core H T P, change target to (T -> target) if P has type T.

source

meta constant tactic.define_core :

name → expr → tactic unit

define_core H T, adds a new goal for T, and change target to let H : T := ?M in target in the current goal.

source

meta constant tactic.definev_core :

name → expr → expr → tactic unit

definev_core H T P, change target to let H : T := P in target if P has type T.

source

meta constant tactic.rotate_left :

ℕ → tactic unit

Rotate goals to the left. That is, rotate_left 1 takes the main goal and puts it to the back of the subgoal list.

source

meta constant tactic.get_goals :

tactic (list expr)

Gets a list of metavariables, one for each goal.

source

meta constant tactic.set_goals :

list expr → tactic unit

Replace the current list of goals with the given one. Each expr in the list should be a metavariable. Any assigned metavariables will be ignored.

source

meta def tactic.mk_tagged_proof (prop pr : expr) (tag : name) :

expr

Convenience function for creating ` for proofs.

source

inductive tactic.new_goals :

Type

non_dep_first : tactic.new_goals
non_dep_only : tactic.new_goals
all : tactic.new_goals

How to order the new goals made from an apply tactic. Supposing we were applying e : ∀ (a:α) (p : P(a)), Q

non_dep_first would produce goals ⊢ P(?m), ⊢ α. It puts the P goal at the front because none of the arguments after p in e depend on p. It doesn't matter what the result Q depends on.
non_dep_only would produce goal ⊢ P(?m).
all would produce goals ⊢ α, ⊢ P(?m).

source

structure tactic.apply_cfg :

Type

md : tactic.transparency
approx : bool
new_goals : tactic.new_goals
instances : bool
auto_param : bool
opt_param : bool
unify : bool

Configuration options for the apply tactic.

md sets how aggressively definitions are unfolded.
new_goals is the strategy for ordering new goals.
instances if tt, then apply tries to synthesize unresolved [...] arguments using type class resolution.
auto_param if tt, then apply tries to synthesize unresolved (h : p . tac_id) arguments using tactic tac_id.
opt_param if tt, then apply tries to synthesize unresolved (a : t := v) arguments by setting them to v.
unify if tt, then apply is free to assign existing metavariables in the goal when solving unification constraints. For example, in the goal |- ?x < succ 0, the tactic apply succ_lt_succ succeeds with the default configuration, but apply_with succ_lt_succ {unify := ff} doesn't since it would require Lean to assign ?x to succ ?y where ?y is a fresh metavariable.

source

meta constant tactic.apply_core (e : expr) (cfg : tactic.apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) :

tactic (list (name × expr))

Apply the expression e to the main goal, the unification is performed using the transparency mode in cfg. Supposing e : Π (a₁:α₁) ... (aₙ:αₙ), P(a₁,...,aₙ) and the target is Q, apply will attempt to unify Q with P(?a₁,...?aₙ). All of the metavariables that are not assigned are added as new metavariables. If cfg.approx is tt, then fallback to first-order unification, and approximate context during unification. cfg.new_goals specifies which unassigned metavariables become new goals, and their order. If cfg.instances is tt, then use type class resolution to instantiate unassigned meta-variables. The fields cfg.auto_param and cfg.opt_param are ignored by this tactic (See tactic.apply). It returns a list of all introduced meta variables and the parameter name associated with them, even the assigned ones.

source

meta constant tactic.mk_meta_univ :

tactic level

source

meta constant tactic.mk_meta_var :

expr → tactic expr

source

meta constant tactic.get_univ_assignment :

level → tactic level

Return the value assigned to the given universe meta-variable. Fail if argument is not an universe meta-variable or if it is not assigned.

source

meta constant tactic.get_assignment :

expr → tactic expr

Return the value assigned to the given meta-variable. Fail if argument is not a meta-variable or if it is not assigned.

source

meta constant tactic.is_assigned :

expr → tactic bool

Return true if the given meta-variable is assigned. Fail if argument is not a meta-variable.

source

meta constant tactic.mk_fresh_name :

tactic name

Make a name that is guaranteed to be unique. Eg _fresh.1001.4667. These will be different for each run of the tactic.

source

meta constant tactic.induction (h : expr) (ns : list name := list.nil) (rec : option name := none) (md : tactic.transparency := semireducible) :

tactic (list (name × list expr × list (name × expr)))

Induction on h using recursor rec, names for the new hypotheses are retrieved from ns. If ns does not have sufficient names, then use the internal binder names in the recursor. It returns for each new goal the name of the constructor (if rec_name is a builtin recursor), a list of new hypotheses, and a list of substitutions for hypotheses depending on h. The substitutions map internal names to their replacement terms. If the replacement is again a hypothesis the user name stays the same. The internal names are only valid in the original goal, not in the type context of the new goal. Remark: if rec_name is not a builtin recursor, we use parameter names of rec_name instead of constructor names.

If rec is none, then the type of h is inferred, if it is of the form C ..., tactic uses C.rec

source

meta constant tactic.cases_core (h : expr) (ns : list name := list.nil) (md : tactic.transparency := semireducible) :

tactic (list (name × list expr × list (name × expr)))

Apply cases_on recursor, names for the new hypotheses are retrieved from ns. h must be a local constant. It returns for each new goal the name of the constructor, a list of new hypotheses, and a list of substitutions for hypotheses depending on h. The number of new goals may be smaller than the number of constructors. Some goals may be discarded when the indices to not match. See induction for information on the list of substitutions.

The cases tactic is implemented using this one, and it relaxes the restriction of h.

Note: There is one "new hypothesis" for every constructor argument. These are usually local constants, but due to dependent pattern matching, they can also be arbitrary terms.

source

meta constant tactic.destruct (e : expr) (md : tactic.transparency := semireducible) :

tactic unit

Similar to cases tactic, but does not revert/intro/clear hypotheses.

source

meta constant tactic.generalize (e : expr) (n : name := name.mk_string "_x" name.anonymous) (md : tactic.transparency := semireducible) :

tactic unit

Generalizes the target with respect to e.

source

meta constant tactic.instantiate_mvars :

expr → tactic expr

instantiate assigned metavariables in the given expression

source

meta constant tactic.add_decl :

declaration → tactic unit

Add the given declaration to the environment

source

meta constant tactic.set_env_core :

environment → tactic unit

Changes the environment to the new_env. The new environment does not need to be a descendant of the old one. Use with care.

source

meta constant tactic.set_env :

environment → tactic unit

Changes the environment to the new_env. new_env needs to be a descendant from the current environment.

source

meta constant tactic.doc_string :

name → tactic string

doc_string env d k returns the doc string for d (if available)

source

meta constant tactic.add_doc_string :

name → string → tactic unit

Set the docstring for the given declaration.

source

meta constant tactic.add_aux_decl (c : name) (type val : expr) (is_lemma : bool) :

tactic expr

Create an auxiliary definition with name c where type and value may contain local constants and meta-variables. This function collects all dependencies (universe parameters, universe metavariables, local constants (aka hypotheses) and metavariables). It updates the environment in the tactic_state, and returns an expression of the form

      (c.{l_1 ... l_n} a_1 ... a_m)

where l_i's and a_j's are the collected dependencies.

source

meta constant tactic.olean_doc_strings :

tactic (list (option string × list (pos × string)))

Returns a list of all top-level (/-! ... -/) docstrings in the active module and imported ones. The returned object is a list of modules, indexed by (some filename) for imported modules and none for the active one, where each module in the list is paired with a list of (position_in_file, docstring) pairs.

source

meta def tactic.module_doc_strings :

tactic (list (option name × string))

Returns a list of docstrings in the active module. An entry in the list can be either:

a top-level (/-! ... -/) docstring, represented as (none, docstring)
a declaration-specific (/-- ... -/) docstring, represented as (some decl_name, docstring)

source

meta constant tactic.set_basic_attribute (attr_name c_name : name) (persistent : bool := ff) (prio : option ℕ := none) :

tactic unit

Set attribute attr_name for constant c_name with the given priority. If the priority is none, then use default

source

meta constant tactic.unset_attribute :

name → name → tactic unit

unset_attribute attr_name c_name

source

meta constant tactic.has_attribute :

name → name → tactic (bool × ℕ)

has_attribute attr_name c_name succeeds if the declaration decl_name has the attribute attr_name. The result is the priority and whether or not the attribute is persistent.

source

meta def tactic.copy_attribute (attr_name src tgt : name) (p : option bool := none) :

tactic unit

copy_attribute attr_name c_name p d_name copy attribute attr_name from src to tgt if it is defined for src; make it persistent if p is tt; if p is none, the copied attribute is made persistent iff it is persistent on src

source

meta constant tactic.decl_name :

tactic name

Name of the declaration currently being elaborated.

source

meta constant tactic.save_type_info {elab : bool} :

expr → expr elab → tactic unit

save_type_info e ref save (typeof e) at position associated with ref

source

meta constant tactic.save_info_thunk :

pos → (unit → format) → tactic unit

source

meta constant tactic.open_namespaces :

tactic (list name)

Return list of currently open namespaces

source

meta constant tactic.kdepends_on (e t : expr) (md : tactic.transparency := reducible) :

tactic bool

Return tt iff t "occurs" in e. The occurrence checking is performed using keyed matching with the given transparency setting.

We say t occurs in e by keyed matching iff there is a subterm s s.t. t and s have the same head, and is_def_eq t s md

The main idea is to minimize the number of is_def_eq checks performed.

source

meta constant tactic.kabstract (e t : expr) (md : tactic.transparency := reducible) (unify : bool := tt) :

tactic expr

Abstracts all occurrences of the term t in e using keyed matching. If unify is ff, then matching is used instead of unification. That is, metavariables occurring in e are not assigned.

source

meta constant tactic.sleep (msecs : ℕ) :

tactic unit

Blocks the execution of the current thread for at least msecs milliseconds. This tactic is used mainly for debugging purposes.

source

meta constant tactic.type_check (e : expr) (md : tactic.transparency := semireducible) :

tactic unit

Type check e with respect to the current goal. Fails if e is not type correct.

source

def tactic.tag :

Type

A tag is a list of names. These are attached to goals to help tactics track them.

Equations

tactic.tag = list name

source

meta constant tactic.enable_tags (b : bool) :

tactic unit

Enable/disable goal tagging.

source

meta constant tactic.tags_enabled :

tactic bool

Return tt iff goal tagging is enabled.

source

meta constant tactic.set_tag (g : expr) (t : tactic.tag) :

tactic unit

Tag goal g with tag t. It does nothing if goal tagging is disabled. Remark: set_goal g [] removes the tag

source

meta constant tactic.get_tag (g : expr) :

tactic tactic.tag

Return tag associated with g. Return [] if there is no tag.

source

meta constant tactic.unfreeze_local_instances :

tactic unit

Avoid this function! Use unfreezingI/resetI/etc. instead!

Unfreezes the current set of local instances. After this tactic, the instance cache is disabled.

source

meta constant tactic.freeze_local_instances :

tactic unit

Freeze the current set of local instances.

source

meta constant tactic.frozen_local_instances :

tactic (option (list expr))

source

meta constant tactic.with_ast {α : Type u} (ast : ℕ) (t : tactic α) :

tactic α

Run the provided tactic, associating it to the given AST node.

source

meta def tactic.induction' (h : expr) (ns : list name := list.nil) (rec : option name := none) (md : tactic.transparency := semireducible) :

tactic unit

source

meta def tactic.cleanup :

tactic unit

Remark: set_goals will erase any solved goal

source

meta def tactic.step {α : Type u} (t : tactic α) :

tactic unit

Auxiliary definition used to implement begin ... end blocks

source

meta def tactic.istep {α : Type u} (line0 col0 line col ast : ℕ) (t : tactic α) :

tactic unit

source

meta def tactic.is_prop (e : expr) :

tactic bool

source

meta def tactic.is_prop_decl (n : name) :

tactic bool

Return true iff n is the name of declaration that is a proposition.

source

meta def tactic.is_proof (e : expr) :

tactic bool

source

meta def tactic.whnf_no_delta (e : expr) :

tactic expr

source

meta def tactic.whnf_ginductive (e : expr) (md : tactic.transparency := semireducible) :

tactic expr

Return e in weak head normal form with respect to the given transparency setting, or e head is a generalized constructor or inductive datatype.

source

meta def tactic.whnf_target :

tactic unit

source

meta def tactic.unsafe_change (e : expr) :

tactic unit

Change the target of the main goal. The input expression must be definitionally equal to the current target. The tactic does not check whether e is definitionally equal to the current target. The error will only be detected by the kernel type checker.

source

meta def tactic.intro (n : name) :

tactic expr

Pi or elet introduction. Given the tactic state ⊢ Π x : α, Y, intro `hello will produce the state hello : α ⊢ Y[x/hello]. Returns the new local constant. Similarly for elet expressions. If the target is not a Pi or elet it will try to put it in WHNF.

source

meta def tactic.intro_fresh (n : name) (offset : option ℕ := none) :

tactic expr

A variant of intro which makes sure that the introduced hypothesis's name is unique in the context. If there is no hypothesis named n in the context yet, intro_fresh n is the same as intro n. If there is already a hypothesis named n, the new hypothesis is named n_1 (or n_2 if n_1 already exists, etc.). If offset is given, the new names are n_offset, n_offset+1 etc.

If n is _, intro_fresh n is the same as intro1. The offset is ignored in this case.

source

meta def tactic.intro1 :

tactic expr

Like intro except the name is derived from the bound name in the Π.

source

meta def tactic.intros :

tactic (list expr)

Repeatedly apply intro1 and return the list of new local constants in order of introduction.

source

meta def tactic.intro_lst (ns : list name) :

tactic (list expr)

Same as intros, except with the given names for the new hypotheses. Use the name _ to instead use the binder's name.

source

meta def tactic.intro_lst_fresh (ns : list name) :

tactic (list expr)

A variant of intro_lst which makes sure that the introduced hypotheses' names are unique in the context. See intro_fresh.

source

meta def tactic.intros_dep :

tactic (list expr)

Introduces new hypotheses with forward dependencies.

source

meta def tactic.introv :

list name → tactic (list expr)

source

meta def tactic.intron' (n : ℕ) :

tactic (list expr)

intron' n introduces n hypotheses and returns the resulting local constants. Fails if there are not at least n arguments to introduce. If you do not need the return value, use intron.

source

meta def tactic.intron_base (n : ℕ) (base : name) (offset : option ℕ := none) :

tactic (list expr)

Like intron' but the introduced hypotheses' names are derived from base, i.e. base, base_1 etc. The new names are unique in the context. If offset is given, the new names will be base_offset, base_offset+1 etc.

source

meta def tactic.intron_with :

ℕ → list name → (name := name.mk_string "_" name.anonymous) → (option ℕ := none) → tactic (list expr × list name)

intron_with i ns base offset introduces i hypotheses using the names from ns. If ns contains less than i names, the remaining hypotheses' names are derived from base and offset (as with intron_base). If base is _, the names are derived from the Π binder names.

Returns the introduced local constants and the remaining names from ns (if ns contains more than i names).

source

meta def tactic.resolve_constant (n : name) :

tactic name

Returns n fully qualified if it refers to a constant, or else fails.

source

meta def tactic.to_expr_strict (q : pexpr) :

tactic expr

source

meta def tactic.revert (l : expr) :

tactic ℕ

Example: with x : ℕ, h : P(x) ⊢ T(x), revert x returns 2 and produces the state ⊢ Π x, P(x) → T(x).

source

meta def tactic.revert_all :

tactic ℕ

source

meta def tactic.clear_lst :

list name → tactic unit

source

meta def tactic.match_not (e : expr) :

tactic expr

source

meta def tactic.match_and (e : expr) :

tactic (expr × expr)

source

meta def tactic.match_or (e : expr) :

tactic (expr × expr)

source

meta def tactic.match_iff (e : expr) :

tactic (expr × expr)

source

meta def tactic.match_eq (e : expr) :

tactic (expr × expr)

source

meta def tactic.match_ne (e : expr) :

tactic (expr × expr)

source

meta def tactic.match_heq (e : expr) :

tactic (expr × expr × expr × expr)

source

meta def tactic.match_refl_app (e : expr) :

tactic (name × expr × expr)

source

meta def tactic.match_app_of (e : expr) (n : name) :

tactic (list expr)

source

meta def tactic.get_local_type (n : name) :

tactic expr

source

meta def tactic.trace_result :

tactic unit

source

meta def tactic.rexact (e : expr) :

tactic unit

source

meta def tactic.any_hyp_aux {α : Type} (f : expr → tactic α) :

list expr → tactic α

source

meta def tactic.any_hyp {α : Type} (f : expr → tactic α) :

tactic α

source

meta def tactic.find_same_type :

expr → list expr → tactic expr

find_same_type t es tries to find in es an expression with type definitionally equal to t

source

meta def tactic.find_assumption (e : expr) :

tactic expr

source

meta def tactic.assumption :

tactic unit

source

meta def tactic.save_info (p : pos) :

tactic unit

source

meta def tactic.swap :

tactic unit

Swap first two goals, do nothing if tactic state does not have at least two goals.

source

meta def tactic.assert (h : name) (t : expr) :

tactic expr

assert h t, adds a new goal for t, and the hypothesis h : t in the current goal.

source

meta def tactic.assertv (h : name) (t v : expr) :

tactic expr

assertv h t v, adds the hypothesis h : t in the current goal if v has type t.

source

meta def tactic.define (h : name) (t : expr) :

tactic expr

define h t, adds a new goal for t, and the hypothesis h : t := ?M in the current goal.

source

meta def tactic.definev (h : name) (t v : expr) :

tactic expr

definev h t v, adds the hypothesis (h : t := v) in the current goal if v has type t.

source

meta def tactic.pose (h : name) (t : option expr := none) (pr : expr) :

tactic expr

Add h : t := pr to the current goal

source

meta def tactic.note (h : name) (t : option expr := none) (pr : expr) :

tactic expr

Add h : t to the current goal, given a proof pr : t

source

meta def tactic.num_goals :

tactic ℕ

Return the number of goals that need to be solved

source

meta def tactic.rotate_right (n : ℕ) [has_mod ℕ] :

tactic unit

Rotate the goals to the right by n. That is, take the goal at the back and push it to the front n times. [NOTE] We have to provide the instance argument [has_mod nat] because mod for nat was not defined yet

source

meta def tactic.rotate :

ℕ → tactic unit

Rotate the goals to the left by n. That is, put the main goal to the back n times.

source

meta def tactic.repeat (t : tactic unit) :

tactic unit

This tactic is applied to each goal. If the application succeeds, the tactic is applied recursively to all the generated subgoals until it eventually fails. The recursion stops in a subgoal when the tactic has failed to make progress. The tactic repeat never fails.

source

meta def tactic.first {α : Type u} :

list (tactic α) → tactic α

first [t_1, ..., t_n] applies the first tactic that doesn't fail. The tactic fails if all t_i's fail.

source

meta def tactic.solve1 {α : Type} (tac : tactic α) :

tactic α

Applies the given tactic to the main goal and fails if it is not solved.

source

meta def tactic.solve {α : Type} (ts : list (tactic α)) :

tactic α

solve [t_1, ... t_n] applies the first tactic that solves the main goal.

source

meta def tactic.focus {α : Type} (ts : list (tactic α)) :

tactic (list α)

focus [t_1, ..., t_n] applies t_i to the i-th goal. Fails if the number of goals is not n. Returns the results of t_i (one per goal).

source

meta def tactic.focus' (ts : list (tactic unit)) :

tactic unit

focus' [t_1, ..., t_n] applies t_i to the i-th goal. Fails if the number of goals is not n.

source

meta def tactic.focus1 {α : Type} (tac : tactic α) :

tactic α

source

meta def tactic.all_goals {α : Type} (tac : tactic α) :

tactic (list α)

Apply the given tactic to all goals. Return one result per goal.

source

meta def tactic.all_goals' (tac : tactic unit) :

tactic unit

Apply the given tactic to all goals.

source

meta def tactic.any_goals {α : Type} (tac : tactic α) :

tactic (list (option α))

Apply tac to any goal where it succeeds. The tactic succeeds if tac succeeds for at least one goal. The returned list contains the result of tac for each goal: some a if tac succeeded, or none if it did not.

source

meta def tactic.any_goals' (tac : tactic unit) :

tactic unit

Apply the given tactic to any goal where it succeeds. The tactic succeeds only if tac succeeds for at least one goal.

source

meta def tactic.seq {α β : Type} (tac1 : tactic α) (tac2 : α → tactic β) :

tactic (list β)

LCF-style AND_THEN tactic. It applies tac1 to the main goal, then applies tac2 to each goal produced by tac1.

source

meta def tactic.seq' (tac1 tac2 : tactic unit) :

tactic unit

LCF-style AND_THEN tactic. It applies tac1, and if succeed applies tac2 to each subgoal produced by tac1

source

meta def tactic.seq_focus {α β : Type} (tac1 : tactic α) (tacs2 : α → list (tactic β)) :

tactic (list β)

Applies tac1 to the main goal, then applies each of the tactics in tacs2 to one of the produced subgoals (like focus').

source

meta def tactic.seq_focus' (tac1 : tactic unit) (tacs2 : list (tactic unit)) :

tactic unit

Applies tac1 to the main goal, then applies each of the tactics in tacs2 to one of the produced subgoals (like focus).

source

@[protected, instance]

meta def tactic.andthen_seq :

has_andthen (tactic unit) (tactic unit) (tactic unit)

source

@[protected, instance]

meta def tactic.andthen_seq_focus :

has_andthen (tactic unit) (list (tactic unit)) (tactic unit)

source

meta constant tactic.is_trace_enabled_for :

name → bool

source

meta def tactic.when_tracing (n : name) (tac : tactic unit) :

tactic unit

Execute tac only if option trace.n is set to true.

source

meta def tactic.fail_if_no_goals :

tactic unit

Fail if there are no remaining goals.

source

meta def tactic.done :

tactic unit

Fail if there are unsolved goals.

source

meta def tactic.apply_opt_param :

tactic unit

source

meta def tactic.apply_auto_param :

tactic unit

source

meta def tactic.has_opt_auto_param (ms : list expr) :

tactic bool

source

meta def tactic.try_apply_opt_auto_param (cfg : tactic.apply_cfg) (ms : list expr) :

tactic unit

source

meta def tactic.has_opt_auto_param_for_apply (ms : list (name × expr)) :

tactic bool

source

meta def tactic.try_apply_opt_auto_param_for_apply (cfg : tactic.apply_cfg) (ms : list (name × expr)) :

tactic unit

source

meta def tactic.apply (e : expr) (cfg : tactic.apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) :

tactic (list (name × expr))

source

meta def tactic.fapply (e : expr) :

tactic (list (name × expr))

Same as apply but all arguments that weren't inferred are added to goal list.

source

meta def tactic.eapply (e : expr) :

tactic (list (name × expr))

Same as apply but only goals that don't depend on other goals are added to goal list.

source

meta def tactic.apply_instance :

tactic unit

Try to solve the main goal using type class resolution.

source

meta def tactic.mk_num_meta_univs :

ℕ → tactic (list level)

Create a list of universe meta-variables of the given size.

source

meta def tactic.mk_const (c : name) :

tactic expr

Return expr.const c [l_1, ..., l_n] where l_i's are fresh universe meta-variables.

source

meta def tactic.applyc (c : name) (cfg : tactic.apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) :

tactic unit

Apply the constant c

source

meta def tactic.eapplyc (c : name) :

tactic unit

source

meta def tactic.save_const_type_info (n : name) {elab : bool} (ref : expr elab) :

tactic unit

source

meta def tactic.mk_mvar :

tactic expr

Create a fresh universe ?u, a metavariable ?T : Type.{?u}, and return metavariable ?M : ?T. This action can be used to create a meta-variable when we don't know its type at creation time

source

meta def tactic.mk_sorry :

tactic expr

Makes a sorry macro with a meta-variable as its type.

source

meta def tactic.admit :

tactic unit

Closes the main goal using sorry.

source

meta def tactic.mk_local' (pp_name : name) (bi : binder_info) (type : expr) :

tactic expr

source

meta def tactic.mk_local_def (pp_name : name) (type : expr) :

tactic expr

source

meta def tactic.mk_local_pis :

expr → tactic (list expr × expr)

source

meta def tactic.get_pi_arity (type : expr) :

tactic ℕ

Compute the arity of the given (Pi-)type

source

meta def tactic.get_arity (fn : expr) :

tactic ℕ

Compute the arity of the given function

source

meta def tactic.triv :

tactic unit

source

meta def tactic.by_contradiction (H : name) :

tactic expr

source

meta def tactic.generalizes (es : list expr) (md : tactic.transparency := semireducible) :

tactic unit

source

meta def tactic.kdependencies (e : expr) (md : tactic.transparency := reducible) :

tactic (list expr)

Return all hypotheses that depends on e The dependency test is performed using kdepends_on with the given transparency setting.

source

meta def tactic.revert_kdependencies (e : expr) (md : tactic.transparency := reducible) :

tactic ℕ

Revert all hypotheses that depend on e

source

meta def tactic.revert_kdeps (e : expr) (md : tactic.transparency := reducible) :

tactic ℕ

source

meta def tactic.cases (e : expr) (ids : list name := list.nil) (md dmd : tactic.transparency := semireducible) :

tactic (list (name × list expr))

Similar to cases_core, but e doesn't need to be a hypothesis. Remark, it reverts dependencies using revert_kdeps.

Two different transparency modes are used md and dmd. The mode md is used with cases_core and dmd with generalize and revert_kdeps.

It returns the constructor names associated with each new goal and the newly introduced hypotheses. Note that while cases_core may return "new hypotheses" that are not local constants, this tactic only returns local constants.

source

meta def tactic.refine (e : pexpr) :

tactic unit

The same as exact except you can add proof holes.

source

meta def tactic.by_cases (e : expr) (h : name) :

tactic unit

by_cases p h splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch. The expression p needs to be a proposition.

The produced proof term is dite p ?m_1 ?m_2.

source

meta def tactic.funext_core :

list name → bool → tactic unit

source

meta def tactic.funext :

tactic unit

source

meta def tactic.funext_lst (ids : list name) :

tactic unit

source

meta def tactic.new_aux_decl_name :

tactic name

source

meta def tactic.abstract (tac : tactic unit) (suffix : option name := none) (zeta_reduce : bool := tt) :

tactic unit

source

meta def tactic.solve_aux {α : Type} (type : expr) (tac : tactic α) :

tactic (α × expr)

solve_aux type tac synthesize an element of 'type' using tactic 'tac'

source

meta def tactic.in_open_namespaces (d : name) :

tactic bool

Return tt iff 'd' is a declaration in one of the current open namespaces

source

meta def tactic.try_for {α : Type u_1} (max : ℕ) (tac : tactic α) :

tactic α

Execute tac for 'max' "heartbeats". The heartbeat is approx. the maximum number of memory allocations (in thousands) performed by 'tac'. This is a deterministic way of interrupting long running tactics.

source

meta def tactic.try_for_time {α : Type u_1} (max : ℕ) (tac : tactic α) :

tactic α

Execute tac for max milliseconds. Useful due to variance in the number of heartbeats taken by various tactics.

source

meta def tactic.updateex_env (f : environment → exceptional environment) :

tactic unit

source

meta def tactic.add_inductive (n : name) (ls : list name) (p : ℕ) (ty : expr) (is : list (name × expr)) (is_meta : bool := ff) :

tactic unit

source

meta def tactic.add_meta_definition (n : name) (lvls : list name) (type value : expr) :

tactic unit

source

meta def tactic.add_protected_decl (d : declaration) :

tactic unit

add declaration d as a protected declaration

source

meta def tactic.is_protected_decl (n : name) :

tactic bool

check if n is the name of a protected declaration

source

meta def tactic.add_defn_equations (lp : list name) (params : list expr) (fn : expr) (eqns : list (list pexpr × expr)) (is_meta : bool) :

tactic unit

add_defn_equations adds a definition specified by a list of equations.

The arguments:

lp: list of universe parameters
params: list of parameters (binders before the colon);
fn: a local constant giving the name and type of the declaration (with params in the local context);
eqns: a list of equations, each of which is a list of patterns (constructors applied to new local constants) and the branch expression;
is_meta: is the definition meta?

add_defn_equations can be used as:

 do my_add ← mk_local_def `my_add `(ℕ → ℕ),
     a ← mk_local_def `a ℕ,
     b ← mk_local_def `b ℕ,
     add_defn_equations [a] my_add
         [ ([``(nat.zero)], a),
           ([``(nat.succ %%b)], my_add b) ])
         ff -- non-meta

to create the following definition:

 def my_add (a : ℕ) : ℕ → ℕ
 | nat.zero := a
 | (nat.succ b) := my_add b

source

meta def tactic.revertible_local_context :

tactic (list expr)

Get the revertible part of the local context. These are the hypotheses that appear after the last frozen local instance in the local context. We call them revertible because revert can revert them, unlike those hypotheses which occur before a frozen instance.

source

meta def tactic.rename_many (renames : name_map name) (strict : bool := tt) (use_unique_names : bool := ff) :

tactic unit

Rename local hypotheses according to the given name_map. The name_map contains as keys those hypotheses that should be renamed; the associated values are the new names.

This tactic can only rename hypotheses which occur after the last frozen local instance. If you need to rename earlier hypotheses, try unfreezing (rename_many ...).

If strict is true, we fail if name_map refers to hypotheses that do not appear in the local context or that appear before a frozen local instance. Conversely, if strict is false, some entries of name_map may be silently ignored.

If use_unique_names is true, the keys of name_map should be the unique names of hypotheses to be renamed. Otherwise, the keys should be display names.

Note that we allow shadowing, so renamed hypotheses may have the same name as other hypotheses in the context. If use_unique_names is false and there are multiple hypotheses with the same display name in the context, they are all renamed.

source

meta def tactic.rename (curr new : name) :

tactic unit

Rename a local hypothesis. This is a special case of rename_many; see there for caveats.

source

meta def tactic.rename_unstable (curr new : name) :

tactic unit

Rename a local hypothesis. Unlike rename and rename_many, this tactic does not preserve the order of hypotheses. Its implementation is simpler (and therefore probably faster) than that of rename.

source

meta def tactic.replace_hyp (h new_type eq_pr : expr) (tag : name := name.mk_string "star" (name.mk_string "unit" name.anonymous)) :

tactic expr

"Replace" hypothesis h : type with h : new_type where eq_pr is a proof that (type = new_type). The tactic actually creates a new hypothesis with the same user facing name, and (tries to) clear h. The clear step fails if h has forward dependencies. In this case, the old h will remain in the local context. The tactic returns the new hypothesis.

source

meta def tactic.main_goal :

tactic expr

source