test: bring Sym-based `mvcgen'` on par with `mvcgen` by sgraf812 · Pull Request #13578 · leanprover/lean4

sgraf812 · 2026-04-29T14:47:56Z

This PR brings the Sym-based mvcgen' to feature parity with mvcgen; the only remaining gap is +jp (join-point handling).

The slight benchmark regressions are due to simplifying VCs out of SPred form, hitting hardest on cases with linearly many VCs like PurePreCond. The ~10% vcgen slowdown is worth it for the cleaner user-visible VCs.

… in `mkSpecContext` This PR rewrites the `mvcgen'` `mkSpecContext` helper to partition the `[...]` argument list into spec theorems and simp lemmas, mirroring the approach used in `Lean.Elab.Tactic.Do.VCGen.mkSpecContext`: each entry is first tried as a spec theorem, and on failure it falls back to a simp/unfold lemma which is processed via `mkSimpContext`. The resulting simp theorems are fed into the migrated spec theorem database so that unfold/simp rules registered by the user are actually picked up. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ia `entails.mk` This PR refactors the post-condition entailment solver to attempt closing the whole `PostCond.entails` goal by reflexivity first via a new `PostCond.entails.rfl` backward rule, before falling back to decomposition via `PostCond.entails.mk`. When the exception subgoal cannot be discharged by reflexivity it is now emitted as a VC instead of raising an error.

… via new `entails.pure` lemma This PR adds `ExceptConds.entails.pure` in `Std.Do.PostCond`, stating that `ExceptConds.entails` is trivially inhabited at `PostShape.pure`, and uses it as a backward rule in the sym mvcgen to discharge the exception side of a `PostCond.entails` goal for pure post shapes before falling back to reflexivity.

… `@[simp]` This PR changes `Invariant`, `StringInvariant`, `StringSliceInvariant` and their `withEarlyReturn`/`withEarlyReturnNewDo` counterparts from `abbrev` to `def` (with `@[simp]` so they still unfold on demand). The motivation is that `SymM` does not unfold `def`s, so these declarations remain visible as applications of a named constant in proof states and can be detected as invariant types by `isSpecInvariantType`. The sym `mvcgen'` `emitVC` is updated to use `isSpecInvariantType` instead of the hard-coded `Std.Do.Invariant` check, so any `@[spec_invariant_type]`-tagged type is classified as an invariant. `String.toNat?_eq_some_of_mem` is updated to feed the relevant unfold lemmas to `simp only` explicitly now that they no longer reduce transparently.

…-do-logic-tests

This PR removes a now-redundant `pure_cons` from the simp argument list of `conjunction_apply`. The earlier `apply_pure_cons` `@[simp]` rule subsumes it, and the `linter.unusedSimpArgs` lint (now enforced) flags it as unused.

sgraf812 · 2026-04-29T14:48:10Z

!bench

leanprover-radar · 2026-04-29T14:55:46Z

Benchmark results for 9693009 against 2ba4c55 are in. There are significant results. @sgraf812

✅ build//instructions: -4.5G (-0.04%)

Large changes (2✅, 1🟥)

✅ build/module/Lean.Meta.Sym.Pattern//instructions: -5.4G (-21.76%)
🟥 mvcgen/sym/PurePrecond/700/kernel//wall-clock: +46ms (+23.47%)
✅ mvcgen/sym/PurePrecond/700/vcgen//wall-clock: -536ms (-61.97%)

Medium changes (2🟥)

🟥 mvcgen/sym/PurePrecond/100/vcgen//wall-clock: +13ms (+10.16%)
🟥 mvcgen/sym/PurePrecond/400/kernel//wall-clock: +18ms (+16.67%)

Small changes (11🟥)

🟥 build/module/Std.Data.String.ToNat//instructions: +625.4M (+11.10%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Do.SPred.DerivedLaws//instructions: +113.3M (+1.34%) (reduced significance based on *//lines)
🟥 build/module/Std.Do.SPred.SPred//instructions: +97.8M (+3.84%) (reduced significance based on *//lines)
🟥 mvcgen/sym/AddSubCancelDeep/100/vcgen//wall-clock: +11ms (+7.05%)
🟥 mvcgen/sym/GetThrowSet/350/kernel//wall-clock: +14ms (+8.14%)
🟥 mvcgen/sym/GetThrowSet/350/vcgen//wall-clock: +8ms (+4.42%)
🟥 mvcgen/sym/GetThrowSet/600/vcgen//wall-clock: +22ms (+9.13%)
🟥 mvcgen/sym/GetThrowSetGrind/50/kernel//wall-clock: +5ms (+10.20%)
🟥 mvcgen/sym/MatchIota/150/vcgen//wall-clock: +9ms (+6.38%)
🟥 mvcgen/sym/MatchIota/50/vcgen//wall-clock: +4ms (+3.10%)
🟥 mvcgen/sym/PurePrecond/100/kernel//wall-clock: +5ms (+17.86%)

