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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Understanding.20tauto.2Elean.20.28mathlib3.29/near/303177080), makes `tauto` always-classical and eliminates `tauto!`.
* Does not yet add any symmetry-based logic or the fancy union-find datastructure from leanprover-community/mathlib#180.
* Adds a `andThenOnSubgoals` tactic combinator in `Mathlib.Tactic.Basic`.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -467,6 +467,7 @@ import Mathlib.Tactic.Spread
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SudoSetOption
 import Mathlib.Tactic.SwapVar
+import Mathlib.Tactic.Tauto
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.Trace
 import Mathlib.Tactic.TypeCheck

Mathlib/Algebra/Group/TypeTags.lean

@@ -130,10 +130,8 @@ instance [Finite α] : Finite (Additive α) :=
 instance [Finite α] : Finite (Multiplicative α) :=
   Finite.of_equiv α (by rfl)
 
--- Porting note: the mathlib3 proof is `by tauto`
 instance [h: Infinite α] : Infinite (Additive α) := h
 
--- Porting note: the mathlib3 proof is `by tauto`
 instance [h: Infinite α] : Infinite (Multiplicative α) := h
 
 instance [Nontrivial α] : Nontrivial (Additive α) :=

Mathlib/Data/Int/Units.lean

@@ -11,6 +11,7 @@ Authors: Jeremy Avigad
 import Mathlib.Data.Nat.Units
 import Mathlib.Data.Int.Basic
 import Mathlib.Algebra.Ring.Units
+import Mathlib.Tactic.Tauto
 
 /-!
 # Lemmas about units in `ℤ`.
@@ -54,15 +55,11 @@ theorem eq_one_or_neg_one_of_mul_eq_one {z w : ℤ} (h : z * w = 1) : z = 1 ∨
   isUnit_iff.mp (isUnit_of_mul_eq_one z w h)
 #align int.eq_one_or_neg_one_of_mul_eq_one Int.eq_one_or_neg_one_of_mul_eq_one
 
--- Porting note: this was proven in mathlib3 with `tauto` which hasn't been ported yet
 theorem eq_one_or_neg_one_of_mul_eq_one' {z w : ℤ} (h : z * w = 1) :
     z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1 := by
   have h' : w * z = 1 := mul_comm z w ▸ h
   rcases eq_one_or_neg_one_of_mul_eq_one h with (rfl | rfl) <;>
-      rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl) <;>
-    try cases h
-  · exact Or.inl ⟨rfl, rfl⟩
-  · exact Or.inr ⟨rfl, rfl⟩
+      rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl) <;> tauto
 #align int.eq_one_or_neg_one_of_mul_eq_one' Int.eq_one_or_neg_one_of_mul_eq_one'
 
 theorem mul_eq_one_iff_eq_one_or_neg_one {z w : ℤ} : z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1 :=

Mathlib/Data/Set/Basic.lean

@@ -12,6 +12,8 @@ import Mathlib.Order.SymmDiff
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.SolveByElim
+import Mathlib.Tactic.Tauto
+
 /-!
 # Basic properties of sets
 
