Simple tactics that are used throughout Batteries.

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

• Batteries.Tactic.tactic_ = Lean.ParserDescr.node `Batteries.Tactic.tactic_ 1024 (Lean.ParserDescr.nonReservedSymbol "_" false)

def Batteries.Tactic.exacts : Lean.ParserDescr

exacts [e1, ..., en] is like exact, using the terms e1, ..., en to close all the current n goals. It raises an error if the number of goals does not match.

Equations

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

def Batteries.Tactic.tacticBy_contra_core : Lean.ParserDescr

by_contra_core is the component of by_contra that turns the goal into the form p → False. by_contra h is defined as by_contra_core followed by rintro h.

• If the goal is a negation ¬q, the goal becomes q → False.
• If the goal has a Decidable instance, it uses Decidable.byContradiction instead of Classical.byContradiction.

Equations

• Batteries.Tactic.tacticBy_contra_core = Lean.ParserDescr.node `Batteries.Tactic.tacticBy_contra_core 1024 (Lean.ParserDescr.nonReservedSymbol "by_contra_core" false)

def Batteries.Tactic.byContra : Lean.ParserDescr

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.
• h can be any pattern supported by rcases/rintro.

Equations

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

def Batteries.Tactic.tacticAbsurd_ : Lean.ParserDescr

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.

Equations

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

def Batteries.Tactic.tacticSplit_ands : Lean.ParserDescr

split_ands applies And.intro on all goals until it does not make progress.

Equations

• Batteries.Tactic.tacticSplit_ands = Lean.ParserDescr.node `Batteries.Tactic.tacticSplit_ands 1024 (Lean.ParserDescr.nonReservedSymbol "split_ands" false)

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

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

def Batteries.Tactic.triv : Lean.ParserDescr

Deprecated variant of trivial.

Equations

• Batteries.Tactic.triv = Lean.ParserDescr.node `Batteries.Tactic.triv 1024 (Lean.ParserDescr.nonReservedSymbol "triv" false)

def Batteries.Tactic.Conv.exact : Lean.ParserDescr

The conv mode tactic exact e closes the goal ⊢ t by rewriting it to t', where e : t = t'.

Equations

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

def Batteries.Tactic.Conv.equals : Lean.ParserDescr

The conv mode tactic equals e claims that the currently focused subexpression is equal to the term e, and proves this claim using the given tactic.

example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
  conv in (_ - _) => equals 0 =>
    -- current goal: ⊢ n - n = 0
    apply Nat.sub_self
  -- current goal: P (fun n => 0)

Equations

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