From dec12626976a9fe271fcf5fcf3bbb548f978aaa2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 16 Oct 2024 14:35:41 +1100
Subject: [PATCH] chore: upstream `classical` tactic (#5730)

---
 src/Init/Tactics.lean               |  9 ++++++++
 src/Lean/Elab/Tactic.lean           |  1 +
 src/Lean/Elab/Tactic/Classical.lean | 34 +++++++++++++++++++++++++++++
 tests/lean/run/classical.lean       | 21 ++++++++++++++++++
 4 files changed, 65 insertions(+)
 create mode 100644 src/Lean/Elab/Tactic/Classical.lean
 create mode 100644 tests/lean/run/classical.lean

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index fe5e05253b..dd2874c965 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -910,6 +910,15 @@ macro_rules | `(tactic| trivial) => `(tactic| simp)
 -/
 syntax "trivial" : tactic
 
+/--
+`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
+local instance.
+
+Note that `classical` is a scoping tactic: it adds the instance only within the
+scope of the tactic.
+-/
+syntax (name := classical) "classical" ppDedent(tacticSeq) : tactic
+
 /--
 The `split` tactic is useful for breaking nested if-then-else and `match` expressions into separate cases.
 For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals.
diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index b8faf9a174..c3b49d277c 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -43,3 +43,4 @@ import Lean.Elab.Tactic.Rewrites
 import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
+import Lean.Elab.Tactic.Classical
diff --git a/src/Lean/Elab/Tactic/Classical.lean b/src/Lean/Elab/Tactic/Classical.lean
new file mode 100644
index 0000000000..787310edc0
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Classical.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Kim Morrison
+-/
+prelude
+import Lean.Elab.Tactic.Basic
+
+/-! # `classical` tactic -/
+
+namespace Lean.Elab.Tactic
+open Lean Meta Elab.Tactic
+
+/--
+`classical t` runs `t` in a scope where `Classical.propDecidable` is a low priority
+local instance.
+-/
+def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) :
+    m α := do
+  modifyEnv Meta.instanceExtension.pushScope
+  Meta.addInstance ``Classical.propDecidable .local 10
+  try
+    t
+  finally
+    modifyEnv Meta.instanceExtension.popScope
+
+@[builtin_tactic Lean.Parser.Tactic.classical]
+def evalClassical : Tactic := fun stx => do
+  match stx with
+  | `(tactic| classical $tacs:tacticSeq) =>
+     classical <| Elab.Tactic.evalTactic tacs
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic
diff --git a/tests/lean/run/classical.lean b/tests/lean/run/classical.lean
new file mode 100644
index 0000000000..4e56bf3e13
--- /dev/null
+++ b/tests/lean/run/classical.lean
@@ -0,0 +1,21 @@
+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) -- will use the decidable instance
+
+-- double check no leakage
+example : Bool := by
+  fail_if_success have := ∀ p, decide p -- no classical in scope
+  exact decide (0 < 1) -- uses the decidable instance
+
+-- check that classical respects tactic blocks
+example : Bool := by
+  fail_if_success have := ∀ p, decide p -- no classical in scope
+  ( -- start a scope
+    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) -- will use the decidable instance