From f11bb86609847fa6873801a4b1d797f0dc29cd1a Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 24 Jul 2026 13:22:45 +0000 Subject: [PATCH 1/4] fix: rank a vcgen call's unfoldings below a named spec MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes a regression where `vcgen [f, h, …]` reported `No spec found` for a sibling call in a self-recursive `f`'s body when the same list both brackets `f` to unfold and names a spec `h` for `f`. The equational and unfold specs a bracketed definition contributes now enter a priority band below an explicitly named spec, so at a recursive call the named spec is applied and `vcgen` stops instead of unfolding the definition again into a branch whose sibling call has no matching spec. The band still sits above `@[spec]` and `@[spec high]`, so a bracketed definition is unfolded ahead of an ambient spec keyed on the same program. --- src/Lean/Elab/Tactic/Do/Attr.lean | 5 +++++ .../Elab/Tactic/Do/Internal/VCGen/SpecDB.lean | 2 +- tests/elab/vcgenAmbientLocalSpec.lean | 16 +++++++++++++++- 3 files changed, 21 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index f433ea0919e4..39256173192e 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -355,6 +355,11 @@ abbrev SpecEntry := SpecTheorem /-- Priority for a spec named explicitly in a `vcgen [...]` argument list. -/ def explicitSpecPrio : Nat := eval_prio high + 20 +/-- Priority for the equational and unfold specs a bracketed definition in a `vcgen [...]` argument +list contributes. Below `explicitSpecPrio` so a spec named in the same list outranks a call's +unfolding, above `eval_prio high` so the unfolding still outranks an ambient `@[spec]`. -/ +def unfoldSpecPrio : Nat := eval_prio high + 10 + /-- Priority for a local hypothesis pulled into `vcgen`'s spec set by `*`. -/ def starSpecPrio : Nat := eval_prio high + 10 diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean index 2d30ffb4549c..ef40d43dd1e1 100644 --- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean +++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean @@ -102,7 +102,7 @@ public def addSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorems) : -- 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 explicitSpecPrio do + for newSpec in ← simpSpecTheorems entries unfoldSpecPrio do specs := Sym.insertPattern specs newSpec.pattern newSpec return { specs, erased } diff --git a/tests/elab/vcgenAmbientLocalSpec.lean b/tests/elab/vcgenAmbientLocalSpec.lean index 85c69ee4b6c5..029c1eeaf138 100644 --- a/tests/elab/vcgenAmbientLocalSpec.lean +++ b/tests/elab/vcgenAmbientLocalSpec.lean @@ -10,7 +10,10 @@ outrank default specs does not shadow a call-site spec, while a priority above t the ambient spec collected from the same hypothesis. `namedBeatsSpec`, `specHighLoses`, and `specHighestWins` isolate the banding against `@[spec]`, `@[spec high]`, and a priority above the band. `unfoldBeatsSpec` checks that a bracketed definition is unfolded ahead of a lossy `@[spec]` keyed on -the same program, including when the program's state type is a variable. +the same program, including when the program's state type is a variable. `namedStopBeatsUnfold` +checks that when the same list brackets a self-recursive definition to unfold and names a spec for it, +the named spec outranks the unfolding at the recursive call, so `vcgen` stops there instead of +unfolding the definition again into a branch whose sibling call has no matching spec. -/ open Std.Internal.Do Lean.Order @@ -116,3 +119,14 @@ theorem unfoldBeatsSpec {σ : Type} (a : σ) : ⦃ fun s => s.1 = a ⦄ (bumpSnd : StateM (σ × Nat) Nat) ⦃ fun _ s => s.1 = a ⦄ := by fail_if_success (vcgen <;> grind) vcgen [bumpSnd] <;> grind + +-- `tail` is bracketed to unfold and `hstop` names a spec for it in the same list. At the recursive +-- `tail f` call `hstop` outranks `tail`'s unfold equation, so `vcgen` stops rather than unfolding +-- `tail` again into a branch whose `item` call `hItem` no longer matches. +theorem namedStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat) + (hItem : ⦃ fun s => s = enc b ++ rest ⦄ item f ⦃ fun r s => r = b ∧ s = rest ⦄) + (hstop : ∀ acc, ⦃ fun s => s = rest ⦄ tail f acc ⦃ fun r s => r = acc ∧ s = rest ⦄) : + ∀ acc, ⦃ fun s => s = '+' :: (enc b ++ rest) ⦄ tail (f + 1) acc + ⦃ fun r s => r = acc + b ∧ s = rest ⦄ := by + intro acc + vcgen [tail, hItem, hstop] <;> grind From 8a6b60075e8884cdd68f9d681db7b4d5e87f2e89 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 24 Jul 2026 13:37:07 +0000 Subject: [PATCH 2/4] fix: respace vcgen call-site priority bands so unfolding ranks below a starred spec This PR fixes `vcgen [f, *]` reporting `No spec found` for a sibling call in a self-recursive `f`'s body: the bracketed definition's unfolding tied the `*` band and won the tie-break, unfolding `f` again at the recursive call instead of applying the `*`-pulled spec. The call-site priorities are respaced onto the RFC's `n * 1000` grid with the strict ordering explicit > star > unfold > `@[spec high]`: `explicitSpecPrio = high + 3000`, `starSpecPrio = high + 2000`, `unfoldSpecPrio = high + 1000`. A bracketed definition's unfolding now ranks strictly below both a named spec and a `*` hypothesis for the same program, and above `@[spec]`/`@[spec high]`. --- src/Lean/Elab/Tactic/Do/Attr.lean | 19 ++++++++++-------- tests/elab/vcgenAmbientLocalSpec.lean | 28 +++++++++++++++++++-------- 2 files changed, 31 insertions(+), 16 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index 39256173192e..15e91c7d2a5f 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -352,16 +352,19 @@ instance : BEq SpecTheorem where abbrev SpecEntry := SpecTheorem -/-- Priority for a spec named explicitly in a `vcgen [...]` argument list. -/ -def explicitSpecPrio : Nat := eval_prio high + 20 +/-- Priority for a spec named explicitly in a `vcgen [...]` argument list. Top of the call-site band: +outranks a `*` hypothesis, a bracketed definition's unfolding, and any ambient `@[spec]`. -/ +def explicitSpecPrio : Nat := eval_prio high + 3000 -/-- Priority for the equational and unfold specs a bracketed definition in a `vcgen [...]` argument -list contributes. Below `explicitSpecPrio` so a spec named in the same list outranks a call's -unfolding, above `eval_prio high` so the unfolding still outranks an ambient `@[spec]`. -/ -def unfoldSpecPrio : Nat := eval_prio high + 10 +/-- Priority for a local hypothesis pulled into `vcgen`'s spec set by `*`. Between `explicitSpecPrio` +and `unfoldSpecPrio`: a named spec outranks it, and it outranks a bracketed definition's unfolding. -/ +def starSpecPrio : Nat := eval_prio high + 2000 -/-- Priority for a local hypothesis pulled into `vcgen`'s spec set by `*`. -/ -def starSpecPrio : Nat := eval_prio high + 10 +/-- Priority for the equational and unfold specs a bracketed definition in a `vcgen [...]` argument +list contributes. Bottom of the call-site band: ranks strictly below both a named spec and a `*` +hypothesis, so either stops a recursion the definition would otherwise keep unfolding, and above +`eval_prio high` so the unfolding still outranks an ambient `@[spec]` or `@[spec high]`. -/ +def unfoldSpecPrio : Nat := eval_prio high + 1000 structure SpecTheorems where specs : DiscrTree SpecTheorem := DiscrTree.empty diff --git a/tests/elab/vcgenAmbientLocalSpec.lean b/tests/elab/vcgenAmbientLocalSpec.lean index 029c1eeaf138..b2bb1eba50fb 100644 --- a/tests/elab/vcgenAmbientLocalSpec.lean +++ b/tests/elab/vcgenAmbientLocalSpec.lean @@ -2,18 +2,20 @@ import Std.Internal.Do import Std.Tactic.Do /-! `vcgen` ranks the specs available at a call site into priority bands: a spec named in the -`vcgen [...]` list outranks a local hypothesis pulled in by `*`, which outranks a spec collected -from an ambient hypothesis. The call-site bands sit just above `high`, so an `@[spec high]` used to -outrank default specs does not shadow a call-site spec, while a priority above the band still does. +`vcgen [...]` list outranks a local hypothesis pulled in by `*`, which outranks a bracketed +definition's unfolding, which outranks a spec collected from an ambient hypothesis. The call-site +bands all sit above `high`, so an `@[spec high]` used to outrank default specs does not shadow a +call-site spec, while a priority above the whole band still does. `viaBinder`, `viaHave`, and `viaStar` prove one goal three ways, checking that a named spec wins over the ambient spec collected from the same hypothesis. `namedBeatsSpec`, `specHighLoses`, and `specHighestWins` isolate the banding against `@[spec]`, `@[spec high]`, and a priority above the band. `unfoldBeatsSpec` checks that a bracketed definition is unfolded ahead of a lossy `@[spec]` keyed on -the same program, including when the program's state type is a variable. `namedStopBeatsUnfold` -checks that when the same list brackets a self-recursive definition to unfold and names a spec for it, -the named spec outranks the unfolding at the recursive call, so `vcgen` stops there instead of -unfolding the definition again into a branch whose sibling call has no matching spec. +the same program, including when the program's state type is a variable. `namedStopBeatsUnfold` and +`starStopBeatsUnfold` check that when the same list brackets a self-recursive definition to unfold and +also supplies a spec for it, once as a named argument and once pulled by `*`, the spec outranks the +unfolding at the recursive call, so `vcgen` stops there instead of unfolding the definition again into +a branch whose sibling call has no matching spec. -/ open Std.Internal.Do Lean.Order @@ -97,7 +99,7 @@ theorem termBeatsSpecHigh (hNamed : ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄ := by vcgen [show ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄ from hNamed] <;> grind -@[spec high + 30] axiom leaf_above : ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄ +@[spec high + 3001] axiom leaf_above : ⦃ fun _ => True ⦄ leaf ⦃ fun r _ => r = 7 ⦄ -- A priority above the call-site band still overrides a named local. theorem specHighestWins (hNamed : ⦃ fun _ => True ⦄ leaf ⦃ fun _ _ => True ⦄) : @@ -130,3 +132,13 @@ theorem namedStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat) ⦃ fun r s => r = acc + b ∧ s = rest ⦄ := by intro acc vcgen [tail, hItem, hstop] <;> grind + +-- The same as `namedStopBeatsUnfold`, but the spec for `tail` is pulled by `*` rather than named. The +-- `*` band still outranks `tail`'s unfold equation at the recursive call, so `vcgen` stops there. +theorem starStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat) + (hItem : ⦃ fun s => s = enc b ++ rest ⦄ item f ⦃ fun r s => r = b ∧ s = rest ⦄) + (hstop : ∀ acc, ⦃ fun s => s = rest ⦄ tail f acc ⦃ fun r s => r = acc ∧ s = rest ⦄) : + ∀ acc, ⦃ fun s => s = '+' :: (enc b ++ rest) ⦄ tail (f + 1) acc + ⦃ fun r s => r = acc + b ∧ s = rest ⦄ := by + intro acc + vcgen [tail, *] <;> grind From 77e604c408a30f2fa5e64f7b4555e24b13ba8bf1 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 24 Jul 2026 13:43:12 +0000 Subject: [PATCH 3/4] feat: add standardized unfold/star/arg priority classes for call-site specs This PR introduces the `unfold`, `star`, and `arg` priority classes to the `prio` syntax category, usable as `@[spec arg]` and the like, standardizing the call-site priority band `vcgen` assigns: `arg = high + 3000` for a spec named in a `vcgen [...]` list, `star = high + 2000` for a hypothesis pulled by `*`, and `unfold = high + 1000` for a bracketed definition's unfolding, giving the strict ordering `arg > star > unfold > high`. `vcgen`'s `explicitSpecPrio`, `starSpecPrio`, and `unfoldSpecPrio` now source their values from `eval_prio arg`, `eval_prio star`, and `eval_prio unfold`. --- src/Init/Notation.lean | 9 +++++++++ src/Lean/Elab/Tactic/Do/Attr.lean | 6 +++--- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 6a86d3cb0f9f..6278f456ed5e 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -141,6 +141,15 @@ The standardized "medium" priority `mid = 500`. This is lower than `default`, an macro "mid" : prio => `(prio| 500) /-- The standardized "high" priority `high = 10000`, for things that should be higher than default priority. -/ macro "high" : prio => `(prio| 10000) +/-- The standardized "unfold" priority `unfold = high + 1000`, for the specs a definition unfolded at a +call site contributes. Above `high`, below `star`. -/ +macro "unfold" : prio => `(prio| high + 1000) +/-- The standardized "star" priority `star = high + 2000`, for a hypothesis pulled into a call site by +`*`. Above `unfold`, below `arg`. -/ +macro "star" : prio => `(prio| high + 2000) +/-- The standardized "arg" priority `arg = high + 3000`, for a spec named explicitly in a call-site +argument list. Above `star`. -/ +macro "arg" : prio => `(prio| high + 3000) /-- Parentheses are used for grouping priority expressions. -/ macro "(" p:prio ")" : prio => return p diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index 15e91c7d2a5f..3c02f2413d3f 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -354,17 +354,17 @@ abbrev SpecEntry := SpecTheorem /-- Priority for a spec named explicitly in a `vcgen [...]` argument list. Top of the call-site band: outranks a `*` hypothesis, a bracketed definition's unfolding, and any ambient `@[spec]`. -/ -def explicitSpecPrio : Nat := eval_prio high + 3000 +def explicitSpecPrio : Nat := eval_prio arg /-- Priority for a local hypothesis pulled into `vcgen`'s spec set by `*`. Between `explicitSpecPrio` and `unfoldSpecPrio`: a named spec outranks it, and it outranks a bracketed definition's unfolding. -/ -def starSpecPrio : Nat := eval_prio high + 2000 +def starSpecPrio : Nat := eval_prio star /-- Priority for the equational and unfold specs a bracketed definition in a `vcgen [...]` argument list contributes. Bottom of the call-site band: ranks strictly below both a named spec and a `*` hypothesis, so either stops a recursion the definition would otherwise keep unfolding, and above `eval_prio high` so the unfolding still outranks an ambient `@[spec]` or `@[spec high]`. -/ -def unfoldSpecPrio : Nat := eval_prio high + 1000 +def unfoldSpecPrio : Nat := eval_prio unfold structure SpecTheorems where specs : DiscrTree SpecTheorem := DiscrTree.empty From f5e95f5abc9eafc3ba4a1344723a55b038fb3dfa Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 24 Jul 2026 14:04:02 +0000 Subject: [PATCH 4/4] refactor: inline vcgen call-site priority values and trim comments This PR drops the `unfold`/`star`/`arg` `prio` notation classes and inlines their values into `explicitSpecPrio`, `starSpecPrio`, and `unfoldSpecPrio` as `eval_prio high + 3000/2000/1000`, and trims the surrounding comments. --- src/Init/Notation.lean | 9 --------- src/Lean/Elab/Tactic/Do/Attr.lean | 20 +++++++------------- tests/elab/vcgenAmbientLocalSpec.lean | 17 ++++++----------- 3 files changed, 13 insertions(+), 33 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 6278f456ed5e..6a86d3cb0f9f 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -141,15 +141,6 @@ The standardized "medium" priority `mid = 500`. This is lower than `default`, an macro "mid" : prio => `(prio| 500) /-- The standardized "high" priority `high = 10000`, for things that should be higher than default priority. -/ macro "high" : prio => `(prio| 10000) -/-- The standardized "unfold" priority `unfold = high + 1000`, for the specs a definition unfolded at a -call site contributes. Above `high`, below `star`. -/ -macro "unfold" : prio => `(prio| high + 1000) -/-- The standardized "star" priority `star = high + 2000`, for a hypothesis pulled into a call site by -`*`. Above `unfold`, below `arg`. -/ -macro "star" : prio => `(prio| high + 2000) -/-- The standardized "arg" priority `arg = high + 3000`, for a spec named explicitly in a call-site -argument list. Above `star`. -/ -macro "arg" : prio => `(prio| high + 3000) /-- Parentheses are used for grouping priority expressions. -/ macro "(" p:prio ")" : prio => return p diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index 3c02f2413d3f..39a7b2fa2b3e 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -352,19 +352,13 @@ instance : BEq SpecTheorem where abbrev SpecEntry := SpecTheorem -/-- Priority for a spec named explicitly in a `vcgen [...]` argument list. Top of the call-site band: -outranks a `*` hypothesis, a bracketed definition's unfolding, and any ambient `@[spec]`. -/ -def explicitSpecPrio : Nat := eval_prio arg - -/-- Priority for a local hypothesis pulled into `vcgen`'s spec set by `*`. Between `explicitSpecPrio` -and `unfoldSpecPrio`: a named spec outranks it, and it outranks a bracketed definition's unfolding. -/ -def starSpecPrio : Nat := eval_prio star - -/-- Priority for the equational and unfold specs a bracketed definition in a `vcgen [...]` argument -list contributes. Bottom of the call-site band: ranks strictly below both a named spec and a `*` -hypothesis, so either stops a recursion the definition would otherwise keep unfolding, and above -`eval_prio high` so the unfolding still outranks an ambient `@[spec]` or `@[spec high]`. -/ -def unfoldSpecPrio : Nat := eval_prio unfold +-- Call-site priority bands, all above `@[spec high]`, ordered named > `*` > unfold. +/-- Priority for a spec named in a `vcgen [...]` argument list. -/ +def explicitSpecPrio : Nat := eval_prio high + 3000 +/-- Priority for a local hypothesis pulled into `vcgen`'s spec set by `*`. -/ +def starSpecPrio : Nat := eval_prio high + 2000 +/-- Priority for the equational and unfold specs a bracketed definition in a `vcgen [...]` list contributes. -/ +def unfoldSpecPrio : Nat := eval_prio high + 1000 structure SpecTheorems where specs : DiscrTree SpecTheorem := DiscrTree.empty diff --git a/tests/elab/vcgenAmbientLocalSpec.lean b/tests/elab/vcgenAmbientLocalSpec.lean index b2bb1eba50fb..844cee78532f 100644 --- a/tests/elab/vcgenAmbientLocalSpec.lean +++ b/tests/elab/vcgenAmbientLocalSpec.lean @@ -4,18 +4,16 @@ import Std.Tactic.Do /-! `vcgen` ranks the specs available at a call site into priority bands: a spec named in the `vcgen [...]` list outranks a local hypothesis pulled in by `*`, which outranks a bracketed definition's unfolding, which outranks a spec collected from an ambient hypothesis. The call-site -bands all sit above `high`, so an `@[spec high]` used to outrank default specs does not shadow a -call-site spec, while a priority above the whole band still does. +bands sit just above `high`, so an `@[spec high]` used to outrank default specs does not shadow a +call-site spec, while a priority above the band still does. `viaBinder`, `viaHave`, and `viaStar` prove one goal three ways, checking that a named spec wins over the ambient spec collected from the same hypothesis. `namedBeatsSpec`, `specHighLoses`, and `specHighestWins` isolate the banding against `@[spec]`, `@[spec high]`, and a priority above the band. `unfoldBeatsSpec` checks that a bracketed definition is unfolded ahead of a lossy `@[spec]` keyed on the same program, including when the program's state type is a variable. `namedStopBeatsUnfold` and -`starStopBeatsUnfold` check that when the same list brackets a self-recursive definition to unfold and -also supplies a spec for it, once as a named argument and once pulled by `*`, the spec outranks the -unfolding at the recursive call, so `vcgen` stops there instead of unfolding the definition again into -a branch whose sibling call has no matching spec. +`starStopBeatsUnfold` check that a spec for the definition, named or pulled by `*`, outranks its +unfolding at a recursive call. -/ open Std.Internal.Do Lean.Order @@ -122,9 +120,7 @@ theorem unfoldBeatsSpec {σ : Type} (a : σ) : fail_if_success (vcgen <;> grind) vcgen [bumpSnd] <;> grind --- `tail` is bracketed to unfold and `hstop` names a spec for it in the same list. At the recursive --- `tail f` call `hstop` outranks `tail`'s unfold equation, so `vcgen` stops rather than unfolding --- `tail` again into a branch whose `item` call `hItem` no longer matches. +-- `tail` is bracketed to unfold, and the named `hstop` outranks its unfolding at the recursive call. theorem namedStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat) (hItem : ⦃ fun s => s = enc b ++ rest ⦄ item f ⦃ fun r s => r = b ∧ s = rest ⦄) (hstop : ∀ acc, ⦃ fun s => s = rest ⦄ tail f acc ⦃ fun r s => r = acc ∧ s = rest ⦄) : @@ -133,8 +129,7 @@ theorem namedStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat) intro acc vcgen [tail, hItem, hstop] <;> grind --- The same as `namedStopBeatsUnfold`, but the spec for `tail` is pulled by `*` rather than named. The --- `*` band still outranks `tail`'s unfold equation at the recursive call, so `vcgen` stops there. +-- As `namedStopBeatsUnfold`, but the spec is pulled by `*`; its band still outranks the unfolding. theorem starStopBeatsUnfold (b : Nat) (rest : List Char) (f : Nat) (hItem : ⦃ fun s => s = enc b ++ rest ⦄ item f ⦃ fun r s => r = b ∧ s = rest ⦄) (hstop : ∀ acc, ⦃ fun s => s = rest ⦄ tail f acc ⦃ fun r s => r = acc ∧ s = rest ⦄) :