Skip to content

fix: apply specs to goals with a registered WP instance in vcgen - #14883

Merged
sgraf812 merged 4 commits into
masterfrom
vcgen-canon-wp-instances
Aug 22, 2026
Merged

fix: apply specs to goals with a registered WP instance in vcgen#14883
sgraf812 merged 4 commits into
masterfrom
vcgen-canon-wp-instances

Conversation

@sgraf812

@sgraf812 sgraf812 commented Aug 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR makes vcgen canonicalize WP instances, so monads may register a diamond WP instance in addition to the low priority WP instance synthesized from WPMonad.toWP.

@sgraf812
fix: canonicalize the WP instance of wp applications in vcgen
2a66006 
A monad may register a bespoke `WP` instance next to its `WPMonad`
instance. The goal's `wp` application then carries the registered
instance, while a backward rule built from a spec stated over
`[WPMonad m Pred EPred]` carries the blanket `WPMonad.toWP` route.
The two spellings are definitionally equal only at instance
transparency, so rule application failed with "No spec applicable".

`work` now canonicalizes the goal target with `Sym.canon`, and
`tryMkBackwardRuleFromSpec` canonicalizes the constructed rule, so
both sides carry the instance that `synthInstance` returns. The
instance guard synthesizes the spec's outstanding instance parameters
and compares the two concrete spellings at instance transparency.

The regression test registers bespoke `WP` instances for two custom
monads, one stating the `toWP` field by name and one via
`inferInstance`. The `Std.WP` interpretations stay
`instance_reducible` definitions: registering them as instances pins
the `outParam` assertion types during synthesis and breaks
lattice-generic contexts such as the section variables in
`tests/elab/vcgenFrames.lean`.
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 21, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 21, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dd7716da5b36bc54601dc3f4257fe74123fa2b8a --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 15:54:10)

@leanprover-bot

leanprover-bot commented Aug 21, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase dd7716da5b36bc54601dc3f4257fe74123fa2b8a --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 15:54:11)

@sgraf812
refactor: simplify canonTarget and the WP instance guard
c10d451 
`canonTarget` reuses `MVarId.replaceTargetDefEqFast` and drops the no-op check. The rule-construction instance guard compares the goal's `WP` instance against the spec's at default transparency (`withDefault <| isDefEqGuarded ...`), which suffices to match a bespoke goal instance against the spec's `WPMonad.toWP` spelling, replacing `isDefEqInstWP`.
@sgraf812
Clean up comments in RuleConstruction.lean
ddd0a8b 
Removed unnecessary explanation about canonicalization and instance arguments in the abstracted rule.
@sgraf812
refactor: drop wp canonicalization, register the WP interpretations a…
b93a53c 
…s instances

The default-transparency instance guard alone fixes spec application for goals with a registered `WP` instance: the rule conclusion pins the goal's own instance arguments, premises keep the spec's `WPMonad.toWP` spelling, and `synthPending` assigns the spec's `WPMonad` metavariable during the guard, so goals and rules stay consistent without canonicalizing either. `Sym.canon` on the constructed rule also rewrote tuple matchers into projections, which destroyed the binder names that `binderNameHint` consumption reads and broke `tests/elab/intrinsicVerification.lean` (also on CI).

The `WP` interpretations in `Std.WP.Monad.Instances` are proper instances now, with `toWP _ := inferInstance`, so the existing tests exercise the registered-instance path and the dedicated regression test is gone. The `Id`-monad theorems in `tests/elab/vcgenFrames.lean` state their assertions at `Prop`: a hypothesis `[WPMonad Id Pred EPred]` over a generic `Pred` denotes no real instance, and instance search, which ignores `outParam` positions during selection, resolves `WP (Id β) …` to the registered `Prop` instance regardless.
@sgraf812 sgraf812 changed the title fix: canonicalize the WP instance of wp applications in vcgen fix: apply specs to goals with a registered WP instance in vcgen Aug 21, 2026
@sgraf812 sgraf812 added the changelog-tactics User facing tactics label Aug 22, 2026
@sgraf812
sgraf812 marked this pull request as ready for review August 22, 2026 08:42
@sgraf812
sgraf812 requested review from TwoFX and kim-em as code owners August 22, 2026 08:42
@sgraf812
sgraf812 enabled auto-merge August 22, 2026 08:42
@sgraf812
sgraf812 added this pull request to the merge queue Aug 22, 2026
@sgraf812
sgraf812 removed this pull request from the merge queue due to a manual request Aug 22, 2026
@sgraf812

sgraf812 commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Aug 22, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for b93a53c against dd7716d are in. There are significant results. @sgraf812

  • ✅ build//instructions: -587.2M (-0.01%)

