feat: add control and arrow_telescope simproc DSL primitives (#13048)

This PR adds two new `sym_simproc` DSL primitives and helper grind-mode
tactics.

Simproc primitives:
- `control` — simplifies control-flow expressions (`if-then-else`,
  `match`, `cond`, `dite`), visiting only conditions and discriminants.
  Intended as a `pre` simproc.
- `arrow_telescope` — simplifies arrow telescopes
  (`p₁ → p₂ → ... → q`) without entering binders. Intended as a `pre`
  simproc.

Grind-mode tactics:
- `show_goals` — displays pending goals (non-terminal `trace_state` for
  grind mode)
- `exact e` — macro delegating to `tactic => exact e`

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Init/Grind/Interactive.lean

@@ -107,6 +107,9 @@ syntax (name := showLocalThms) "show_local_thms" : grind
 -/
 syntax (name := showTerm) "show_term " grindSeq : grind
 
+/-- Shows the pending goals. -/
+syntax (name := showGoals) "show_goals" : grind
+
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
@@ -315,5 +318,8 @@ Only available in `sym =>` mode.
 -/
 syntax (name := symSimp) "simp" (ppSpace colGt ident)? (" [" ident,* "]")? : grind
 
+/-- `exact e` closes the main goal if its target type matches that of `e`. -/
+macro "exact " e:term : grind => `(grind| tactic => exact $e:term)
+
 end Grind
 end Lean.Parser.Tactic

src/Init/Sym/Simp/SimprocDSL.lean

@@ -49,6 +49,14 @@ syntax (name := ground) "ground" : sym_simproc
 /-- Simplify telescope binders but not the final body. -/
 syntax (name := telescope) "telescope" : sym_simproc
 
+/-- Simplify control-flow expressions (`if-then-else`, `match`, `cond`, `dite`).
+Visits only conditions and discriminants. Intended as a `pre` simproc. -/
+syntax (name := control) "control" : sym_simproc
+
+/-- Simplify arrow telescopes (`p₁ → p₂ → ... → q`) without entering binders.
+Simplifies each `pᵢ` and `q` individually. Intended as a `pre` simproc. -/
+syntax (name := arrowTelescope) "arrow_telescope" : sym_simproc
+
 /-- Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites. -/
 syntax (name := rewriteSet) "rewrite" ident (" with " sym_discharger)? : sym_simproc
 

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -76,6 +76,10 @@ def evalGrindSeq : GrindTactic := fun stx =>
 @[builtin_grind_tactic skip] def evalSkip : GrindTactic := fun _ =>
   return ()
 
+@[builtin_grind_tactic showGoals] def evalShowGoals : GrindTactic := fun _ => do
+  let goals ← getUnsolvedGoalMVarIds
+  addRawTrace (goalsToMessageData goals)
+
 @[builtin_grind_tactic paren] def evalParen : GrindTactic := fun stx =>
   evalGrindTactic stx[1]
 

src/Lean/Elab/Tactic/Grind/SimprocDSLBuiltin.lean

@@ -9,6 +9,8 @@ import Lean.Elab.Tactic.Grind.SimprocDSL
 import Init.Sym.Simp.SimprocDSL
 import Lean.Meta.Sym.Simp.EvalGround
 import Lean.Meta.Sym.Simp.Telescope
+import Lean.Meta.Sym.Simp.ControlFlow
+import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Sym.Simp.Rewrite
 namespace Lean.Elab.Tactic.Grind
 open Meta Sym.Simp
@@ -23,6 +25,14 @@ def elabSimprocGround : SymSimprocElab := fun _ =>
 def elabSimprocTelescope : SymSimprocElab := fun _ =>
   return simpTelescope
 
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.control]
+def elabSimprocControl : SymSimprocElab := fun _ =>
+  return simpControl
+
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.arrowTelescope]
+def elabSimprocArrowTelescope : SymSimprocElab := fun _ =>
+  return simpArrowTelescope
+
 @[builtin_sym_simproc self]
 def elabSimprocSelf : SymSimprocElab := fun _ =>
   return simp

tests/elab/sym_simp_dsl_control1.lean

@@ -0,0 +1,97 @@
+/-! Tests for `control` and `arrow_telescope` simproc DSL primitives.
+Based on `sym_simp_4.lean` but using `register_sym_simp` + DSL instead of custom Lean tactics. -/
+
+register_sym_simp mySimp where
+  pre  := control >> arrow_telescope
+  post := ground >> rewrite [and_true] with self
+
+example : (if true then a else b) = a := by
+  sym => simp mySimp
+
+example : (if True then a else b) = a := by
+  sym => simp mySimp
+
+example : (if False then a else b) = b := by
+  sym => simp mySimp
+
+/--
+trace: case grind
+α✝ : Sort u_1
+x : α✝
+p q : Prop
+h : p → q
+⊢ p → q
+-/
+#guard_msgs in
+example (p q : Prop) (h : p → q) : True → p → x = x → q := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact h
+
+example (p q : Prop) : q → p → True := by
+  sym => simp mySimp
+
+example (p q : Prop) : q → p → x = x := by
+  sym => simp mySimp
+
+example (q : Prop) : q → x ≠ x → True := by
+  sym => simp mySimp
+
+example (α : Type) (p : Prop) : α → p → x = x := by
+  sym => simp mySimp
+
+example (q : Prop) (α : Type) (p : Prop) : q → α → p → x = x := by
+  sym => simp mySimp
+
+example (α β : Type) (p q : Prop) : q → β → p → α → True := by
+  sym => simp mySimp
+
+/--
+trace: case grind
+α : Type u
+x : α
+p : Prop
+h : α → p → True → α
+⊢ α → p → True → α
+-/
+#guard_msgs in
+example (α : Type u) (x : α) (p : Prop) (h : α → p → True → α) : α → p → x = x → α := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact h
+
+set_option linter.unusedVariables false
+
+def F := False
+
+/--
+trace: case grind
+α : Type
+x : α
+q : Prop
+h : F
+⊢ ∀ (a b : α), q
+-/
+#guard_msgs in
+example (α : Type) (x : α) (q : Prop) (h : F) : (a : α) → x = x → (b : α) → True → q := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact False.elim h
+
+/--
+trace: case grind
+α : Sort u
+x : α
+p q : Prop
+h : F
+⊢ ∀ (a : α) {b : α}, q
+-/
+#guard_msgs in
+example (α : Sort u) (x : α) (p q : Prop) (h : F) : (a : α) → x = x → {b : α} → True → (q ∧ True) := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact False.elim h