mathlib-lean-pr-testing · 2026-04-29T16:17:43Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2ba4c55a8498ac495129feeca1ee6dbc9165a8db --onto 3c6317b6d77a565b4217532d1190ac6955dba842. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-29 16:17:43)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2ba4c55a8498ac495129feeca1ee6dbc9165a8db --onto 0a6c31520b2ebaa6e71227454b46ebfb4986ae7b. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-30 06:40:27)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 19baa470e58e04c5832ef7100e9f5de57d9a7704 --onto 0a6c31520b2ebaa6e71227454b46ebfb4986ae7b. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-30 15:59:33)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 94a29d19520cecdf3a2ad10c9cdfed4b07e92ec5 --onto dae325700c89e23c453b1d6d5ed5432d87880062. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-05 10:48:48)

leanprover-bot · 2026-04-29T16:17:45Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2ba4c55a8498ac495129feeca1ee6dbc9165a8db --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-29 16:17:45)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 19baa470e58e04c5832ef7100e9f5de57d9a7704 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-30 15:59:35)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 94a29d19520cecdf3a2ad10c9cdfed4b07e92ec5 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-05 10:48:49)

Renames `down_apply_pure_elim` to `down_pure_intro` and relocates it under the `# Pure` section of `DerivedLaws.lean`, matching #13582 as merged. Reverts the six `Invariant.withEarlyReturn`/`withEarlyReturnNewDo` variants to `abbrev` and reverts `Std/Data/String/ToNat.lean` to its pre-PR state, matching the final form of #13583. Updates the local `VCGen.lean` reference to the renamed `SPred.down_pure_intro` lemma and restores `mkFreshPair_triple` to legacy `mvcgen -elimLets +trivial` (it remains blocked under `mvcgen'`).

…-do-logic-tests

…VCs, fix tests

sgraf812 · 2026-05-05T09:54:37Z

!bench

leanprover-radar · 2026-05-05T09:54:43Z

Benchmark results for f3373d0 against 94a29d1 are in. There are significant results. @sgraf812

🟥 build exited with code 1
🟥 other exited with code 1

No significant changes detected.

…-do-logic-tests

sgraf812 · 2026-05-05T09:59:33Z

!bench

leanprover-radar · 2026-05-05T09:59:39Z

Benchmark results for 9166b0c against 94a29d1 are in. There are significant results. @sgraf812

🟥 build//instructions: +520.1M (+0.00%)

Large changes (1✅, 1🟥)

🟥 mvcgen/sym/PurePrecond/700/kernel//wall-clock: +41ms (+21.03%)
✅ mvcgen/sym/PurePrecond/700/vcgen//wall-clock: -516ms (-61.28%)

Medium changes (3🟥)

🟥 mvcgen/sym/GetThrowSet/350/vcgen//wall-clock: +13ms (+7.18%)
🟥 mvcgen/sym/PurePrecond/100/vcgen//wall-clock: +14ms (+11.02%)
🟥 mvcgen/sym/PurePrecond/400/kernel//wall-clock: +14ms (+13.08%)

Small changes (10🟥)

🟥 mvcgen/sym/AddSubCancel/500/vcgen//wall-clock: +8ms (+3.42%)
🟥 mvcgen/sym/AddSubCancelDeep/100/vcgen//wall-clock: +9ms (+5.73%)
🟥 mvcgen/sym/AddSubCancelSimp/100/vcgen//wall-clock: +13ms (+5.00%)
🟥 mvcgen/sym/GetThrowSet/100/vcgen//wall-clock: +8ms (+5.84%)
🟥 mvcgen/sym/GetThrowSet/600/vcgen//wall-clock: +26ms (+10.79%)
🟥 mvcgen/sym/GetThrowSetGrind/50/kernel//wall-clock: +5ms (+10.20%)
🟥 mvcgen/sym/MatchIota/150/vcgen//wall-clock: +10ms (+7.09%)
🟥 mvcgen/sym/MatchIota/50/vcgen//wall-clock: +4ms (+3.10%)
🟥 mvcgen/sym/PurePrecond/100/kernel//wall-clock: +4ms (+14.81%)
🟥 mvcgen/sym/ReaderState/1000/vcgen//wall-clock: +26ms (+6.72%)

sgraf812 and others added 20 commits April 10, 2026 12:30

fix: panic in mkBackwardRuleForSplit

d3c3ad2

FIXME: temporary Pattern.match? fix

ac66210

feat: "Eta expand" SimpSpec Theorems

