The `tauto` tactic.

source
def Mathlib.Tactic.Tauto.distribNotOnceAt (hypFVar : Lean.Expr) (g : Lean.MVarId) :
Lean.MetaM Lean.Meta.AssertAfterResult

Tries to apply de-Morgan-like rules on a hypothesis.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.Tauto.distribNotOnceAt hypFVar g = g.withContext (Lean.throwError (Lean.toMessageData "not fvar " ++ Lean.toMessageData hypFVar))

Instances For

source
structure Mathlib.Tactic.Tauto.DistribNotState :
Type

State of the `distribNotAt` function. We need to carry around the list of remaining hypothesis as fvars so that we can incrementally apply the `AssertAfterResult.subst` from each step to each of them. Otherwise, they could end up referring to old hypotheses.

- fvars : List Lean.Expr

  The list of hypothesis left to work on, renamed to be up-to-date with the current goal.

- currentGoal : Lean.MVarId

  The current goal.

Instances For

source
partial def Mathlib.Tactic.Tauto.distribNotAt (nIters : ℕ) (state : DistribNotState) :
Lean.MetaM DistribNotState

Calls `distribNotAt` on the head of `state.fvars` up to `nIters` times, returning early on failure.

source
partial def Mathlib.Tactic.Tauto.distribNotAux (fvars : List Lean.Expr) (g : Lean.MVarId) :
Lean.MetaM Lean.MVarId

For each fvar in `fvars`, calls `distribNotAt` and carries along the resulting renamings.

source
def Mathlib.Tactic.Tauto.distribNot :
Lean.Elab.Tactic.TacticM Unit

Tries to apply de-Morgan-like rules on all hypotheses. Always succeeds, regardless of whether any progress was actually made.

Equations

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

Instances For

source
structure Mathlib.Tactic.Tauto.Config :
Type

Config for the `tauto` tactic. Currently empty. TODO: add `closer` option.

Instances For

source
def Mathlib.Tactic.Tauto.elabConfig :
Lean.Syntax → Lean.Elab.Tactic.TacticM Config

Function elaborating `Config`.

Equations

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

Instances For

source
def Mathlib.Tactic.Tauto.coreConstructorMatcher (e : Q(Prop)) :
Lean.MetaM Bool

Matches propositions where we want to apply the `constructor` tactic in the core loop of `tauto`.

Equations

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

Instances For

source
def Mathlib.Tactic.Tauto.casesMatcher (e : Q(Prop)) :
Lean.MetaM Bool

Matches propositions where we want to apply the `cases` tactic in the core loop of `tauto`.

Equations

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

Instances For

source
def Mathlib.Tactic.Tauto.tautoCore :
Lean.Elab.Tactic.TacticM Unit

The core loop of the `tauto` tactic. Repeatedly tries to break down propositions until no more progress can be made. Tries `assumption` and `contradiction` at every step, to discharge goals as soon as possible. Does not do anything that requires backtracking.

TODO: The Lean 3 version uses more-powerful versions of `contradiction` and `assumption` that additionally apply `symm` and use a fancy union-find data structure to avoid duplicated work.

Equations

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

Instances For

source
def Mathlib.Tactic.Tauto.finishingConstructorMatcher (e : Q(Prop)) :
Lean.MetaM Bool

Matches propositions where we want to apply the `constructor` tactic in the finishing stage of `tauto`.

Equations

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

Instances For

source
def Mathlib.Tactic.Tauto.tautology :
Lean.Elab.Tactic.TacticM Unit

Implementation of the `tauto` tactic.

Equations

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

Instances For

source
def Mathlib.Tactic.Tauto.tauto :
Lean.ParserDescr

`tauto` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _` and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged using `reflexivity` or `solve_by_elim`. This is a finishing tactic: it either closes the goal or raises an error.

The Lean 3 version of this tactic by default attempted to avoid classical reasoning where possible. This Lean 4 version makes no such attempt. The `itauto` tactic is designed for that purpose.

Equations

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

Instances For

source
opaque linter.tacticAnalysis.tautoToGrind :
Lean.Option Bool

Report places where `tauto` can be replaced by `grind`.

source
def tautoToGrind :
Mathlib.TacticAnalysis.Config

Report places where `tauto` can be replaced by `grind`.

Equations

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

Instances For

source
opaque linter.tacticAnalysis.regressions.tautoToGrind :
Lean.Option Bool

Debug `grind` by identifying places where it does not yet supersede `tauto`.

source
def tautoToGrindRegressions :
Mathlib.TacticAnalysis.Config

Debug `grind` by identifying places where it does not yet supersede `tauto`.

Equations

- tautoToGrindRegressions = Mathlib.TacticAnalysis.grindReplacementWith "tauto" `Mathlib.Tactic.Tauto.tauto

Instances For