Skip to content

feat: vcgen destructures binders by @[vcgen_rintro] rules - #16291

Merged
sgraf812 merged 4 commits into
leanprover:masterfrom
sgraf812:sg/vcgen-rintro
Nov 6, 2026
Merged

feat: vcgen destructures binders by @[vcgen_rintro] rules#16291
sgraf812 merged 4 commits into
leanprover:masterfrom
sgraf812:sg/vcgen-rintro

Conversation

@sgraf812

@sgraf812 sgraf812 commented Nov 5, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR adds the attribute @[vcgen_rintro], which tells vcgen how to destructure a binder while it introduces the binders of a goal, like a fixed rintro pattern. For example, with

@[vcgen_rintro] theorem forall_mem_cons_intro {G : α → Prop} (ha : G a) (hl : ∀ x, x ∈ l → G x) :
    ∀ x, x ∈ a :: l → G x := List.forall_mem_cons.mpr ⟨ha, hl⟩

@[vcgen_rintro] theorem forall_mem_nil_intro {G : α → Prop} : ∀ x, x ∈ ([] : List α) → G x :=
  fun _ h => nomatch h

the goal ∀ n, n ∈ [1, 2, 3] → G n yields the verification conditions G 1, G 2 and G 3.

🤖 Generated with Claude Code

@github-actions github-actions Bot closed this Nov 5, 2026
@sgraf812 sgraf812 reopened this Nov 5, 2026
@leanprover leanprover deleted a comment from github-actions Bot Nov 5, 2026
@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 Nov 5, 2026
@sgraf812 @claude
feat: vcgen destructures binders by @[vcgen_rintro] rules
7a1ec17 
The attribute `@[vcgen_rintro]` registers a theorem whose conclusion is a
`∀` telescope ending in an application of a parameter `G`. `vcgen` keys
the rules in a discrimination tree by their conclusion. At each binder of
a `∀` target, it applies the first matching rule as a backward rule, and
otherwise introduces the binder. With rules for `x ∈ a :: l` and `x ∈ []`,
the target `∀ n, n ∈ [1, 2, 3] → G n` splits into the goals `G 1`, `G 2`
and `G 3`.

`vcgen` always uses the rules `Prod.forall_intro`, `PUnit.forall_intro`
and `True.forall_intro`. `Prod.forall_intro` replaces the special case
for binders over pairs.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QPKmiUooPkkAEYh2giBqfH
@sgraf812 sgraf812 changed the title feat: vcgen destructures premises by @[vcgen_rintro] rules feat: vcgen destructures binders by @[vcgen_rintro] rules Nov 5, 2026
@sgraf812

sgraf812 commented Nov 5, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Nov 5, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 7a1ec17 against 7633a28 are in. There are significant results. @sgraf812

  • 🟥 build//instructions: +3.7G (+0.04%)

Large changes (15🟥)

  • 🟥 compiled/liasolver//instructions: +174.3k (+0.01%)
  • 🟥 compiled/workspaceSymbolsNewRanges//instructions: +175.1k (+0.03%)
  • 🟥 vcgen/IfsJP/120/kernel//wall-clock: +8ms (+17.34%)
  • 🟥 vcgen/IfsJP/120/vcgen//wall-clock: +33ms (+18.21%)
  • 🟥 vcgen/IfsJP/160/kernel//wall-clock: +15ms (+24.53%)
  • 🟥 vcgen/IfsJP/160/vcgen//wall-clock: +52ms (+20.56%)
  • 🟥 vcgen/IfsJP/80/kernel//wall-clock: +5ms (+16.95%)
  • 🟥 vcgen/MatchesJP/40/vcgen//wall-clock: +27ms (+26.49%)
  • 🟥 vcgen/MatchesJP/60/vcgen//wall-clock: +45ms (+29.67%)
  • 🟥 vcgen/PurePrecond/2400/kernel//wall-clock: +64ms (+23.81%)
  • 🟥 vcgen/PurePrecond/2400/vcgen//wall-clock: +166ms (+54.76%)
  • 🟥 vcgen/PurePrecond/400/kernel//wall-clock: +6ms (+23.47%)
  • 🟥 vcgen/PurePrecond/400/vcgen//wall-clock: +22ms (+47.02%)
  • 🟥 vcgen/PurePrecond/4400/kernel//wall-clock: +189ms (+33.28%)
  • 🟥 vcgen/PurePrecond/4400/vcgen//wall-clock: +368ms (+57.37%)

