fix: vcgen [f] unfolding of definitions by root match

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -14,6 +14,7 @@ public import Lean.Elab.Tactic.Do.ConjunctivePre
 import Init.While
 import Init.Syntax
 import Lean.Meta.Sym.Simp.DiscrTree
+import Lean.Meta.DiscrTree.Util
 
 public section
 
@@ -515,6 +516,12 @@ private def etaExpandEqPattern (pattern : Sym.Pattern) (eqTy : Expr) : Sym.Patte
         checkTypeMask? := none }
     (newPattern, k)
 
+/-- Whether some hypothesis of the equation type is an overlap hypothesis
+(see `Simp.isEqnThmHypothesis`), as in the wildcard-row equation of an overlapping `match`. -/
+private def hasOverlapHypothesis : Expr → Bool
+  | .forallE _ d b _ => Simp.isEqnThmHypothesis d || hasOverlapHypothesis b
+  | _ => false
+
 /--
 Create a `SpecTheorem` from a simp/equational declaration `declName : ∀ xs, lhs = rhs`, keyed on the
 LHS. Function-level equations (e.g. class projection unfold lemmas) are eta-expanded so the
@@ -531,38 +538,81 @@ def mkSpecTheoremFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option Sp
   let (pattern, etaArgs) := etaExpandEqPattern pattern eqTy
   return some { pattern, proof := .global declName, kind := .simp etaArgs, priority := prio }
 
+/--
+The unfold theorem `declName.eq_def` through which a definition in a simp set's `toUnfold`
+rewrites, the spec-database counterpart of `simp`'s delta unfolding. `none` for a recursive
+definition, whose unconditional unfolding would not terminate.
+-/
+def unfoldSpecEqn? (declName : Name) : MetaM (Option Name) := do
+  if (← isRecursiveDefinition declName) then return none
+  getUnfoldEqnFor? declName (nonRec := true)
+
+/--
+The spec theorems the simp entries `entries` contribute, the single place a `vcgen [...]` argument or
+an `attribute [spec] f` definition (through `mkSimpEntryOfDeclToUnfold`) turns into specs:
+- each `.thm` entry, keyed on its left-hand side (`mkSpecTheoremFromSimpDecl?`) at `prio`, skipping
+  wildcard-row equations guarded by an overlap hypothesis (as a spec such an equation matches any
+  call and strands the hypothesis as a verification condition),
+- each `.toUnfold` definition through its unfold theorem `f.eq_def` (`unfoldSpecEqn?`) at priority
+  `0`, below every equation, so a call with an opaque discriminant still rewrites to the underlying
+  `match` expression, which `vcgen` then splits.
+A single malformed entry is traced and skipped rather than aborting the set.
+-/
+def simpSpecTheorems (entries : Array SimpEntry) (prio : Nat) : MetaM (Array SpecTheorem) := do
+  let mut result := #[]
+  for entry in entries do
+    match entry with
+    | .thm thm =>
+      if let .decl declName .. := thm.origin then
+        try
+          if hasOverlapHypothesis (← getConstInfo declName).type then
+            trace[Elab.Tactic.Do.specAttr] "Skipping overlap-hypothesis equation {declName}"
+          else if let some spec ← mkSpecTheoremFromSimpDecl? declName prio then
+            result := result.push spec
+        catch e =>
+          trace[Elab.Tactic.Do.specAttr] "Failed to add simp spec {declName}: {e.toMessageData}"
+    | .toUnfold declName =>
+      try
+        if let some eqDef ← unfoldSpecEqn? declName then
+          if let some spec ← mkSpecTheoremFromSimpDecl? eqDef 0 then
+            result := result.push spec
+      catch e =>
+        trace[Elab.Tactic.Do.specAttr] "Failed to add unfold spec {declName}: {e.toMessageData}"
+    | .toUnfoldThms .. => pure ()
+  return result
+
 /--
 Register the equational lemmas of a `@[spec]`-annotated declaration as `.simp` entries with the
-given priority. An equational proposition is registered directly; a definition is registered via its
-equation lemmas (`getEqnsFor?`). Anything else throws, since it cannot serve as a `vcgen` spec.
+given priority. An equational proposition is registered directly; a definition is registered via the
+specs its simp entries contribute (`simpSpecTheorems`). Anything else throws, since it cannot serve as
+a `vcgen` spec.
 -/
 def SpecExtension.addSimpSpecTheoremsFromConst (ext : SpecExtension) (declName : Name) (prio : Nat)
     (attrKind : AttributeKind) : MetaM Unit := do
-  let add (declName : Name) : MetaM Unit := do
-    if let some thm ← mkSpecTheoremFromSimpDecl? declName prio then
-      ext.add thm attrKind
   let info ← getConstInfo declName
   if (← isProp info.type) then