@@ -253,9 +255,8 @@ theorem mem_of_mem_of_subset {x : α} {s t : Set α} (hx : x ∈ s) (h : s ⊆ t
   h hx
 #align set.mem_of_mem_of_subset Set.mem_of_mem_of_subset
 
--- Porting note: was `by tauto`
-theorem forall_in_swap {p : α → β → Prop} : (∀ a ∈ s, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ s, p a b :=
-  ⟨fun h b a ha => h a ha b, fun h a ha b => h b a ha⟩
+theorem forall_in_swap {p : α → β → Prop} : (∀ a ∈ s, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ s, p a b := by
+  tauto
 #align set.forall_in_swap Set.forall_in_swap
 
 /-! ### Lemmas about `mem` and `setOf` -/
@@ -2195,24 +2196,7 @@ theorem ite_inter_inter (t s₁ s₂ s₁' s₂' : Set α) :
     t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂' := by
   ext x
   simp only [Set.ite, Set.mem_inter_iff, Set.mem_diff, Set.mem_union]
-  -- Porting note: this use to be `itauto`:
-  exact
-  { mp := λ (h0 : (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ x ∉ t) =>
-      ⟨h0.elim (λ (h1 : (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) => Or.inl ⟨h1.left.left, h1.right⟩)
-        (λ (h1 : (x ∈ s₁' ∧ x ∈ s₂') ∧ x ∉ t) =>
-            Or.inr ⟨h1.left.left, λ (h2 : x ∈ t) => h1.right h2⟩),
-      h0.elim (λ (h3 : (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) => Or.inl ⟨h3.left.right, h3.right⟩)
-        (λ (h3 : (x ∈ s₁' ∧ x ∈ s₂') ∧ x ∉ t) =>
-            Or.inr ⟨h3.left.right, λ (h4 : x ∈ t) => h3.right h4⟩)⟩,
-    mpr := λ (h5 : (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ x ∉ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ x ∉ t)) =>
-      h5.right.elim
-        (λ (h6 : x ∈ s₂ ∧ x ∈ t) =>
-            h5.left.elim (λ (h7 : x ∈ s₁ ∧ x ∈ t) => Or.inl ⟨⟨h7.left, h6.left⟩, h7.right⟩)
-              (λ (h7 : x ∈ s₁' ∧ x ∉ t) => (h7.right h6.right).elim))
-        (λ (h6 : x ∈ s₂' ∧ x ∉ t) =>
-            h5.left.elim (λ (h8 : x ∈ s₁ ∧ x ∈ t) => (h6.right h8.right).elim)
-              (λ (h8 : x ∈ s₁' ∧ x ∉ t) =>
-                Or.inr ⟨⟨h8.left, h6.left⟩, λ (h9 : x ∈ t) => h8.right h9⟩)) }
+  tauto
 #align set.ite_inter_inter Set.ite_inter_inter
 
 theorem ite_inter (t s₁ s₂ s : Set α) : t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s := by

Mathlib/Data/Set/Prod.lean

@@ -577,12 +577,7 @@ theorem disjoint_diagonal_offDiag : Disjoint (diagonal α) s.offDiag :=
 theorem offDiag_inter : (s ∩ t).offDiag = s.offDiag ∩ t.offDiag :=
   ext fun x => by
     simp only [mem_offDiag, mem_inter_iff]
-    -- Porting note: was `tauto`
-    constructor
-    · rintro ⟨⟨h0, h1⟩, ⟨h2, h3⟩, h4⟩
-      refine ⟨⟨h0, h2, h4⟩, ⟨h1, h3, h4⟩⟩
-    · rintro ⟨⟨h0, h1, h2⟩, ⟨h3, h4, -⟩⟩
-      exact ⟨⟨h0, h3⟩, ⟨h1, h4⟩, h2⟩
+    tauto
 #align set.off_diag_inter Set.offDiag_inter
 
 variable {s t}

Mathlib/Lean/Meta.lean

@@ -20,9 +20,10 @@ The new hypothesis is given the same user name as the original,
 it attempts to avoid reordering hypotheses, and the original is cleared if possible.
 -/
 -- adapted from Lean.Meta.replaceLocalDeclCore
-def replace (g : MVarId) (hyp : FVarId) (typeNew proof : Expr) :
+def replace (g : MVarId) (hyp : FVarId) (proof : Expr) (typeNew : Option Expr := none) :
     MetaM AssertAfterResult :=
   g.withContext do
+    let typeNew := typeNew.getD (← inferType proof)
     let ldecl ← hyp.getDecl
     -- `typeNew` may contain variables that occur after `hyp`.
     -- Thus, we use the auxiliary function `findMaxFVar` to ensure `typeNew` is well-formed
@@ -52,6 +53,21 @@ def existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId := do
       pure sg2)
     mvar
 
+/-- Applies `intro` repeatedly until it fails. We use this instead of
+`Lean.MVarId.intros` to allowing unfolding.
+For example, if we want to do introductions for propositions like `¬p`,
+the `¬` needs to be unfolded into `→ False`, and `intros` does not do such unfolding. -/
+partial def intros! (mvarId : MVarId) : MetaM (Array FVarId × MVarId) :=
+  run #[] mvarId
+  where
+  /-- Implementation of `intros!`. -/
+  run (acc : Array FVarId) (g : MVarId) :=
+  try
+    let ⟨f, g⟩ ← mvarId.intro1
+    run (acc.push f) g
+  catch _ =>
+    pure (acc, g)
+
 end Lean.MVarId
 
 namespace Lean.Meta
@@ -77,6 +93,12 @@ end Lean.Meta
 
 namespace Lean.Elab.Tactic
 
+/-- Analogue of `liftMetaTactic` for tactics that return a single goal. -/
+-- I'd prefer to call that `liftMetaTactic1`,
+-- but that is taken in core by a function that lifts a `tac : MVarId → MetaM (Option MVarId)`.
+def liftMetaTactic' (tac : MVarId → MetaM MVarId) : TacticM Unit :=
+  liftMetaTactic fun g => do pure [← tac g]
+
 /-- Analogue of `liftMetaTactic` for tactics that do not return any goals. -/
 def liftMetaFinishingTactic (tac : MVarId → MetaM Unit) : TacticM Unit :=
   liftMetaTactic fun g => do tac g; pure []

Mathlib/Mathport/Syntax.lean

@@ -66,6 +66,7 @@ import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SwapVar
+import Mathlib.Tactic.Tauto
 import Mathlib.Tactic.Trace
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.Use
@@ -204,9 +205,6 @@ syntax termList := " [" term,* "]"
 /- S -/ syntax (name := suggest) "suggest" (config)? (ppSpace num)?
   (simpArgs)? (" using " (colGt binderIdent)+)? : tactic
 
-/- B -/ syntax (name := tauto) "tauto" (config)? : tactic
-/- B -/ syntax (name := tauto!) "tauto!" (config)? : tactic
-
 /- M -/ syntax (name := truncCases) "trunc_cases " term (" with " (colGt binderIdent)+)? : tactic
 
 /- E -/ syntax (name := applyNormed) "apply_normed " term : tactic

Mathlib/Tactic/Core.lean

@@ -119,6 +119,24 @@ def allGoals (tac : TacticM Unit) : TacticM Unit := do
           throw ex
   setGoals mvarIdsNew.toList
 
+/-- Simulates the `<;>` tactic combinator. First runs `tac1` and then runs
+    `tac2` on all newly-generated subgoals.
+-/
+def andThenOnSubgoals (tac1 : TacticM Unit)  (tac2 : TacticM Unit) : TacticM Unit :=
+  focus do tac1; allGoals tac2
+
+variable [Monad m] [MonadExceptOf Exception m]
+
+/-- Repeats a tactic at most `n` times, stopping sooner if the
+tactic fails. Always succeeds. -/
+def iterateAtMost : Nat → m Unit → m Unit
+| 0, _ => pure ()
+| n + 1, tac => try tac; iterateAtMost n tac catch _ => pure ()
+
+/-- Repeats a tactic until it fails. Always succeeds. -/
+partial def iterateUntilFailure (tac : m Unit) : m Unit :=
+  try tac; iterateUntilFailure tac catch _ => pure ()
+
 end Lean.Elab.Tactic
 
 namespace Mathlib

Mathlib/Tactic/Relation/Symm.lean

@@ -64,7 +64,7 @@ elab "symm" loc:((Parser.Tactic.location)?) : tactic =>
     onRel (← h.getType) fun g e ↦ do
       let (xs, _, targetTy) ← withReducible <| forallMetaTelescopeReducing (← inferType e)
       let .true ← isDefEq xs.back (.fvar h) | failure
-      pure (← g.replace h (← instantiateMVars targetTy) (mkAppN e xs)).mvarId
+      pure (← g.replace h (mkAppN e xs) (← instantiateMVars targetTy)).mvarId
   let atTarget := withMainContext do
     onRel (← getMainTarget) fun g e ↦ do
       let (xs, _, targetTy) ← withReducible <| forallMetaTelescopeReducing (← inferType e)

Mathlib/Tactic/SplitIfs.lean

@@ -15,13 +15,6 @@ namespace Mathlib.Tactic
 
 open Lean Elab.Tactic Parser.Tactic Lean.Meta
 
-/-- Simulates the `<;>` tactic combinator.
--/
-private def tac_and_then : TacticM Unit → TacticM Unit → TacticM Unit :=
-fun tac1 tac2 ↦ focus do
-  tac1
-  allGoals tac2
-
 /-- A position where a split may apply.
 -/
 private inductive SplitPosition
@@ -83,7 +76,7 @@ private def splitIf1 (cond: Expr) (hName : Name) (loc : Location) : TacticM Unit
   let splitCases := liftMetaTactic fun mvarId ↦ do
     let (s1, s2) ← mvarId.byCases cond hName
     pure [s1.mvarId, s2.mvarId]
-  tac_and_then splitCases (reduceIfsAt loc)
+  andThenOnSubgoals splitCases (reduceIfsAt loc)
 
 /-- Pops off the front of the list of names, or generates a fresh name if the
 list is empty.
@@ -120,10 +113,11 @@ private partial def splitIfsCore
   if done.contains cond then return ()
   let no_split ← valueKnown cond
   if no_split then
-    tac_and_then (reduceIfsAt loc) (splitIfsCore loc hNames (cond::done) <|> pure ())
+    andThenOnSubgoals (reduceIfsAt loc) (splitIfsCore loc hNames (cond::done) <|> pure ())
   else do
     let hName ← getNextName hNames
-    tac_and_then (splitIf1 cond hName loc) ((splitIfsCore loc hNames (cond::done)) <|> pure ())
+    andThenOnSubgoals (splitIf1 cond hName loc) ((splitIfsCore loc hNames (cond::done)) <|>
+      pure ())
 
 /-- Splits all if-then-else-expressions into multiple goals.
 Given a goal of the form `g (if p then x else y)`, `split_ifs` will produce