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

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

TODO. Semantically feature-complete with mvcgen. Just needs more work for invariant sections, config settings and join point handling.

… 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)

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)

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

sgraf812 · 2026-04-30T18:07:27Z

!bench

leanprover-radar · 2026-04-30T18:07:33Z

Benchmark results for 3621d83 against 19baa47 are in. There are significant results. @sgraf812

✅ build//instructions: -6.1G (-0.05%)

Large changes (2✅, 2🟥)

✅ build/module/Lean.Meta.Sym.Pattern//instructions: -5.4G (-21.79%)
🟥 mvcgen/sym/PurePrecond/400/kernel//wall-clock: +22ms (+20.75%)
🟥 mvcgen/sym/PurePrecond/700/kernel//wall-clock: +50ms (+25.91%)
✅ mvcgen/sym/PurePrecond/700/vcgen//wall-clock: -539ms (-61.88%)

Medium changes (1🟥)

🟥 mvcgen/sym/PurePrecond/100/vcgen//wall-clock: +15ms (+11.72%)

Small changes (9🟥)

🟥 mvcgen/sym/AddSubCancelDeep/100/vcgen//wall-clock: +10ms (+6.45%)
🟥 mvcgen/sym/AddSubCancelSimp/100/vcgen//wall-clock: +16ms (+6.15%)
🟥 mvcgen/sym/GetThrowSet/100/vcgen//wall-clock: +8ms (+5.84%)
🟥 mvcgen/sym/GetThrowSet/350/vcgen//wall-clock: +10ms (+5.52%)
🟥 mvcgen/sym/GetThrowSet/600/vcgen//wall-clock: +25ms (+10.42%)
🟥 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: +5ms (+3.91%)
🟥 mvcgen/sym/PurePrecond/100/kernel//wall-clock: +6ms (+22.22%)

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

chore: reduction stuff

3621d83

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
sgraf812 wants to merge 26 commits intomasterfrom
worktree-sym-mvcgen-do-logic-tests

sgraf812 commented Apr 29, 2026

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 Apr 30, 2026

Uh oh!

leanprover-radar commented Apr 30, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

sgraf812 commented Apr 29, 2026

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 Apr 30, 2026

Uh oh!

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

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

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 Apr 30, 2026 •

edited

Loading