mathlib3 documentation

core / init.meta.tactic

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

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.

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.

@[protected, instance]
@[protected, instance]
@[reducible]
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.
@[reducible]
meta def tactic_result (α : Type u_1) :
Type u_1
meta def tactic.failed {α : Type} :

Cause the tactic to fail with no error message.

meta def tactic.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) :
@[protected, instance]
meta def tactic.up {α : Type u₂} (t : tactic α) :
meta def tactic.down {α : Type u₂} (t : tactic (ulift α)) :
@[class]
meta structure interactive.executor (m : Type Type u) [monad m] :
Type (max 1 u)

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 of this typeclass
@[protected, instance]

Default executor instance for tactics themselves

meta def tactic.skip  :

Does nothing.

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

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

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

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

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

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.

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

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.

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

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

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

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

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

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

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

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

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

meta def tactic.returnopt {α : Type u} (e : option α) :
@[protected, instance]
meta def tactic.opt_to_tac {α : Type u} :
meta def tactic.decorate_ex {α : Type u} (msg : format) (t : tactic α) :

Decorate t's exceptions with msg.

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

Set the tactic_state.

Get the tactic_state.

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

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.

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

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.

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

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.

meta def tactic.save_options {α : Type} (t : tactic α) :
meta def tactic.returnex {α : Type} (e : exceptional α) :
@[protected, instance]
meta def tactic.ex_to_tac {α : Type} :
@[protected, instance]
meta def tactic.pp {α : Type u} [has_to_tactic_format α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
meta def reflected.has_to_tactic_format {α : Sort u_1} (a : α) :
@[protected, instance]
meta def tactic.trace {α : Type u} [has_to_tactic_format α] (a : α) :
meta def tactic.timetac {α : Type u} (desc : string) (t : thunk (tactic α)) :
inductive tactic.transparency  :

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.
Instances for tactic.transparency
meta constant tactic.eval_expr (α : Type u) [reflected (Type u) α] :

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

meta constant tactic.result  :

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.

meta constant tactic.format_result  :

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.

meta constant tactic.target  :

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

meta constant tactic.intron  :
meta constant tactic.clear  :

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

meta constant tactic.revert_lst  :

revert_lst : list exprtactic 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).

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

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.

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

meta constant tactic.head_beta  :

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

meta constant tactic.head_zeta  :

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

meta constant tactic.zeta  :

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

meta constant tactic.head_eta  :

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

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

Similar to unify, but it treats metavariables as constants.

meta constant tactic.infer_type  :

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

meta constant tactic.get_local  :

Get the local_const expr for the given name.

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

meta constant tactic.local_context  :

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

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

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.

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

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

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

meta constant tactic.mk_congr  :

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

meta constant tactic.mk_eq_refl  :

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

meta constant tactic.mk_eq_symm  :

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

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

meta constant tactic.mk_eq_mp  :

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

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

meta constant tactic.subst_core  :

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.

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

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

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.

meta constant tactic.is_class  :

Return true if the given expression is a type class.

meta constant tactic.mk_instance  :

Try to create an instance of the given type class.

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

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.

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

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

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

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

meta constant tactic.rotate_left  :

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

meta constant tactic.get_goals  :

Gets a list of metavariables, one for each goal.

meta constant tactic.set_goals  :

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.

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

