Mathlib tactics - mathlib docs

Instance cache tactics

For performance reasons, Lean does not automatically update its database of class instances during a proof. The group of tactics described below helps to force such updates. For a simple (but very artificial) example, consider the function default from the core library. It has type Π (α : Sort u) [inhabited α], α, so one can use default only if Lean can find a registered instance of inhabited α. Because the database of such instance is not automatically updated during a proof, the following attempt won't work (Lean will not pick up the instance from the local context):

def my_id (α : Type) : α → α :=
begin
  intro x,
  have : inhabited α := ⟨x⟩,
  exact default, -- Won't work!
end

However, it will work, producing the identity function, if one replaces have by its variant haveI described below.

resetI: Reset the instance cache. This allows any instances currently in the context to be used in typeclass inference.
unfreezingI { tac }: Unfreeze local instances while executing the tactic tac.
introI/introsI: intro/intros followed by resetI. Like intro/intros, but uses the introduced variable in typeclass inference.
casesI: like cases, but can also be used with instance arguments.
substI: like subst, but can also substitute in type-class arguments
haveI/letI: have/let followed by resetI. Used to add typeclasses to the context so that they can be used in typeclass inference.
exactI: resetI followed by exact. Like exact, but uses all variables in the context for typeclass inference.

Tags:

type class
context management

Related declarations

Import using

imported by default

abel

Evaluate expressions in the language of additive, commutative monoids and groups. It attempts to prove the goal outright if there is no at specifier and the target is an equality, but if this fails, it falls back to rewriting all monoid expressions into a normal form. If there is an at specifier, it rewrites the given target into a normal form.

abel! will use a more aggressive reducibility setting to identify atoms. This can prove goals that abel cannot, but is more expensive.

example {α : Type*} {a b : α} [add_comm_monoid α] : a + (b + a) = a + a + b := by abel
example {α : Type*} {a b : α} [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel
example {α : Type*} {a b : α} [add_comm_group α] (hyp : a + a - a = b - b) : a = 0 :=
by { abel at hyp, exact hyp }
example {α : Type*} {a b : α} [add_comm_group α] : (a + b) - (id a + b) = 0 := by abel!

Tags:

arithmetic
decision procedure

Related declarations

tactic.interactive.abel

Import using

import tactic.abel
import tactic

abstract

abstract id { t } tries to use tactic t to solve the main goal. If it succeeds, it abstracts the goal as an independent definition or theorem with name id. If id is omitted, a name is generated automatically.

Tags:

core
proof extraction

Related declarations

tactic.interactive.abstract

Import using

imported by default

ac_mono

ac_mono reduces the f x ⊑ f y, for some relation ⊑ and a monotonic function f to x ≺ y.

ac_mono* unwraps monotonic functions until it can't.

ac_mono^k, for some literal number k applies monotonicity k times.

ac_mono := h, with h a hypothesis, unwraps monotonic functions and uses h to solve the remaining goal. Can be combined with * or ^k: ac_mono* := h

ac_mono : p asserts p and uses it to discharge the goal result unwrapping a series of monotonic functions. Can be combined with * or ^k: ac_mono* : p

In the case where f is an associative or commutative operator, ac_mono will consider any possible permutation of its arguments and use the one the minimizes the difference between the left-hand side and the right-hand side.

To use it, first import tactic.monotonicity.

ac_mono can be used as follows:

example (x y z k m n : ℕ)
  (h₀ : z ≥ 0)
  (h₁ : x ≤ y) :
  (m + x + n) * z + k ≤ z * (y + n + m) + k :=
begin
  ac_mono,
  -- ⊢ (m + x + n) * z ≤ z * (y + n + m)
  ac_mono,
  -- ⊢ m + x + n ≤ y + n + m
  ac_mono,
end

As with mono*, ac_mono* solves the goal in one go and so does ac_mono* := h₁. The latter syntax becomes especially interesting in the following example:

example (x y z k m n : ℕ)
  (h₀ : z ≥ 0)
  (h₁ : m + x + n ≤ y + n + m) :
  (m + x + n) * z + k ≤ z * (y + n + m) + k :=
by ac_mono* := h₁.

By giving ac_mono the assumption h₁, we are asking ac_refl to stop earlier than it would normally would.

Tags:

monotonicity

Related declarations

tactic.interactive.ac_mono

Import using

import tactic.monotonicity.interactive
import tactic

ac_refl

Proves a goal of the form s = t when s and t are expressions built up out of a binary operation, and equality can be proved using associativity and commutativity of that operation.

Tags:

core
lemma application
finishing

Related declarations

Import using

imported by default

all_goals

all_goals { t } applies the tactic t to every goal, and succeeds if each application succeeds.

Tags:

core
goal management

Related declarations

tactic.interactive.all_goals

Import using

imported by default

any_goals

any_goals { t } applies the tactic t to every goal, and succeeds if at least one application succeeds.

Tags:

core
goal management

Related declarations

tactic.interactive.any_goals

Import using

imported by default

apply

The apply tactic tries to match the current goal against the conclusion of the type of term. The argument term should be a term well-formed in the local context of the main goal. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones.

The apply tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.

Tags:

core
basic
lemma application

Related declarations

tactic.interactive.apply

Import using

imported by default

apply_assumption

apply_assumption looks for an assumption of the form ... → ∀ _, ... → head where head matches the current goal.

If this fails, apply_assumption will call symmetry and try again.

If this also fails, apply_assumption will call exfalso and try again, so that if there is an assumption of the form P → ¬ Q, the new tactic state will have two goals, P and Q.

Optional arguments:

lemmas: a list of expressions to apply, instead of the local constants
tac: a tactic to run on each subgoal after applying an assumption; if this tactic fails, the corresponding assumption will be rejected and the next one will be attempted.

Tags:

context management
lemma application

Related declarations

tactic.interactive.apply_assumption

Import using

import tactic.solve_by_elim
import tactic.basic

apply_auto_param

If the target of the main goal is an auto_param, executes the associated tactic.

Tags:

core
lemma application

Related declarations

tactic.interactive.apply_auto_param

Import using

imported by default

apply_congr

Apply a congruence lemma inside conv mode.

When called without an argument apply_congr will try applying all lemmas marked with @[congr]. Otherwise apply_congr e will apply the lemma e.

Recall that a goal that appears as ∣ X in conv mode represents a goal of ⊢ X = ?m, i.e. an equation with a metavariable for the right hand side.

To successfully use apply_congr e, e will need to be an equation (possibly after function arguments), which can be unified with a goal of the form X = ?m. The right hand side of e will then determine the metavariable, and conv will subsequently replace X with that right hand side.

As usual, apply_congr can create new goals; any of these which are not equations with a metavariable on the right hand side will be hard to deal with in conv mode. Thus apply_congr automatically calls intros on any new goals, and fails if they are not then equations.

In particular it is useful for rewriting inside the operand of a finset.sum, as it provides an extra hypothesis asserting we are inside the domain.

For example:

example (f g : ℤ → ℤ) (S : finset ℤ) (h : ∀ m ∈ S, f m = g m) :
  finset.sum S f = finset.sum S g :=
begin
  conv_lhs
  { -- If we just call `congr` here, in the second goal we're helpless,
    -- because we are only given the opportunity to rewrite `f`.
    -- However `apply_congr` uses the appropriate `@[congr]` lemma,
    -- so we get to rewrite `f x`, in the presence of the crucial `H : x ∈ S` hypothesis.
    apply_congr,
    skip,
    simp [h, H], }
end

In the above example, when the apply_congr tactic is called it gives the hypothesis H : x ∈ S which is then used to rewrite the f x to g x.

Tags:

conv
congruence
rewriting

Related declarations

conv.interactive.apply_congr

Import using

import tactic.converter.apply_congr
import tactic.basic

apply_fun

Apply a function to an equality or inequality in either a local hypothesis or the goal.

If we have h : a = b, then apply_fun f at h will replace this with h : f a = f b.
If we have h : a ≤ b, then apply_fun f at h will replace this with h : f a ≤ f b, and create a subsidiary goal monotone f. apply_fun will automatically attempt to discharge this subsidiary goal using mono, or an explicit solution can be provided with apply_fun f at h using P, where P : monotone f.
If the goal is a ≠ b, apply_fun f will replace this with f a ≠ f b.
If the goal is a = b, apply_fun f will replace this with f a = f b, and create a subsidiary goal injective f. apply_fun will automatically attempt to discharge this subsidiary goal using local hypotheses, or if f is actually an equiv, or an explicit solution can be provided with apply_fun f using P, where P : injective f.
If the goal is a ≤ b (or similarly for a < b), and f is actually an order_iso, apply_fun f will replace the goal with f a ≤ f b. If f is anything else (e.g. just a function, or an equiv), apply_fun will fail.

Typical usage is:

open function

example (X Y Z : Type) (f : X → Y) (g : Y → Z) (H : injective $ g ∘ f) :
  injective f :=
begin
  intros x x' h,
  apply_fun g at h,
  exact H h
end

Tags:

context management

Related declarations

tactic.interactive.apply_fun

Import using

import tactic.apply_fun
import tactic

apply_instance

This tactic tries to close the main goal ... ⊢ t by generating a term of type t using type class resolution.

Tags:

core
type class

Related declarations

tactic.interactive.apply_instance

Import using

imported by default

apply_opt_param

If the target of the main goal is an opt_param, assigns the default value.

Tags:

core
lemma application

Related declarations

tactic.interactive.apply_opt_param

Import using

imported by default

apply_rules

apply_rules hs n applies the list of lemmas hs and assumption on the first goal and the resulting subgoals, iteratively, at most n times. n is optional, equal to 50 by default. You can pass an apply_cfg option argument as apply_rules hs n opt. (A typical usage would be with apply_rules hs n { md := reducible }), which asks apply_rules to not unfold semireducible definitions (i.e. most) when checking if a lemma matches the goal.)

hs can contain user attributes: in this case all theorems with this attribute are added to the list of rules.

For instance:

@[user_attribute]
meta def mono_rules : user_attribute :=
{ name := `mono_rules,
  descr := "lemmas usable to prove monotonicity" }

attribute [mono_rules] add_le_add mul_le_mul_of_nonneg_right

lemma my_test {a b c d e : real} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) :
a + c * e + a + c + 0 ≤ b + d * e + b + d + e :=
-- any of the following lines solve the goal:
add_le_add (add_le_add (add_le_add (add_le_add h1 (mul_le_mul_of_nonneg_right h2 h3)) h1 ) h2) h3
by apply_rules [add_le_add, mul_le_mul_of_nonneg_right]
by apply_rules [mono_rules]
by apply_rules mono_rules
```

Tags:

lemma application

Related declarations

tactic.interactive.apply_rules

Import using

import tactic.interactive
import tactic.basic

apply_with

Similar to the apply tactic, but allows the user to provide a apply_cfg configuration object.

Tags:

core
lemma application

Related declarations

tactic.interactive.apply_with

Import using

imported by default

assoc_rewrite

assoc_rewrite [h₀,← h₁] at ⊢ h₂ behaves like rewrite [h₀,← h₁] at ⊢ h₂ with the exception that associativity is used implicitly to make rewriting possible.

It works for any function f for which an is_associative f instance can be found.

example {α : Type*} (f : α → α → α) [is_associative α f] (a b c d x : α) :
  let infix `~` := f in
  b ~ c = x → (a ~ b ~ c ~ d) = (a ~ x ~ d) :=
begin
  intro h,
  assoc_rw h,
end

Tags:

rewriting

Related declarations

Import using

import tactic.rewrite
import tactic.basic

assume

Assuming the target of the goal is a Pi or a let, assume h : t unifies the type of the binder with t and introduces it with name h, just like intro h. If h is absent, the tactic uses the name this. If t is omitted, it will be inferred.

assume (h₁ : t₁) ... (hₙ : tₙ) introduces multiple hypotheses. Any of the types may be omitted, but the names must be present.

Tags:

core
logic

Related declarations

tactic.interactive.assume

Import using

imported by default

assumption

This tactic looks in the local context for a hypothesis whose type is equal to the goal target. If it finds one, it uses it to prove the goal, and otherwise it fails.

Tags:

core
basic
finishing

Related declarations

tactic.interactive.assumption

Import using

imported by default

assumption'

Try to apply assumption to all goals.

Tags:

core
goal management

Related declarations

tactic.interactive.assumption'

Import using

imported by default

async

Proves the first goal asynchronously as a separate lemma.

Tags:

core
goal management
combinator
proof extraction

Related declarations

tactic.interactive.async

Import using

imported by default

by_cases

by_cases p splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch. You can specify the name of the new hypothesis using the syntax by_cases h : p.

If p is not already decidable, by_cases will use the instance classical.prop_decidable p.

Tags:

core
basic
logic
case bashing

Related declarations

tactic.interactive.by_cases

Import using

imported by default

by_contra / by_contradiction

If the target of the main goal is a proposition p, by_contra h reduces the goal to proving false using the additional hypothesis h : ¬ p. If h is omitted, a name is generated automatically.

This tactic requires that p is decidable. To ensure that all propositions are decidable via classical reasoning, use open_locale classical (or local attribute [instance, priority 10] classical.prop_decidable if you are not using mathlib).

Tags:

core
logic

Related declarations

Import using

imported by default

by_contra'

If the target of the main goal is a proposition p, by_contra' reduces the goal to proving false using the additional hypothesis h : ¬ p. by_contra' h can be used to name the hypothesis h : ¬ p. The hypothesis ¬ p will be negation normalized using push_neg. For instance, ¬ a < b will be changed to b ≤ a. by_contra' h : q will normalize negations in ¬ p, normalize negations in q, and then check that the two normalized forms are equal. The resulting hypothesis is the pre-normalized form, q.

If the name h is not explicitly provided, then this will be used as name.

This tactic uses classical reasoning. It is a variant on the tactic by_contra (tactic.interactive.by_contra).

Examples:

example : 1 < 2 :=
begin
  by_contra' h,
  -- h : 2 ≤ 1 ⊢ false
end

example : 1 < 2 :=
begin
  by_contra' h : ¬ 1 < 2,
  -- h : ¬ 1 < 2 ⊢ false
end
```

Tags:

logic

Related declarations

tactic.interactive.by_contra'

Import using

import tactic.by_contra
import tactic

cancel_denoms

cancel_denoms attempts to remove numerals from the denominators of fractions. It works on propositions that are field-valued inequalities.

variables {α : Type} [linear_ordered_field α] (a b c : α)

example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c :=
begin
  cancel_denoms at h,
  exact h
end

example (h : a > 0) : a / 5 > 0 :=
begin
  cancel_denoms,
  exact h
end
```

Tags:

simplification

Related declarations

tactic.interactive.cancel_denoms

Import using

import tactic.cancel_denoms
import tactic

case

Focuses on a goal ('case') generated by induction, cases or with_cases.

The goal is selected by giving one or more names which must match exactly one goal. A goal is matched if the given names are a suffix of its goal tag. Additionally, each name in the sequence can be abbreviated to a suffix of the corresponding name in the goal tag. Thus, a goal with tag

nat.zero, list.nil

can be selected with any of these invocations (among others):

case nat.zero list.nil {...}
case nat.zero nil      {...}
case zero     nil      {...}
case          nil      {...}

Additionally, the form

case C : N₀ ... Nₙ {...}

can be used to rename hypotheses introduced by the preceding cases/induction/with_cases, using the names Nᵢ. For example:

example (xs : list ℕ) : xs = xs :=
begin
  induction xs,
  case nil { reflexivity },
  case cons : x xs ih {
    -- x : ℕ, xs : list ℕ, ih : xs = xs
    reflexivity }
end

Note that this renaming functionality only work reliably directly after an induction/cases/with_cases. If you need to perform additional work after an induction or cases (e.g. introduce hypotheses in all goals), use with_cases.

Multiple cases can be handled by the same tactic block with

case [A : N₀ ... Nₙ, B : M₀ ... Mₙ] {...}

Tags:

core
goal management

Related declarations

tactic.interactive.case

Import using

imported by default

cases

Assuming x is a variable in the local context with an inductive type, cases x splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the case split affects that hypothesis as well.

For example, given n : nat and a goal with a hypothesis h : P n and target Q n, cases n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypothesis h : P (nat.succ a) and target Q (nat.succ a). Here the name a is chosen automatically.

cases e, where e is an expression instead of a variable, generalizes e in the goal, and then cases on the resulting variable.

cases e with y₁ ... yₙ, where e is a variable or an expression, specifies that the sequence of names y₁ ... yₙ should be used for the arguments to the constructors, including implicit arguments. If the list does not include enough names for all of the arguments, additional names are generated automatically. If too many names are given, the extra ones are ignored. Underscores can be used in the list, in which case the corresponding names are generated automatically.

cases h : e, where e is a variable or an expression, performs cases on e as above, but also adds a hypothesis h : e = ... to each hypothesis, where ... is the constructor instance for that particular case.

Tags:

core
basic
induction

Related declarations

tactic.interactive.cases

Import using

imported by default

cases_matching / casesm

cases_matching p applies the cases tactic to a hypothesis h : type if type matches the pattern p.

cases_matching [p_1, ..., p_n] applies the cases tactic to a hypothesis h : type if type matches one of the given patterns.

cases_matching* p is a more efficient and compact version of focus1 { repeat { cases_matching p } }. It is more efficient because the pattern is compiled once.

casesm is shorthand for cases_matching.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.

cases_matching* [_ ∨ _, _ ∧ _]

Tags:

core
induction
context management

Related declarations

Import using

imported by default

cases_type

cases_type I applies the cases tactic to a hypothesis h : (I ...)
cases_type I_1 ... I_n applies the cases tactic to a hypothesis h : (I_1 ...) or ... or h : (I_n ...)
cases_type* I is shorthand for focus1 { repeat { cases_type I } }
cases_type! I only applies cases if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.

cases_type* or and

Tags:

core
induction
context management

Related declarations

tactic.interactive.cases_type

Import using

imported by default

category_theory.elementwise_of

With w : ∀ ..., f ≫ g = h (with universal quantifiers tolerated), elementwise_of w : ∀ ... (x : X), g (f x) = h x.

Although elementwise_of is not a tactic or a meta program, its type is generated through meta-programming to make it usable inside normal expressions.

Tags:

category theory

Related declarations

category_theory.elementwise_of

Import using

import tactic.elementwise

category_theory.reassoc_of

reassoc_of h takes local assumption h and add a ≫ f term on the right of both sides of the equality. Instead of creating a new assumption from the result, reassoc_of h stands for the proof of that reassociated statement. This keeps complicated assumptions that are used only once or twice from polluting the local context.

In the following, assumption h is needed in a reassociated form. Instead of proving it as a new goal and adding it as an assumption, we use reassoc_of h as a rewrite rule which works just as well.

example (X Y Z W : C) (x : X ⟶ Y) (y : Y ⟶ Z) (z z' : Z ⟶ W) (w : X ⟶ Z)
  (h : x ≫ y = w)
  (h' : y ≫ z = y ≫ z') :
  x ≫ y ≫ z = w ≫ z' :=
begin
  -- reassoc_of h : ∀ {X' : C} (f : W ⟶ X'), x ≫ y ≫ f = w ≫ f
  rw [h',reassoc_of h],
end

Although reassoc_of is not a tactic or a meta program, its type is generated through meta-programming to make it usable inside normal expressions.

Tags:

category theory

Related declarations

category_theory.reassoc_of

Import using

import tactic.reassoc_axiom
import tactic

cc (congruence closure)

The congruence closure tactic cc tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b). It is a finishing tactic, i.e. it is meant to close the current goal, not to make some inconclusive progress. A mostly trivial example would be:

example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by cc

As an example requiring some thinking to do by hand, consider:

example (f : ℕ → ℕ) (x : ℕ)
  (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
  f x = x :=
by cc

The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas.

The cc implementation in Lean does a few more tricks: for example it derives a=b from nat.succ a = nat.succ b, and nat.succ a != nat.zero for any a.

The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)
The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).

Tags:

core
finishing

Related declarations

tactic.interactive.cc

Import using

imported by default

change

change u replaces the target t of the main goal to u provided that t is well formed with respect to the local context of the main goal and t and u are definitionally equal.

change u at h will change a local hypothesis to u.

change t with u at h1 h2 ... will replace t with u in all the supplied hypotheses (or *), or in the goal if no at clause is specified, provided that t and u are definitionally equal.

Tags:

core
basic
renaming

Related declarations

tactic.interactive.change

Import using

imported by default

change'

The logic of change x with y at l fails when there are dependencies. change' mimics the behavior of change, except in the case of change x with y at l. In this case, it will correctly replace occurences of x with y at all possible hypotheses in l. As long as x and y are defeq, it should never fail.

Tags:

renaming

Related declarations

Import using

import tactic.interactive
import tactic.basic

choose

choose a b h h' using hyp takes an hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b for some P Q : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and two assumptions: h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.

choose! a b h h' using hyp does the same, except that it will remove dependency of the functions on propositional arguments if possible. For example if Y is a proposition and A and B are nonempty in the above example then we will instead get a : X → A, b : X → B, and the assumptions h : ∀ (x : X) (y : Y), P x y (a x) (b x) and h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).

Examples:

example (h : ∀n m : ℕ, ∃i j, m = n + i ∨ m + j = n) : true :=
begin
  choose i j h using h,
  guard_hyp i : ℕ → ℕ → ℕ,
  guard_hyp j : ℕ → ℕ → ℕ,
  guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n,
  trivial
end

example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : true :=
begin
  choose! f h h' using h,
  guard_hyp f : ℕ → ℕ,
  guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i,
  guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i,
  trivial,
end

Tags:

classical logic

Related declarations

tactic.interactive.choose

Import using

import tactic.choose
import tactic.basic

classical

Make every proposition in the context decidable.

Tags:

classical logic
type class

Related declarations

tactic.interactive.classical

Import using

import tactic.interactive
import tactic.basic

clear

clear h₁ ... hₙ tries to clear each hypothesis hᵢ from the local context.

Tags:

core
context management

Related declarations

tactic.interactive.clear

Import using

imported by default

clear'

An improved version of the standard clear tactic. clear is sensitive to the order of its arguments: clear x y may fail even though both x and y could be cleared (if the type of y depends on x). clear' lifts this limitation.

example {α} {β : α → Type} (a : α) (b : β a) : unit :=
begin
  try { clear a b }, -- fails since `b` depends on `a`
  clear' a b,        -- succeeds
  exact ()
end

Tags:

context management

Related declarations

Import using

import tactic.clear
import tactic.basic

clear_

Clear all hypotheses starting with _, like _match and _let_match.

Tags:

context management

Related declarations

tactic.interactive.clear_

Import using

import tactic.interactive
import tactic.basic

clear_aux_decl

clear_aux_decl clears every aux_decl in the local context for the current goal. This includes the induction hypothesis when using the equation compiler and _let_match and _fun_match.

It is useful when using a tactic such as finish, simp * or subst that may use these auxiliary declarations, and produce an error saying the recursion is not well founded.

example (n m : ℕ) (h₁ : n = m) (h₂ : ∃ a : ℕ, a = n ∧ a = m) : 2 * m = 2 * n :=
let ⟨a, ha⟩ := h₂ in
begin
  clear_aux_decl, -- subst will fail without this line
  subst h₁
end

example (x y : ℕ) (h₁ : ∃ n : ℕ, n * 1 = 2) (h₂ : 1 + 1 = 2 → x * 1 = y) : x = y :=
let ⟨n, hn⟩ := h₁ in
begin
  clear_aux_decl, -- finish produces an error without this line
  finish
end
```

Tags:

context management

Related declarations

Import using

import tactic.interactive
import tactic.basic

clear_except

clear_except h₀ h₁ deletes all the assumptions it can except for h₀ and h₁.

Tags:

context management

Related declarations

tactic.interactive.clear_except

Import using

import tactic.interactive
import tactic.basic

clear_value

clear_value n₁ n₂ ... clears the bodies of the local definitions n₁, n₂ ..., changing them into regular hypotheses. A hypothesis n : α := t is changed to n : α.

Tags:

context management

Related declarations

tactic.interactive.clear_value

Import using

import tactic.interactive
import tactic.basic

comp_val

Close goals of the form n ≠ m when n and m have type nat, char, string, int or fin sz, and they are literals. It also closes goals of the form n < m, n > m, n ≤ m and n ≥ m for nat. If the goal is of the form n = m, then it tries to close it using reflexivity.

In mathlib, consider using norm_num instead for numeric types.

Tags:

core
arithmetic

Related declarations

tactic.interactive.comp_val

Import using

imported by default

congr

The congr tactic attempts to identify both sides of an equality goal A = B, leaving as new goals the subterms of A and B which are not definitionally equal. Example: suppose the goal is x * f y = g w * f z. Then congr will produce two goals: x = g w and y = z.

If x y : t, and an instance subsingleton t is in scope, then any goals of the form x = y are solved automatically.

Note that congr can be over-aggressive at times; the congr' tactic in mathlib provides a more refined approach, by taking a parameter that limits the recursion depth.

Tags:

core
congruence

Related declarations

tactic.interactive.congr

Import using

imported by default

congr'

Same as the congr tactic, but takes an optional argument which gives the depth of recursive applications.

This is useful when congr is too aggressive in breaking down the goal.
For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr' produces the goals ⊢ x = y and ⊢ y = x, while congr' 2 produces the intended ⊢ x + y = y + x.
If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
You can use congr' with p (: n)? to call ext p (: n)? to all subgoals generated by congr'. For example, if the goal is ⊢ f '' s = g '' s then congr' with x generates the goal x : α ⊢ f x = g x.

Tags:

congruence

Related declarations

Import using

import tactic.congr
import tactic.basic

constructor

This tactic applies to a goal such that its conclusion is an inductive type (say I). It tries to apply each constructor of I until it succeeds.

Tags:

core
logic

Related declarations

tactic.interactive.constructor

Import using

imported by default

continuity / continuity'

continuity solves goals of the form continuous f by applying lemmas tagged with the continuity user attribute.

example {X Y : Type*} [topological_space X] [topological_space Y]
  (f₁ f₂ : X → Y) (hf₁ : continuous f₁) (hf₂ : continuous f₂)
  (g : Y → ℝ) (hg : continuous g) : continuous (λ x, (max (g (f₁ x)) (g (f₂ x))) + 1) :=
by continuity

will discharge the goal, generating a proof term like ((continuous.comp hg hf₁).max (continuous.comp hg hf₂)).add continuous_const

You can also use continuity!, which applies lemmas with { md := semireducible }. The default behaviour is more conservative, and only unfolds reducible definitions when attempting to match lemmas with the goal.

continuity? reports back the proof term it found.

Tags:

lemma application

Related declarations

Import using

import topology.tactic

contradiction

The contradiction tactic attempts to find in the current local context a hypothesis that is equivalent to an empty inductive type (e.g. false), a hypothesis of the form c_1 ... = c_2 ... where c_1 and c_2 are distinct constructors, or two contradictory hypotheses.

Tags:

core
basic
finishing

Related declarations

tactic.interactive.contradiction

Import using

imported by default

contrapose

Transforms the goal into its contrapositive.

contrapose turns a goal P → Q into ¬ Q → ¬ P
contrapose! turns a goal P → Q into ¬ Q → ¬ P and pushes negations inside P and Q using push_neg
contrapose h first reverts the local assumption h, and then uses contrapose and intro h
contrapose! h first reverts the local assumption h, and then uses contrapose! and intro h
contrapose h with new_h uses the name new_h for the introduced hypothesis

Tags:

logic

Related declarations

tactic.interactive.contrapose

Import using

import tactic.push_neg
import tactic.basic

conv

conv {...} allows the user to perform targeted rewriting on a goal or hypothesis, by focusing on particular subexpressions.

See https://leanprover-community.github.io/extras/conv.html for more details.

Inside conv blocks, mathlib currently additionally provides

erw,
ring, ring2 and ring_exp,
norm_num,
norm_cast,
apply_congr, and
conv (within another conv).

apply_congr applies congruence lemmas to step further inside expressions, and sometimes gives better results than the automatically generated congruence lemmas used by congr.

Using conv inside a conv block allows the user to return to the previous state of the outer conv block after it is finished. Thus you can continue editing an expression without having to start a new conv block and re-scoping everything. For example:

example (a b c d : ℕ) (h₁ : b = c) (h₂ : a + c = a + d) : a + b = a + d :=
by conv
{ to_lhs,
  conv
  { congr, skip,
    rw h₁ },
  rw h₂, }

Without conv, the above example would need to be proved using two successive conv blocks, each beginning with to_lhs.

Also, as a shorthand, conv_lhs and conv_rhs are provided, so that

example : 0 + 0 = 0 :=
begin
  conv_lhs { simp }
end

just means

example : 0 + 0 = 0 :=
begin
  conv { to_lhs, simp }
end

and likewise for to_rhs.

Tags:

core

Related declarations

tactic.interactive.conv

Import using

imported by default

conv: congr

Navigate into every argument of the current head function. A target of | (a * b) * c will turn into the two targets | a * b and | c.

Tags:

conv

Related declarations

conv.interactive.congr

Import using

imported by default

conv: find

Navigate into the first scope matching the expression.

For a target of | ∀ c, a + (b + c) = 1, find (b + _) { ... } will run the tactics within the {} with a target of | b + c.

Tags:

conv

Related declarations

conv.interactive.find

Import using

imported by default

conv: for

Navigate into the numbered scopes matching the expression.

For a target of | λ c, 10 * c + 20 * c + 30 * c, for (_ * _) [1, 3] { ... } will run the tactics within the {} with first a target of | 10 * c, then a target of | 30 * c.

Tags:

conv

Related declarations

conv.interactive.for

Import using

imported by default

conv: funext

Navigate into the contents of top-level λ binders. A target of | λ a, a + b will turn into the target | a + b and introduce a into the local context. If there are multiple binders, all of them will be entered, and if there are none, this tactic is a no-op.

Tags:

conv

Related declarations

conv.interactive.funext

Import using

imported by default

conv: skip

End conversion of the current goal. This is often what is needed when muscle memory would type sorry.

Tags:

conv

Related declarations

conv.interactive.skip

Import using

imported by default

conv: to_lhs

Navigate to the left-hand-side of a relation. A goal of | a = b will turn into the goal | a.

Tags:

conv

Related declarations

conv.interactive.to_lhs

Import using

imported by default

conv: to_rhs

Navigate to the right-hand-side of a relation. A goal of | a = b will turn into the goal | b.

Tags:

conv

Related declarations

conv.interactive.to_rhs

Import using

imported by default

convert

The exact e and refine e tactics require a term e whose type is definitionally equal to the goal. convert e is similar to refine e, but the type of e is not required to exactly match the goal. Instead, new goals are created for differences between the type of e and the goal. For example, in the proof state

n : ℕ,
e : prime (2 * n + 1)
⊢ prime (n + n + 1)

the tactic convert e will change the goal to

⊢ n + n = 2 * n

In this example, the new goal can be solved using ring.

The convert tactic applies congruence lemmas eagerly before reducing, therefore it can fail in cases where exact succeeds:

def p (n : ℕ) := true
example (h : p 0) : p 1 := by exact h -- succeeds
example (h : p 0) : p 1 := by convert h -- fails, with leftover goal `1 = 0`

If x y : t, and an instance subsingleton t is in scope, then any goals of the form x = y are solved automatically.

The syntax convert ← e will reverse the direction of the new goals (producing ⊢ 2 * n = n + n in this example).

Internally, convert e works by creating a new goal asserting that the goal equals the type of e, then simplifying it using congr'. The syntax convert e using n can be used to control the depth of matching (like congr' n). In the example, convert e using 1 would produce a new goal ⊢ n + n + 1 = 2 * n + 1.

Tags:

congruence

Related declarations

tactic.interactive.convert

Import using

import tactic.congr
import tactic.basic

convert_to

convert_to g using n attempts to change the current goal to g, but unlike change, it will generate equality proof obligations using congr' n to resolve discrepancies. convert_to g defaults to using congr' 1.

convert_to is similar to convert, but convert_to takes a type (the desired subgoal) while convert takes a proof term. That is, convert_to g using n is equivalent to convert (_ : g) using n.

Tags:

congruence

Related declarations

Import using

import tactic.congr
import tactic.basic

dec_trivial

dec_trivial tries to use decidability to prove a goal (i.e., using exact dec_trivial). The variant dec_trivial! will revert all hypotheses on which the target depends, before it tries exact dec_trivial.

Example:

example (n : ℕ) (h : n < 2) : n = 0 ∨ n = 1 :=
by dec_trivial!

Tags:

basic
finishing

Related declarations

tactic.interactive.dec_trivial

Import using

import tactic.dec_trivial
import tactic.basic

delta

Similar to dunfold, but performs a raw delta reduction, rather than using an equation associated with the defined constants.

Tags:

core
simplification

Related declarations

tactic.interactive.delta

Import using

imported by default

destruct

Assuming x is a variable in the local context with an inductive type, destruct x splits the main goal, producing one goal for each constructor of the inductive type, in which x is assumed to be a general instance of that constructor. In contrast to cases, the local context is unchanged, i.e. no elements are reverted or introduced.

For example, given n : nat and a goal with a hypothesis h : P n and target Q n, destruct n produces one goal with target n = 0 → Q n, and one goal with target ∀ (a : ℕ), (λ (w : ℕ), n = w → Q n) (nat.succ a). Here the name a is chosen automatically.

Tags:

core
induction

Related declarations

tactic.interactive.destruct

Import using

imported by default

done

Fail if there are unsolved goals.

Tags:

core
goal management

Related declarations

tactic.interactive.done

Import using

imported by default

dsimp

dsimp is similar to simp, except that it only uses definitional equalities.

Tags:

core
simplification

Related declarations

tactic.interactive.dsimp

Import using

imported by default

dunfold

Similar to unfold, but only uses definitional equalities.

Tags:

core
simplification

Related declarations

tactic.interactive.dunfold

Import using

imported by default

eapply

Similar to the apply tactic, but only creates subgoals for non-dependent premises that have not been fixed by type inference or type class resolution.

Tags:

core
lemma application

Related declarations

tactic.interactive.eapply

Import using

imported by default

econstructor

Similar to constructor, but only non-dependent premises are added as new goals.

Tags:

core
logic

Related declarations

tactic.interactive.econstructor

Import using

imported by default

elide / unelide

The elide n (at ...) tactic hides all subterms of the target goal or hypotheses beyond depth n by replacing them with hidden, which is a variant on the identity function. (Tactics should still mostly be able to see through the abbreviation, but if you want to unhide the term you can use unelide.)

The unelide (at ...) tactic removes all hidden subterms in the target types (usually added by elide).

Tags:

goal management
context management
rewriting

Related declarations

Import using

import tactic.elide
import tactic.basic

erewrite / erw

A variant of rw that uses the unifier more aggressively, unfolding semireducible definitions.

Tags:

core
rewriting

Related declarations

Import using

imported by default

exact

This tactic provides an exact proof term to solve the main goal. If t is the goal and p is a term of type u then exact p succeeds if and only if t and u can be unified.

Tags:

core
basic
finishing

Related declarations

tactic.interactive.exact

Import using

imported by default

exacts

Like exact, but takes a list of terms and checks that all goals are discharged after the tactic.

Tags:

core
finishing

Related declarations

tactic.interactive.exacts

Import using

imported by default

exfalso

Replaces the target of the main goal by false.

Tags:

core
basic
logic

Related declarations

tactic.interactive.exfalso

Import using

imported by default

existsi

existsi e will instantiate an existential quantifier in the target with e and leave the instantiated body as the new target. More generally, it applies to any inductive type with one constructor and at least two arguments, applying the constructor with e as the first argument and leaving the remaining arguments as goals.

existsi [e₁, ..., eₙ] iteratively does the same for each expression in the list.

Note: in mathlib, the use tactic is an equivalent tactic which sometimes is smarter with unification.

Tags:

core
logic

Related declarations

tactic.interactive.existsi

Import using

imported by default

ext1 / ext

ext1 id selects and apply one extensionality lemma (with attribute ext), using id, if provided, to name a local constant introduced by the lemma. If id is omitted, the local constant is named automatically, as per intro.
ext applies as many extensionality lemmas as possible;
ext ids, with ids a list of identifiers, finds extensionality lemmas and applies them until it runs out of identifiers in ids to name the local constants.
ext can also be given an rcases pattern in place of an identifier. This will destruct the introduced local constant.

Placing a ? after ext/ext1 (e.g. ext? i ⟨a,b⟩ : 3) will display a sequence of tactic applications that can replace the call to ext/ext1.
set_option trace.ext true will trace every attempted lemma application, along with the time it takes for the application to succeed or fail. This is useful for debugging slow ext calls.

When trying to prove:

α β : Type,
f g : α → set β
⊢ f = g

applying ext x y yields:

α β : Type,
f g : α → set β,
x : α,
y : β
⊢ y ∈ f x ↔ y ∈ g x

by applying functional extensionality and set extensionality.

When trying to prove:

α β γ : Type
f g : α × β → γ
⊢ f = g

applying ext ⟨a, b⟩ yields:

α β γ : Type,
f g : α × β → γ,
a : α,
b : β
⊢ f (a, b) = g (a, b)

by applying functional extensionality and destructing the introduced pair.

In the previous example, applying ext? ⟨a,b⟩ will produce the trace message:

Try this: apply funext, rintro ⟨a, b⟩

A maximum depth can be provided with ext x y z : 3.

Tags:

rewriting
logic

Related declarations

Import using

import tactic.ext
import tactic.basic

extract_goal

Format the current goal as a stand-alone example. Useful for testing tactics or creating minimal working examples.

extract_goal: formats the statement as an example declaration
extract_goal my_decl: formats the statement as a lemma or def declaration called my_decl
extract_goal with i j k: only use local constants i, j, k in the declaration

Examples:

example (i j k : ℕ) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k :=
begin
  extract_goal,
     -- prints:
     -- example (i j k : ℕ) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k :=
     -- begin
     --   admit,
     -- end
  extract_goal my_lemma
     -- prints:
     -- lemma my_lemma (i j k : ℕ) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k :=
     -- begin
     --   admit,
     -- end
end

example {i j k x y z w p q r m n : ℕ} (h₀ : i ≤ j) (h₁ : j ≤ k) (h₁ : k ≤ p) (h₁ : p ≤ q) : i ≤ k :=
begin
  extract_goal my_lemma,
    -- prints:
    -- lemma my_lemma {i j k x y z w p q r m n : ℕ}
    --   (h₀ : i ≤ j)
    --   (h₁ : j ≤ k)
    --   (h₁ : k ≤ p)
    --   (h₁ : p ≤ q) :
    --   i ≤ k :=
    -- begin
    --   admit,
    -- end

  extract_goal my_lemma with i j k
    -- prints:
    -- lemma my_lemma {p i j k : ℕ}
    --   (h₀ : i ≤ j)
    --   (h₁ : j ≤ k)
    --   (h₁ : k ≤ p) :
    --   i ≤ k :=
    -- begin
    --   admit,
    -- end
end

example : true :=
begin
  let n := 0,
  have m : ℕ, admit,
  have k : fin n, admit,
  have : n + m + k.1 = 0, extract_goal,
    -- prints:
    -- example (m : ℕ)  : let n : ℕ := 0 in ∀ (k : fin n), n + m + k.val = 0 :=
    -- begin
    --   intros n k,
    --   admit,
    -- end
end
```

Tags:

goal management
proof extraction
debugging

Related declarations

tactic.interactive.extract_goal

Import using

import tactic.interactive
import tactic.basic

fail_if_success

Fails if the given tactic succeeds.

Tags:

core
testing
combinator

Related declarations

tactic.interactive.fail_if_success

Import using

imported by default

fapply

Similar to the apply tactic, but does not reorder goals.

Tags:

core
lemma application

Related declarations

tactic.interactive.fapply

Import using

imported by default

fconstructor

Similar to constructor, but does not reorder goals.

Tags:

logic
goal management

Related declarations

tactic.interactive.fconstructor

Import using

import tactic.interactive
import tactic.basic

field_simp

The goal of field_simp is to reduce an expression in a field to an expression of the form n / d where neither n nor d contains any division symbol, just using the simplifier (with a carefully crafted simpset named field_simps) to reduce the number of division symbols whenever possible by iterating the following steps:

write an inverse as a division
in any product, move the division to the right
if there are several divisions in a product, group them together at the end and write them as a single division
reduce a sum to a common denominator

If the goal is an equality, this simpset will also clear the denominators, so that the proof can normally be concluded by an application of ring or ring_exp.

field_simp [hx, hy] is a short form for simp [-one_div, -mul_eq_zero, hx, hy] with field_simps {discharger := [field_simp.ne_zero]}

Note that this naive algorithm will not try to detect common factors in denominators to reduce the complexity of the resulting expression. Instead, it relies on the ability of ring to handle complicated expressions in the next step.

As always with the simplifier, reduction steps will only be applied if the preconditions of the lemmas can be checked. This means that proofs that denominators are nonzero should be included. The fact that a product is nonzero when all factors are, and that a power of a nonzero number is nonzero, are included in the simpset, but more complicated assertions (especially dealing with sums) should be given explicitly. If your expression is not completely reduced by the simplifier invocation, check the denominators of the resulting expression and provide proofs that they are nonzero to enable further progress.

To check that denominators are nonzero, field_simp will look for facts in the context, and will try to apply norm_num to close numerical goals.

The invocation of field_simp removes the lemma one_div from the simpset, as this lemma works against the algorithm explained above. It also removes mul_eq_zero : x * y = 0 ↔ x = 0 ∨ y = 0, as norm_num can not work on disjunctions to close goals of the form 24 ≠ 0, and replaces it with mul_ne_zero : x ≠ 0 → y ≠ 0 → x * y ≠ 0 creating two goals instead of a disjunction.

For example,

example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
  a + b / x + c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) :=
