From 75ec8e42c82ff31010beb2245ffadda3d72374a4 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 30 Mar 2026 12:03:43 +0200 Subject: [PATCH] test: simplify assumptions in `mvcgen' with grind` benchmark (#13186) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean b/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean index ceee64a96d..bcebf50ec7 100644 --- a/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean +++ b/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean @@ -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]