Basic tactics and utilities for tactic writing

This file defines some basic utilities for tactic writing, and also

• a dummy variables macro (which warns that the Lean 4 name is variable)
• the introv tactic, which allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses,
• an assumption macro, calling the assumption tactic on all goals
• the tactics match_target and clear_aux_decl (clearing all auxiliary declarations from the context).

def Mathlib.Tactic.variables : Lean.ParserDescr

Syntax for the variables command: this command is just a stub, and merely warns that it has been renamed to variable in Lean 4.

Equations

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

def Mathlib.Tactic.elabVariables : Lean.Elab.Command.CommandElab

The variables command: this is just a stub, and merely warns that it has been renamed to variable in Lean 4.

Equations

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

def Mathlib.Tactic.pushFVarAliasInfo {m : Type → Type} [Monad m] [Lean.Elab.MonadInfoTree m] (oldFVars newFVars : Array Lean.FVarId) (newLCtx : Lean.LocalContext) : m Unit

Given two arrays of FVarIds, one from an old local context and the other from a new local context, pushes FVarAliasInfos into the info tree for corresponding pairs of FVarIds. Recall that variables linked this way should be considered to be semantically identical.

The effect of this is, for example, the unused variable linter will see that variables from the first array are used if corresponding variables in the second array are used.

Equations

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

def Mathlib.Tactic.introv : Lean.ParserDescr

The tactic introv allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses. Any dependent hypotheses are assigned their default names.

Examples:

example : ∀ a b : Nat, a = b → b = a := by
  introv h,
  exact h.symm

The state after introv h is

a b : ℕ,
h : a = b
⊢ b = a

example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂

The state after introv h₁ h₂ is

a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c

Equations

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

def Mathlib.Tactic.evalIntrov : Lean.Elab.Tactic.Tactic

Equations

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

partial def Mathlib.Tactic.evalIntrov.introsDep : Lean.Elab.Tactic.TacticM Unit

def Mathlib.Tactic.evalIntrov.intro1PStep : Lean.Elab.Tactic.TacticM Unit

Equations

• Mathlib.Tactic.evalIntrov.intro1PStep = Lean.Elab.Tactic.liftMetaTactic fun (goal : Lean.MVarId) => do let __discr ← goal.intro1P match __discr with | (fst, goal) => pure [goal]

def Mathlib.Tactic.tacticAssumption' : Lean.ParserDescr

Try calling assumption on all goals; succeeds if it closes at least one goal.

Equations

• Mathlib.Tactic.tacticAssumption' = Lean.ParserDescr.node `Mathlib.Tactic.tacticAssumption' 1024 (Lean.ParserDescr.nonReservedSymbol "assumption'" false)

def Mathlib.Tactic.tacticMatch_target_ : Lean.ParserDescr

Equations

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

def Mathlib.Tactic.clearAuxDecl : Lean.ParserDescr

This tactic clears all auxiliary declarations from the context.

Equations

• Mathlib.Tactic.clearAuxDecl = Lean.ParserDescr.node `Mathlib.Tactic.clearAuxDecl 1024 (Lean.ParserDescr.nonReservedSymbol "clear_aux_decl" false)

def LibraryNote : Type

A mathlib library note: the note's content should be contained in its doc-string.

Equations

• LibraryNote = Unit

def commandLibrary_note2___ : Lean.ParserDescr

library_note2 «my note» /-- documentation -/ creates a library note named my note in the Mathlib.LibraryNote namespace, whose content is /-- documentation -/. You can access this note using, for example, #print Mathlib.LibraryNote.«my note».

Equations

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

def commandLibrary_note2____1 : Lean.ParserDescr

Support the old library_note "foo" syntax, with a deprecation warning.

Equations

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

def Mathlib.LibraryNote.«partially-applied ext lemmas» : LibraryNote

When possible, ext lemmas are stated without a full set of arguments. As an example, for bundled homs f, g, and of, f.comp of = g.comp of → f = g is a better ext lemma than (∀ x, f (of x) = g (of x)) → f = g, as the former allows a second type-specific extensionality lemmas to be applied to f.comp of = g.comp of. If the domain of of is ℕ or ℤ and of is a RingHom, such a lemma could then make the goal f (of 1) = g (of 1).

For bundled morphisms, there is a ext lemma that always applies of the form (∀ x, ⇑f x = ⇑g x) → f = g. When adding type-specific ext lemmas like the one above, we want these to be tried first. This happens automatically since the type-specific lemmas are inevitably defined later.

Equations

• Mathlib.LibraryNote.«partially-applied ext lemmas» = ()