chore: upstream classical tactic

Std.lean

@@ -102,6 +102,7 @@ import Std.Tactic.Alias
 import Std.Tactic.Basic
 import Std.Tactic.ByCases
 import Std.Tactic.Case
+import Std.Tactic.Classical
 import Std.Tactic.CoeExt
 import Std.Tactic.Congr
 import Std.Tactic.Exact
@@ -122,6 +123,7 @@ import Std.Tactic.NoMatch
 import Std.Tactic.NormCast.Ext
 import Std.Tactic.NormCast.Lemmas
 import Std.Tactic.OpenPrivate
+import Std.Tactic.PermuteGoals
 import Std.Tactic.PrintDependents
 import Std.Tactic.RCases
 import Std.Tactic.Replace

Std/Tactic/Classical.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Elab.ElabRules
+
+/-! # `classical` and `classical!` tactics -/
+
+namespace Mathlib.Tactic
+open Lean Meta
+
+/--
+`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 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
+
+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.
+-/
+-- FIXME: using ppDedent looks good in the common case, but produces the incorrect result when
+-- the `classical` does not scope over the rest of the block.
+elab "classical" tacs:ppDedent(tacticSeq) : tactic => do
+  modifyEnv Meta.instanceExtension.pushScope
+  Meta.addInstance ``Classical.propDecidable .local 10
+  try Elab.Tactic.evalTactic tacs
+  finally modifyEnv Meta.instanceExtension.popScope

Std/Tactic/PermuteGoals.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2022 Arthur Paulino. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur Paulino, Mario Carneiro
+-/
+
+import Lean
+import Std.Data.List.Basic
+
+/-!
+# The `on_goal`, `pick_goal`, and `swap` tactics.
+
+`pick_goal n` moves the `n`-th goal to the front. If `n` is negative this is counted from the back.
+
+`on_goal n => tacSeq` focuses on the `n`-th goal and runs a tactic block `tacSeq`.
+If `tacSeq` does not close the goal any resulting subgoals are inserted back into the list of goals.
+If `n` is negative this is counted from the back.
+
+`swap` is a shortcut for `pick_goal 2`, which interchanges the 1st and 2nd goals.
+-/
+
+namespace Mathlib.Tactic
+
+open Lean Elab.Tactic
+
+/--
+If the current goals are `g₁ ⋯ gᵢ ⋯ gₙ`, `splitGoalsAndGetNth i` returns
+`(gᵢ, [g₁, ⋯, gᵢ₋₁], [gᵢ₊₁, ⋯, gₙ])`.
+
+If `reverse` is passed as `true`, the `i`-th goal is picked by counting backwards.
+For instance, `splitGoalsAndGetNth 1 true` puts the last goal in the first component
+of the returned term.
+-/
+def splitGoalsAndGetNth (nth : Nat) (reverse : Bool := false) :
+    TacticM (MVarId × List MVarId × List MVarId) := do
+  if nth = 0 then throwError "goals are 1-indexed"
+  let goals ← getGoals
+  let nGoals := goals.length
+  if nth > nGoals then throwError "goal index out of bounds"
+  let n := if ¬reverse then nth - 1 else nGoals - nth
+  let (gl, g :: gr) := goals.splitAt n | throwNoGoalsToBeSolved
+  pure (g, gl, gr)
+
+/--
+`pick_goal n` will move the `n`-th goal to the front.
+
+`pick_goal -n` will move the `n`-th goal (counting from the bottom) to the front.
+
+See also `Tactic.rotate_goals`, which moves goals from the front to the back and vice-versa.
+-/
+elab "pick_goal " reverse:"-"? n:num : tactic => do
+  let (g, gl, gr) ← splitGoalsAndGetNth n.1.toNat !reverse.isNone
+  setGoals $ g :: (gl ++ gr)
+
+/-- `swap` is a shortcut for `pick_goal 2`, which interchanges the 1st and 2nd goals. -/
+macro "swap" : tactic => `(tactic| pick_goal 2)
+
+/--
+`on_goal n => tacSeq` creates a block scope for the `n`-th goal and tries the sequence
+of tactics `tacSeq` on it.
+
+`on_goal -n => tacSeq` does the same, but the `n`-th goal is chosen by counting from the
+bottom.
+
+The goal is not required to be solved and any resulting subgoals are inserted back into the
+list of goals, replacing the chosen goal.
+-/
+elab "on_goal " reverse:"-"? n:num " => " seq:tacticSeq : tactic => do
+  let (g, gl, gr) ← splitGoalsAndGetNth n.1.toNat !reverse.isNone
+  setGoals [g]
+  evalTactic seq
+  setGoals $ gl ++ (← getUnsolvedGoals) ++ gr

test/classical.lean

@@ -0,0 +1,32 @@
+import Std.Tactic.Classical
+import Std.Tactic.PermuteGoals
+import Std.Tactic.GuardExpr
+
+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
+
+-- 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
+  on_goal 1 =>
+    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

test/on_goal.lean

@@ -0,0 +1,44 @@
+import Std.Tactic.GuardExpr
+import Std.Tactic.PermuteGoals
+
+example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by
+  intros
+  constructor
+  on_goal 2 =>
+    guard_target = q ∧ r
+    constructor
+    assumption
+    -- Note that we have not closed all the subgoals here.
+  guard_target = p
+  assumption
+  guard_target = r
+  assumption
+
+example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by
+  intros a b c
+  constructor
+  fail_if_success on_goal -3 => unreachable!
+  fail_if_success on_goal -1 => exact a
+  fail_if_success on_goal 0 => unreachable!
+  fail_if_success on_goal 2 => exact a
+  fail_if_success on_goal 3 => unreachable!
+  on_goal 1 => exact a
+  constructor
+  swap
+  exact c
+  exact b
+
+example (p q : Prop) : p → q → p ∧ q := by
+  intros a b
+  constructor
+  fail_if_success pick_goal -3
+  fail_if_success pick_goal 0
+  fail_if_success pick_goal 3
+  pick_goal -1
+  exact b
+  exact a
+
+example (p : Prop) : p → p := by
+  intros
+  fail_if_success swap -- can't swap with a single goal
+  assumption