-    add declName
-  else if let some eqns ← getEqnsFor? declName then
-    eqns.forM add
+    if let some thm ← mkSpecTheoremFromSimpDecl? declName prio then
+      ext.add thm attrKind
+  else if info.isDefinition then
+    for thm in ← simpSpecTheorems (← mkSimpEntryOfDeclToUnfold declName) prio do
+      ext.add thm attrKind
   else
     throwError "'{declName}' is neither an equational theorem nor a definition with unfold equations"
 
 /--
 The spec proofs a `@[spec]` constant contributes to the database: the constant itself for a
-`Triple`/`⊑ wp` spec, the equation itself for an equational spec, or its equation lemmas for a
-definition registered to unfold. Mirrors `addSimpSpecTheoremsFromConst` so `[-foo]` erases exactly
-the entries that annotating `foo` inserted.
+`Triple`/`⊑ wp` spec, the equation itself for an equational spec, or the specs its simp set
+contributes for a definition registered to unfold. Mirrors `addSimpSpecTheoremsFromConst` so `[-foo]`
+erases exactly the entries that annotating `foo` inserted.
 -/
 def specEraseProofs (declName : Name) : MetaM (Array SpecProof) := do
   if (← mkSpecTheoremFromConst declName).isSome then
     return #[.global declName]
   let info ← getConstInfo declName
   if (← isProp info.type) then
     return #[.global declName]
-  else if let some eqns ← getEqnsFor? declName then
-    return eqns.map (.global ·)
+  else if info.isDefinition then
+    return (← simpSpecTheorems (← mkSimpEntryOfDeclToUnfold declName) (eval_prio default)).map (·.proof)
   else
     return #[]
 

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

@@ -116,7 +116,7 @@ public def mkContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg := false)
             specThms := specThms.insert thm
         catch _ => continue
   let backwardRules ← VCGen.mkBackwardRules
-  let allSpecThms ← extendWithSimpSpecs specThms simpThms
+  let allSpecThms ← addSimpSpecs specThms simpThms
   let ctx : VCGen.Context := { backwardRules }
   return (ctx, { specs := allSpecThms })
 

src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean

@@ -18,8 +18,8 @@ open Lean Meta Elab Tactic Sym
 Spec-theorem database used by `vcgen`. The `@[spec]` attribute already stores
 `Std.Internal.Do` specs as pattern-keyed `SpecTheorem`s (see `Lean.Elab.Tactic.Do.Attr`);
 this module adds the operations the VC generator needs on top: instantiating a spec to
-`pre ⊑ wp …` form, migrating the equational lemmas registered through the `mvcgen_simp`
-side of `@[spec]` into the same database, and looking up the specs matching a program.
+`pre ⊑ wp …` form, folding a `vcgen [...]` call's simp-style arguments into the same
+database, and looking up the specs matching a program.
 -/
 
 namespace Lean.Elab.Tactic.Do.Internal
@@ -79,16 +79,13 @@ public def SpecAttr.SpecTheorem.global? (specThm : SpecTheorem) : Option Name :=
 namespace VCGen
 
 /--
-Extend the `@[spec]` database with the equational lemmas registered through the `mvcgen_simp`
-side of `@[spec]`:
-- simp theorem declarations registered directly as `@[spec]`,
-- unfold entries registered with `attribute [spec] foo`, using stored equation lemmas when
-  available and falling back to `Meta.getEqnsFor?`.
+Extend the spec `database` with the specs a `vcgen [...]` call's simp-style arguments contribute
+(`simpSpecTheorems` over the `simpThms` that `mkSimpContext` collected).
 
 Hoare triple and `⊑ wp` specs are already in `database`: the attribute stores them pattern-keyed
 at annotation time.
 -/
-public def extendWithSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorems) :
+public def addSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorems) :
     MetaM SpecTheorems := do
   let mut specs := database.specs
   -- Erased entries are still inserted into `specs` below; `findSpecs` filters them out
@@ -97,28 +94,16 @@ public def extendWithSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorem
     match SpecProof.ofOrigin o with
     | some p => acc.insert p
     | none => acc
-  -- Add simp spec theorems (equational lemmas registered via `@[spec]`)
-  for simpThm in simpThms.post.values do
-    if let .decl declName .. := simpThm.origin then
-      try
-        if let some newSpec ← mkSpecTheoremFromSimpDecl? declName simpThm.priority then
-          specs := Sym.insertPattern specs newSpec.pattern newSpec
-      catch e =>
-        trace[Elab.Tactic.Do.vcgen] "Failed to add simp spec {declName}: {e.toMessageData}"
-  -- Add definitions to unfold (registered via `attribute [spec] foo`)
-  for declName in simpThms.toUnfold.toList do
-    let eqThms ← match simpThms.toUnfoldThms.find? declName with
-      | some eqThms => pure eqThms
-      | none =>
-        -- No explicit equational theorems stored; generate them via `getEqnsFor?`
-        let some eqThms ← Meta.getEqnsFor? declName | continue
-        pure eqThms
-    for eqThm in eqThms do
-      try
-        if let some newSpec ← mkSpecTheoremFromSimpDecl? eqThm (prio := eval_prio default) then
-          specs := Sym.insertPattern specs newSpec.pattern newSpec
-      catch e =>
-        trace[Elab.Tactic.Do.vcgen] "Failed to add unfold spec {declName}/{eqThm}: {e.toMessageData}"
+  -- Only post-rewrite simp lemmas become specs, so a `↓`-marked (pre-rewrite) argument is dropped.
+  for simpThm in simpThms.pre.values do
+    logWarning m!"`vcgen` uses only post-rewrite simp lemmas as specs; ignoring the pre-rewrite \
+      lemma `{simpThm.origin.key}`."
+  -- `mkSimpContext` splits a bracketed definition into its equations (in `post`) and a `toUnfold`
+  -- entry; feed both back to `simpSpecTheorems` as the `SimpEntry`s the definition would produce.
+  let entries := simpThms.post.values.map (SimpEntry.thm ·)
+    ++ simpThms.toUnfold.toList.toArray.map (SimpEntry.toUnfold ·)
+  for newSpec in ← simpSpecTheorems entries (eval_prio default) do
+    specs := Sym.insertPattern specs newSpec.pattern newSpec
   return { specs, erased }
 
 end VCGen

