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