Documentation

<;>

t <;> [t1; t2; ...; tn] focuses on the first goal and applies t, which should result in n subgoals. It then applies each ti to the corresponding goal and collects the resulting subgoals.

Tags:

Defined in module:

Batteries.Tactic.SeqFocus

_

_ in tactic position acts like the done tactic: it fails and gives the list of goals if there are any. It is useful as a placeholder after starting a tactic block such as by _ to make it syntactically correct and show the current goal.

Tags:

Defined in module:

Batteries.Tactic.Init

absurd

Given a proof h of p, absurd h changes the goal to ⊢ ¬ p. If p is a negation ¬q then the goal is changed to ⊢ q instead.

Tags:

Defined in module:

Batteries.Tactic.Init

by_contra

by_contra h proves ⊢ p by contradiction, introducing a hypothesis h : ¬p and proving False.

• If p is a negation ¬q, h : q will be introduced instead of ¬¬q.
• If p is decidable, it uses Decidable.byContradiction instead of Classical.byContradiction.
• If h is omitted, the introduced variable will be called this.

Tags:

Defined in module:

Batteries.Tactic.Init

case

• case _ : t => tac finds the first goal that unifies with t and then solves it using tac or else fails. Like show, it changes the type of the goal to t. The _ can optionally be a case tag, in which case it only looks at goals whose tag would be considered by case (goals with an exact tag match, followed by goals with the tag as a suffix, followed by goals with the tag as a prefix).

• case _ n₁ ... nₘ : t => tac additionally names the m most recent hypotheses with inaccessible names to the given names. The names are renamed before matching against t. The _ can optionally be a case tag.

• case _ : t := e is short for case _ : t => exact e.

• case _ : t₁ | _ : t₂ | ... => tac is equivalent to (case _ : t₁ => tac); (case _ : t₂ => tac); ... but with all matching done on the original list of goals -- each goal is consumed as they are matched, so patterns may repeat or overlap.

• case _ : t will make the matched goal be the first goal. case _ : t₁ | _ : t₂ | ... makes the matched goals be the first goals in the given order.

• case _ : t := _ and case _ : t := ?m are the same as case _ : t but in the ?m case the goal tag is changed to m. In particular, the goal becomes metavariable ?m.

Tags:

Defined in module:

Batteries.Tactic.Case

case'

case' _ : t => tac is similar to the case _ : t => tac tactic, but it does not ensure the goal has been solved after applying tac, nor does it admit the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

Tags:

Defined in module:

Batteries.Tactic.Case

congr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ f as ≍ f bs. The optional parameter is the depth of the 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.

Tags:

Defined in module:

Batteries.Tactic.Congr

congr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ f as ≍ f bs.

• congr n controls the depth of the 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:

Defined in module:

Batteries.Tactic.Congr

eapply

eapply e is like apply e but it does not add subgoals for variables that appear in the types of other goals. Note that this can lead to a failure where there are no goals remaining but there are still metavariables in the term:

example (h : ∀ x : Nat, x = x → True) : True := by
  eapply h
  rfl
  -- no goals
-- (kernel) declaration has metavariables '_example'

Tags:

Defined in module:

Batteries.Tactic.Init

exacts

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

Tags:

Defined in module:

Batteries.Tactic.Init

fapply

fapply e is like apply e but it adds goals in the order they appear, rather than putting the dependent goals first.

Tags:

Defined in module:

Batteries.Tactic.Init

generalize_proofs

generalize_proofs ids* [at locs]? generalizes proofs in the current goal, turning them into new local hypotheses.

• generalize_proofs generalizes proofs in the target.
• generalize_proofs at h₁ h₂ generalized proofs in hypotheses h₁ and h₂.
• generalize_proofs at * generalizes proofs in the entire local context.
• generalize_proofs pf₁ pf₂ pf₃ uses names pf₁, pf₂, and pf₃ for the generalized proofs. These can be _ to not name proofs.

If a proof is already present in the local context, it will use that rather than create a new local hypothesis.

When doing generalize_proofs at h, if h is a let binding, its value is cleared, and furthermore if h duplicates a preceding local hypothesis then it is eliminated.

The tactic is able to abstract proofs from under binders, creating universally quantified proofs in the local context. To disable this, use generalize_proofs -abstract. The tactic is also set to recursively abstract proofs from the types of the generalized proofs. This can be controlled with the maxDepth configuration option, with generalize_proofs (config := { maxDepth := 0 }) turning this feature off.

