Work on adding benchmarks based on the Rocq standard library.#3

Merged

triviajon merged 72 commits into

triviajon:mainfrom

DIJamner:stdlib-benchmark-plan

Jul 5, 2026

Commits on Jun 28, 2026

Add plan for Rocq standard library benchmark suite

DIJamner
and
claude
committed
Adapt stdlib benchmark plan to generated induction principles

DIJamner
and
claude
committed
Support constructor via compat prelude in stdlib benchmark plan

DIJamner
and
claude
committed
Add Rocq stdlib benchmark suite

DIJamner
and
claude
committed
Elaborate stdlib statement types via Rocq Set Printing All

DIJamner
and
claude
committed
Expand stdlib corpus with polymorphic eq + existential lemmas

DIJamner
and
claude
committed
Subtract per-engine startup floor from stdlib benchmark times

DIJamner
and
claude
committed
Group stdlib corpus one file per module, matching the library structure

DIJamner
and
claude
committed
Expand stdlib benchmark with computational induction over fixpoints

DIJamner
and
claude
committed
Get list lemmas working in the stdlib benchmark (Lists module)

DIJamner
and
claude
committed
Add statement-vs-stdlib fidelity check to the stdlib benchmark

DIJamner
and
claude
committed
Flip curated add_assoc/app_assoc to match stdlib orientation exactly

DIJamner
and
claude
committed
Separate proofs with blank lines in generated .me for readability

DIJamner
and
claude
committed
Anchor the scatter parity line at the startup-floor cross

DIJamner
and
claude
committed
Give the scatter independent, tightly-padded axes

DIJamner
and
claude
committed
Document the corpus-proof vs stdlib-proof fidelity gap

DIJamner
and
claude
committed
Fix proof-fidelity: MEngine *does* have `;` (and combinators)

DIJamner
and
claude
committed
Add an f_equal approximation to the compat prelude; use it in Lists

DIJamner
and
claude
committed
Document why destr_bool/destruct_all aren't implementable as MEngine tactics

DIJamner
and
claude
committed
Expand stdlib benchmark corpus from 52 to 75 lemmas

DIJamner
and
claude
committed
Fix destruct translation for recursive types (nat/list)

DIJamner
and
claude
committed
Add map/rev to the stdlib benchmark (Lists 5 -> 9 lemmas)

DIJamner
and
claude
committed
Use semicolons in the stdlib benchmark proofs, as the real stdlib does

DIJamner
and
claude
committed
Use `repeat` in the stdlib benchmark, as the real stdlib does

DIJamner
and
claude
committed
Document the parsed-but-stubbed tactic combinators in the benchmark

DIJamner
and
claude
committed
Prove xorb_true_r by reflexivity in the stdlib benchmark, as the real stdlib does

DIJamner
and
claude
committed
Add max/min, sub_succ, map_map, rev_unit to the stdlib benchmark (75 -> 88 lemmas)

DIJamner
and
claude
committed
Plot startup-subtracted proof time, not whole-file time, in the stdlib scatter

DIJamner
and
claude
committed
Show run-to-run noise as error bars in the stdlib scatter

DIJamner
and
claude
committed

Commits on Jul 1, 2026

Commits on Jul 2, 2026

Audit-fix the stdlib benchmark scripts

DIJamner
and
claude
committed

Commits on Jul 3, 2026

Commits on Jul 4, 2026