Medium changes (3✅, 6🟥)

  • 🟥 compiled/ilean_roundtrip//instructions: +169.0k (+0.00%)
  • 🟥 compiled/parser//instructions: +2.5M (+0.01%)
  • 🟥 compiled/phashmap//instructions: +174.1k (+0.00%)
  • 🟥 compiled/rbmap_library//instructions: +171.0k (+0.00%)
  • ✅ elab/string_simp_ne//maxrss: -16MiB (-0.90%)
  • ✅ elab/sym_let_to_have_chain//maxrss: -17MiB (-0.97%)
  • ✅ elab/sym_let_to_have_nested//maxrss: -14MiB (-0.82%)
  • 🟥 lake/inundation/startup//instructions: +192.9k (+0.10%)
  • 🟥 vcgen/MatchesJP/60/kernel//wall-clock: +9ms (+9.07%)

Small changes (11✅, 146🟥)

  • 🟥 compiled/incr_header_load//instructions: +241.9k (+0.07%)
  • ✅ elab/big_match//maxrss: -6MiB (-0.37%)
  • 🟥 elab/bv_normalize_cast//instructions: +378.6k (+0.05%)
  • ✅ elab/sym_arith_norm//maxrss: -17MiB (-1.01%)
  • ✅ elab/sym_lift_lets_chain//maxrss: -12MiB (-0.70%)
  • ✅ elab/sym_lift_lets_parallel//maxrss: -16MiB (-0.89%)
  • ✅ elab/sym_lift_lets_spine//maxrss: -16MiB (-0.88%)
  • 🟥 vcgen/GetThrowSet/200/vcgen//wall-clock: +5ms (+11.61%)
  • 🟥 vcgen/IfsJP/80/vcgen//wall-clock: +19ms (+16.55%)
  • 🟥 vcgen/MatchesJP/20/vcgen//wall-clock: +13ms (+22.41%)
  • 🟥 vcgen/MatchesJP/40/kernel//wall-clock: +4ms (+6.26%)
  • 🟥 vcgen/WideJP/180/vcgen//wall-clock: +4ms (+12.55%)
  • and 145 hidden

@sgraf812 @claude
perf: keep only Prod.forall_intro built in, and introduce binder pr…
77ff450 
…efixes at once

`vcgen` uses `Prod.forall_intro` as its only built-in `@[vcgen_rintro]`
rule. `PUnit.forall_intro` and `True.forall_intro` stay available for
registration. `forallIntro?` introduces the binders before the first
`∀` that a rule matches in one step, and `getRIntros` computes the
entries of the built-in rules once.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QPKmiUooPkkAEYh2giBqfH
@sgraf812

sgraf812 commented Nov 6, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Nov 6, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 77ff450 against 7633a28 are in. There are significant results. @sgraf812

  • 🟥 build//instructions: +4.3G (+0.05%)

Large changes (6🟥)

  • 🟥 compiled/ilean_roundtrip//instructions: +220.2k (+0.00%)
  • 🟥 compiled/liasolver//instructions: +226.8k (+0.01%)
  • 🟥 compiled/phashmap//instructions: +227.3k (+0.00%)
  • 🟥 compiled/rbmap_library//instructions: +226.8k (+0.00%)
  • 🟥 compiled/workspaceSymbolsNewRanges//instructions: +223.7k (+0.03%)
  • 🟥 lake/inundation/startup//instructions: +248.2k (+0.13%)

Medium changes (1🟥)

  • 🟥 compiled/parser//instructions: +2.5M (+0.01%)

Small changes (5✅, 172🟥)

  • 🟥 compiled/incr_header_load//instructions: +293.7k (+0.08%)
  • 🟥 elab/bv_normalize_cast//instructions: +412.5k (+0.05%)
  • 🟥 vcgen/RegFile/128/vcgen//wall-clock: +7ms (+7.29%)
  • and 174 hidden

@sgraf812 @claude
perf: vcgen matches each binder against @[vcgen_rintro] rules once
5292c98 
`forallIntro?` walks the binders of the target in one pass. It matches each
`∀` binder against the rule tree once, introduces the binders between two
matches at once, and continues after a matched rule that does not apply
without rescanning the telescope.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01D74FF61KPDjY3k6hEEbrmc
@sgraf812

sgraf812 commented Nov 6, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Nov 6, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 5292c98 against 7633a28 are in. There are significant results. @sgraf812

  • 🟥 build//instructions: +4.4G (+0.05%)

