The tauto tactic.

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))

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.

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.

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.

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.

structure Mathlib.Tactic.Tauto.Config : Type

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

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.

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.

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.

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.

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.

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.

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.