Documentation

Std.Tactic.Basic

exfalso converts a goal ⊢ tgt into False by applying False.elim.

Equations

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

Equations

fail_if_success t fails if the tactic t succeeds.

Equations
  • One or more equations did not get rendered due to their size.

rwa calls rw, then closes any remaining goals using assumption.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

iterate n tac runs tac exactly n times. iterate tac runs tac repeatedly until failure.

To run multiple tactics, one can do iterate (tac₁; tac₂; ⋯) or

iterate
  tac₁
  tac₂
  ⋯
Equations
  • One or more equations did not get rendered due to their size.

repeat' tac runs tac on all of the goals to produce a new list of goals, then runs tac again on all of those goals, and repeats until tac fails on all remaining goals.

Equations
  • One or more equations did not get rendered due to their size.

repeat1 tac applies tac to main goal at least once. If the application succeeds, the tactic is applied recursively to the generated subgoals until it eventually fails.

Equations
  • One or more equations did not get rendered due to their size.

subst_eqs applies subst to all equalities in the context as long as it makes progress.

Equations

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

Equations

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

Equations
  • One or more equations did not get rendered due to their size.

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'
Equations
  • One or more equations did not get rendered due to their size.

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

Equations

conv tactic to close a goal using an equality theorem.

Equations
  • One or more equations did not get rendered due to their size.