b0b8e75

feat: Eta-expand and simplify VCs as much as possible

974309d

introsSimp refactoring

77f86b2

feat: discharge trivial ExceptConds (true, false)

712ece3

feat: improve introSPredEntails

e2d8256

feat: implement iota reduction in reduceHead?, remove letE case

17ed8e4

feat: do introSPredEntails in solve

6d138f4

feat: S SPred.pure simp rules

888e3f5

fix: reducibility in reduceHead?

76c3899

tests ported from doLogicTests

7c51555

feat: framing pure facts into hpost VCs

db95d10

improve SPred.entails solver

d495f91

Merge remote-tracking branch 'origin/master' into worktree-sym-mvcgen…

dc220a3

…-do-logic-tests

chore: drop unused pure_cons simp arg in conjunction_apply

9693009

This PR removes a now-redundant `pure_cons` from the simp argument list of `conjunction_apply`. The earlier `apply_pure_cons` `@[simp]` rule subsumes it, and the `linter.unusedSimpArgs` lint (now enforced) flags it as unused.

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 29, 2026

sgraf812 added 5 commits April 30, 2026 05:57

feat: grind annotation for Invariant definitions

0f8f0f6

feat: Respect eta potential of spec

3ce5128

Merge remote-tracking branch 'origin/master' into worktree-sym-mvcgen…

b128bf4

…-do-logic-tests

feat: discharge trivial conjunctions eagerly

8734abb

sgraf812 added 12 commits April 30, 2026 18:28

test

fc03538

split VCGen into separate modules

60501d5

remove trace message from test

7df0bef

split solve function into parts

3ab0bf5

feat: support config options and invariants in mvcgen'

53d75d0

feat: join points in mvcgen', phase 3a

4d0fda6

feat: handle fuel, trivial and inline invariants

9bd2d9b

only mark invariant goals synth opaque if not elaborated immediately

708de76

tests

5738416

feat: join points phase 3a, for real

2050597

fix: local context in error messages

88c3b81

feat: error on missing spec, elab invariant subgoals before emitting …

c297c72

…VCs, fix tests

Merge remote-tracking branch 'origin/master' into worktree-sym-mvcgen…

9166b0c

…-do-logic-tests

sgraf812 force-pushed the worktree-sym-mvcgen-do-logic-tests branch from f3373d0 to 9166b0c Compare May 5, 2026 09:58

sgraf812 changed the title ~~test: Bring Sym-based mvcgen' on par with mvcgen~~ test: ring Sym-based mvcgen' on par with mvcgen May 5, 2026

sgraf812 changed the title ~~test: ring Sym-based mvcgen' on par with mvcgen~~ test: bring Sym-based mvcgen' on par with mvcgen May 5, 2026

sgraf812 marked this pull request as ready for review May 5, 2026 12:07

sgraf812 enabled auto-merge May 5, 2026 12:07

sgraf812 added this pull request to the merge queue May 5, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks May 5, 2026

sgraf812 added this pull request to the merge queue May 5, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks May 5, 2026

Garmelon added this pull request to the merge queue May 5, 2026

Merged via the queue into master with commit 42eb038 May 5, 2026
26 of 30 checks passed

sgraf812 deleted the worktree-sym-mvcgen-do-logic-tests branch May 5, 2026 13:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

test: bring Sym-based `mvcgen'` on par with `mvcgen`#13578

test: bring Sym-based `mvcgen'` on par with `mvcgen`#13578
Garmelon merged 40 commits intomasterfrom
worktree-sym-mvcgen-do-logic-tests

sgraf812 commented Apr 29, 2026 •

edited

Loading

Uh oh!

sgraf812 commented Apr 29, 2026

Uh oh!

leanprover-radar commented Apr 29, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 29, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Apr 29, 2026 •

edited

Loading

Uh oh!

sgraf812 commented May 5, 2026

Uh oh!

leanprover-radar commented May 5, 2026 •

edited

Loading

Uh oh!

sgraf812 commented May 5, 2026

Uh oh!

leanprover-radar commented May 5, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

sgraf812 commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgraf812 commented Apr 29, 2026

Uh oh!

leanprover-radar commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgraf812 commented May 5, 2026

Uh oh!

leanprover-radar commented May 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgraf812 commented May 5, 2026

Uh oh!

leanprover-radar commented May 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

sgraf812 commented Apr 29, 2026 •

edited

Loading

leanprover-radar commented Apr 29, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Apr 29, 2026 •

edited

Loading

leanprover-bot commented Apr 29, 2026 •

edited

Loading

leanprover-radar commented May 5, 2026 •

edited

Loading

leanprover-radar commented May 5, 2026 •

edited

Loading