Documentation

Std.Tactic.Basic

source
ink
def Std.Tactic.tacticExfalso :
Lean.ParserDescr

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

Equations
source
ink
def Std.Tactic.tactic_ :
Lean.ParserDescr

_ 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
source
ink
def Std.Tactic.failIfSuccessConv :
Lean.ParserDescr

fail_if_success t fails if the tactic t succeeds.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Std.Tactic.tacticRwa__ :
Lean.ParserDescr

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

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Std.Tactic.exacts :
Lean.ParserDescr

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.
source
ink
def Std.Tactic.byContra :
Lean.ParserDescr

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.
source
ink
def Std.Tactic.tacticIterate____ :
Lean.ParserDescr

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.
source
ink
def Std.Tactic.tacticRepeat'_ :
Lean.ParserDescr

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.
source
ink
def Std.Tactic.tacticRepeat1_ :
Lean.ParserDescr

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.
source
ink
def Std.Tactic.tacticSubst_eqs :
Lean.ParserDescr

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

Equations
source
ink
def Std.Tactic.tacticSplit_ands :
Lean.ParserDescr

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

Equations
source
ink
def Std.Tactic.tacticFapply_ :
Lean.ParserDescr

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.
source
ink
def Std.Tactic.tacticEapply_ :
Lean.ParserDescr

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.
source
ink
def Std.Tactic.triv :
Lean.ParserDescr

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
source
ink
def Std.Tactic.Conv.exact :
Lean.ParserDescr

conv tactic to close a goal using an equality theorem.

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