begin
  field_simp,
  ring
end

See also the cancel_denoms tactic, which tries to do a similar simplification for expressions that have numerals in denominators. The tactics are not related: cancel_denoms will only handle numeric denominators, and will try to entirely remove (numeric) division from the expression by multiplying by a factor.

Tags:

simplification
arithmetic

Related declarations

tactic.interactive.field_simp

Import using

import tactic.field_simp
import tactic

filter_upwards

filter_upwards [h₁, ⋯, hₙ] replaces a goal of the form s ∈ f and terms h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f with ∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s. The list is an optional parameter, [] being its default value.

filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ is a short form for { filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }.

filter_upwards [h₁, ⋯, hₙ] using e is a short form for { filter_upwards [h1, ⋯, hn], exact e }.

Combining both shortcuts is done by writing filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e. Note that in this case, the aᵢ terms can be used in e.

Tags:

goal management
lemma application

Related declarations

tactic.interactive.filter_upwards

Import using

import order.filter.basic

fin_cases

fin_cases h performs case analysis on a hypothesis of the form h : A, where [fintype A] is available, or h : a ∈ A, where A : finset X, A : multiset X or A : list X.

fin_cases * performs case analysis on all suitable hypotheses.

As an example, in

example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
begin
  fin_cases *; simp,
  all_goals { assumption }