Convenience function for creating ` for proofs.

inductive 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).
Instances for tactic.new_goals
structure tactic.apply_cfg  :

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.
Instances for tactic.apply_cfg

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.

meta constant tactic.mk_meta_univ  :

Create a fresh meta universe variable.

meta constant tactic.mk_meta_var  :

Create a fresh meta-variable with the given type. The scope of the new meta-variable is the local context of the main goal.

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.

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

meta constant tactic.is_assigned  :

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

meta constant tactic.mk_fresh_name  :

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

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

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.

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

Generalizes the target with respect to e.

instantiate assigned metavariables in the given expression

Add the given declaration to the environment

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

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

meta constant tactic.doc_string  :

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

Set the docstring for the given declaration.

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

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.

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.

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)
meta constant tactic.set_basic_attribute (attr_name c_name : name) (persistent : bool := bool.ff) (prio : option := option.none) :

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

unset_attribute attr_name c_name

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.

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

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

meta constant tactic.decl_name  :

Name of the declaration currently being elaborated.

meta constant tactic.save_type_info {elab : bool} :

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

meta constant tactic.open_namespaces  :

Return list of currently open namespaces

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.

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.

meta constant tactic.sleep (msecs : ) :

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

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

def tactic.tag  :

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

Equations
meta constant tactic.enable_tags (b : bool) :

Enable/disable goal tagging.

meta constant tactic.tags_enabled  :

Return tt iff goal tagging is enabled.

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

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

meta constant tactic.get_tag (g : expr) :

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

By default, Lean only considers local instances in the header of declarations. This has two main benefits. 1- Results produced by the type class resolution procedure can be easily cached. 2- The set of local instances does not have to be recomputed.

This approach has the following disadvantages: 1- Frozen local instances cannot be reverted. 2- Local instances defined inside of a declaration are not considered during type class resolution.

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

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

Freeze the current set of local instances.

Return the list of frozen local instances. Return none if local instances were not frozen.

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

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

meta def tactic.cleanup  :

Remark: set_goals will erase any solved goal

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

Auxiliary definition used to implement begin ... end blocks

meta def tactic.istep {α : Type u} (line0 col0 line col ast : ) (t : tactic α) :
meta def tactic.is_prop (e : expr) :
meta def tactic.is_prop_decl (n : name) :

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

meta def tactic.is_proof (e : 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.

meta def tactic.unsafe_change (e : expr) :

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.

meta def tactic.intro (n : name) :

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.

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

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.

meta def tactic.intro1  :

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

meta def tactic.intros  :

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

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

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

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

Introduces new hypotheses with forward dependencies.

meta def tactic.intron' (n : ) :

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.

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

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.

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

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

meta def tactic.revert (l : expr) :

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

Revert "all" hypotheses. Actually, the tactic only reverts hypotheses occurring after the last frozen local instance. Recall that frozen local instances cannot be reverted, use unfreezing revert_all instead.

meta def tactic.match_not (e : expr) :
meta def tactic.match_and (e : expr) :
meta def tactic.match_or (e : expr) :
meta def tactic.match_iff (e : expr) :
meta def tactic.match_eq (e : expr) :
meta def tactic.match_ne (e : expr) :
meta def tactic.match_app_of (e : expr) (n : name) :
meta def tactic.rexact (e : expr) :
meta def tactic.any_hyp_aux {α : Type} (f : expr tactic α) :
meta def tactic.any_hyp {α : Type} (f : expr tactic α) :

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

meta def tactic.save_info (p : pos) :
meta def tactic.swap  :

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

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

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

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

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

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

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

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

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

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

Add h : t := pr to the current goal

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

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

meta def tactic.num_goals  :

Return the number of goals that need to be solved

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

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

meta def tactic.repeat (t : 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

Apply the given tactic to all goals.

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

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.

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

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

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

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

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

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

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

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

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

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

@[protected, instance]
@[protected, instance]
meta def tactic.when_tracing (n : name) (tac : tactic unit) :

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

Fail if there are no remaining goals.

meta def tactic.done  :

Fail if there are unsolved goals.

meta def tactic.fapply (e : expr) :

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

meta def tactic.eapply (e : expr) :

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

Try to solve the main goal using type class resolution.

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

meta def tactic.mk_const (c : name) :

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

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

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

meta def tactic.mk_sorry  :

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

meta def tactic.admit  :

Closes the main goal using sorry.

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

Compute the arity of the given (Pi-)type

meta def tactic.get_arity (fn : expr) :

Compute the arity of the given function

meta def tactic.triv  :

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

Revert all hypotheses that depend on e

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.

meta def tactic.refine (e : pexpr) :

The same as exact except you can add proof holes.

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

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.

meta def tactic.abstract (tac : tactic unit) (suffix : option name := option.none) (zeta_reduce : bool := bool.tt) :
meta def tactic.solve_aux {α : Type} (type : expr) (tac : tactic α) :

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

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

meta def tactic.try_for {α : Type u_1} (max : ) (tac : 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.

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

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

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

Add a new inductive datatype to the environment name, universe parameters, number of parameters, type, constructors (name and type), is_meta

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

add declaration d as a protected declaration

check if n is the name of a protected declaration

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

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

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.

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

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.

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

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

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

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.

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

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

Goal tagging support

meta def tactic.with_enable_tags {α : Type} (t : tactic α) (b : bool := bool.tt) :
meta def tactic.subst (h : expr) :
meta def list.for_each {α : Type u_1} :
meta def list.any_of {α : Type u_1} {β : Type} :
list α tactic β) tactic β

Install monad laws tactic and use it to prove some instances.

meta def order_laws_tac  :

Try to prove with iff.refl.

meta def monad_from_pure_bind {m : Type u Type v} (pure : Π {α : Type u}, α m α) (bind : Π {α β : Type u}, m α m β) m β) :
@[protected, instance]
meta def task.monad  :
meta def tactic.replace_target (new_target pr : expr) (tag : name := name.mk_string "star" (name.mk_string "unit" name.anonymous)) :
meta def tactic.eval_pexpr (α : Type) [reflected Type α] (e : pexpr) :
meta def tactic.run_simple {α : Type u_1} :