vcgen: no `f.eq_def` fallback for a recursive function whose equation lemmas are conditional ("No spec found")
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 15/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Active
- Domain
- compilers
Research direction
Start in Lean/Elab/Tactic/Do/Attr.lean: simpSpecTheorems and hasOverlapHypothesis decide which equation lemmas are skipped, and unfoldSpecEqn? decides when the f.eq_def fallback is offered. Run the reproducer's step_spec theorem, which fails with 'No spec found', and compare it with step_spec', which passes. Done means vcgen [step, ih] unfolds the cons case via the fallback without looping. The issue leaves open whether to add a guard against explicit specs or a smaller step budget, so the design needs a maintainer decision first.
Written by the indexing model from the issue text.
Description
This issue was written by Claude (an AI assistant) on behalf of @nomeata.
Found while moving con-leche's cached-to-pure simulation proofs (a few thousand lines) to vcgen + grind (sym … => vcgen … <;> finish). Each case has a workaround in con-leche; the reproducer below is standalone.
For a structurally recursive function whose step has an inner
overlapping match, vcgen [step] finds no spec for a call with an
opaque discriminant, although vcgen [step.eq_def] works.
vcgen [f] contributes f's equation lemmas, skips the ones with an
overlap hypothesis (simpSpecTheorems, hasOverlapHypothesis,
Lean/Elab/Tactic/Do/Attr.lean), and falls back to the unconditional
f.eq_def (priority 0) only for a NON-recursive f (unfoldSpecEqn?:
"none for a recursive definition, whose unconditional unfolding would
not terminate"). But in vcgen an unfolding is one rewriting step per
program occurrence: a recursive call is met with the induction
hypothesis first (an explicit spec, priority high + 3000, beats the
fallback) and the walk is bounded by stepLimit anyway.
(Caveat from con-leche: where the induction hypothesis does NOT apply,
e.g. a missing case split, eq_def keeps unfolding the recursive call
until the step limit — one walk spent 113 G instructions before failing.
So the fallback may want a "only if no explicit spec matches the
recursive call" guard, or a smaller step budget, rather than being on
unconditionally.)
Expected: vcgen [step, ih] unfolds step t (a :: rest) via the
eq_def fallback, as for a non-recursive definition.
Observed (v4.35.0 and nightly-2026-10-15): "No spec found for program step t (a :: rest)".
Workaround: vcgen [step.eq_def, ih] (works; con-leche task #359 uses
it for every cached loop: betaPeelI, inferSpineI, inferLamsI, …).
import Std.WP
import Std.Tactic.Do
open Std.WP
open scoped Lean.Order
set_option experimental.vcgen true
inductive T where
| lam (b : T)
| leaf (n : Nat)
| node (l r : T)
def step : T → List Nat → StateT Nat (Except String) Nat
| _, [] => pure 0
| t, a :: rest =>
match t with
| .lam b => step b rest
| _ => do modify (· + a); pure a
/-- Fails: No spec found for program step t (a :: rest). -/
theorem step_spec (t : T) (xs : List Nat) (s₀ : Nat) :
⦃fun s => s = s₀⦄ step t xs ⦃fun _ s => s₀ ≤ s; ⊤⦄ := by
induction xs generalizing t s₀ with
| nil => vcgen [step] with finish
| cons a rest ih => vcgen [step, ih] with finish
/-- Works. -/
theorem step_spec' (t : T) (xs : List Nat) (s₀ : Nat) :
⦃fun s => s = s₀⦄ step t xs ⦃fun _ s => s₀ ≤ s; ⊤⦄ := by
induction xs generalizing t s₀ with
| nil => vcgen [step] with finish
| cons a rest ih => vcgen [step.eq_def, ih] with finish
- Dominant language
- Lean
- Stars
- 9.6k
- Forks
- 1.1k
- Avg merge
- 1d 1h
- Merged PRs (30d)
- 279
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 1 day ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupOpenbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15674 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
generated by fuzzer llvm:transforms miscompilation
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
llvm/llvm-project#234047 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
WebAssembly/spec#2284 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
ProvableHQ/leo#29657 ·
-
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
llvm/torch-mlir#4840 ·
Maintainers usually reply within 5 days