mathlib documentation

Similar to constructor, but does not reorder goals.

try_for n { tac } executes tac for n ticks, otherwise uses sorry to close the goal. Never fails. Useful for debugging.

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

Unfold coercion-related definitions

Unfold auxiliary definitions associated with the current declaration.

For debugging only. This tactic checks the current state for any missing dropped goals and restores them. Useful when there are no goals to solve but "result contains meta-variables".

Like try { tac }, but in the case of failure it continues from the failure state instead of reverting to the original state.

id { tac } is the same as tac, but it is useful for creating a block scope without requiring the goal to be solved at the end like { tac }. It can also be used to enclose a non-interactive tactic for patterns like tac1; id {tac2} where tac2 is non-interactive.

work_on_goal n { tac } creates a block scope for the n-goal (indexed from zero), and does not require that the goal be solved at the end (any remaining subgoals are inserted back into the list of goals).

Typically usage might look like: intros, simp, apply lemma_1, work_on_goal 2 { dsimp, simp }, refl

See also id { tac }, which is equivalent to work_on_goal 0 { tac }.

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

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

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

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.

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.

Make every proposition in the context decidable.

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

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

go from (x₀ : t₀) (x₁ : t₀) (x₂ : t₀) to (x₀ x₁ x₂ : t₀)

Remove identity functions from a term. These are normally automatically generated with terms like show t, from p or (p : t) which translate to some variant on @id t p in order to retain the type.

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

guard_hyp h := t fails if the hypothesis h does not have type t. We use this tactic for writing tests. Fixes guard_hyp by instantiating meta variables

match_hyp h := t fails if the hypothesis h does not match the type t (which may be a pattern). We use this tactic for writing tests.

guard_expr_strict t := e fails if the expr t is not equal to e. By contrast to guard_expr, this tests strict (syntactic) equality. We use this tactic for writing tests.

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

guard_hyp_strict h := t fails if the hypothesis h does not have type syntactically equal to t. We use this tactic for writing tests.

success_if_fail_with_msg { tac } msg succeeds if the interactive tactic tac fails with error message msg (for test writing purposes).

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

apply_field functions as have_field, apply field, clear field

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

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.

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, hx, hy] with field_simps

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.

The invocation of field_simp removes the lemma one_div (which is marked as a simp lemma in core) from the simpset, as this lemma works against the algorithm explained above.

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 [hx, hy],
  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.

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

a weaker version of trivial that tries to solve the goal by reflexivity or by reducing it to true, unfolding only reducible constants.

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 triv, 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]

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

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.

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.

ac_change is convert_to followed by ac_refl. It is useful for rearranging/reassociating e.g. sums:

example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N :=
begin
  ac_change a + d + e + f + c + g + b ≤ _,
-- ⊢ a + d + e + f + c + g + b ≤ N
end

ac_change g using n is convert_to g using n; try {ac_refl}.

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

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

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

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

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

revert_after n reverts all the hypotheses after n.

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

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

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.