end

after fin_cases p; simp, there are three goals, f 0, f 1, and f 2.

fin_cases h with l takes a list of descriptions for the cases of h. These should be definitionally equal to and in the same order as the default enumeration of the cases.

For example,

example (x y : ℕ) (h : x ∈ [1, 2]) : x = y :=
begin
  fin_cases h with [1, 1+1],
end

produces two cases: 1 = y and 1 + 1 = y.

When using fin_cases a on data a defined with let, the tactic will not be able to clear the variable a, and will instead produce hypotheses this : a = .... These hypotheses can be given a name using fin_cases a using ha.

For example,

example (f : ℕ → fin 3) : true :=
begin
  let a := f 3,
  fin_cases a using ha,
end

produces three goals with hypotheses ha : a = 0, ha : a = 1, and ha : a = 2.

Tags:

case bashing

Related declarations

tactic.interactive.fin_cases

Import using

import tactic.fin_cases
import tactic

finish / clarify / safe

These tactics do straightforward things: they call the simplifier, split conjunctive assumptions, eliminate existential quantifiers on the left, and look for contradictions. They rely on ematching and congruence closure to try to finish off a goal at the end.

The procedures do split on disjunctions and recreate the smt state for each terminal call, so they are only meant to be used on small, straightforward problems.

finish: solves the goal or fails
clarify: makes as much progress as possible while not leaving more than one goal
safe: splits freely, finishes off whatever subgoals it can, and leaves the rest

All accept an optional list of simplifier rules, typically definitions that should be expanded. (The equations and identities should not refer to the local context.) All also accept an optional list of ematch lemmas, which must be preceded by using.

Tags:

logic
finishing

Related declarations

Import using

import tactic.finish
import tactic.basic

focus

focus { t } temporarily hides all goals other than the first, applies t, and then restores the other goals. It fails if there are no goals.

Tags:

core
goal management
combinator

Related declarations

tactic.interactive.focus

Import using

imported by default

from

A synonym for exact that allows writing have/suffices/show ..., from ... in tactic mode.

Tags:

core
finishing

Related declarations

tactic.interactive.from

Import using

imported by default

fsplit

Just like split, fsplit applies the constructor when the type of the target is an inductive data type with one constructor. However it does not reorder goals or invoke auto_param tactics.

Tags:

logic
goal management

Related declarations

tactic.interactive.fsplit

Import using

import tactic.core
import tactic.basic

funext

Apply function extensionality and introduce new hypotheses. The tactic funext will keep applying new the funext lemma until the goal target is not reducible to

  |-  ((fun x, ...) = (fun x, ...))

The variant funext h₁ ... hₙ applies funext n times, and uses the given identifiers to name the new hypotheses.

Note also the mathlib tactic ext, which applies as many extensionality lemmas as possible.

Tags:

core
logic

Related declarations

tactic.interactive.funext

Import using

imported by default

generalize

generalize : e = x replaces all occurrences of e in the target with a new hypothesis x of the same type.

generalize h : e = x in addition registers the hypothesis h : e = x.

Tags:

core
context management

Related declarations

tactic.interactive.generalize

Import using

imported by default

generalize'

generalize' : e = x replaces all occurrences of e in the target with a new hypothesis x of the same type.

generalize' h : e = x in addition registers the hypothesis h : e = x.

generalize' is similar to generalize. The difference is that generalize' : e = x also succeeds when e does not occur in the goal. It is similar to set, but the resulting hypothesis x is not a local definition.

Tags:

context management

Related declarations

tactic.interactive.generalize'

Import using

import tactic.interactive
import tactic.basic

generalize_hyp

Like generalize but also considers assumptions specified by the user. The user can also specify to omit the goal.

Tags:

context management

Related declarations

tactic.interactive.generalize_hyp

Import using

import tactic.interactive
import tactic.basic

generalize_proofs

Generalize proofs in the goal, naming them with the provided list.

For example:

example : list.nth_le [1, 2] 1 dec_trivial = 2 :=
begin
  -- ⊢ [1, 2].nth_le 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nth_le 1 h = 2
end

Tags:

context management

Related declarations

tactic.interactive.generalize_proofs

Import using

import tactic.generalize_proofs
import tactic.basic

generalizes

Generalizes the target over multiple expressions. For example, given the goal

P : ∀ n, fin n → Prop
n : ℕ
f : fin n
⊢ P (nat.succ n) (fin.succ f)

you can use generalizes [n'_eq : nat.succ n = n', f'_eq : fin.succ f == f'] to get

P : ∀ n, fin n → Prop
n : ℕ
f : fin n
n' : ℕ
n'_eq : n' = nat.succ n
f' : fin n'
f'_eq : f' == fin.succ f
⊢ P n' f'

The expressions must be given in dependency order, so [f'_eq : fin.succ f == f', n'_eq : nat.succ n = n'] would fail since the type of fin.succ f is nat.succ n.

You can choose to omit some or all of the generated equations. For the above example, generalizes [nat.succ n = n', fin.succ f == f'] gets you

P : ∀ n, fin n → Prop
n : ℕ
f : fin n
n' : ℕ
f' : fin n'
⊢ P n' f'

After generalization, the target type may no longer type check. generalizes will then raise an error.

Tags:

context management

Related declarations

tactic.interactive.generalizes

Import using

import tactic.generalizes
import tactic.basic

group

Tactic for normalizing expressions in multiplicative groups, without assuming commutativity, using only the group axioms without any information about which group is manipulated.

(For additive commutative groups, use the abel tactic instead.)

Example:

example {G : Type} [group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a :=
begin
  group at h, -- normalizes `h` which becomes `h : c = d`
  rw h,       -- the goal is now `a*d*d⁻¹ = a`
  group,      -- which then normalized and closed
end

Tags:

decision procedure
simplification

Related declarations

tactic.interactive.group

Import using

import tactic.group
import tactic

guard_hyp

guard_hyp h : t fails if the hypothesis h does not have type t. We use this tactic for writing tests.

Tags:

core
testing
context management

Related declarations

tactic.interactive.guard_hyp

Import using

imported by default

guard_target

guard_target t fails if the target of the main goal is not t. We use this tactic for writing tests.

Tags:

core
testing
goal management

Related declarations

tactic.interactive.guard_target

Import using

imported by default

guard_target'

guard_target' t fails if the target of the main goal is not definitionally equal to t. We use this tactic for writing tests. The difference with guard_target is that this uses definitional equality instead of alpha-equivalence.

Tags:

testing

Related declarations

tactic.interactive.guard_target'

Import using

import tactic.interactive
import tactic.basic

h_generalize

h_generalize Hx : e == x matches on cast _ e in the goal and replaces it with x. It also adds Hx : e == x as an assumption. If cast _ e appears multiple times (not necessarily with the same proof), they are all replaced by x. cast eq.mp, eq.mpr, eq.subst, eq.substr, eq.rec and eq.rec_on are all treated as casts.

h_generalize Hx : e == x with h adds hypothesis α = β with e : α, x : β;
h_generalize Hx : e == x with _ chooses automatically chooses the name of assumption α = β;
h_generalize! Hx : e == x reverts Hx;
when Hx is omitted, assumption Hx : e == x is not added.

Tags:

context management

Related declarations

tactic.interactive.h_generalize

Import using

import tactic.interactive
import tactic.basic

have

have h : t := p adds the hypothesis h : t to the current goal if p a term of type t. If t is omitted, it will be inferred.

have h : t adds the hypothesis h : t to the current goal and opens a new subgoal with target t. The new subgoal becomes the main goal. If t is omitted, it will be replaced by a fresh metavariable.

If h is omitted, the name this is used.

Tags:

core
basic
context management

Related declarations

tactic.interactive.have

Import using

imported by default

hint

hint lists possible tactics which will make progress (that is, not fail) against the current goal.

example {P Q : Prop} (p : P) (h : P → Q) : Q :=
begin
  hint,
  /- the following tactics make progress:
     ----
     Try this: solve_by_elim
     Try this: finish
     Try this: tauto
  -/
  solve_by_elim,
end

You can add a tactic to the list that hint tries by either using

attribute [hint_tactic] my_tactic, if my_tactic is already of type tactic string (tactic unit is allowed too, in which case the printed string will be the name of the tactic), or
add_hint_tactic "my_tactic", specifying a string which works as an interactive tactic.

Tags:

search
Try this

Related declarations

tactic.interactive.hint

Import using

import tactic.hint
import tactic.basic

induction

Assuming x is a variable in the local context with an inductive type, induction x applies induction on x to the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor and an inductive hypothesis is added for each recursive argument to the constructor. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the inductive hypothesis incorporates that hypothesis as well.

For example, given n : nat and a goal with a hypothesis h : P n and target Q n, induction n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypotheses h : P (nat.succ a) and ih₁ : P a → Q a and target Q (nat.succ a). Here the names a and ih₁ ire chosen automatically.

induction e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.

induction e with y₁ ... yₙ, where e is a variable or an expression, specifies that the sequence of names y₁ ... yₙ should be used for the arguments to the constructors and inductive hypotheses, including implicit arguments. If the list does not include enough names for all of the arguments, additional names are generated automatically. If too many names are given, the extra ones are ignored. Underscores can be used in the list, in which case the corresponding names are generated automatically. Note that for long sequences of names, the case tactic provides a more convenient naming mechanism.

induction e using r allows the user to specify the principle of induction that should be used. Here r should be a theorem whose result type must be of the form C t, where C is a bound variable and t is a (possibly empty) sequence of bound variables

induction e generalizing z₁ ... zₙ, where z₁ ... zₙ are variables in the local context, generalizes over z₁ ... zₙ before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.

induction h : t will introduce an equality of the form h : t = C x y, asserting that the input term is equal to the current constructor case, to the context.

Tags:

core
basic
induction

Related declarations

tactic.interactive.induction

Import using

imported by default

inhabit

inhabit α tries to derive a nonempty α instance and then upgrades this to an inhabited α instance. If the target is a Prop, this is done constructively; otherwise, it uses classical.choice.

example (α) [nonempty α] : ∃ a : α, true :=
begin
  inhabit α,
  existsi default,
  trivial
end

Tags:

context management
type class

Related declarations

tactic.interactive.inhabit

Import using

import tactic.interactive
import tactic.basic

injection

The injection tactic is based on the fact that constructors of inductive data types are injections. That means that if c is a constructor of an inductive datatype, and if (c t₁) and (c t₂) are two terms that are equal then t₁ and t₂ are equal too.

If q is a proof of a statement of conclusion t₁ = t₂, then injection applies injectivity to derive the equality of all arguments of t₁ and t₂ placed in the same positions. For example, from (a::b) = (c::d) we derive a=c and b=d. To use this tactic t₁ and t₂ should be constructor applications of the same constructor.

Given h : a::b = c::d, the tactic injection h adds two new hypothesis with types a = c and b = d to the main goal. The tactic injection h with h₁ h₂ uses the names h₁ and h₂ to name the new hypotheses.

Tags:

core
structures
induction

Related declarations

tactic.interactive.injection

Import using

imported by default

injections

injections with h₁ ... hₙ iteratively applies injection to hypotheses using the names h₁ ... hₙ.

Tags:

core
structures
induction

Related declarations

tactic.interactive.injections

Import using

imported by default

injections_and_clear

Calls injection on each hypothesis, and then, for each hypothesis on which injection succeeds, clears the old hypothesis.

Tags:

context management

Related declarations

tactic.interactive.injections_and_clear

Import using

import tactic.core
import tactic.basic

interval_cases

interval_cases n searches for upper and lower bounds on a variable n, and if bounds are found, splits into separate cases for each possible value of n.

As an example, in

example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 :=
begin
  interval_cases n,
  all_goals {simp}
end

after interval_cases n, the goals are 3 = 3 ∨ 3 = 4 and 4 = 3 ∨ 4 = 4.

You can also explicitly specify a lower and upper bound to use, as interval_cases using hl hu. The hypotheses should be in the form hl : a ≤ n and hu : n < b, in which case interval_cases calls fin_cases on the resulting fact n ∈ set.Ico a b.

You can also explicitly specify a name to use for the hypothesis added, as interval_cases n with hn or interval_cases n using hl hu with hn.

In particular, interval_cases n

inspects hypotheses looking for lower and upper bounds of the form a ≤ n and n < b (although in ℕ, ℤ, and ℕ+ bounds of the form a < n and n ≤ b are also allowed), and also makes use of lower and upper bounds found via le_top and bot_le (so for example if n : ℕ, then the bound 0 ≤ n is found automatically), then
calls fin_cases on the synthesised hypothesis n ∈ set.Ico a b, assuming an appropriate fintype instance can be found for the type of n.

The variable n can belong to any type α, with the following restrictions:

only bounds on which expr.to_rat succeeds will be considered "explicit" (TODO: generalise this?)
an instance of decidable_eq α is available,
an explicit lower bound can be found amongst the hypotheses, or from bot_le n,
an explicit upper bound can be found amongst the hypotheses, or from le_top n,
if multiple bounds are located, an instance of linear_order α is available, and
an instance of fintype set.Ico l u is available for the relevant bounds.

Tags:

case bashing

Related declarations

tactic.interactive.interval_cases

Import using

import tactic.interval_cases
import tactic

intro / intros

If the current goal is a Pi/forall ∀ x : t, u (resp. let x := t in u) then intro puts x : t (resp. x := t) in the local context. The new subgoal target is u.

If the goal is an arrow t → u, then it puts h : t in the local context and the new goal target is u.

If the goal is neither a Pi/forall nor begins with a let binder, the tactic intro applies the tactic whnf until an introduction can be applied or the goal is not head reducible. In the latter case, the tactic fails.

The variant intro z uses the identifier z to name the new hypothesis.

The variant intros will keep introducing new hypotheses until the goal target is not a Pi/forall or let binder.

The variant intros h₁ ... hₙ introduces n new hypotheses using the given identifiers to name them.

Tags:

core
basic
logic

Related declarations

Import using

imported by default

introv

The tactic introv allows the user to automatically introduce the variables of a theorem and explicitly name the hypotheses involved. The given names are used to name non-dependent hypotheses.

Examples:

example : ∀ a b : nat, a = b → b = a :=
begin
  introv h,
  exact h.symm
end

The state after introv h is

a b : ℕ,
h : a = b
⊢ b = a

example : ∀ a b : nat, a = b → ∀ c, b = c → a = c :=
begin
  introv h₁ h₂,
  exact h₁.trans h₂
end

The state after introv h₁ h₂ is

a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c

Tags:

core
logic

Related declarations

tactic.interactive.introv

Import using

imported by default

itauto

A decision procedure for intuitionistic propositional logic. Unlike finish and tauto! this tactic never uses the law of excluded middle (without the ! option), and the proof search is tailored for this use case. (itauto! will work as a classical SAT solver, but the algorithm is not very good in this situation.)

example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto

itauto [a, b] will additionally attempt case analysis on a and b assuming that it can derive decidable a and decidable b. itauto * will case on all decidable propositions that it can find among the atomic propositions, and itauto! * will case on all propositional atoms. Warning: This can blow up the proof search, so it should be used sparingly.

Tags:

logic
propositional logic
intuitionistic logic
decision procedure

Related declarations

tactic.interactive.itauto

Import using

import tactic.itauto
import tactic.basic

iterate

iterate { t } repeatedly applies tactic t until t fails. iterate { t } always succeeds.

iterate n { t } applies t n times.

Tags:

core
combinator

Related declarations

tactic.interactive.iterate

Import using

imported by default

left / right

left applies the first constructor when the type of the target is an inductive data type with two constructors.

Similarly, right applies the second constructor.

Tags:

core
basic
logic

Related declarations

Import using

imported by default

let

let h : t := p adds the hypothesis h : t := p to the current goal if p a term of type t. If t is omitted, it will be inferred.

let h : t adds the hypothesis h : t := ?M to the current goal and opens a new subgoal ?M : t. The new subgoal becomes the main goal. If t is omitted, it will be replaced by a fresh metavariable.

If h is omitted, the name this is used.

Note the related mathlib tactic set a := t with h, which adds the hypothesis h : a = t to the local context and replaces t with a everywhere it can.

Tags:

core
basic
logic
context management

Related declarations

tactic.interactive.let

Import using

imported by default

library_search

library_search is a tactic to identify existing lemmas in the library. It tries to close the current goal by applying a lemma from the library, then discharging any new goals using solve_by_elim.

If it succeeds, it prints a trace message exact ... which can replace the invocation of library_search.

Typical usage is:

example (n m k : ℕ) : n * (m - k) = n * m - n * k :=
by library_search -- Try this: exact mul_tsub n m k

library_search using h₁ h₂ will only show solutions that make use of the local hypotheses h₁ and h₂.

By default library_search only unfolds reducible definitions when attempting to match lemmas against the goal. Previously, it would unfold most definitions, sometimes giving surprising answers, or slow answers. The old behaviour is still available via library_search!.

You can add additional lemmas to be used along with local hypotheses after the application of a library lemma, using the same syntax as for solve_by_elim, e.g.

example {a b c d: nat} (h₁ : a < c) (h₂ : b < d) : max (c + d) (a + b) = (c + d) :=
begin
  library_search [add_lt_add], -- Says: `Try this: exact max_eq_left_of_lt (add_lt_add h₁ h₂)`
end

You can also use library_search with attr to include all lemmas with the attribute attr.

Tags:

search
Try this

Related declarations

tactic.interactive.library_search

Import using

import tactic.suggest
import tactic.basic

lift

Lift an expression to another type.

Usage: 'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?.
If n : ℤ and hn : n ≥ 0 then the tactic lift n to ℕ using hn creates a new constant of type ℕ, also named n and replaces all occurrences of the old variable (n : ℤ) with ↑n (where n in the new variable). It will remove n and hn from the context.
- So for example the tactic lift n to ℕ using hn transforms the goal n : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3 to n : ℕ, h : P ↑n ⊢ ↑n = 3 (here P is some term of type ℤ → Prop).
The argument using hn is optional, the tactic lift n to ℕ does the same, but also creates a new subgoal that n ≥ 0 (where n is the old variable).
- So for example the tactic lift n to ℕ transforms the goal n : ℤ, h : P n ⊢ n = 3 to two goals n : ℕ, h : P ↑n ⊢ ↑n = 3 and n : ℤ, h : P n ⊢ n ≥ 0.
You can also use lift n to ℕ using e where e is any expression of type n ≥ 0.
Use lift n to ℕ with k to specify the name of the new variable.
Use lift n to ℕ with k hk to also specify the name of the equality ↑k = n. In this case, n will remain in the context. You can use rfl for the name of hk to substitute n away (i.e. the default behavior).
You can also use lift e to ℕ with k hk where e is any expression of type ℤ. In this case, the hk will always stay in the context, but it will be used to rewrite e in all hypotheses and the target.
- So for example the tactic lift n + 3 to ℕ using hn with k hk transforms the goal n : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n to the goal n : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n.
The tactic lift n to ℕ using h will remove h from the context. If you want to keep it, specify it again as the third argument to with, like this: lift n to ℕ using h with n rfl h.
More generally, this can lift an expression from α to β assuming that there is an instance of can_lift α β. In this case the proof obligation is specified by can_lift.cond.
Given an instance can_lift β γ, it can also lift α → β to α → γ; more generally, given β : Π a : α, Type*, γ : Π a : α, Type*, and [Π a : α, can_lift (β a) (γ a)], it automatically generates an instance can_lift (Π a, β a) (Π a, γ a).

lift is in some sense dual to the zify tactic. lift (z : ℤ) to ℕ will change the type of an integer z (in the supertype) to ℕ (the subtype), given a proof that z ≥ 0; propositions concerning z will still be over ℤ. zify changes propositions about ℕ (the subtype) to propositions about ℤ (the supertype), without changing the type of any variable.

Tags:

coercions

Related declarations

tactic.interactive.lift

Import using

import tactic.lift
import tactic.basic

linarith

linarith attempts to find a contradiction between hypotheses that are linear (in)equalities. Equivalently, it can prove a linear inequality by assuming its negation and proving false.

In theory, linarith should prove any goal that is true in the theory of linear arithmetic over the rationals. While there is some special handling for non-dense orders like nat and int, this tactic is not complete for these theories and will not prove every true goal. It will solve goals over arbitrary types that instantiate linear_ordered_comm_ring.

An example:

example (x y z : ℚ) (h1 : 2*x  < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0)  : false :=
by linarith

linarith will use all appropriate hypotheses and the negation of the goal, if applicable.

linarith [t1, t2, t3] will additionally use proof terms t1, t2, t3.

linarith only [h1, h2, h3, t1, t2, t3] will use only the goal (if relevant), local hypotheses h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.

linarith! will use a stronger reducibility setting to try to identify atoms. For example,

example (x : ℚ) : id x ≥ x :=
by linarith

will fail, because linarith will not identify x and id x. linarith! will. This can sometimes be expensive.

linarith {discharger := tac, restrict_type := tp, exfalso := ff} takes a config object with five optional arguments:

discharger specifies a tactic to be used for reducing an algebraic equation in the proof stage. The default is ring. Other options currently include ring SOP or simp for basic problems.
restrict_type will only use hypotheses that are inequalities over tp. This is useful if you have e.g. both integer and rational valued inequalities in the local context, which can sometimes confuse the tactic.
transparency controls how hard linarith will try to match atoms to each other. By default it will only unfold reducible definitions.
If split_hypotheses is true, linarith will split conjunctions in the context into separate hypotheses.
If exfalso is false, linarith will fail when the goal is neither an inequality nor false. (True by default.)

A variant, nlinarith, does some basic preprocessing to handle some nonlinear goals.

The option set_option trace.linarith true will trace certain intermediate stages of the linarith routine.

Tags:

arithmetic
decision procedure
finishing

Related declarations

tactic.interactive.linarith

Import using

import tactic.linarith.frontend
import tactic

mapply

Similar to the apply tactic, but uses matching instead of unification. apply_match t is equivalent to apply_with t {unify := ff}

Tags:

core
lemma application

Related declarations

tactic.interactive.mapply

Import using

imported by default

match_target

match_target t fails if target does not match pattern t.

Tags:

core
testing
goal management

Related declarations

tactic.interactive.match_target

Import using

imported by default

mono

mono applies a monotonicity rule.
mono* applies monotonicity rules repetitively.
mono with x ≤ y or mono with [0 ≤ x,0 ≤ y] creates an assertion for the listed propositions. Those help to select the right monotonicity rule.
mono left or mono right is useful when proving strict orderings: for x + y < w + z could be broken down into either
- left: x ≤ w and y < z or
- right: x < w and y ≤ z
mono using [rule1,rule2] calls simp [rule1,rule2] before applying mono.
The general syntax is mono '*'? ('with' hyp | 'with' [hyp1,hyp2])? ('using' [hyp1,hyp2])? mono_cfg?

To use it, first import tactic.monotonicity.

Here is an example of mono:

example (x y z k : ℤ)
  (h : 3 ≤ (4 : ℤ))
  (h' : z ≤ y) :
  (k + 3 + x) - y ≤ (k + 4 + x) - z :=
begin
  mono, -- unfold `(-)`, apply add_le_add
  { -- ⊢ k + 3 + x ≤ k + 4 + x
    mono, -- apply add_le_add, refl
    -- ⊢ k + 3 ≤ k + 4
    mono },
  { -- ⊢ -y ≤ -z
    mono /- apply neg_le_neg -/ }
end

More succinctly, we can prove the same goal as:

example (x y z k : ℤ)
  (h : 3 ≤ (4 : ℤ))
  (h' : z ≤ y) :
  (k + 3 + x) - y ≤ (k + 4 + x) - z :=
by mono*

Tags:

monotonicity

Related declarations

tactic.interactive.mono

Import using

import tactic.monotonicity.interactive
import tactic

nlinarith

An extension of linarith with some preprocessing to allow it to solve some nonlinear arithmetic problems. (Based on Coq's nra tactic.) See linarith for the available syntax of options, which are inherited by nlinarith; that is, nlinarith! and nlinarith only [h1, h2] all work as in linarith. The preprocessing is as follows:

For every subterm a ^ 2 or a * a in a hypothesis or the goal, the assumption 0 ≤ a ^ 2 or 0 ≤ a * a is added to the context.
For every pair of hypotheses a1 R1 b1, a2 R2 b2 in the context, R1, R2 ∈ {<, ≤, =}, the assumption 0 R' (b1 - a1) * (b2 - a2) is added to the context (non-recursively), where R ∈ {<, ≤, =} is the appropriate comparison derived from R1, R2.

Tags:

arithmetic
decision procedure
finishing

Related declarations

tactic.interactive.nlinarith

Import using

import tactic.linarith.frontend
import tactic

nontriviality

Attempts to generate a nontrivial α hypothesis.

The tactic first looks for an instance using apply_instance.

If the goal is an (in)equality, the type α is inferred from the goal. Otherwise, the type needs to be specified in the tactic invocation, as nontriviality α.

The nontriviality tactic will first look for strict inequalities amongst the hypotheses, and use these to derive the nontrivial instance directly.

Otherwise, it will perform a case split on subsingleton α ∨ nontrivial α, and attempt to discharge the subsingleton goal using simp [lemmas] with nontriviality, where [lemmas] is a list of additional simp lemmas that can be passed to nontriviality using the syntax nontriviality α using [lemmas].

example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
begin
  nontriviality, -- There is now a `nontrivial R` hypothesis available.
  assumption,
end

example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
  nontriviality, -- There is now a `nontrivial R` hypothesis available.
  apply mul_comm,
end

example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 :=
begin
  nontriviality R, -- there is now a `nontrivial R` hypothesis available.
  dec_trivial
end

def myeq {α : Type} (a b : α) : Prop := a = b

example {α : Type} (a b : α) (h : a = b) : myeq a b :=
begin
  success_if_fail { nontriviality α }, -- Fails
  nontriviality α using [myeq], -- There is now a `nontrivial α` hypothesis available
  assumption
end
```

Tags:

logic
type class

Related declarations

tactic.interactive.nontriviality

Import using

import logic.nontrivial
import tactic

norm_cast

The norm_cast family of tactics is used to normalize casts inside expressions. It is basically a simp tactic with a specific set of lemmas to move casts upwards in the expression. Therefore it can be used more safely as a non-terminating tactic. It also has special handling of numerals.

For instance, given an assumption

a b : ℤ
h : ↑a + ↑b < (10 : ℚ)

writing norm_cast at h will turn h into

h : a + b < 10

You can also use exact_mod_cast, apply_mod_cast, rw_mod_cast or assumption_mod_cast. Writing exact_mod_cast h and apply_mod_cast h will normalize the goal and h before using exact h or apply h. Writing assumption_mod_cast will normalize the goal and for every expression h in the context it will try to normalize h and use exact h. rw_mod_cast acts like the rw tactic but it applies norm_cast between steps.

push_cast rewrites the expression to move casts toward the leaf nodes. This uses norm_cast lemmas in the forward direction. For example, ↑(a + b) will be written to ↑a + ↑b. It is equivalent to simp only with push_cast. It can also be used at hypotheses with push_cast at h and with extra simp lemmas with push_cast [int.add_zero].

example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
  ((a + b : ℕ) : ℤ) = 10 :=
begin
  push_cast,
  push_cast at h1,
  push_cast [int.add_zero] at h2,
end

The implementation and behavior of the norm_cast family is described in detail at https://lean-forward.github.io/norm_cast/norm_cast.pdf.

Tags:

coercions
simplification

Related declarations

Import using

import tactic.norm_cast
import tactic.basic

norm_fin

Rewrites occurrences of fin expressions to normal form anywhere in the goal. The norm_num extension will only rewrite fin expressions if they appear in equalities and inequalities. For example if the goal is P (2 + 2 : fin 3) then norm_num will not do anything but norm_fin will reduce the goal to P 1.

example : (5 : fin 7) = fin.succ (fin.succ 3) := by norm_num
example (P : fin 7 → Prop) (h : P 5) : P (fin.succ (fin.succ 3)) := by norm_fin; exact h

Tags:

arithmetic
decision procedure

Related declarations

tactic.interactive.norm_fin

Import using

import tactic.norm_fin

norm_num

Normalises numerical expressions. It supports the operations + - * / ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions.

Add-on tactics marked as @[norm_num] can extend the behavior of norm_num to include other functions. This is used to support several other functions on nat like prime, min_fac and factors.

import data.real.basic

example : (2 : ℝ) + 2 = 4 := by norm_num
example : (12345.2 : ℝ) ≠ 12345.3 := by norm_num
example : (73 : ℝ) < 789/2 := by norm_num
example : 123456789 + 987654321 = 1111111110 := by norm_num
example (R : Type*) [ring R] : (2 : R) + 2 = 4 := by norm_num
example (F : Type*) [linear_ordered_field F] : (2 : F) + 2 < 5 := by norm_num
example : nat.prime (2^13 - 1) := by norm_num
example : ¬ nat.prime (2^11 - 1) := by norm_num
example (x : ℝ) (h : x = 123 + 456) : x = 579 := by norm_num at h; assumption

The variant norm_num1 does not call simp.

Both norm_num and norm_num1 can be called inside the conv tactic.

The tactic apply_normed normalises a numerical expression and tries to close the goal with the result. Compare:

def a : ℕ := 2^100
#print a -- 2 ^ 100

def normed_a : ℕ := by apply_normed 2^100
#print normed_a -- 1267650600228229401496703205376

Tags:

arithmetic
decision procedure

Related declarations

Import using

import tactic.norm_num
import tactic

nth_rewrite / nth_rewrite_lhs / nth_rewrite_rhs

nth_rewrite n rules performs only the nth possible rewrite using the rules. The tactics nth_rewrite_lhs and nth_rewrite_rhs are variants that operate on the left and right hand sides of an equation or iff.

Note: n is zero-based, so nth_rewrite 0 h will rewrite along h at the first possible location.

In more detail, given rules = [h1, ..., hk], this tactic will search for all possible locations where one of h1, ..., hk can be rewritten, and perform the nth occurrence.

Example: Given a goal of the form a + x = x + b, and hypothesis h : x = y, the tactic nth_rewrite 1 h will change the goal to a + x = y + b.

The core rewrite has a occs configuration setting intended to achieve a similar purpose, but this doesn't really work. (If a rule matches twice, but with different values of arguments, the second match will not be identified.)

Tags:

rewriting

Related declarations

Import using

import tactic.nth_rewrite.default
import tactic

obtain

The obtain tactic is a combination of have and rcases. See rcases for a description of supported patterns.

obtain ⟨patt⟩ : type,
{ ... }

is equivalent to

have h : type,
{ ... },
rcases h with ⟨patt⟩

The syntax obtain ⟨patt⟩ : type := proof is also supported.

If ⟨patt⟩ is omitted, rcases will try to infer the pattern.

If type is omitted, := proof is required.

Tags:

induction

Related declarations

tactic.interactive.obtain

Import using

import tactic.rcases
import tactic.basic

pi_instance

pi_instance constructs an instance of my_class (Π i : I, f i) where we know Π i, my_class (f i). If an order relation is required, it defaults to pi.partial_order. Any field of the instance that pi_instance cannot construct is left untouched and generated as a new goal.

Tags:

type class

Related declarations

tactic.interactive.pi_instance

Import using

import tactic.pi_instances
import tactic

pretty_cases

Query the proof goal and print the skeleton of a proof by cases.

For example, let us consider the following proof:

example {α} (xs ys : list α) (h : xs ~ ys) : true :=
begin
  induction h,
  pretty_cases,
    -- Try this:
    --   case list.perm.nil :
    --   { admit },
    --   case list.perm.cons : h_x h_l₁ h_l₂ h_a h_ih
    --   { admit },
    --   case list.perm.swap : h_x h_y h_l
    --   { admit },
    --   case list.perm.trans : h_l₁ h_l₂ h_l₃ h_a h_a_1 h_ih_a h_ih_a_1
    --   { admit },
end

The output helps the user layout the cases and rename the introduced variables.

Tags:

context management
goal management

Related declarations

tactic.interactive.pretty_cases

Import using

import tactic.pretty_cases
import tactic.basic

push_neg

Push negations in the goal of some assumption.

For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Variables names are conserved.

This tactic pushes negations inside expressions. For instance, given an assumption

h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)

writing push_neg at h will turn h into

h : ∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),

(the pretty printer does not use the abreviations ∀ δ > 0 and ∃ ε > 0 but this issue has nothing to do with push_neg). Note that names are conserved by this tactic, contrary to what would happen with simp using the relevant lemmas. One can also use this tactic at the goal using push_neg, at every assumption and the goal using push_neg at * or at selected assumptions and the goal using say push_neg at h h' ⊢ as usual.

Tags:

logic

Related declarations

tactic.interactive.push_neg

Import using

import tactic.push_neg
import tactic.basic

rcases

rcases is a tactic that will perform cases recursively, according to a pattern. It is used to destructure hypotheses or expressions composed of inductive types like h1 : a ∧ b ∧ c ∨ d or h2 : ∃ x y, trans_rel R x y. Usual usage might be rcases h1 with ⟨ha, hb, hc⟩ | hd or rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩ for these examples.

Each element of an rcases pattern is matched against a particular local hypothesis (most of which are generated during the execution of rcases and represent individual elements destructured from the input expression). An rcases pattern has the following grammar:

A name like x, which names the active hypothesis as x.
A blank _, which does nothing (letting the automatic naming system used by cases name the hypothesis).
A hyphen -, which clears the active hypothesis and any dependents.
The keyword rfl, which expects the hypothesis to be h : a = b, and calls subst on the hypothesis (which has the effect of replacing b with a everywhere or vice versa).
A type ascription p : ty, which sets the type of the hypothesis to ty and then matches it against p. (Of course, ty must unify with the actual type of h for this to work.)
A tuple pattern ⟨p1, p2, p3⟩, which matches a constructor with many arguments, or a series of nested conjunctions or existentials. For example if the active hypothesis is a ∧ b ∧ c, then the conjunction will be destructured, and p1 will be matched against a, p2 against b and so on.
An alteration pattern p1 | p2 | p3, which matches an inductive type with multiple constructors, or a nested disjunction like a ∨ b ∨ c.

A pattern like ⟨a, b, c⟩ | ⟨d, e⟩ will do a split over the inductive datatype, naming the first three parameters of the first constructor as a,b,c and the first two of the second constructor d,e. If the list is not as long as the number of arguments to the constructor or the number of constructors, the remaining variables will be automatically named. If there are nested brackets such as ⟨⟨a⟩, b | c⟩ | d then these will cause more case splits as necessary. If there are too many arguments, such as ⟨a, b, c⟩ for splitting on ∃ x, ∃ y, p x, then it will be treated as ⟨a, ⟨b, c⟩⟩, splitting the last parameter as necessary.

rcases also has special support for quotient types: quotient induction into Prop works like matching on the constructor quot.mk.

rcases h : e with PAT will do the same as rcases e with PAT with the exception that an assumption h : e = PAT will be added to the context.

rcases? e will perform case splits on e in the same way as rcases e, but rather than accepting a pattern, it does a maximal cases and prints the pattern that would produce this case splitting. The default maximum depth is 5, but this can be modified with rcases? e : n.

Tags:

induction

Related declarations

tactic.interactive.rcases

Import using

import tactic.rcases
import tactic.basic

refine

This tactic behaves like exact, but with a big difference: the user can put underscores _ in the expression as placeholders for holes that need to be filled, and refine will generate as many subgoals as there are holes.

Note that some holes may be implicit. The type of each hole must either be synthesized by the system or declared by an explicit type ascription like (_ : nat → Prop).

Tags:

core
basic
lemma application

Related declarations

tactic.interactive.refine

Import using

imported by default

refine_struct

refine_struct { .. } acts like refine but works only with structure instance literals. It creates a goal for each missing field and tags it with the name of the field so that have_field can be used to generically refer to the field currently being refined.

As an example, we can use refine_struct to automate the construction of semigroup instances:

refine_struct ( { .. } : semigroup α ),
-- case semigroup, mul
-- α : Type u,
-- ⊢ α → α → α

-- case semigroup, mul_assoc
-- α : Type u,
-- ⊢ ∀ (a b c : α), a * b * c = a * (b * c)

have_field, used after refine_struct _, poses field as a local constant with the type of the field of the current goal:

refine_struct ({ .. } : semigroup α),
{ have_field, ... },
{ have_field, ... },

behaves like

refine_struct ({ .. } : semigroup α),
{ have field := @semigroup.mul, ... },
{ have field := @semigroup.mul_assoc, ... },

Tags:

structures

Related declarations

Import using

import tactic.interactive
import tactic.basic

refl / reflexivity

This tactic applies to a goal whose target has the form t ~ u where ~ is a reflexive relation, that is, a relation which has a reflexivity lemma tagged with the attribute [refl]. The tactic checks whether t and u are definitionally equal and then solves the goal.

Tags:

core
basic
finishing

Related declarations

Import using

imported by default

rename

Rename one or more local hypotheses. The renamings are given as follows:

rename x y             -- rename x to y
rename x → y           -- ditto
rename [x y, a b]      -- rename x to y and a to b
rename [x → y, a → b]  -- ditto

Note that if there are multiple hypotheses called x in the context, then rename x y will rename all of them. If you want to rename only one, use dedup first.

Tags:

core
renaming

Related declarations

tactic.interactive.rename

Import using

imported by default

rename_var

rename_var old new renames all bound variables named old to new in the goal. rename_var old new at h does the same in hypothesis h. This is meant for teaching bound variables only. Such a renaming should never be relevant to Lean.

example (P : ℕ →  ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
  rename_var n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
  rename_var m n, -- goal is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
  exact h -- Lean does not care about those bound variable names
end

Tags:

renaming

Related declarations

tactic.interactive.rename_var

Import using

import tactic.rename_var
import tactic.basic

repeat

repeat { t } applies t 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 { t } never fails.

Tags:

core
combinator

Related declarations

tactic.interactive.repeat

Import using

imported by default

replace

Acts like have, but removes a hypothesis with the same name as this one. For example if the state is h : p ⊢ goal and f : p → q, then after replace h := f h the goal will be h : q ⊢ goal, where have h := f h would result in the state h : p, h : q ⊢ goal. This can be used to simulate the specialize and apply at tactics of Coq.

Tags:

context management

Related declarations

tactic.interactive.replace

Import using

import tactic.interactive
import tactic.basic

revert

revert h₁ ... hₙ applies to any goal with hypotheses h₁ ... hₙ. It moves the hypotheses and their dependencies to the target of the goal. This tactic is the inverse of intro.

Tags:

core
context management
goal management

Related declarations

tactic.interactive.revert

Import using

imported by default

revert_after

revert_after n reverts all the hypotheses after n.

Tags:

context management
goal management

Related declarations

tactic.interactive.revert_after

Import using

import tactic.interactive
import tactic.basic

revert_deps

revert_deps n₁ n₂ ... reverts all the hypotheses that depend on one of n₁, n₂, ... It does not revert n₁, n₂, ... themselves (unless they depend on another nᵢ).

Tags:

context management
goal management

Related declarations

tactic.interactive.revert_deps

Import using

import tactic.interactive
import tactic.basic

revert_target_deps

Reverts all local constants on which the target depends (recursively).

Tags:

context management
goal management

Related declarations

tactic.interactive.revert_target_deps

Import using

import tactic.interactive
import tactic.basic

ring

Tactic for solving equations in the language of commutative (semi)rings. ring! will use a more aggressive reducibility setting to identify atoms.

If the goal is not solvable, it falls back to rewriting all ring expressions into a normal form, with a suggestion to use ring_nf instead, if this is the intent. See also ring1, which is the same as ring but without the fallback behavior.

Based on Proving Equalities in a Commutative Ring Done Right in Coq by Benjamin Grégoire and Assia Mahboubi.

Tags:

arithmetic
simplification
decision procedure

Related declarations

Import using

import tactic.ring
import tactic

ring_exp

Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent.

This tactic extends ring: it should solve every goal that ring can solve. Additionally, it knows how to evaluate expressions with complicated exponents (where ring only understands constant exponents). The variants ring_exp! and ring_exp_eq! use a more aggessive reducibility setting to determine equality of atoms.

For example:

example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring_exp
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring_exp
example (x y : ℕ) : x + id y = y + id x := by ring_exp!

Tags:

arithmetic
simplification
decision procedure

Related declarations

tactic.interactive.ring_exp

Import using

import tactic.ring_exp
import tactic

rintro

The rintro tactic is a combination of the intros tactic with rcases to allow for destructuring patterns while introducing variables. See rcases for a description of supported patterns. For example, rintro (a | ⟨b, c⟩) ⟨d, e⟩ will introduce two variables, and then do case splits on both of them producing two subgoals, one with variables a d e and the other with b c d e.

rintro, unlike rcases, also supports the form (x y : ty) for introducing and type-ascripting multiple variables at once, similar to binders.

rintro? will introduce and case split on variables in the same way as rintro, but will also print the rintro invocation that would have the same result. Like rcases?, rintro? : n allows for modifying the depth of splitting; the default is 5.

rintros is an alias for rintro.

Tags:

induction

Related declarations

Import using

import tactic.rcases
import tactic.basic

rotate

rotate moves the first goal to the back. rotate n will do this n times.

See also tactic.interactive.swap, which moves the nth goal to the front.

Tags:

goal management

Related declarations

tactic.interactive.rotate

Import using

import tactic.interactive
import tactic.basic

rw / rewrite

rw e applies an equation or iff e as a rewrite rule to the main goal. If e is preceded by left arrow (← or <-), the rewrite is applied in the reverse direction. If e is a defined constant, then the equational lemmas associated with e are used. This provides a convenient way to unfold e.

rw [e₁, ..., eₙ] applies the given rules sequentially.

rw e at l rewrites e at location(s) l, where l is either * or a list of hypotheses in the local context. In the latter case, a turnstile ⊢ or |- can also be used, to signify the target of the goal.

rewrite is synonymous with rw.

Tags:

core
basic
rewriting

Related declarations

Import using

imported by default

rwa

rewrite followed by assumption.

Tags:

core
rewriting

Related declarations

tactic.interactive.rwa

Import using

imported by default

scc

scc uses the available equivalences and implications to prove a goal of the form p ↔ q.

example (p q r : Prop) (hpq : p → q) (hqr : q ↔ r) (hrp : r → p) : p ↔ r :=
by scc

The variant scc' populates the local context with all equivalences that scc is able to prove. This is mostly useful for testing purposes.

Tags:

logic

Related declarations

Import using

import tactic.scc
import tactic

set

set a := t with h is a variant of let a := t. It adds the hypothesis h : a = t to the local context and replaces t with a everywhere it can.

set a := t with ←h will add h : t = a instead.

set! a := t with h does not do any replacing.

example (x : ℕ) (h : x = 3)  : x + x + x = 9 :=
begin
  set y := x with ←h_xy,
/-
x : ℕ,
y : ℕ := x,
h_xy : x = y,
h : y = 3
⊢ y + y + y = 9
-/
end

Tags:

context management

Related declarations

tactic.interactive.set

Import using

import tactic.interactive
import tactic.basic

show

show t finds the first goal whose target unifies with t. It makes that the main goal, performs the unification, and replaces the target with the unified version of t.

Tags:

core
goal management
renaming

Related declarations

tactic.interactive.show

Import using

imported by default

show_term

show_term { tac } runs the tactic tac, and then prints the term that was constructed.

This is useful for

constructing term mode proofs from tactic mode proofs, and
understanding what tactics are doing, and how metavariables are handled.

As an example, in

example {P Q R : Prop} (h₁ : Q → P) (h₂ : R) (h₃ : R → Q) : P ∧ R :=
by show_term { tauto }

the term mode proof ⟨h₁ (h₃ h₂), eq.mpr rfl h₂⟩ produced by tauto will be printed.

As another example, if the goal is ℕ × ℕ, show_term { split, exact 0 } will print refine (0, _), and afterwards there will be one remaining goal (of type ℕ). This indicates that split, exact 0 partially filled in the original metavariable, but created a new metavariable for the resulting sub-goal.

Tags:

debugging

Related declarations

tactic.interactive.show_term

Import using

import tactic.show_term
import tactic.basic

simp

The simp tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants.

simp simplifies the main goal target using lemmas tagged with the attribute [simp].

simp [h₁ h₂ ... hₙ] simplifies the main goal target using the lemmas tagged with the attribute [simp] and the given hᵢ's, where the hᵢ's are expressions. If hᵢ is preceded by left arrow (← or <-), the simplification is performed in the reverse direction. If an hᵢ is a defined constant f, then the equational lemmas associated with f are used. This provides a convenient way to unfold f.

simp [*] simplifies the main goal target using the lemmas tagged with the attribute [simp] and all hypotheses.

simp * is a shorthand for simp [*].

simp only [h₁ h₂ ... hₙ] is like simp [h₁ h₂ ... hₙ] but does not use [simp] lemmas

simp [-id_1, ... -id_n] simplifies the main goal target using the lemmas tagged with the attribute [simp], but removes the ones named idᵢ.

simp at h₁ h₂ ... hₙ simplifies the non-dependent hypotheses h₁ : T₁ ... hₙ : Tₙ. The tactic fails if the target or another hypothesis depends on one of them. The token ⊢ or |- can be added to the list to include the target.

simp at * simplifies all the hypotheses and the target.

simp * at * simplifies target and all (non-dependent propositional) hypotheses using the other hypotheses.

simp with attr₁ ... attrₙ simplifies the main goal target using the lemmas tagged with any of the attributes [attr₁], ..., [attrₙ] or [simp].

Tags:

core
simplification

Related declarations

tactic.interactive.simp

Import using

imported by default

simp_intros

simp_intros h₁ h₂ ... hₙ is similar to intros h₁ h₂ ... hₙ except that each hypothesis is simplified as it is introduced, and each introduced hypothesis is used to simplify later ones and the final target.

As with simp, a list of simplification lemmas can be provided. The modifiers only and with behave as with simp.

Tags:

core
simplification

Related declarations

tactic.interactive.simp_intros

Import using

imported by default

simp_result

simp_result { tac } attempts to run a tactic block tac, intercepts any results the tactic block would have assigned to the goals, and runs simp on those results before assigning the simplified values to the original goals.

You can use the usual interactive syntax for simp, e.g. simp_result only [a, b, c] with attr { tac }.

dsimp_result { tac } works similarly, internally using dsimp (and so only simplifiying along definitional lemmas).

Tags:

simplification

Related declarations

Import using

import tactic.simp_result
import tactic.basic

simp_rw

simp_rw functions as a mix of simp and rw. Like rw, it applies each rewrite rule in the given order, but like simp it repeatedly applies these rules and also under binders like ∀ x, ..., ∃ x, ... and λ x, ....

Usage:

simp_rw [lemma_1, ..., lemma_n] will rewrite the goal by applying the lemmas in that order. A lemma preceded by ← is applied in the reverse direction.
simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ will rewrite the given hypotheses.
simp_rw [...] at ⊢ h₁ ... hₙ rewrites the goal as well as the given hypotheses.
simp_rw [...] at * rewrites in the whole context: all hypotheses and the goal.

Lemmas passed to simp_rw must be expressions that are valid arguments to simp.

For example, neither simp nor rw can solve the following, but simp_rw can:

example {α β : Type} {f : α → β} {t : set β} :
  (∀ s, f '' s ⊆ t) = ∀ s : set α, ∀ x ∈ s, x ∈ f ⁻¹' t :=
by simp_rw [set.image_subset_iff, set.subset_def]

Tags:

simplification

Related declarations

tactic.interactive.simp_rw

Import using

import tactic.simp_rw
import tactic.basic

simpa

This is a "finishing" tactic modification of simp. It has two forms.

simpa [rules, ...] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.
simpa [rules, ...] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

Tags:

simplification

Related declarations

tactic.interactive.simpa

Import using

import tactic.simpa
import tactic.basic

skip

A do-nothing tactic that always succeeds.

Tags:

core
combinator

Related declarations

tactic.interactive.skip

Import using

imported by default

slice

slice_lhs a b { tac } zooms to the left hand side, uses associativity for categorical composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.

slice_rhs a b { tac } zooms to the right hand side, uses associativity for categorical composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.

Tags:

category theory

Related declarations

Import using

import tactic.slice
import tactic

solve1

solve1 { t } applies the tactic t to the main goal and fails if it is not solved.

Tags:

core
combinator
goal management

Related declarations

tactic.interactive.solve1

Import using

imported by default

solve_by_elim

solve_by_elim calls apply on the main goal to find an assumption whose head matches and then repeatedly calls apply on the generated subgoals until no subgoals remain, performing at most max_depth recursive steps.

solve_by_elim discharges the current goal or fails.

solve_by_elim performs back-tracking if subgoals can not be solved.

By default, the assumptions passed to apply are the local context, rfl, trivial, congr_fun and congr_arg.

The assumptions can be modified with similar syntax as for simp:

solve_by_elim [h₁, h₂, ..., hᵣ] also applies the named lemmas.
solve_by_elim with attr₁ ... attrᵣ also applies all lemmas tagged with the specified attributes.
solve_by_elim only [h₁, h₂, ..., hᵣ] does not include the local context, rfl, trivial, congr_fun, or congr_arg unless they are explicitly included.
solve_by_elim [-id_1, ... -id_n] uses the default assumptions, removing the specified ones.

solve_by_elim* tries to solve all goals together, using backtracking if a solution for one goal makes other goals impossible.

optional arguments passed via a configuration argument as solve_by_elim { ... }

max_depth: number of attempts at discharging generated sub-goals
discharger: a subsidiary tactic to try at each step when no lemmas apply (e.g. cc may be helpful).
pre_apply: a subsidiary tactic to run at each step before applying lemmas (e.g. intros).
accept: a subsidiary tactic list expr → tactic unit that at each step, before any lemmas are applied, is passed the original proof terms as reported by get_goals when solve_by_elim started (but which may by now have been partially solved by previous apply steps). If the accept tactic fails, solve_by_elim will abort searching the current branch and backtrack. This may be used to filter results, either at every step of the search, or filtering complete results (by testing for the absence of metavariables, and then the filtering condition).

Tags:

search

Related declarations

tactic.interactive.solve_by_elim

Import using

import tactic.solve_by_elim
import tactic.basic

sorry / admit

Closes the main goal using sorry. Takes an optional ignored tactic block.

The ignored tactic block is useful for "commenting out" part of a proof during development:

begin
  split,
  sorry { expensive_tactic },

end
```

Tags:

core
testing
debugging

Related declarations

Import using

imported by default

specialize

The tactic specialize h a₁ ... aₙ works on local hypothesis h. The premises of this hypothesis, either universal quantifications or non-dependent implications, are instantiated by concrete terms coming either from arguments a₁ ... aₙ. The tactic adds a new hypothesis with the same name h := h a₁ ... aₙ and tries to clear the previous one.

Tags:

core
context management
lemma application

Related declarations

tactic.interactive.specialize

Import using

imported by default

split

Applies the constructor when the type of the target is an inductive data type with one constructor.

Tags:

core
basic
logic

Related declarations

tactic.interactive.split

Import using

imported by default

split_ifs

Splits all if-then-else-expressions into multiple goals.

Given a goal of the form g (if p then x else y), split_ifs will produce two goals: p ⊢ g x and ¬p ⊢ g y.

If there are multiple ite-expressions, then split_ifs will split them all, starting with a top-most one whose condition does not contain another ite-expression.

split_ifs at * splits all ite-expressions in all hypotheses as well as the goal.

split_ifs with h₁ h₂ h₃ overrides the default names for the hypotheses.

Tags:

case bashing

Related declarations

tactic.interactive.split_ifs

Import using

import tactic.split_ifs
import tactic.basic

squeeze_simp / squeeze_simpa / squeeze_dsimp / squeeze_scope

squeeze_simp, squeeze_simpa and squeeze_dsimp perform the same task with the difference that squeeze_simp relates to simp while squeeze_simpa relates to simpa and squeeze_dsimp relates to dsimp. The following applies to squeeze_simp, squeeze_simpa and squeeze_dsimp.

squeeze_simp behaves like simp (including all its arguments) and prints a simp only invocation to skip the search through the simp lemma list.

For instance, the following is easily solved with simp:

example : 0 + 1 = 1 + 0 := by simp

To guide the proof search and speed it up, we may replace simp with squeeze_simp:

example : 0 + 1 = 1 + 0 := by squeeze_simp
-- prints:
-- Try this: simp only [add_zero, eq_self_iff_true, zero_add]

squeeze_simp suggests a replacement which we can use instead of squeeze_simp.

example : 0 + 1 = 1 + 0 := by simp only [add_zero, eq_self_iff_true, zero_add]

squeeze_simp only prints nothing as it already skips the simp list.

This tactic is useful for speeding up the compilation of a complete file. Steps:

search and replace simp with squeeze_simp (the space helps avoid the replacement of simp in @[simp]) throughout the file.
Starting at the beginning of the file, go to each printout in turn, copy the suggestion in place of squeeze_simp.
after all the suggestions were applied, search and replace squeeze_simp with simp to remove the occurrences of squeeze_simp that did not produce a suggestion.

Known limitation(s):

in cases where squeeze_simp is used after a ; (e.g. cases x; squeeze_simp), squeeze_simp will produce as many suggestions as the number of goals it is applied to. It is likely that none of the suggestion is a good replacement but they can all be combined by concatenating their list of lemmas. squeeze_scope can be used to combine the suggestions: by squeeze_scope { cases x; squeeze_simp }
sometimes, simp lemmas are also _refl_lemma and they can be used without appearing in the resulting proof. squeeze_simp won't know to try that lemma unless it is called as squeeze_simp?

Tags:

simplification
Try this

Related declarations

Import using

import tactic.squeeze
import tactic.basic

subst

Given hypothesis h : x = t or h : t = x, where x is a local constant, subst h substitutes x by t everywhere in the main goal and then clears h.

Tags:

core
rewriting

Related declarations

tactic.interactive.subst

Import using

imported by default

subst'

If the expression q is a local variable with type x = t or t = x, where x is a local constant, tactic.interactive.subst' q substitutes x by t everywhere in the main goal and then clears q. If q is another local variable, then we find a local constant with type q = t or t = q and substitute t for q.

Like tactic.interactive.subst, but fails with a nicer error message if the substituted variable is a local definition. It is trickier to fix this in core, since tactic.is_local_def is in mathlib.

Tags:

context management

Related declarations

tactic.interactive.subst'

Import using

import tactic.interactive
import tactic.basic

subst_vars

Apply subst to all hypotheses of the form h : x = t or h : t = x.

Tags:

core
rewriting

Related declarations

tactic.interactive.subst_vars

Import using

imported by default

substs

Multiple subst. substs x y z is the same as subst x, subst y, subst z.

Tags:

rewriting

Related declarations

tactic.interactive.substs

Import using

import tactic.interactive
import tactic.basic

success_if_fail

Succeeds if the given tactic fails.

Tags:

core
testing
combinator

Related declarations

tactic.interactive.success_if_fail

Import using

imported by default

suffices

suffices h : t is the same as have h : t, tactic.swap. In other words, it adds the hypothesis h : t to the current goal and opens a new subgoal with target t.

Tags:

core
basic
goal management

Related declarations

tactic.interactive.suffices

Import using

imported by default

suggest

suggest lists possible usages of the refine tactic and leaves the tactic state unchanged. It is intended as a complement of the search function in your editor, the #find tactic, and library_search.

suggest takes an optional natural number num as input and returns the first num (or less, if all possibilities are exhausted) possibilities ordered by length of lemma names. The default for num is 50.

suggest using h₁ h₂ will only show solutions that make use of the local hypotheses h₁ and h₂.

For performance reasons suggest uses monadic lazy lists (mllist). This means that suggest might miss some results if num is not large enough. However, because suggest uses monadic lazy lists, smaller values of num run faster than larger values.

An example of suggest in action,

example (n : nat) : n < n + 1 :=
begin suggest, sorry end

prints the list,

Try this: exact nat.lt.base n
Try this: exact nat.lt_succ_self n
Try this: refine not_le.mp _
Try this: refine gt_iff_lt.mp _
Try this: refine nat.lt.step _
Try this: refine lt_of_not_ge _
...

Tags:

search
Try this

Related declarations

tactic.interactive.suggest

Import using

import tactic.suggest
import tactic.basic

swap

swap n will move the nth goal to the front. swap defaults to swap 2, and so interchanges the first and second goals.

See also tactic.interactive.rotate, which moves the first n goals to the back.

Tags:

goal management

Related declarations

tactic.interactive.swap

Import using

import tactic.interactive
import tactic.basic

symmetry

This tactic applies to a goal whose target has the form t ~ u where ~ is a symmetric relation, that is, a relation which has a symmetry lemma tagged with the attribute [symm]. It replaces the target with u ~ t.

Tags:

core
basic
lemma application

Related declarations

tactic.interactive.symmetry

Import using

imported by default

tautology

This tactic (with shorthand tauto) breaks down assumptions of the form _ ∧ _, _ ∨ _, _ ↔ _ and ∃ _, _ and splits a goal of the form _ ∧ _, _ ↔ _ or ∃ _, _ until it can be discharged using reflexivity or solve_by_elim. This is a finishing tactic: it either closes the goal or raises an error.

The variants tautology! and tauto! use the law of excluded middle.

For instance, one can write:

example (p q r : Prop) [decidable p] [decidable r] : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by tauto

and the decidability assumptions can be dropped if tauto! is used instead of tauto.

tauto {closer := tac} will use tac on any subgoals created by tauto that it is unable to solve before failing.

Tags:

logic
decision procedure

Related declarations

Import using

import tactic.tauto
import tactic.basic

tfae

The tfae tactic suite is a set of tactics that help with proving that certain propositions are equivalent. In data/list/basic.lean there is a section devoted to propositions of the form

tfae [p1, p2, ..., pn]

where p1, p2, through, pn are terms of type Prop. This proposition asserts that all the pi are pairwise equivalent. There are results that allow to extract the equivalence of two propositions pi and pj.

To prove a goal of the form tfae [p1, p2, ..., pn], there are two tactics. The first tactic is tfae_have. As an argument it takes an expression of the form i arrow j, where i and j are two positive natural numbers, and arrow is an arrow such as →, ->, ←, <-, ↔, or <->. The tactic tfae_have : i arrow j sets up a subgoal in which the user has to prove the equivalence (or implication) of pi and pj.

The remaining tactic, tfae_finish, is a finishing tactic. It collects all implications and equivalences from the local context and computes their transitive closure to close the main goal.

tfae_have and tfae_finish can be used together in a proof as follows:

example (a b c d : Prop) : tfae [a,b,c,d] :=
begin
  tfae_have : 3 → 1,
  { /- prove c → a -/ },
  tfae_have : 2 → 3,
  { /- prove b → c -/ },
  tfae_have : 2 ← 1,
  { /- prove a → b -/ },
  tfae_have : 4 ↔ 2,
  { /- prove d ↔ b -/ },
    -- a b c d : Prop,
    -- tfae_3_to_1 : c → a,
    -- tfae_2_to_3 : b → c,
    -- tfae_1_to_2 : a → b,
    -- tfae_4_iff_2 : d ↔ b
    -- ⊢ tfae [a, b, c, d]
  tfae_finish,
end

Tags:

logic

Related declarations

Import using

import tactic.tfae
import tactic

tidy

Use a variety of conservative tactics to solve goals.

tidy? reports back the tactic script it found. As an example

example : ∀ x : unit, x = unit.star :=
begin
  tidy? -- Prints the trace message: "Try this: intros x, exact dec_trivial"
end

The default list of tactics is stored in tactic.tidy.default_tidy_tactics. This list can be overridden using tidy { tactics := ... }. (The list must be a list of tactic string, so that tidy? can report a usable tactic script.)

Tactics can also be added to the list by tagging them (locally) with the [tidy] attribute.

Tags:

search
Try this
finishing

Related declarations

tactic.interactive.tidy

Import using

import tactic.tidy
import tactic.basic

trace

trace a displays a in the tracing buffer.

Tags:

core
debugging
testing

Related declarations

tactic.interactive.trace

Import using

imported by default

trace_simp_set

Just construct the simp set and trace it. Used for debugging.

Tags:

core
debugging
testing

Related declarations

tactic.interactive.trace_simp_set

Import using

imported by default

trace_state

This tactic displays the current state in the tracing buffer.

Tags:

core
debugging
testing

Related declarations

tactic.interactive.trace_state

Import using

imported by default

transitivity

This tactic applies to a goal whose target has the form t ~ u where ~ is a transitive relation, that is, a relation which has a transitivity lemma tagged with the attribute [trans].

transitivity s replaces the goal with the two subgoals t ~ s and s ~ u. If s is omitted, then a metavariable is used instead.

Tags:

core
lemma application

Related declarations

tactic.interactive.transitivity

Import using

imported by default

triv

Tries to solve the goal using a canonical proof of true or the reflexivity tactic. Unlike trivial or trivial', does not the contradiction tactic.

Tags:

finishing

Related declarations

tactic.interactive.triv

Import using

import tactic.interactive
import tactic.basic

trivial

Tries to solve the current goal using a canonical proof of true, or the reflexivity tactic, or the contradiction tactic.

Tags:

core
finishing

Related declarations

tactic.interactive.trivial

Import using

imported by default

trivial'

A weaker version of trivial that tries to solve the goal using a canonical proof of true or the reflexivity tactic (unfolding only reducible constants, so can fail faster than trivial), and otherwise tries the contradiction tactic.

Tags:

finishing

Related declarations

tactic.interactive.trivial'

Import using

import tactic.interactive
import tactic.basic

trunc_cases

trunc_cases e performs case analysis on a trunc expression e, attempting the following strategies:

when the goal is a subsingleton, calling induction e using trunc.rec_on_subsingleton,
when the goal does not depend on e, calling fapply trunc.lift_on e, and using intro and clear afterwards to make the goals look like we used induction,
otherwise, falling through to trunc.rec_on, and in the new invariance goal calling cases h_p on the useless h_p : true hypothesis, and then attempting to simplify the eq.rec.

trunc_cases e with h names the new hypothesis h. If e is a local hypothesis already, trunc_cases defaults to reusing the same name.

trunc_cases e with h h_a h_b will use the names h_a and h_b for the new hypothesis in the invariance goal if trunc_cases uses trunc.lift_on or trunc.rec_on.

Finally, if the new hypothesis from inside the trunc is a type class, trunc_cases resets the instance cache so that it is immediately available.

Tags:

case bashing

Related declarations

tactic.interactive.trunc_cases

Import using

import tactic.trunc_cases
import tactic.basic

try

try { t } tries to apply tactic t, but succeeds whether or not t succeeds.

Tags:

core
combinator

Related declarations

tactic.interactive.try

Import using

imported by default

type_check

Type check the given expression, and trace its type.

Tags:

core
debugging
testing

Related declarations

tactic.interactive.type_check

Import using

imported by default

unfold

Given defined constants e₁ ... eₙ, unfold e₁ ... eₙ iteratively unfolds all occurrences in the target of the main goal, using equational lemmas associated with the definitions.

As with simp, the at modifier can be used to specify locations for the unfolding.

Tags:

core
basic
rewriting

Related declarations

tactic.interactive.unfold

Import using

imported by default

unfold1

Similar to unfold, but does not iterate the unfolding.

Tags:

core
rewriting

Related declarations

tactic.interactive.unfold1

Import using

imported by default

unfold_coes

Unfold coercion-related definitions

Tags:

simplification

Related declarations

tactic.interactive.unfold_coes

Import using

import tactic.interactive
import tactic.basic

unfold_projs

This tactic unfolds all structure projections.

Tags:

core
rewriting

Related declarations

tactic.interactive.unfold_projs

Import using

imported by default

unify_equations

unify_equations eq₁ ... eqₙ performs a form of first-order unification on the hypotheses eqᵢ. The eqᵢ must be homogeneous or heterogeneous equations. Unification means that the equations are simplified using various facts about constructors. For instance, consider this goal:

P : ∀ n, fin n → Prop
n m : ℕ
f : fin n
g : fin m
h₁ : n + 1 = m + 1
h₂ : f == g
h₃ : P n f
⊢ P m g

After unify_equations h₁ h₂, we get

P : ∀ n, fin n → Prop
n : ℕ
f : fin n
h₃ : P n f
⊢ P n f

In the example, unify_equations uses the fact that every constructor is injective to conclude n = m from h₁. Then it replaces every m with n and moves on to h₂. The types of f and g are now equal, so the heterogeneous equation turns into a homogeneous one and g is replaced by f. Note that the equations are processed from left to right, so unify_equations h₂ h₁ would not simplify as much.

In general, unify_equations uses the following steps on each equation until none of them applies any more:

Constructor injectivity: if nat.succ n = nat.succ m then n = m.
Substitution: if x = e for some hypothesis x, then x is replaced by e everywhere.
No-confusion: nat.succ n = nat.zero is a contradiction. If we have such an equation, the goal is solved immediately.
Cycle elimination: n = nat.succ n is a contradiction.
Redundancy: if t = u but t and u are already definitionally equal, then this equation is removed.
Downgrading of heterogeneous equations: if t == u but t and u have the same type (up to definitional equality), then the equation is replaced by t = u.

Tags:

simplification

Related declarations

tactic.interactive.unify_equations

Import using

import tactic.unify_equations
import tactic.basic

use

Similar to existsi. use x will instantiate the first term of an ∃ or Σ goal with x. It will then try to close the new goal using trivial', or try to simplify it by applying exists_prop. Unlike existsi, x is elaborated with respect to the expected type. use will alternatively take a list of terms [x0, ..., xn].

use will work with constructors of arbitrary inductive types.

Examples:

example (α : Type) : ∃ S : set α, S = S :=
by use ∅

example : ∃ x : ℤ, x = x :=
by use 42

example : ∃ n > 0, n = n :=
begin
  use 1,
  -- goal is now 1 > 0 ∧ 1 = 1, whereas it would be ∃ (H : 1 > 0), 1 = 1 after existsi 1.
  exact ⟨zero_lt_one, rfl⟩,
end

example : ∃ a b c : ℤ, a + b + c = 6 :=
by use [1, 2, 3]

example : ∃ p : ℤ × ℤ, p.1 = 1 :=
by use ⟨1, 42⟩

example : Σ x y : ℤ, (ℤ × ℤ) × ℤ :=
by use [1, 2, 3, 4, 5]

inductive foo
| mk : ℕ → bool × ℕ → ℕ → foo

example : foo :=
by use [100, tt, 4, 3]
```

Tags:

logic

Related declarations

Import using

import tactic.interactive
import tactic.basic

with_cases

Apply t to the main goal and revert any new hypothesis in the generated goals. If t is a supported tactic or chain of supported tactics (e.g. induction, cases, apply, constructor), the generated goals are also tagged with case tags. You can then use case to focus such tagged goals.

Two typical uses of with_cases:

Applying a custom eliminator:

lemma my_nat_rec :
  ∀ n {P : ℕ → Prop} (zero : P 0) (succ : ∀ n, P n → P (n + 1)), P n := ...

example (n : ℕ) : n = n :=
begin
  with_cases { apply my_nat_rec n },
  case zero { refl },
  case succ : m ih { refl }
end

Enabling the use of case after a chain of case-splitting tactics:

example (n m : ℕ) : unit :=
begin
  with_cases { cases n; induction m },
  case nat.zero nat.zero { exact () },
  case nat.zero nat.succ : k { exact () },
  case nat.succ nat.zero : i { exact () },
  case nat.succ nat.succ : k i ih_i { exact () }
end

Tags:

core
combinator

Related declarations

tactic.interactive.with_cases

Import using

imported by default

wlog

Without loss of generality: reduces to one goal under variables permutations.

Given a goal of the form g xs, a predicate p over a set of variables, as well as variable permutations xs_i. Then wlog produces goals of the form

The case goal, i.e. the permutation xs_i covers all possible cases: ⊢ p xs_0 ∨ ⋯ ∨ p xs_n The main goal, i.e. the goal reduced to xs_0: (h : p xs_0) ⊢ g xs_0 The invariant goals, i.e. g is invariant under xs_i: (h : p xs_i) (this : g xs_0) ⊢ gs xs_i

Either the permutation is provided, or a proof of the disjunction is provided to compute the permutation. The disjunction need to be in assoc normal form, e.g. p₀ ∨ (p₁ ∨ p₂). In many cases the invariant goals can be solved by AC rewriting using cc etc.

Example: On a state (n m : ℕ) ⊢ p n m the tactic wlog h : n ≤ m using [n m, m n] produces the following states: (n m : ℕ) ⊢ n ≤ m ∨ m ≤ n (n m : ℕ) (h : n ≤ m) ⊢ p n m (n m : ℕ) (h : m ≤ n) (this : p n m) ⊢ p m n

wlog supports different calling conventions. The name h is used to give a name to the introduced case hypothesis. If the name is avoided, the default will be case.

(1) wlog : p xs0 using [xs0, …, xsn] Results in the case goal p xs0 ∨ ⋯ ∨ ps xsn, the main goal (case : p xs0) ⊢ g xs0 and the invariance goals (case : p xsi) (this : g xs0) ⊢ g xsi.

(2) wlog : p xs0 := r using xs0 The expression r is a proof of the shape p xs0 ∨ ⋯ ∨ p xsi, it is also used to compute the variable permutations.

(3) wlog := r using xs0 The expression r is a proof of the shape p xs0 ∨ ⋯ ∨ p xsi, it is also used to compute the variable permutations. This is not as stable as (2), for example p cannot be a disjunction.

(4) wlog : R x y using x y and wlog : R x y Produces the case R x y ∨ R y x. If R is ≤, then the disjunction discharged using linearity. If using x y is avoided then x and y are the last two variables appearing in the expression R x y.

Tags:

logic

Related declarations

tactic.interactive.wlog

Import using

import tactic.wlog
import tactic

zify

The zify tactic is used to shift propositions from ℕ to ℤ. This is often useful since ℤ has well-behaved subtraction.

example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b :=
begin
  zify,
  zify at h,
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/
end

zify can be given extra lemmas to use in simplification. This is especially useful in the presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.

example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : false :=
begin
  zify [hab] at h,
  /- h : ↑a - ↑b < ↑c -/
end

zify makes use of the @[zify] attribute to move propositions, and the push_cast tactic to simplify the ℤ-valued expressions.

zify is in some sense dual to the lift tactic. lift (z : ℤ) to ℕ will change the type of an integer z (in the supertype) to ℕ (the subtype), given a proof that z ≥ 0; propositions concerning z will still be over ℤ. zify changes propositions about ℕ (the subtype) to propositions about ℤ (the supertype), without changing the type of any variable.

Tags:

coercions
transport

Related declarations

tactic.interactive.zify

Import using

import tactic.zify
import tactic