chore: remove decide! tactic

This PR removes the `decide!` tactic in favor of `decide +kernel` (breaking change).

src/Init/Tactics.lean

@@ -1155,7 +1155,7 @@ Configuration for the `decide` tactic family.
 structure DecideConfig where
   /-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
   This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
-  however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/
+  however kernel reduction ignores transparency settings. -/
   kernel : Bool := false
   /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
   admitting the result via the axiom `Lean.ofReduceBool`.  This can be significantly more efficient,
@@ -1165,7 +1165,9 @@ structure DecideConfig where
   native : Bool := false
   /-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/
   zetaReduce : Bool := true
-  /-- If true (default: false), then when preprocessing reverts free variables. -/
+  /-- If true (default: false), then when preprocessing, removes irrelevant variables and reverts the local context.
+  A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
+  or if it is a proposition that refers to a relevant variable. -/
   revert : Bool := false
 
 /--
@@ -1240,17 +1242,6 @@ example : 1 + 1 = 2 := by rfl
 -/
 syntax (name := decide) "decide" optConfig : tactic
 
-/--
-`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
-It has the following properties:
-- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
-- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
-  and once during kernel type checking), the `decide!` tactic reduces it exactly once.
-
-The `decide!` syntax is short for `decide +kernel`.
--/
-syntax (name := decideBang) "decide!" optConfig : tactic
-
 /--
 `native_decide` is a synonym for `decide +native`.
 It will attempt to prove a goal of type `p` by synthesizing an instance

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -542,11 +542,6 @@ declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
   let cfg ← elabDecideConfig stx[1]
   evalDecideCore `decide cfg
 
-@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  let cfg := { cfg with kernel := true }
-  evalDecideCore `decide! cfg
-
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
   let cfg ← elabDecideConfig stx[1]
   let cfg := { cfg with native := true }

tests/lean/run/decideBang.lean → tests/lean/run/decideTacticKernel.lean

@@ -1,12 +1,12 @@
 /-!
-# `decide!` tests
+# `decide +kernel` tests
 -/
 
 /-!
 Very basic tests
 -/
 theorem foo1 : True := by decide
-theorem foo2 : True := by decide!
+theorem foo2 : True := by decide +kernel
 
 /-!
 Tests of the error message when goal is false.
@@ -21,12 +21,12 @@ is false
 theorem foo3 : False := by decide
 
 /--
-error: tactic 'decide!' proved that the proposition
+error: tactic 'decide' proved that the proposition
   False
 is false
 -/
 #guard_msgs in
-theorem foo4 : False := by decide!
+theorem foo4 : False := by decide +kernel
 
 /-!
 The kernel sees through irreducible definitions
@@ -47,26 +47,26 @@ After unfolding the instances 'instDecidableEqNat' and 'Nat.decEq', reduction go
 -/
 #guard_msgs in theorem gcd_eq1 : irred 3 = 3 := by decide
 
-theorem gcd_eq2 : irred 3 = 3 := by decide!
+theorem gcd_eq2 : irred 3 = 3 := by decide +kernel
 
 
 /-!
-The proofs from `decide!` are cached.
+The proofs from `decide +kernel` are cached.
 -/
 
-theorem thm1 : ∀ x < 100, x * x ≤ 10000 := by decide!
+theorem thm1 : ∀ x < 100, x * x ≤ 10000 := by decide +kernel
 
-theorem thm1' : ∀ x < 100, x * x ≤ 10000 := by decide!
+theorem thm1' : ∀ x < 100, x * x ≤ 10000 := by decide +kernel
 
 -- (Note: when run within VS Code, these tests fail since the auxLemmas have a `lean.run` prefix.)
 /--
 info: theorem thm1 : ∀ (x : Nat), x < 100 → x * x ≤ 10000 :=
-decideBang._auxLemma.3
+decideTacticKernel._auxLemma.3
 -/
 #guard_msgs in #print thm1
 /--
 info: theorem thm1' : ∀ (x : Nat), x < 100 → x * x ≤ 10000 :=
-decideBang._auxLemma.3
+decideTacticKernel._auxLemma.3
 -/
 #guard_msgs in #print thm1'
 
@@ -81,9 +81,9 @@ error: expected type must not contain free variables
 Use the '+revert' option to automatically cleanup and revert free variables.
 -/
 #guard_msgs in
-example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide!
+example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide +kernel
 
-example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide! +revert
+example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide +kernel +revert
 
 
 /--
@@ -93,4 +93,4 @@ Can handle universe levels.
 instance (p : PUnit.{u} → Prop) [Decidable (p PUnit.unit)] : Decidable (∀ x : PUnit.{u}, p x) :=
   decidable_of_iff (p PUnit.unit) (by constructor; rintro _ ⟨⟩; assumption; intro h; apply h)
 
-example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide!
+example : ∀ (x : PUnit.{u}), x = PUnit.unit := by decide +kernel