Large changes (11✅, 3🟥)

  • 🟥 compiled/rbmap_checkpoint//instructions: +3.7G (+28.98%)
  • 🟥 compiled/rbmap_checkpoint//task-clock: +475ms (+32.57%)
  • 🟥 compiled/rbmap_checkpoint//wall-clock: +487ms (+33.24%)
  • ✅ elab/big_beq//maxrss: -25MiB (-1.40%)
  • ✅ elab/big_deceq//maxrss: -24MiB (-1.37%)
  • ✅ elab/big_deceq_rec//maxrss: -24MiB (-1.37%)
  • ✅ elab/big_match_nat//maxrss: -25MiB (-1.39%)
  • ✅ elab/delayed_lift//maxrss: -25MiB (-1.39%)
  • ✅ elab/delayed_sharing//maxrss: -25MiB (-1.40%)
  • ✅ elab/let_to_have_closed_body//maxrss: -24MiB (-1.33%)
  • ✅ elab/lift_lets_parallel//maxrss: -25MiB (-1.39%)
  • ✅ elab/lift_lets_spine//maxrss: -25MiB (-1.38%)
  • ✅ elab/string_simp_ne//maxrss: -25MiB (-1.35%)
  • ✅ elab/sym_let_to_have_nested//maxrss: -25MiB (-1.35%)

Medium changes (14✅, 1🟥)

  • 🟥 compiled/const_fold//instructions: +257.4M (+3.58%)
  • ✅ compiled/const_fold//maxrss: -2MiB (-0.14%)
  • ✅ elab/big_beq_rec//maxrss: -22MiB (-1.24%)
  • ✅ elab/big_match//maxrss: -25MiB (-1.36%)
  • ✅ elab/big_match_partial//maxrss: -25MiB (-1.36%)
  • ✅ elab/cbv_divisors//maxrss: -27MiB (-1.49%)
  • ✅ elab/delayed_assign//maxrss: -25MiB (-1.39%)
  • ✅ elab/let_to_have_chain//maxrss: -26MiB (-1.47%)
  • ✅ elab/lift_lets_binders//maxrss: -24MiB (-1.34%)
  • ✅ elab/lift_lets_chain//maxrss: -24MiB (-1.35%)
  • ✅ elab/lift_lets_dag//maxrss: -27MiB (-1.52%)
  • ✅ elab/sym_let_to_have_chain//maxrss: -27MiB (-1.49%)
  • ✅ elab/sym_lift_lets_chain//maxrss: -22MiB (-1.19%)
  • ✅ elab/sym_lift_lets_parallel//maxrss: -25MiB (-1.32%)
  • ✅ elab/sym_lift_lets_spine//maxrss: -25MiB (-1.31%)

Small changes (12✅, 6🟥)

  • ✅ build/module/Std.WP.Monad.Conjunctive//instructions: -32.8M (-2.57%)
  • ✅ build/module/Std.WP.Monad.Lemmas//instructions: -215.1M (-3.25%) (reduced significance based on absolute threshold)
  • ✅ build/module/Std.WP.Triple.SpecLemmas//instructions: -277.2M (-1.70%) (reduced significance based on absolute threshold)
  • 🟥 compiled/const_fold//task-clock: +96ms (+8.79%)
  • 🟥 compiled/const_fold//wall-clock: +98ms (+9.01%)
  • ✅ compiled/incr_header_save//maxrss: -9MiB (-0.45%)
  • ✅ elab/big_match_nat_split//maxrss: -26MiB (-1.42%)
  • ✅ elab/bv_decide_incremental//maxrss: -29MiB (-1.40%)
  • 🟥 elab/bv_stress_replicate//maxrss: +15MiB (+2.01%)
  • ✅ elab/cbv_decide//maxrss: -29MiB (-1.57%)
  • ✅ elab/cbv_merge_sort//maxrss: -25MiB (-1.36%)
  • ✅ elab/grind_cases_next//maxrss: -27MiB (-1.46%)
  • ✅ elab/let_to_have_nested//maxrss: -21MiB (-1.16%)
  • ✅ elab/mut_rec_wf//maxrss: -25MiB (-1.33%)
  • ✅ elab/sym_let_to_have_closed_body//maxrss: -20MiB (-0.92%)
  • 🟥 vcgen/AddSubCancelDeep/100/vcgen//wall-clock: +4ms (+16.32%)
  • 🟥 vcgen/AddSubCancelDeep/500/vcgen//wall-clock: +4ms (+5.45%)
  • 🟥 vcgen/AddSubCancelSimp/100/kernel//wall-clock: +1ms (+8.39%)

@sgraf812
sgraf812 added this pull request to the merge queue Aug 22, 2026
Merged via the queue into master with commit e3b3b04 Aug 22, 2026
34 checks passed
@sgraf812
sgraf812 deleted the vcgen-canon-wp-instances branch August 25, 2026 07:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner
@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@sgraf812 @leanprover-bot @leanprover-radar