1.9. Basic tactics / assumptions

rfl

This tactic applies to a goal whose target has the form x ~ x, where ~ is equality, heterogeneous equality or any relation that has a reflexivity lemma tagged with the attribute @[refl].

symm

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

• symm at h will rewrite a hypothesis h : t ~ u to h : u ~ t.

trans

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

• trans s replaces the goal with the two subgoals t ~ s and s ~ u.

• If s is omitted, then a metavariable is used instead.

Additionally, trans also applies to a goal whose target has the form t → u, in which case it replaces the goal with t → s and s → u.

assumption

assumption tries to solve the main goal using a hypothesis of compatible type, or else fails. Note also the ‹t› term notation, which is a shorthand for show t by assumption.

exact

exact e closes the main goal if its target type matches that of e.

apply

apply e tries to match the current goal against the conclusion of e's type. 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.

apply at

apply t at i will use forward reasoning with t at the hypothesis i. Explicitly, if t : α₁ → ⋯ → αᵢ → ⋯ → αₙ and i has type αᵢ, then this tactic will add metavariables/goals for any terms of αⱼ for j = 1, …, i-1, then replace the type of i with αᵢ₊₁ → ⋯ → αₙ by applying those metavariables and the original i.

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

generalize

• generalize ([h :] e = x),+ replaces all occurrences es in the main goal with a fresh hypothesis xs. If h is given, h : e = x is introduced as well.

• generalize e = x at h₁ ... hₙ also generalizes occurrences of e inside h₁, ..., hₙ.

• generalize e = x at * will generalize occurrences of e everywhere.

have

The have tactic is for adding hypotheses to the local context of the main goal.

• have h : t := e adds the hypothesis h : t if e is a term of type t.

• have h := e uses the type of e for t.

• have : t := e and have := e use this for the name of the hypothesis.

• have pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that have only one applicable constructor. For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.

let

The let tactic is for adding definitions to the local context of the main goal.

• let x : t := e adds the definition x : t := e if e is a term of type t.

• let x := e uses the type of e for t.

• let : t := e and let := e use this for the name of the hypothesis.

• let pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that let only one applicable constructor. For example, given p : α × β × γ, let ⟨x, y, z⟩ := p produces the local variables x : α, y : β, and z : γ.

replace

Acts like have, but removes a hypothesis with the same name as this one if possible. For example, if the state is:

Then after replace h : β the state will be:

case h
f : α → β
h : α
⊢ β

f : α → β
h : β
⊢ goal

whereas have h : β would result in:

case h
f : α → β
h : α
⊢ β

f : α → β
h✝ : α
h : β
⊢ goal

suffices

Given a main goal ctx ⊢ t, suffices h : t' from e replaces the main goal with ctx ⊢ t', e must have type t in the context ctx, h : t'.

The variant suffices h : t' by tac is a shorthand for suffices h : t' from by tac. If h : is omitted, the name this is used.

obtain

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

obtain ⟨patt⟩ : type := proof

is equivalent to

have h : type := proof
rcases h with ⟨patt⟩

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

If type is omitted, := proof is required.

refine

refine e behaves like exact e, except that named (?x) or unnamed (?_) holes in e that are not solved by unification with the main goal's target type are converted into new goals, using the hole's name, if any, as the goal case name.

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 using the same strategies as the congr! tactic. For example, in the proof state

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

the tactic convert e using 2 will change the goal to

⊢ n + n = 2 * n

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

The using 2 indicates it should iterate the congruence algorithm up to two times, where convert e would use an unrestricted number of iterations and lead to two impossible goals: ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2.

A variant configuration is convert (config := .unfoldSameFun) e, which only equates function applications for the same function (while doing so at the higher default transparency). This gives the same goal of ⊢ n + n = 2 * n without needing using 2.

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`

Limiting the depth of recursion can help with this. For example, convert h using 1 will work in this case.

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.

Refer to the congr! tactic to understand the congruence operations. One of its many features is that if x y : t and an instance Subsingleton t is in scope, then any goals of the form x = y are solved automatically.

Like congr!, convert takes an optional with clause of rintro patterns, for example convert e using n with x y z.

The convert tactic also takes a configuration option, for example

convert (config := {transparency := .default}) h

These are passed to congr!. See Congr!.Config for options.

constructor

If the main goal's target type is an inductive type, constructor solves it with the first matching constructor, or else fails.

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.

intro

The syntax intro. is deprecated in favor of nofun.

revert

revert x... is the inverse of intro x...: it moves the given hypotheses into the main goal's target type.