tests/elab/vcgenUnfoldMatchDef.lean

@@ -0,0 +1,78 @@
+import Std.Tactic.Do
+import Std.Internal.Do
+
+/-!
+Test for `vcgen [f]` where `f` is defined by a root `match` on its arguments. With an opaque
+discriminant the constructor equations cannot rewrite the call, so the unfold theorem `f.eq_def`
+rewrites it to the `match` expression and `vcgen` splits it, mirroring `simp`'s unfolding of
+non-recursive definitions. The wildcard-row equation of an overlapping `match` must not be used
+as a spec: it matches any call and would strand its overlap hypothesis as an unprovable
+verification condition.
+-/
+
+set_option mvcgen.warning false
+
+def dep (n : Option Nat) : Id Nat :=
+  match n with | some y => pure (y + 1) | none => pure 2
+
+/-- Overlapping wildcard row: its equation is guarded by an overlap hypothesis. -/
+def wild (n m : Option Nat) : Id Nat :=
+  match n, m with
+  | some y, some z => pure (y + z + 1)
+  | _, _ => pure 1
+
+/-- Reducible: `mkSimpEntryOfDeclToUnfold` yields no equations for it, so it contributes only its
+unfold theorem, matching `simp`'s delta unfolding of reducible definitions. -/
+@[reducible] def red (n : Option Nat) : Id Nat :=
+  match n with | some y => pure (y + 1) | none => pure 2
+
+/-- Recursive: no `eq_def` fallback, so an opaque discriminant still reports a missing spec
+instead of unfolding indefinitely. -/
+def recf (n : Nat) : Id Nat :=
+  match n with | 0 => pure 1 | n + 1 => recf n
+
+section
+open Lean.Order Std.Internal.Do
+
+example (n : Option Nat) : ⦃ True ⦄ dep n ⦃ fun r => r > 0 ⦄ := by
+  vcgen [dep] with finish
+
+-- A concrete discriminant is rewritten by the constructor equation directly.
+example : ⦃ True ⦄ dep (some 5) ⦃ fun r => r = 6 ⦄ := by
+  vcgen [dep] with finish
+
+example (n m : Option Nat) : ⦃ True ⦄ wild n m ⦃ fun r => r > 0 ⦄ := by
+  vcgen [wild] with finish
+
+example (n : Option Nat) : ⦃ True ⦄ red n ⦃ fun r => r > 0 ⦄ := by
+  vcgen [red] with finish
+
+-- The global attribute goes through the same registration.
+attribute [local spec] wild in
+example (n m : Option Nat) : ⦃ True ⦄ wild n m ⦃ fun r => r > 0 ⦄ := by
+  vcgen with finish
+
+/--
+error: Failed to apply rule SpecProof.global recf.eq_2 for
+  recf n
+target:
+  ⊤ ⊑ wp (recf n) (LT.lt 0) ⊥
+Pred:
+  Prop
+excessArgs: []
+rule type:
+  ∀ (Pre : Prop) (n_2 : Nat) (Q : Nat → Prop) (E : EPost⟨⟩), Pre ⊑ wp (recf n_2) Q E → Pre ⊑ wp (recf n_2.succ) Q E
+-/
+#guard_msgs (whitespace := lax) in
+example (n : Nat) : ⦃ True ⦄ recf n ⦃ fun r => r > 0 ⦄ := by
+  vcgen [recf] with finish
+
+-- Only post-rewrite simp lemmas become specs; a `↓` (pre-rewrite) argument is ignored with a warning.
+@[simp] theorem two_eq : (1 + 1 : Nat) = 2 := rfl
+
+/-- warning: `vcgen` uses only post-rewrite simp lemmas as specs; ignoring the pre-rewrite lemma `two_eq`. -/
+#guard_msgs in
+example (n : Option Nat) : ⦃ True ⦄ dep n ⦃ fun r => r > 0 ⦄ := by
+  vcgen [dep, ↓ two_eq] with finish
+
+end