Large changes (3✅, 6🟥)

  • 🟥 compiled/ilean_roundtrip//instructions: +221.2k (+0.00%)
  • 🟥 compiled/liasolver//instructions: +230.9k (+0.01%)
  • 🟥 compiled/phashmap//instructions: +223.2k (+0.00%)
  • 🟥 compiled/rbmap_library//instructions: +224.3k (+0.00%)
  • 🟥 compiled/workspaceSymbolsNewRanges//instructions: +223.8k (+0.03%)
  • ✅ elab/let_to_have_chain//maxrss: -24MiB (-1.42%)
  • ✅ elab/sym_let_to_have_chain//maxrss: -24MiB (-1.37%)
  • ✅ elab/sym_let_to_have_nested//maxrss: -21MiB (-1.22%)
  • 🟥 lake/inundation/startup//instructions: +243.1k (+0.13%)

Medium changes (14✅, 1🟥)

  • 🟥 compiled/parser//instructions: +2.5M (+0.01%)
  • ✅ elab/cbv_merge_sort//maxrss: -32MiB (-1.78%)
  • ✅ elab/delayed_lift//maxrss: -24MiB (-1.40%)
  • ✅ elab/delayed_sharing//maxrss: -24MiB (-1.40%)
  • ✅ elab/let_to_have_closed_body//maxrss: -23MiB (-1.35%)
  • ✅ elab/lift_lets_binders//maxrss: -25MiB (-1.46%)
  • ✅ elab/lift_lets_chain//maxrss: -24MiB (-1.38%)
  • ✅ elab/lift_lets_dag//maxrss: -24MiB (-1.39%)
  • ✅ elab/lift_lets_parallel//maxrss: -23MiB (-1.37%)
  • ✅ elab/lift_lets_spine//maxrss: -24MiB (-1.42%)
  • ✅ elab/string_simp_ne//maxrss: -23MiB (-1.31%)
  • ✅ elab/sym_arith_norm//maxrss: -24MiB (-1.41%)
  • ✅ elab/sym_lift_lets_chain//maxrss: -20MiB (-1.11%)
  • ✅ elab/sym_lift_lets_parallel//maxrss: -23MiB (-1.26%)
  • ✅ elab/sym_lift_lets_spine//maxrss: -24MiB (-1.31%)

Small changes (11✅, 174🟥)

  • 🟥 build/profile/grind ac//wall-clock: +3ms (+197.69%)
  • 🟥 compiled/deriv//maxrss: +332kiB (+0.08%)
  • 🟥 compiled/incr_header_load//instructions: +295.7k (+0.08%)
  • ✅ elab/cbv_decide//maxrss: -23MiB (-1.25%)
  • ✅ elab/delayed_assign//maxrss: -17MiB (-1.02%)
  • ✅ elab/let_to_have_nested//maxrss: -20MiB (-1.14%)
  • ✅ elab/many_commands//maxrss: -26MiB (-0.60%)
  • ✅ elab/mut_rec_wf//maxrss: -21MiB (-1.18%)
  • ✅ elab/share_common_rec_app//maxrss: -24MiB (-1.14%)
  • 🟥 vcgen/AdcChain/250/vcgen//wall-clock: +7ms (+10.44%)
  • 🟥 vcgen/IfsJP/80/vcgen//wall-clock: +12ms (+10.20%)
  • and 174 hidden

@sgraf812
sgraf812 marked this pull request as ready for review November 6, 2026 11:14
@sgraf812
sgraf812 requested review from TwoFX and kim-em as code owners November 6, 2026 11:14
@sgraf812
sgraf812 enabled auto-merge November 6, 2026 11:14
@sgraf812 sgraf812 added the changelog-tactics User facing tactics label Nov 6, 2026
@sgraf812 @claude
test: register the PUnit and True rintro rules in the test only
29be2ab 
`PUnit.forall_intro` and `True.forall_intro` move from
`Std.WP.Automation` into `tests/elab/vcgenRIntro.lean`. `vcgen` uses only
`Prod.forall_intro` as a built-in rule, and `True.forall_intro` showed up
in the completions of `True.` in `travellingCompletions`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01D74FF61KPDjY3k6hEEbrmc
@sgraf812
sgraf812 added this pull request to the merge queue Nov 6, 2026
Merged via the queue into leanprover:master with commit d85fd7c Nov 6, 2026
15 checks passed
@sgraf812
sgraf812 deleted the sg/vcgen-rintro branch November 7, 2026 04:29
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.

2 participants

@sgraf812 @leanprover-radar