For example:

def List.nthLe {α} (l : List α) (n : ℕ) (_h : n < l.length) : α := sorry
example : List.nthLe [1, 2] 1 (by simp) = 2 := by
  -- ⊢ [1, 2].nthLe 1 ⋯ = 2
  generalize_proofs h
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2

Tags:

Defined in module:

Batteries.Tactic.GeneralizeProofs

intro

The syntax intro. is deprecated in favor of nofun.

Tags:

Defined in module:

Batteries.Tactic.NoMatch

map_tacs

Assuming there are n goals, map_tacs [t1; t2; ...; tn] applies each ti to the respective goal and leaves the resulting subgoals.

Tags:

Defined in module:

Batteries.Tactic.SeqFocus

match

The syntax match ⋯ with. has been deprecated in favor of nomatch ⋯.

Both now support multiple discriminants.

Tags:

Defined in module:

Batteries.Tactic.NoMatch

on_goal

on_goal n => tacSeq creates a block scope for the n-th goal and tries the sequence of tactics tacSeq on it.

on_goal -n => tacSeq does the same, but the n-th goal is chosen by counting from the bottom.

The goal is not required to be solved and any resulting subgoals are inserted back into the list of goals, replacing the chosen goal.

Tags:

Defined in module:

Batteries.Tactic.PermuteGoals

pick_goal

pick_goal n will move the n-th goal to the front.

pick_goal -n will move the n-th goal (counting from the bottom) to the front.

See also Tactic.rotate_goals, which moves goals from the front to the back and vice-versa.

Tags:

Defined in module:

Batteries.Tactic.PermuteGoals

rcongr

Repeatedly apply congr and ext, using the given patterns as arguments for ext.

There are two ways this tactic stops:

• congr fails (makes no progress), after having already applied ext.
• congr canceled out the last usage of ext. In this case, the state is reverted to before the congr was applied.

For example, when the goal is

⊢ (fun x => f x + 3) '' s = (fun x => g x + 3) '' s

then rcongr x produces the goal

x : α ⊢ f x = g x

This gives the same result as congr; ext x; congr.

In contrast, congr would produce

⊢ (fun x => f x + 3) = (fun x => g x + 3)

and congr with x (or congr; ext x) would produce

x : α ⊢ f x + 3 = g x + 3

Tags:

Defined in module:

Batteries.Tactic.Congr

split_ands

split_ands applies And.intro until it does not make progress.

Tags:

Defined in module:

Batteries.Tactic.Init

squeeze_scope

The squeeze_scope tactic allows aggregating multiple calls to simp coming from the same syntax but in different branches of execution, such as in cases x <;> simp. The reported simp call covers all simp lemmas used by this syntax.

@[simp] def bar (z : Nat) := 1 + z
@[simp] def baz (z : Nat) := 1 + z

@[simp] def foo : Nat → Nat → Nat
  | 0, z => bar z
  | _+1, z => baz z

example : foo x y = 1 + y := by
  cases x <;> simp? -- two printouts:
  -- "Try this: simp only [foo, bar]"
  -- "Try this: simp only [foo, baz]"

example : foo x y = 1 + y := by
  squeeze_scope
    cases x <;> simp -- only one printout: "Try this: simp only [foo, baz, bar]"

Tags:

Defined in module:

Batteries.Tactic.SqueezeScope

swap

swap is a shortcut for pick_goal 2, which interchanges the 1st and 2nd goals.

Tags:

Defined in module:

Batteries.Tactic.PermuteGoals

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.

Tags:

Defined in module:

Batteries.Tactic.Trans

transitivity

Synonym for trans tactic.

Tags:

Defined in module:

Batteries.Tactic.Trans

triv

Deprecated variant of trivial.

Tags:

Defined in module:

Batteries.Tactic.Init

unreachable!

This tactic causes a panic when run (at compile time). (This is distinct from exact unreachable!, which inserts code which will panic at run time.)

It is intended for tests to assert that a tactic will never be executed, which is otherwise an unusual thing to do (and the unreachableTactic linter will give a warning if you do).

The unreachableTactic linter has a special exception for uses of unreachable!.

example : True := by trivial <;> unreachable!

Tags:

Defined in module:

Batteries.Tactic.Unreachable