Commit 2022-12-21 04:17 3f9ce172

View on Github →

feat: implement basic version of tauto tactic (#1081) Adds a basic version of the tauto tactic, mostly a line-by-line translation of the Lean 3 version.

As per this zulip discussion, makes tauto always-classical and eliminates tauto!.
Does not yet add any symmetry-based logic or the fancy union-find datastructure from https://github.com/leanprover-community/mathlib/pull/180.
Adds a andThenOnSubgoals tactic combinator in Mathlib.Tactic.Basic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/TypeTags.lean

Modified Mathlib/Data/Int/Units.lean

Modified Mathlib/Data/Set/Basic.lean

modified theorem Set.forall_in_swap

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Lean/Meta.lean

added def Lean.Elab.Tactic.liftMetaTactic'

modified def Lean.MVarId.replace

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Core.lean

added def Lean.Elab.Tactic.andThenOnSubgoals

added def Lean.Elab.Tactic.iterateAtMost

Modified Mathlib/Tactic/Relation/Symm.lean

Modified Mathlib/Tactic/SplitIfs.lean

Created Mathlib/Tactic/Tauto.lean

added structure Mathlib.Tactic.Tauto.Config

added def Mathlib.Tactic.Tauto.casesMatcher

added def Mathlib.Tactic.Tauto.coreConstructorMatcher

added def Mathlib.Tactic.Tauto.distribNot

added def Mathlib.Tactic.Tauto.distribNotAt

added def Mathlib.Tactic.Tauto.finishingConstructorMatcher

added def Mathlib.Tactic.Tauto.tautoCore

added def Mathlib.Tactic.Tauto.tautology

Created test/Tauto.lean