chore: upstream repeat/split_ands/subst_eqs (#3305)

Small tactics used in the implementation of `ext`.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>

src/Init/Tactics.lean

@@ -894,6 +894,22 @@ The tactic `nomatch h` is shorthand for `exact nomatch h`.
 macro "nomatch " es:term,+ : tactic =>
   `(tactic| exact nomatch $es:term,*)
 
+/--
+`repeat' tac` runs `tac` on all of the goals to produce a new list of goals,
+then runs `tac` again on all of those goals, and repeats until `tac` fails on all remaining goals.
+-/
+syntax (name := repeat') "repeat' " tacticSeq : tactic
+
+/--
+`repeat1' tac` applies `tac` to main goal at least once. If the application succeeds,
+the tactic is applied recursively to the generated subgoals until it eventually fails.
+-/
+syntax (name := repeat1') "repeat1' " tacticSeq : tactic
+
+/-- `and_intros` applies `And.intro` until it does not make progress. -/
+syntax "and_intros" : tactic
+macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
+
 end Tactic
 
 namespace Attr

src/Init/TacticsExtra.lean

@@ -41,4 +41,26 @@ macro_rules
   | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
     expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
 
+/--
+`iterate n tac` runs `tac` exactly `n` times.
+`iterate tac` runs `tac` repeatedly until failure.
+
+`iterate`'s argument is a tactic sequence,
+so multiple tactics can be run using `iterate n (tac₁; tac₂; ⋯)` or
+```lean
+iterate n
+  tac₁
+  tac₂
+  ⋯
+```
+-/
+syntax "iterate" (ppSpace num)? ppSpace tacticSeq : tactic
+macro_rules
+  | `(tactic| iterate $seq:tacticSeq) =>
+    `(tactic| try ($seq:tacticSeq); iterate $seq:tacticSeq)
+  | `(tactic| iterate $n $seq:tacticSeq) =>
+    match n.1.toNat with
+    | 0 => `(tactic| skip)
+    | n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq)
+
 end Lean.Parser.Tactic

src/Lean/Elab/Tactic.lean

@@ -25,4 +25,5 @@ import Lean.Elab.Tactic.Calc
 import Lean.Elab.Tactic.Congr
 import Lean.Elab.Tactic.Guard
 import Lean.Elab.Tactic.RCases
+import Lean.Elab.Tactic.Repeat
 import Lean.Elab.Tactic.Change

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -324,6 +324,12 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 @[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>
   liftMetaTactic fun mvarId => return [← substVars mvarId]
 
+/--
+`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
+replacing the left side of the equality with the right, until no more progress can be made.
+-/
+elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs)
+
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
   If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.

src/Lean/Elab/Tactic/Repeat.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Scott Morrison
+-/
+import Lean.Meta.Tactic.Repeat
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.Tactic
+
+@[builtin_tactic repeat']
+def evalRepeat' : Tactic := fun stx => do
+  match stx with
+  | `(tactic| repeat' $tac:tacticSeq) =>
+     setGoals (← Meta.repeat' (evalTacticAtRaw tac) (← getGoals))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic repeat1']
+def evalRepeat1' : Tactic := fun stx => do
+  match stx with
+  | `(tactic| repeat1' $tac:tacticSeq) =>
+    setGoals (← Meta.repeat1' (evalTacticAtRaw tac) (← getGoals))
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Meta/Tactic.lean

@@ -28,4 +28,5 @@ import Lean.Meta.Tactic.Rename
 import Lean.Meta.Tactic.LinearArith
 import Lean.Meta.Tactic.AC
 import Lean.Meta.Tactic.Refl
-import Lean.Meta.Tactic.Congr
+import Lean.Meta.Tactic.Congr
+import Lean.Meta.Tactic.Repeat

src/Lean/Meta/Tactic/Repeat.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Scott Morrison
+-/
+import Lean.Meta.Basic
+
+namespace Lean.Meta
+/--
+Implementation of `repeat'` and `repeat1'`.
+
+`repeat'Core f` runs `f` on all of the goals to produce a new list of goals,
+then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
+or until `maxIters` total calls to `f` have occurred.
+
+Returns a boolean indicating whether `f` succeeded at least once, and
+all the remaining goals (i.e. those on which `f` failed).
+-/
+def repeat'Core [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
+    (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) :
+    m (Bool × List MVarId) := do
+  let (progress, acc) ← go maxIters false goals [] #[]
+  pure (progress, (← acc.filterM fun g => not <$> g.isAssigned).toList)
+where
+  /-- Auxiliary for `repeat'Core`. `repeat'Core.go f maxIters progress goals stk acc` evaluates to
+  essentially `acc.toList ++ repeat' f (goals::stk).join maxIters`: that is, `acc` are goals we will
+  not revisit, and `(goals::stk).join` is the accumulated todo list of subgoals. -/
+  go : Nat → Bool → List MVarId → List (List MVarId) → Array MVarId → m (Bool × Array MVarId)
+  | _, p, [], [], acc => pure (p, acc)
+  | n, p, [], goals::stk, acc => go n p goals stk acc
+  | n, p, g::goals, stk, acc => do
+    if ← g.isAssigned then
+      go n p goals stk acc
+    else
+      match n with
+      | 0 => pure <| (p, acc.push g ++ goals |> stk.foldl .appendList)
+      | n+1 =>
+        match ← observing? (f g) with
+        | some goals' => go n true goals' (goals::stk) acc
+        | none => go n p goals stk (acc.push g)
+termination_by n p goals stk _ => (n, stk, goals)
+
+/--
+`repeat' f` runs `f` on all of the goals to produce a new list of goals,
+then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
+or until `maxIters` total calls to `f` have occurred.
+Always succeeds (returning the original goals if `f` fails on all of them).
+-/
+def repeat' [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
+    (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) :=
+  repeat'Core f goals maxIters <&> (·.2)
+
+/--
+`repeat1' f` runs `f` on all of the goals to produce a new list of goals,
+then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
+or until `maxIters` total calls to `f` have occurred.
+Fails if `f` does not succeed at least once.
+-/
+def repeat1' [Monad m] [MonadError m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
+    (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) := do
+  let (.true, goals) ← repeat'Core f goals maxIters | throwError "repeat1' made no progress"
+  pure goals
+
+end Lean.Meta

tests/lean/run/and_intros.lean

@@ -0,0 +1,7 @@
+example (hp : p) (hq : q) (hr : r) : (p ∧ q) ∧ (q ∧ (r ∧ p)) := by
+  and_intros
+  · exact hp
+  · exact hq
+  · exact hq
+  · exact hr
+  · exact hp