max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: simplify assumptions in mvcgen' with grind benchmark (#13186)

Browse source 
This PR adds `simplifying_assumptions [Nat.add_assoc]` to the
`vcgen_get_throw_set_grind` benchmark, recovering hypothesis
simplification lost in a54eafb ("refactor: decouple solve from grind").
That refactor introduced `PreTac.processHypotheses` which wraps
`simpNewHyps`, but the call sites in `work` and `main` call
`Grind.processHypotheses` directly, leaving `simpNewHyps` as dead code.
Without it, long `s + 1 + … + 1` chains are never collapsed, causing an
asymptotic slowdown visible by a factor of 2 at n=150 (largest radar
input size).

Benchmark results (VCGen time in ms):

| n | Before | After | Speedup |
|---|--------|-------|---------|
| 50 | 222 | 186 | 1.2× |
| 100 | 391 | 251 | 1.6× |
| 150 | 647 | 329 | 2.0× |
| 200 | 995 | 415 | 2.4× |
| 300 | 1894 | 589 | 3.2× |

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Sebastian Graf 2026-03-30 12:03:43 +02:00 • committed by GitHub
parent 9fc62b7042
commit 75ec8e42c8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean
View file

@ -15,5 +15,7 @@ set_option maxHeartbeats 100000000
-- Benchmark `mvcgen' with grind`: grind integrated into VCGen loop for incremental
-- context internalization. This avoids O(n) re-internalization per VC.
#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail)
-- `simplifying_assumptions [Nat.add_assoc]` here speeds up grind and kernel checking by a factor
-- of 2 because long chains `s + 1 + ... + 1` are collapsed into `s + n`.
#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' simplifying_assumptions [Nat.add_assoc] with grind) `(tactic| fail)
[50, 100, 150]