feat: vcgen destructures binders by @[vcgen_rintro] rules

src/Lean/Elab/Tactic/VCGen.lean

@@ -16,6 +16,7 @@ public import Lean.Elab.Tactic.VCGen.Entails
 public import Lean.Elab.Tactic.VCGen.Solve
 public import Lean.Elab.Tactic.VCGen.Driver
 public import Lean.Elab.Tactic.VCGen.SimpAttr
+public import Lean.Elab.Tactic.VCGen.RIntroAttr
 public import Lean.Elab.Tactic.VCGen.Frontend
 
 /-!
@@ -31,5 +32,6 @@ The `vcgen` tactic, split across the modules above.
 - `VCGen.Solve` — the main `solve` step / `SolveResult`.
 - `VCGen.Driver` — the worklist driver (`work`, `emitVC`, `main`, `Result`).
 - `VCGen.SimpAttr` — the `@[vcgen_simp]` theorem set.
+- `VCGen.RIntroAttr` — the `@[vcgen_rintro]` binder destructuring rules.
 - `VCGen.Frontend` — the `vcgen` syntax + tactic elaborator + `mkSpecContext`.
 -/

src/Lean/Elab/Tactic/VCGen/Context.lean

@@ -11,6 +11,7 @@ public import Lean.Elab.Tactic.VCGen.SpecDB
 public import Lean.Elab.Tactic.VCGen.FrameProc
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Simp.DiscrTree
+public import Lean.Elab.Tactic.VCGen.RIntroAttr
 public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Tactic.Grind.Types
 
@@ -106,6 +107,8 @@ public structure Context where
   /-- The `@[frameproc]` registry snapshot taken at frontend init. `solve` selects a procedure per
   program node by the node's monad. -/
   frameProcs : FrameProcs := {}
+  /-- The `@[vcgen_rintro]` rules, keyed by their conclusion. -/
+  rintros : DiscrTree RIntroEntry := .empty
   /-- The `Sym.simp` methods that rewrite hypotheses, state arguments and verification conditions
   with the `@[vcgen_simp]` theorems and those of the `simp [...]` clause. `none` when the `simp`
   config option is `false`. -/
@@ -201,6 +204,8 @@ public structure State where
   /-- Caches the frame rule (`meet_op_wp_upperAdjoint_le_wp`), keyed by the `WPMonad` instance
   and the number of excess state arguments. -/
   frameBackwardRuleCache : Std.HashMap (ExprPtr × Nat) FrameBackwardRule := {}
+  /-- Caches the backward rules of the `@[vcgen_rintro]` rules, keyed by declaration name. -/
+  rintroBackwardRuleCache : Std.HashMap Name BackwardRule := {}
   /-- The frame database from the `frames` clause. -/
   frameDB : FrameDB := {}
   /--

src/Lean/Elab/Tactic/VCGen/Frontend.lean

@@ -152,7 +152,7 @@ public def mkContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg := false)
         catch _ => continue
   let backwardRules ← mkBackwardRules
   let allSpecThms ← addSimpSpecs specThms simpThms
-  let ctx : Context := { backwardRules }
+  let ctx : Context := { backwardRules, rintros := ← getRIntros }
   return (ctx, { specs := allSpecThms })
 
 /-- True iff `m` carries a `WPMonad m _ _` instance, i.e. it is a genuine weakest-precondition monad

