Skip to content

Commit

Permalink
feat: propose removing classical! (leanprover-community#752)
Browse files Browse the repository at this point in the history
* feat: propose removing classical!

* update test

* deprecation
  • Loading branch information
kim-em authored Apr 24, 2024
1 parent 0ad0ebc commit 4a54f26
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 37 deletions.
34 changes: 7 additions & 27 deletions Std/Tactic/Classical.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
-/
Expand Down
12 changes: 2 additions & 10 deletions test/classical.lean
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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

0 comments on commit 4a54f26

Please sign in to comment.