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.
Move goal n to the front.
rotate n cyclically shifts the goals n times. rotate defaults to rotate 1.
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.
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 propositions in the context decidable
Like generalize but also considers assumptions specified by the user. The user can also specify to omit the goal.
Similar to refine but generates equality proof obligations for every discrepancy between the goal and the type of the rule. convert e using n (with n : ℕ) bounds the depth of the search for discrepancies, analogous to congr' n.
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)
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
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: apply the list of rules hs (given as pexpr) and assumption on the first goal and the resulting subgoals, iteratively, at most n times. n is 50 by default. hs can contain user attributes: in this case all theorems with this attribute are added to the list of rules.
example, with or without user attribute:
@[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 :=
by apply_rules mono_rules
-- any of the following lines would also work:
-- 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]
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.
choose a b h using hyp takes an hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b for some P : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and a proposition h stating ∀ (x : X) (y : Y), P x y (a x y) (b x y). It presumably also works with dependent versions.
Example:
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
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. 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 : ∃ 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.
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, using congr' n to resolve discrepancies.
convert_to g defaults to using congr' 1.
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.
clear_except h₀ h₁ deletes all the assumptions it can except for h₀ and h₁.
mk_paragraph right_margin ls packs ls into a paragraph where the lines have length at most right_margin
Format the current goal as a stand-alone example. Useful for testing tactic.
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
-- end
extract_goal my_lemma
-- lemma my_lemma {i j k : ℕ} (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k :=
-- begin
-- 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
-- end
extract_goal my_lemma with i j k
-- prints:
-- lemma my_lemma {i j k : ℕ} : i ≤ k :=
-- begin
-- end
end