src/Lean/Elab/Tactic/VCGen/RIntroAttr.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Lean.ScopedEnvExtension
+public import Lean.Attributes
+public import Lean.Meta.Sym.Apply
+public import Lean.Meta.Sym.Simp.DiscrTree
+
+/-!
+The `@[vcgen_rintro]` attribute registers the rules by which `vcgen` destructures a binder while it
+introduces the binders of the target, like an `rintro` pattern fixed per binder type.
+
+A rule is a theorem whose conclusion is a `∀` telescope ending in an application of a parameter
+`G`. Its premises are the binders up to the last one that mentions `G`, and its conclusion is the
+rest. Take
+```
+theorem List.forall_mem_cons_intro {G : α → Prop} (ha : G a) (hl : ∀ x, x ∈ l → G x) :
+    ∀ x, x ∈ a :: l → G x
+```
+with the conclusion `∀ x, x ∈ a :: l → G x`. It turns the target `∀ x ∈ [a, b], G x` into the
+goals `G a` and `∀ x ∈ [b], G x`. The rules are keyed in a discrimination tree by their
+conclusion, whose `∀` binders become `.arrow` keys over the binder type and the body. At each
+binder of the target, `vcgen` applies the first matching rule in priority order as a backward rule
+to the remaining target, and otherwise introduces the binder.
+
+`vcgen` always uses the rule `Prod.forall_intro`.
+-/
+
+open Lean Meta Sym
+
+public section
+
+namespace Lean.Elab.Tactic.VCGen
+
+/-- One `@[vcgen_rintro]` rule: the theorem `declName`, whose first `numPremises` binders are the
+premises, with the discrimination tree keys `keys` of its conclusion. -/
+structure RIntroEntry where
+  declName : Name
+  numPremises : Nat
+  keys : Array DiscrTree.Key
+  prio : Nat
+  deriving Inhabited
+
+instance : BEq RIntroEntry where
+  beq e₁ e₂ := e₁.declName == e₂.declName
+
+/-- The rules `vcgen` uses without registration. -/
+def builtinRIntros : Array Name := #[`Prod.forall_intro]
+
+builtin_initialize rintroExt : SimpleScopedEnvExtension RIntroEntry (DiscrTree RIntroEntry) ←
+  registerSimpleScopedEnvExtension {
+    initial  := .empty
+    addEntry := fun d e => d.insertKeyValue e.keys e
+  }
+
+/-- Check that the conclusion of `declName` is a `∀` telescope ending in an application of a
+parameter, and compute its `RIntroEntry`. -/
+def mkRIntroEntry (declName : Name) (prio : Nat) : MetaM RIntroEntry := do
+  let info ← getConstInfo declName
+  let (numBinders, numPremises) ← forallTelescope info.type fun xs body => do
+    let some g := body.getAppFn.fvarId?
+      | throwError "`@[vcgen_rintro]`: the conclusion of `{declName}` does not end in an \
+          application of a parameter"
+    let mut numPremises := 0
+    for h : i in [:xs.size] do
+      if xs[i].fvarId! == g || (← inferType xs[i]).containsFVar g then
+        numPremises := i + 1
+    return (xs.size, numPremises)
+  if numPremises == numBinders then
+    throwError "`@[vcgen_rintro]`: the conclusion of `{declName}` is not a `∀`"
+  let rule ← mkBackwardRuleFromDecl declName (some numPremises)
+  return { declName, numPremises, keys := rule.pattern.mkDiscrTreeKeys, prio }
+
+/-- The entries of the rules of `builtinRIntros`, computed once. -/
+builtin_initialize builtinRIntroEntries : IO.Ref (Std.HashMap Name RIntroEntry) ← IO.mkRef {}
+
+/-- The rules registered with `@[vcgen_rintro]`, and the rules of `builtinRIntros` that exist in
+the environment. -/
+def getRIntros : MetaM (DiscrTree RIntroEntry) := do
+  let mut d := rintroExt.getState (← getEnv)
+  for declName in builtinRIntros do
+    if (← getEnv).contains declName then
+      let e ← match (← builtinRIntroEntries.get)[declName]? with
+        | some e => pure e
+        | none =>
+          let e ← mkRIntroEntry declName (eval_prio default)
+          builtinRIntroEntries.modify (·.insert declName e)
+          pure e
+      d := d.insertKeyValue e.keys e
+  return d
+
+builtin_initialize registerBuiltinAttribute {
+  ref   := by exact decl_name%
+  name  := `vcgen_rintro
+  descr := "register a rule by which `vcgen` destructures a binder while introducing binders"
+  add   := fun declName stx kind => do
+    let prio ← getAttrParamOptPrio stx[1]
+    let e ← (mkRIntroEntry declName prio).run'
+    rintroExt.add e kind
+}
+
+end Lean.Elab.Tactic.VCGen

src/Lean/Elab/Tactic/VCGen/RuleCache.lean

@@ -96,5 +96,17 @@ public def mkFrameBackwardRuleCached (fp : FrameProc) (info : WPApp) :
   modify fun st => { st with frameBackwardRuleCache := st.frameBackwardRuleCache.insert key frule }
   return frule
 
+/--
+Cached construction of the backward rule of the `@[vcgen_rintro]` rule `e`. The rule abstracts
+the `e.numPremises` premises and matches the conclusion of `e`.
+
+Cache key: the declaration name of `e`.
+-/
+public def mkBackwardRuleForRIntroCached (e : RIntroEntry) : VCGenM BackwardRule := do
+  if let some rule := (← get).rintroBackwardRuleCache[e.declName]? then return rule
+  let rule ← (← liftMetaM <| mkBackwardRuleFromDecl e.declName (some e.numPremises)).shareCommon
+  modify fun st => { st with rintroBackwardRuleCache := st.rintroBackwardRuleCache.insert e.declName rule }
+  return rule
+
 
 end Lean.Elab.Tactic.VCGen

src/Lean/Elab/Tactic/VCGen/Solve.lean

@@ -15,7 +15,6 @@ public import Lean.Meta.Sym.InstantiateS
 public import Lean.Meta.Sym.Simp.App
 import Lean.Meta.Sym.InferType
 import Lean.Meta.Sym.InstantiateMVarsS
-import Init.Data.Prod
 
 open Lean Meta Elab Tactic Sym Sym.Internal
 open Lean.Elab.Tactic.VCGen.SpecAttr
@@ -64,36 +63,55 @@ def consumeMData? (goal : MVarId) (target : Expr) : VCGenM (Option MVarId) := do
   unless target.isMData do return none
   return some (← goal.replaceTargetDefEqFast target.consumeMData)
 
-/-- Split `∀ p : Nat × Nat, P p` into `∀ a b, P (a, b)`. -/
-def splitProdBinder (goal : MVarId) (target : Expr) : VCGenM MVarId :=
-  goal.withContext do
-  let .forallE _ dom body _ := target | return goal
-  let dom ← instantiateMVarsIfMVarAppS dom
-  let_expr c@Prod α β := dom | return goal
-  let us := c.constLevels!
-  let mk ← mkAppNS (← mkConstS ``Prod.mk us) #[α, β, .bvar 1, .bvar 0]
-  let newTarget := Expr.forallE `a α (.forallE `b β (body.instantiate1 mk) .default) .default
-  let g ← liftMetaM <| mkFreshExprSyntheticOpaqueMVar (← shareCommon newTarget)
-  let motive := Expr.lam `p dom body .default
-  let prodForall ← mkAppNS (← mkConstS ``Prod.forall us) #[α, β, motive]
-  goal.assign <| mkApp4 (.const ``Iff.mpr []) target newTarget prodForall g
-  return g.mvarId!
-
-/-- Strategy 1: simp the target, then introduce binders if the target is a `∀`. -/
+/-- Apply the backward rule `rule` of a `@[vcgen_rintro]` rule to `goal`. The types of the new goals
+are instantiated, so that the rule parameter `G` is beta-reduced at its arguments. -/
+def applyRIntroRule (goal : MVarId) (rule : BackwardRule) : VCGenM (Option (List MVarId)) := do
+  let .goals gs ← rule.apply goal | return none
+  some <$> gs.mapM fun g => do
+    let ty ← g.getType
+    let ty' ← instantiateMVarsS ty
+    if isSameExpr ty ty' then return g
+    g.replaceTargetDefEqFast ty'
+
+/-- Strategy 1a: apply the first of the `@[vcgen_rintro]` rules `entries`, in priority order, that
+applies to the target of `goal`. -/
+def applyRIntroRules (goal : MVarId) (entries : Array RIntroEntry) :
+    VCGenM (Option (List MVarId)) := do
+  for entry in entries.insertionSort (·.prio > ·.prio) do
+    if let some gs ← applyRIntroRule goal (← mkBackwardRuleForRIntroCached entry) then
+      trace[Elab.Tactic.Do.vcgen] "Applied rintro rule {entry.declName}"
+      return some gs
+    trace[Elab.Tactic.Do.vcgen] "Rintro rule {entry.declName} does not apply"
+  return none
+
+/-- Strategy 1: simp the target, then introduce its binders. One pass over the binders matches each
+`∀` binder against the `@[vcgen_rintro]` rules once. A matching rule destructures the binder, and
+the binders between two matches are introduced at once. -/
 def forallIntro? (oldGoal : MVarId) (target : Expr) : VCGenM (Option (List MVarId)) := do
   unless target.isForall do return none
   let oldGoal ← instantiateBinderDomains oldGoal
   let mut goal ← match ← simpGoalTelescope oldGoal with
     | .closed => return some []
     | .goal goal => pure goal
     | .noProgress => pure oldGoal
-  let mut target ← goal.getType
-  while target.isForall do
-    let n := numBindersToIntro target
-    let goal' ← if n == 0 then splitProdBinder goal target else introsHygienicN goal n
-    if goal' == goal then break
-    goal := goal'
-    target ← goal.getType
+  let rintros := (← read).rintros
+  let mut e ← goal.getType
+  let mut n := 0
+  repeat
+    match e with
+    | .forallE _ _ b _ =>
+      let entries := Sym.getMatch (← getMCtx) rintros e
+      unless entries.isEmpty do
+        goal ← introsHygienicN goal n
+        n := 0
+        if let some gs ← applyRIntroRules goal entries then return some gs
+      n := n + 1
+      e := b
+    | .letE _ _ _ b _ =>
+      n := n + 1
+      e := b
+    | _ => break
+  goal ← introsHygienicN goal n
   if goal == oldGoal then
     throwError "Failed to intro forall target {goal}"
   return some [goal]

src/Lean/Elab/Tactic/VCGen/Util.lean

@@ -116,10 +116,9 @@ public def processHypotheses (goal : Grind.Goal) : VCGenM Grind.Goal := do
 public def isProgramName (n : Name) : Bool :=
   !n.hasMacroScopes && !n.isImplementationDetail
 
-/-- The leading binders of `type`, stopping at a binder over a product: `∀ (n : Nat) (p : α × β)`
-counts one, because `solve` splits `p` into one binder per component first. -/
+/-- The number of leading `∀` and `let` binders of `type`. -/
 public def numBindersToIntro : Expr → Nat
-  | .forallE _ d b _ => if d.isAppOf ``Prod then 0 else numBindersToIntro b + 1
+  | .forallE _ _ b _ => numBindersToIntro b + 1
   | .letE _ _ _ b _ => numBindersToIntro b + 1
   | _ => 0
 
@@ -172,9 +171,10 @@ public def simpGoalTelescope (goal : MVarId) : VCGenM Sym.SimpGoalResult := do
 Introduce the excess state arguments of an entailment goal `pre ⊑ rhs` whose lattice type is a
 function type `σ₁ → … → σₙ → α`: repeatedly apply `stateArgIntro` (a backward rule for
 `Lean.Order.le_of_forall_le`) and introduce the new state binder, until the lattice type is
-no longer a function type. Returns `none` when the carrier is not a function type (nothing to
-introduce); throws when the carrier is a function type that `le_of_forall_le` cannot peel, such as a
-dependent function lattice `(a : α) → β a → …`.
+no longer a function type. A state binder that a `@[vcgen_rintro]` rule matches stays in the
+target for `solve` to destructure. Returns `none` when the carrier is not a function type (nothing
+to introduce); throws when the carrier is a function type that `le_of_forall_le` cannot peel, such
+as a dependent function lattice `(a : α) → β a → …`.
 -/
 public partial def introsExcessArgs (goal : MVarId) :
     VCGenM (Option MVarId) := goal.withContext do
@@ -183,6 +183,7 @@ public partial def introsExcessArgs (goal : MVarId) :
   unless α.isForall do return none
   let .goals [goal] ← (← read).backwardRules.stateArgIntro.applyChecked goal
     | throwError "failed to apply {.ofConstName ``Lean.Order.le_of_forall_le} to goal{indentExpr type}"
+  unless (Sym.getMatch (← getMCtx) (← read).rintros (← goal.getType)).isEmpty do return some goal
   let goal ← introsHygienic goal
   return (← introsExcessArgs goal) <|> some goal
 

src/Std/WP/Automation.lean

@@ -32,4 +32,10 @@ attribute [simp, grind norm] Variant.evalsTo_ofMeasure Variant.evalsBelow_ofMeas
 
 end Std.WP
 
+/-! ## The built-in `vcgen_rintro` rule -/
+
+theorem Prod.forall_intro {α : Type _} {β : Type _} {G : α × β → Prop} (h : ∀ a b, G (a, b)) :
+    ∀ p, G p :=
+  fun (a, b) => h a b
+
 end