feat: repeat tactical for grind interactive mode (#10748)

This PR implements the `repeat` tactical for the `grind` interactive
mode.

src/Init/Grind/Interactive.lean

@@ -158,5 +158,16 @@ macro "admit" : grind => `(grind| sorry)
 /-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
 syntax (name := fail) "fail" (ppSpace str)? : grind
 
+/--
+`repeat tac` repeatedly applies `tac` so long as it succeeds.
+The tactic `tac` may be a tactic sequence, and if `tac` fails at any point in its execution,
+`repeat` will revert any partial changes that `tac` made to the tactic state.
+The tactic `tac` should eventually fail, otherwise `repeat tac` will run indefinitely.
+-/
+syntax "repeat " grindSeq : grind
+
+macro_rules
+  | `(grind| repeat $seq) => `(grind| first | ($seq); repeat $seq | skip)
+
 end Grind
 end Lean.Parser.Tactic

tests/lean/run/grind_interactive.lean

@@ -376,6 +376,19 @@ example (as bs cs : Array α) (v₁ v₂ : α)
     instantiate = Array.getElem_set
     instantiate ← Array.getElem_set
 
+example (as bs cs : Array α) (v₁ v₂ : α)
+        (i₁ i₂ j : Nat)
+        (h₁ : i₁ < as.size)
+        (h₂ : bs = as.set i₁ v₁)
+        (h₃ : i₂ < bs.size)
+        (h₃ : cs = bs.set i₂ v₂)
+        (h₄ : i₁ ≠ j ∧ i₂ ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  grind =>
+    repeat instantiate =Array.getElem_set
+
 opaque p : Nat → Prop
 opaque q : Nat → Prop
 opaque f : Nat → Nat