From 4a54f26203f47428c389297a2448d6348bb97484 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 24 Apr 2024 13:37:10 +1000
Subject: [PATCH] feat: propose removing classical! (#752)

* feat: propose removing classical!

* update test

* deprecation
---
 Std/Tactic/Classical.lean | 34 +++++++---------------------------
 test/classical.lean       | 12 ++----------
 2 files changed, 9 insertions(+), 37 deletions(-)

diff --git a/Std/Tactic/Classical.lean b/Std/Tactic/Classical.lean
index cf05a4d59f..48417290c1 100644
--- a/Std/Tactic/Classical.lean
+++ b/Std/Tactic/Classical.lean
@@ -5,25 +5,11 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.ElabRules
 
-/-! # `classical` and `classical!` tactics -/
+/-! # `classical` tactic -/
 
 namespace Std.Tactic
 open Lean Meta Elab.Tactic
 
-/--
-`classical!` adds a proof of `Classical.propDecidable` as a local variable, which makes it
-available for instance search and effectively makes all propositions decidable.
-```
-noncomputable def foo : Bool := by
-  classical!
-  have := ∀ p, decide p -- uses the classical instance
-  exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable
-```
-Consider using `classical` instead if you want to use the decidable instance when available.
--/
-macro (name := classical!) "classical!" : tactic =>
-  `(tactic| have em := Classical.propDecidable)
-
 /--
 `classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
 local instance.
@@ -37,21 +23,15 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t :
   finally
     modifyEnv Meta.instanceExtension.popScope
 
+/-- `classical!` has been removed; use `classical` instead -/
+-- Deprecated 2024-04-19
+elab "classical!" : tactic => do
+  throwError "`classical!` has been removed; use `classical` instead"
+
 /--
 `classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
-local instance. It differs from `classical!` in that `classical!` uses a local variable,
-which has high priority:
-```
-noncomputable def foo : Bool := by
-  classical!
-  have := ∀ p, decide p -- uses the classical instance
-  exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable
+local instance.
 
-def bar : Bool := by
-  classical
-  have := ∀ p, decide p -- uses the classical instance
-  exact decide (0 < 1) -- uses the decidable instance
-```
 Note that (unlike lean 3) `classical` is a scoping tactic - it adds the instance only within the
 scope of the tactic.
 -/
diff --git a/test/classical.lean b/test/classical.lean
index b65762ae7b..6af8ca3bb8 100644
--- a/test/classical.lean
+++ b/test/classical.lean
@@ -1,20 +1,12 @@
 import Std.Tactic.Classical
 import Std.Tactic.PermuteGoals
 
-noncomputable example : Bool := by
-  fail_if_success have := ∀ p, decide p -- no classical in scope
-  classical!
-  have := ∀ p, decide p -- uses the classical instance
-  -- uses the classical instance even though `0 < 1` is decidable
-  guard_expr decide (0 < 1) = @decide (0 < 1) (‹(a : Prop) → Decidable a› _)
-  exact decide (0 < 1)
-
 example : Bool := by
   fail_if_success have := ∀ p, decide p -- no classical in scope
   classical
   have := ∀ p, decide p -- uses the classical instance
   guard_expr decide (0 < 1) = @decide (0 < 1) (Nat.decLt 0 1)
-  exact decide (0 < 1) -- uses the decidable instance
+  exact decide (0 < 1) -- will use the decidable instance
 
 -- double check no leakage
 example : Bool := by
@@ -28,4 +20,4 @@ example : Bool := by
     classical
     have := ∀ p, decide p -- uses the classical instance
   fail_if_success have := ∀ p, decide p -- no classical in scope again
-  exact decide (0 < 1) -- uses the decidable instance
+  exact decide (0 < 1) -- will use the decidable instance