chore: upstream on_goal / pick_goal / swap (#241)

Std.lean

@@ -137,6 +137,7 @@ import Std.Tactic.NormCast
 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.PrintPrefix
 import Std.Tactic.RCases

Std/Tactic/PermuteGoals.lean

@@ -0,0 +1,70 @@
+/-
+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 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 Std.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/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