diff --git a/Mathlib.lean b/Mathlib.lean index b11f414cc8b77..4594fae078a40 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean index 380ee498f9e52..61828e21b1aaa 100644 --- a/Mathlib/Algebra/Group/TypeTags.lean +++ b/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 α) := diff --git a/Mathlib/Data/Int/Units.lean b/Mathlib/Data/Int/Units.lean index 53122c8da9098..57cb8a509bc63 100644 --- a/Mathlib/Data/Int/Units.lean +++ b/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 := diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 0c3ff8f3729c9..71d39da4686ed 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/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 diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean index 9b41b81985a5c..696ffb7f39733 100644 --- a/Mathlib/Data/Set/Prod.lean +++ b/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} diff --git a/Mathlib/Lean/Meta.lean b/Mathlib/Lean/Meta.lean index e9025e1cbfa8d..ed83c27e54288 100644 --- a/Mathlib/Lean/Meta.lean +++ b/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 [] diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean index 3d9f5c2aa2890..4987961bdbf1c 100644 --- a/Mathlib/Mathport/Syntax.lean +++ b/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 diff --git a/Mathlib/Tactic/Core.lean b/Mathlib/Tactic/Core.lean index 6a55fa171460f..17866714d4752 100644 --- a/Mathlib/Tactic/Core.lean +++ b/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 diff --git a/Mathlib/Tactic/Relation/Symm.lean b/Mathlib/Tactic/Relation/Symm.lean index 3e29bb4e549ef..5c4728a8aadcd 100644 --- a/Mathlib/Tactic/Relation/Symm.lean +++ b/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) diff --git a/Mathlib/Tactic/SplitIfs.lean b/Mathlib/Tactic/SplitIfs.lean index 8d3246c8d0ab3..ac3bb4288613f 100644 --- a/Mathlib/Tactic/SplitIfs.lean +++ b/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 diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean new file mode 100644 index 0000000000000..9a27b2ac6e36a --- /dev/null +++ b/Mathlib/Tactic/Tauto.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2018 Simon Hudon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Simon Hudon, David Renshaw +-/ + +import Lean +import Mathlib.Init.Logic +import Mathlib.Init.Propext +import Mathlib.Logic.Basic +import Mathlib.Tactic.CasesM +import Mathlib.Tactic.Classical +import Mathlib.Tactic.Core +import Mathlib.Tactic.SolveByElim +import Qq.Match + +/-! +The `tauto` tactic. +-/ + +namespace Mathlib.Tactic.Tauto + +open Lean Elab.Tactic Parser.Tactic Lean.Meta +open Qq + +initialize registerTraceClass `tauto + +/-- Tries to apply de-Morgan-like rules on a hypothesis. -/ +def distribNotAt (h : LocalDecl) (g : MVarId) : MetaM MVarId := do + let e : Q(Prop) ← (do guard (← inferType h.type).isProp; pure h.type) + let replace (p : Expr) := g.replace h.fvarId p + let result ← match e with + | ~q(¬ ($a : Prop) = $b) => do + let h' : Q(¬$a = $b) := h.toExpr + replace q(mt Iff.to_eq $h') + | ~q(($a : Prop) = $b) => do + let h' : Q($a = $b) := h.toExpr + replace q(Eq.to_iff $h') + | ~q(¬ (($a : Prop) ∧ $b)) => do + let h' : Q(¬($a ∧ $b)) := h.toExpr + let _inst ← synthInstanceQ (q(Decidable $b) : Q(Type)) + replace q(Decidable.not_and'.mp $h') + | ~q(¬ (($a : Prop) ∨ $b)) => do + let h' : Q(¬($a ∨ $b)) := h.toExpr + replace q(not_or.mp $h') + | ~q(¬ (($a : Prop) ≠ $b)) => do + let h' : Q(¬($a ≠ $b)) := h.toExpr + let _inst ← synthInstanceQ (q(Decidable ($a = $b)) : Q(Type)) + replace q(Decidable.of_not_not $h') + | ~q(¬¬ ($a : Prop)) => do + let h' : Q(¬¬$a) := h.toExpr + let _inst ← synthInstanceQ (q(Decidable $a) : Q(Type)) + replace q(Decidable.of_not_not $h') + | ~q(¬ ((($a : Prop)) → $b)) => do + let h' : Q(¬($a → $b)) := h.toExpr + let _inst ← synthInstanceQ (q(Decidable $a) : Q(Type)) + replace q(Decidable.not_imp.mp $h') + | ~q(¬ (($a : Prop) ↔ $b)) => do + let h' : Q(¬($a ↔ $b)) := h.toExpr + let _inst ← synthInstanceQ (q(Decidable $b) : Q(Type)) + replace q(Decidable.not_iff.mp $h') + | ~q(($a : Prop) ↔ $b) => do + let h' : Q($a ↔ $b) := h.toExpr + let _inst ← synthInstanceQ (q(Decidable $b) : Q(Type)) + replace q(Decidable.iff_iff_and_or_not_and_not.mp $h') + | ~q((((($a : Prop)) → False) : Prop)) => + throwError "distribNot found nothing to work on with negation" + | ~q((((($a : Prop)) → $b) : Prop)) => do + let h' : Q($a → $b) := h.toExpr + let _inst ← synthInstanceQ (q(Decidable $a) : Q(Type)) + replace q(Decidable.not_or_of_imp $h') + | _ => throwError "distribNot found nothing to work on" + pure result.mvarId + +/-- +Tries to apply de-Morgan-like rules on all hypotheses. +Always succeeds, regardless of whether any progress was actually made. +-/ +def distribNot : TacticM Unit := withMainContext do + for h in ← getLCtx do + iterateAtMost 3 $ liftMetaTactic' (distribNotAt h) + +/-- Config for the `tauto` tactic. Currently empty. TODO: add `closer` option. -/ +structure Config + +/-- Function elaborating `Config`. -/ +declare_config_elab elabConfig Config + +/-- Matches propositions where we want to apply the `constructor` tactic +in the core loop of `tauto`. -/ +def coreConstructorMatcher (e : Q(Prop)) : MetaM Bool := match e with + | ~q(_ ∧ _) => pure true + | ~q(_ ↔ _) => pure true + | ~q(True) => pure true + | _ => pure false + +/-- Matches propositions where we want to apply the `cases` tactic +in the core loop of `tauto`. -/ +def casesMatcher (e : Q(Prop)) : MetaM Bool := match e with + | ~q(_ ∧ _) => pure true + | ~q(_ ∨ _) => pure true + | ~q(Exists _) => pure true + | ~q(False) => pure true + | _ => pure false + +@[inherit_doc] +local infixl: 50 " <;> " => andThenOnSubgoals + +/-- 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. +-/ +def tautoCore : TacticM Unit := do + _ ← tryTactic (evalTactic (← `(tactic| contradiction))) + _ ← tryTactic (evalTactic (← `(tactic| assumption))) + iterateUntilFailure do + let gs ← getUnsolvedGoals + allGoals ( + liftMetaTactic (fun m => do pure [(← m.intros!).2]) <;> + distribNot <;> + liftMetaTactic (casesMatching · casesMatcher) <;> + (do _ ← tryTactic (evalTactic (← `(tactic| contradiction)))) <;> + (do _ ← tryTactic (evalTactic (←`(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;> + liftMetaTactic (fun m => do pure [(← m.intros!).2]) <;> + liftMetaTactic (constructorMatching · coreConstructorMatcher) <;> + do _ ← tryTactic (evalTactic (← `(tactic| assumption)))) + let gs' ← getUnsolvedGoals + if gs == gs' then failure -- no progress + pure () + +/-- Matches propositions where we want to apply the `constructor` tactic in the +finishing stage of `tauto`. -/ +def finishingConstructorMatcher (e : Q(Prop)) : MetaM Bool := match e with + | ~q(_ ∧ _) => pure true + | ~q(_ ↔ _) => pure true + | ~q(Exists _) => pure true + | ~q(True) => pure true + | _ => pure false + +/-- Implementation of the `tauto` tactic. -/ +def tautology : TacticM Unit := focus do + evalTactic (← `(tactic| classical!)) + tautoCore + allGoals (iterateUntilFailure + (evalTactic (← `(tactic| rfl)) <|> + evalTactic (← `(tactic| solve_by_elim)) <|> + liftMetaTactic (constructorMatching · finishingConstructorMatcher))) + done + +/-- +`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. +-/ +syntax (name := tauto) "tauto" (config)? : tactic + +elab_rules : tactic | `(tactic| tauto $[$cfg:config]?) => do + let _cfg ← elabConfig (mkOptionalNode cfg) + tautology diff --git a/test/Tauto.lean b/test/Tauto.lean new file mode 100644 index 0000000000000..f2ce5ae193ffd --- /dev/null +++ b/test/Tauto.lean @@ -0,0 +1,136 @@ +/- +Copyright (c) 2018 Simon Hudon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Simon Hudon, David Renshaw +-/ +import Mathlib.Tactic.Tauto + +section tauto₀ +variable (p q r : Prop) +variable (h : p ∧ q ∨ p ∧ r) + +example : p ∧ p := +by tauto + +end tauto₀ + +section tauto₁ +variable (α : Type) +variable (p q r : α → Prop) +variable (h : (∃ x, p x ∧ q x) ∨ (∃ x, p x ∧ r x)) + +example : ∃ x, p x := +by tauto + +end tauto₁ + +section tauto₂ +variable (α : Type) +variable (x : α) +variable (p q r : α → Prop) +variable (h₀ : (∀ x, p x → q x → r x) ∨ r x) +variable (h₁ : p x) +variable (h₂ : q x) + +example : ∃ x, r x := +by tauto + +end tauto₂ + +section tauto₃ + +example (p : Prop) : p ∧ True ↔ p := by tauto +example (p : Prop) : p ∨ False ↔ p := by tauto + +example (p q : Prop) (h : p ≠ q) : ¬ p ↔ q := by tauto +example (p q : Prop) (h : ¬ p = q) : ¬ p ↔ q := by tauto + +example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := + by tauto +example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := + by tauto + +example (p q : Prop) (h : ¬ (p ↔ q)) (h' : ¬ p) : q := by tauto +example (p q : Prop) (h : ¬ (p ↔ q)) (h' : p) : ¬ q := by tauto +example (p q : Prop) (h : ¬ (p ↔ q)) (h' : q) : ¬ p := by tauto +example (p q : Prop) (h : ¬ (p ↔ q)) (h' : ¬ q) : p := by tauto + +example (p q : Prop) (h : ¬ (p ↔ q)) (h' : ¬ q) (h'' : ¬ p) : False := +by tauto + +example (p q r : Prop) (h : p ↔ q) (h' : r ↔ q) (h'' : ¬ r) : ¬ p := +by tauto + +example (p q r : Prop) (h : p ↔ q) (h' : r ↔ q) : p ↔ r := +by tauto + +example (p q r : Prop) (h : ¬ p = q) (h' : r = q) : p ↔ ¬ r := by tauto + +example (p : Prop) : p → ¬ (p → ¬ p) := by tauto +example (p : Prop) (em : p ∨ ¬ p) : ¬ (p ↔ ¬ p) := by tauto + +example (P : Nat → Prop) (n : Nat) : P n → n = 7 ∨ n = 0 ∨ ¬ (n = 7 ∨ n = 0) ∧ P n := +by tauto + +section modulo_symmetry +variable {p q r : Prop} {α : Type} {x y : α} +variable (h : x = y) +variable (h'' : (p ∧ q ↔ q ∨ r) ↔ (r ∧ p ↔ r ∨ q)) + +-- Currently this hits a "failed to show termination error" +-- because it erroneously used a recursive hypothesis. +-- See https://github.com/leanprover-community/mathlib4/issues/1061 and +-- https://github.com/leanprover/lean4/issues/1963 +-- example (h' : ¬ y = x) : p ∧ q := by tauto + +/- +example (h' : p ∧ ¬ y = x) : p ∧ q := by tauto +example : y = x := by tauto +example (h' : ¬ x = y) : p ∧ q := by tauto +example : x = y := by tauto +-/ +end modulo_symmetry + +section pair_eq_pair_iff + +variable (α : Type) +variable (x y z w : α) + +-- This example is taken from pair_eq_pair_iff in Data.Set.Basic. +-- It currently doesn't work because `tauto` does not apply `symm`. +--example : ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ +-- (z = x ∨ z = y) ∧ (w = x ∨ w = y) → x = z ∧ y = w ∨ x = w ∧ y = z := +--by tauto + +end pair_eq_pair_iff + +end tauto₃ + +/- +section closer + +example {α : Type*} {β : Type*} (a : α) + {s_1 : set α} : + (∃ (a_1 : α), a_1 = a ∨ a_1 ∈ s_1) := +begin + tauto {closer := `[simp]} +end + +variables {p q r : Prop} {α : Type} {x y z w : α} +variables (h : x = y) (h₁ : y = z) (h₂ : z = w) +variables (h'' : (p ∧ q ↔ q ∨ r) ↔ (r ∧ p ↔ r ∨ q)) +include h h₁ h₂ h'' + +example : (((r ∧ p ↔ r ∨ q) ∧ (q ∨ r)) → (p ∧ (x = w) ∧ (¬ x = w → p ∧ q ∧ r))) := +begin + tauto {closer := `[cc]} +end + +end closer +-/ + +/- Zulip discussion: +https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/tauto!.20fails.20on.20ne +-/ +example {x y : Nat} (h : ¬x ≠ y) : x = y := +by tauto