Work on adding benchmarks based on the Rocq standard library.#3
Merged
Conversation
Adds benchmarks/stdlib/PLAN.md: a plan for a per-file benchmark comparing MEngine vs Rocq on a curated, auto-translatable subset of the Rocq stdlib. No implementation changes — planning artifact only. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Rebased onto induction-principle-with-ih, which makes MEngine generate proper <T>_ind (with induction hypotheses) for parametric and non-parametric inductives. Update the plan accordingly: - Replace the "no induction" stance with an emulation strategy: translate `induction x` to `intro x; apply (T_ind (fun x => <body>)); <cases>`, with the IH named as Rocq does. New section 5a documents the mechanics verified against the engine. - Record the two Tier-2 caveats that still gate computational induction (apply-with-fixpoint-motive segfault; ground-only iota), with pointers to the bugs/ reproducers, and note that closing them is the biggest corpus-expansion lever and is now in scope. - Relax the "do not edit the engine" constraint to an engine baseline, and update the translator rules, compat prelude, roadmap, and risks. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Reframe constructor from a translator hard-stop to a runtime tactic emulated in the compat prelude, the same way split/left/right already are. It needs no engine change: match Goal reads the goal head, first tries constructors in declaration order, and eapply leaves multi-arg constructors' arguments as subgoals. - Sec. 2: move constructor off the "still missing" list. - Sec. 4: pass constructor/constructor n through to the prelude tactic; flag only when the goal head isn't enumerated. Drop it from hard-stop. - New sec. 6a: document the tactic, the constructor n -> eapply C_n shortcut, soundness under "flag, never guess," the leverage (it unblocks the relational lemmas that already work), and limitations (no eexists witness-guessing; a fully generic engine-level version is deferred). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The per-module Rocq-stdlib benchmark machinery: translator, corpus runner, compat prelude, report generator, and the initial Bool/Logic/Nat/le corpus. The enabling kernel fixes it relies on live on the engine-fixes branch this is based on. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The surface translator had to desugar notation and *synthesise* the
implicit type argument of `=`, which failed for any non-nat/bool equality
and for polymorphic lists (eq-type inference and list element types were
the cases we'd given up on).
Replace this for statements: `translate.py --elaborate` replays the unit
through Rocq with `Set Printing All` + one `Check` per statement and
translates the fully-explicit, notation-free type Rocq prints. Every
implicit (the `T` of `@eq T x y`, a list's element type) is already
supplied, so no synthesis is needed and notation/literals are gone.
- New elaborated-form parser (lex_elab/ElabParser/parse_elab) over the
Set Printing All grammar (`@head`, qualified names, multi-binder
forall/fun, `->`); reuses the existing `emit`. Only Nat.* heads are
qualified and are mapped to compat names; other qualified heads are
flagged, never guessed.
- rocq_elaborate(): temp .v + coqc, parse Check output to {name: type}.
- translate_definition/translate_axiom/translate_unit take an `elab` map;
tactic terms and `--report`/`--dir` triage stay on the surface path
(terms in tactics aren't always elaborable).
- stdlib_bench.py `test` runs the translator with --elaborate --coq.
- Drop `From ... Require` so list units' preambles strip cleanly.
All 26 Tier-A units regenerate byte-identically through the new path and
pass the faithfulness gate. Docs (PLAN/README) updated.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The Set Printing All elaboration (prev commit) supplies every implicit argument, so polymorphic statements that the old surface translator could not handle — anything with an implicit type argument it had to synthesise — now translate faithfully. This adds the units that unlock and that prove today (no fixpoint reduction needed on the proof side): - eq (5): eq_refl_x, eq_sym, eq_trans, f_equal, f_equal2 over an arbitrary type A. The `T` of `@eq T x y` (and the `B` of `@eq B (f x) (f y)`) now come straight from Rocq instead of being synthesised. Proved by reflexivity/symmetry/rewrite. - ex (2): ex_intro and `exists y, y = x`. The implicit A of `@ex A P` is now supplied. Emitting these surfaced a translator bug: a binder-headed application argument (the predicate `fun y => …` of `ex A (fun y => …)`) was printed without parentheses, which MEngine's parser rejects. `emit` now parenthesizes fun/forall/arrow arguments. Corpus 26 -> 33 units; all pass the faithfulness gate (rocq compiles, mengine proves, mengine.me re-derivable with no drift). New `eq`/`ex` categories wired through stdlib_bench.py + report.py; README scope updated. Lists stay excluded: statements translate but the proof side still needs symbolic-fixpoint conversion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Whole-file timing was unfair to Rocq: an empty .v already costs ~62 ms (process + auto-loaded Prelude), which is essentially the entire measured time for every trivial unit, so the headline ~30x "speedup" was really a process-startup ratio, not a proof-speed ratio. MEngine likewise pays ~4 ms for prelude + compat before any proof. `run` now times each engine's preamble alone (empty .v for Rocq, compat prelude with no unit for MEngine) with extra trials, stores it as a startup baseline, and `report` subtracts it to isolate the marginal statement+proof cost. Residuals at or below the baseline's own jitter are shown as ~0 (indistinguishable from startup), and the scatter draws both startup floors so the "everything sits on the floor" effect is visible. For the current Tier-A corpus all 33 proofs land below the noise floor on both engines. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The corpus had been split into 33 one-lemma files. That misrepresents how the standard library is organized (coqc compiles a .v module, not a lemma) and guarantees every proof stays below process startup, so the comparison only ever measured startup speed. Consolidate into four module files mirroring the stdlib's own structure — Bool (Coq.Bool.Bool, 11), Logic (Coq.Init.Logic, 13), Nat (Coq.Init.Nat, 5), Peano (Coq.Init.Peano / le, 4). Each mengine.me is regenerated from its consolidated rocq.v via translate.py --elaborate, so the faithfulness gate still holds (4/4 pass). unit_tier/_category now treat a unit as a module; the report shows a per-module lemma count, list shows lemmas per module. Combined with the startup-baseline subtraction, grouping lifts the proof work above the noise floor for the larger modules: Logic now shows a real ~20x startup-subtracted proof speedup (Bool clears the floor too), instead of 33 units all pinned at ~0. Smaller modules (Nat, Peano) still sit within Rocq's startup jitter and are reported honestly as ~0. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Now that symbolic-fixpoint reduction works, the bulk of stdlib arithmetic is reachable by induction. The corpus grows from 33 to 48 Tier-A lemmas: Nat 5->13 (add_0_r, add_succ_r, add_comm, add_assoc, mul_0_r/1_l/1_r, eqb_refl, leb_refl, ... by induction) and Bool 11->18 (more single-variable case analysis). Kernel fixes that unblock the standard `induction; simpl; rewrite IHn` idiom (all pure, soundness-preserving; 431 kernel tests + every examples/*.me pass): - fix_reduction.c / normalize.c: cbv/whnf hold a fixpoint *constant* folded until its decreasing argument is constructor-headed (fix_reduce_app then unfolds and fires it). A stuck recursive call therefore stays headed by the `add`/`mul` constant instead of a bare fix node, so `simpl` makes progress and rewrite/congruence can match it. `add (S n) m` reduces to `S (add n m)` while `add n m` stays matchable. - unify.c / rewrite_internal.c / tactic_interp.c / core.c: `rewrite` works with a *quantified* induction hypothesis whose stored type is the eliminator's beta-redex `(motive) n`. The rewrite path weak-head-normalizes that type before reading off / instantiating the equality, and `_get_lhs_eq` returns NULL (clean failure) instead of dereferencing a non-eq type. - expression.c: init_app_expression_wc no longer pre-rejects a function whose type is a Pi only up to reduction; _construct_app_type already whnfs, so a redex-typed IH can be applied. - type_compat.c: _open_compat records the actual-side hole assignment (symmetric to the expected side) so the eliminator's index evar left by a quantified motive is cascade-filled by fill_hole instead of lingering as a stray open goal. Benchmark/translator: - translate.py emits builtin `rewrite <lemma> with eq` (kernel rewrite engine) instead of the scripted `rewrite_s`, which cannot read the equation off a redex-typed IH; the induction scaffold runs `simpl` after introducing the recursive args + IH so `motive (S x)` is reduced before the case body. - manifest `excluded` updated: computational induction and single-variable case-with-constant-RHS are now Tier A; the remaining boundary is multi-variable/nested case analysis, parametric `list` induction, and induction over an inductive relation. - examples/computational_induction_rewrite.me added as regression coverage for the quantified-IH rewrite path (add_succ_r, add_0_r, add_comm). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Two kernel fixes unblock reduction over parametric inductives, then the benchmark grows a Lists module proved by parametric `list_ind` induction. Kernel: - mixed_subst.c: preserve a match parameter-slot pattern variable's delta-reducible body alias (`_ := A`) when rebuilding a branch under a substitution. Both rebuilders (`_simple_topdown_psubst` and the spine-rebuild path) dropped it, so reducing a fixpoint over a parametric constructor (`app A (cons A x xs) k`) lost the alias, failed to type-check the branch body, and crashed on the resulting NULL. - map.c: `map_new_with_capacity` now rounds up to a power of two. The open-addressing map masks indices with `hash & (capacity - 1)`, valid only for power-of-two capacities. `iota_reduce` sizes its pattern-substitution map to the constructor argument count (3 for `cons`), so a `cons` match built a capacity-3 map whose absent-key lookups probed forever. Benchmark: - compat prelude declares list/option with A as a parameter, so MEngine generates the Rocq-shaped parametric `list_ind`. - translate.py handles parametric induction: peels leading binders to the induction variable, supplies the type parameter to the eliminator (`apply (list_ind A <motive>)`), and reads case-binder names from an `induction l as [| x l IHl]` intro-pattern. - new corpus/Lists module: app_nil_l, app_nil_r, app_assoc, length_app. - manifest no longer excludes parametric list induction; README/PLAN updated. All 431 kernel tests and every examples/*.me still pass; the full corpus (52 lemmas across 5 modules) runs AddressSanitizer-clean through the engine. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
DIJamner
force-pushed
the
stdlib-benchmark-plan
branch
from
c3ded55 to
692636e
Compare
Merged
The corpus rocq.v files are hand-curated re-statements of stdlib lemmas (real stdlib files don't translate to MEngine). That curation step was unverified: a curated statement could silently drift from the library lemma it claims to be. Add `stdlib_bench.py fidelity`, which uses Rocq's own kernel to compare each curated statement to its real counterpart in the installed stdlib: - corpus/stdlib_map.json maps every curated lemma to a stdlib ref (checked convertible via `Check (<ref> : <curated>).`), a mirror ref (`relation: symmetry`, verified by `intros; symmetry; apply <ref>`), or `original` (ground/bespoke, no named stdlib lemma). - The map must cover every curated lemma; unmapped lemmas, stale entries, non-convertible claims, and unresolved refs all fail (exit 1). The check surfaced two real orientation divergences: stdlib Nat.add_assoc and List.app_assoc are stated in the opposite orientation, so the curated add_assoc/app_assoc are their mirrors (now recorded and verified equivalent up to eq_sym). Every ref/relation was confirmed against the installed Rocq (9.0.1) before being recorded — flag, never guess. Result over the current corpus: 39 convertible, 2 symmetry-variant, 11 original, 0 mismatches. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The fidelity check had flagged Nat.add_assoc and List.app_assoc as symmetry-variants: stdlib states them n+(m+p)=(n+m)+p and l++(m++n)= (l++m)++n, while the corpus stated the mirror. Flip both curated statements so every corpus statement is convertible (exact match) to its stdlib counterpart, not merely equivalent up to eq_sym. The proofs are structurally unchanged: goal and induction hypothesis flip together, so the forward `rewrite IH` still fires. Regenerated mengine.me (MEngine still proves both) and manifest digests; updated stdlib_map.json entries to plain convertible and synced README orientation references. Fidelity over the corpus is now 41 convertible, 0 symmetry-variant, 11 original, 0 mismatches. The symmetry mechanism is retained for future curation but no current lemma uses it. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
translate_unit emitted every statement and proof line flat, so a module's proofs ran together with no visual break. Insert a blank line before each top-level item (statement + proof). Regenerated all five corpus .me files; the faithfulness gate still passes (no drift, MEngine runs clean). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The parity diagonal was y = x through the origin, which assumes zero startup. Whole-file time is startup + proof, so y = x makes every point look far below parity — the dishonest, startup-dominated ratio. Draw the honest "equal proof time" line instead: y - m0 = x - r0, a slope-1 line anchored where the two startup floors meet (r0, m0), marked with a dot at the cross. A point on it has equal proof time on both engines; below it MEngine's proof is faster, above it slower. On log-log axes it bends at the floor cross and asymptotes to y = x. Falls back to naive y = x only when no baselines are recorded. This surfaces that Lists is actually slower-proof on MEngine (above the line) while Bool/Logic/Nat/Peano are faster (below) — invisible under the old origin-anchored diagonal. Regenerated the plot + REPORT.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The data now sits in one corner (Rocq is startup-bound ~65ms, MEngine proofs are ~ms), but the axes were a shared square [lo,hi] on both — a leftover from the y=x parity convention — wasting most of the canvas. Set x and y limits independently, each padded around its own data and startup floor. Equal aspect is no longer needed since the parity line is an explicit curve, not a 45° diagonal. The points now fill the plot and are individually legible. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
`fidelity` already checks every curated *statement* is convertible to its
stdlib counterpart. The corpus *proof scripts*, though, are re-derived in
MEngine's tactic subset, not the stdlib's verbatim proofs — and for almost
every lemma they structurally cannot be. This records why, auditably.
Add `proof_fidelity.py` + a `proof-fidelity` subcommand that regenerates
`corpus/PROOF_FIDELITY.md`, re-extracting each lemma's real proof straight
from the installed stdlib (asks `coqc` `About <ref>` for the exact source
location, reads back the verbatim `Proof … Qed` block — flag, never guess)
and classifying the divergence:
- near-match library proof is reflexivity/trivial; corpus matches (5)
- untranslatable concrete script uses destr_bool / `;` / auto / f_equal /
destruct N — tactics MEngine lacks (20)
- functor lemma is Include-generated over the abstract Numbers/
Structures functors (most arithmetic); no concrete-nat
script exists to copy (10)
- constructor maps to an inductive constructor; no proof script at all (6)
- original no named stdlib counterpart (11)
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Correction: the earlier doc wrongly listed `;` sequencing (and `auto`/ `trivial`/`now`) as constructs "MEngine has no equivalent of". MEngine's tactic language has `;`, `||`, `try`, `repeat`, `first […]`, `match Goal` (src/tacticlanguage, TAC_SEQ) and emulates `auto`/`trivial`/`now`/`simpl`/ `symmetry` in the prelude + compat prelude — the corpus proofs use `;` themselves (`split; assumption`). Narrow the blocking set to constructs genuinely absent (the `destr_bool`/ `destruct_all` Ltac macros, `f_equal`, `destruct N`/`destruct H`, `apply … in H`, `discriminate`, `inversion`, `lia`/`ring`, `nzinduct`/`nzsimpl`/ `autorewrite`, `false_hyp`), and add a "weaker emulation" tier for `auto` (present but far weaker than Rocq's hint search) so length_app is explained without claiming a missing combinator. Notes now state explicitly that the gap is leaf tactics, not sequencing. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Implement `Tactic f_equal` in the stdlib-benchmark compat prelude: a single-layer structural congruence built on the kernel's `Bad_App_Congruence` (the same congruence `rewrite` already trusts), so it adds no new axioms. For a goal `eq T (h .. a) (h .. b)` it peels one application layer into the function and argument equalities and discharges the unchanged layer by reflexivity, leaving the differing argument — e.g. `cons A a X = cons A a Y` becomes `X = Y`. It deliberately does not recurse into the argument subgoal (that is the proof obligation, not a congruence — recursing there manufactures false subgoals, which broke app_assoc in an earlier attempt). Wire it through: move `f_equal` from translate.py's UNSUPPORTED to DIRECT_TACTICS, and rewrite the Lists cons cases to use `f_equal` (mirroring the stdlib's own `induction l; simpl; f_equal; auto`) instead of a blunt `rewrite IHl`. The peeled argument is discharged with the IH explicitly (`exact (IHl m n)`) because MEngine's `apply` cannot instantiate the quantified, redex-typed IH. This gives f_equal continuous regression coverage via `test`. Update proof_fidelity.py: f_equal moves from "absent" to the weaker-emulation tier (approximation now exists), and notes/README are corrected accordingly. All gates pass: test 5/5, fidelity 41 convertible / 0 mismatch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
…tactics The Bool corpus is flagged `untranslatable` because the stdlib proves it with the `destr_bool` Ltac macro. Record the concrete obstacles to writing that macro (and the `destruct_all` it builds on) as faithful MEngine tactics: - no goal-abstraction primitive, so the `bool_ind` motive for a hypothesis destruct can't be synthesised (the corpus only abstracts via name-shadowing in literal source); - `eunify` does no higher-order motive inference; - no hypothesis clearing, so `destruct_all`'s recursion wouldn't terminate; - no `discriminate` (vacuous for this corpus, but part of the macro). New DESTR_BOOL_OBSTACLES.md, linked from the proof-fidelity section of the README. No engine changes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Add as much of the Rocq stdlib as MEngine + the compat prelude can prove, auto-translated with zero manual edits and kernel-checked against the installed library (every new statement is `match` in `fidelity`). Nat (13 -> 27): the full additive *and multiplicative* theory now proves — add_succ_l/add_1_l/add_1_r, mul_0_l/mul_succ_l/mul_succ_r/mul_comm, mul_add_distr_r/mul_add_distr_l/mul_assoc, plus sub_0_l/sub_0_r/sub_diag and pred_succ. The multi-step arithmetic proofs interleave `symmetry` (the scripted rewrite only fires on the goal's left side) and use fully-applied lemma instances (`rewrite (mul_comm m n)`) where the leftmost occurrence would be wrong. Bool (18 -> 24): negb_involutive_reverse, andb_negb_r, orb_negb_r, xorb_false_r/xorb_true_l/xorb_true_r. Lists (4 -> 5): app_comm_cons (kept Require-free, so map/rev stay out). Logic (13 -> 14): f_equal3. Peano (4 -> 5): le_succ_diag_r. Compat prelude gains `pred`; translator maps Nat.pred. Regenerated mengine.me, manifest, stdlib_map, PROOF_FIDELITY, results, REPORT, and the scatter. The larger corpus lifts proof time above the startup floor, so the report now shows a real proof-speed comparison (Nat proof ~36 ms MEngine vs ~61 ms Rocq) rather than pure process-startup noise. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
`destruct x` on a recursive type was mistranslated: the translator emulates both `induction` and `destruct` through the same recursive `<T>_ind` (MEngine generates no non-recursive case principle), whose step case always binds an induction hypothesis `P n -> P (S n)`. `induction` introduced it; `destruct` skipped it — but the `P n ->` is physically in the subgoal, so after `intro n` the goal was still an arrow, and the case body's `simpl`/`reflexivity` failed with "No branch matched in match Goal". Only `destruct` on `bool` (no recursive argument, hence no IH) worked. Fix: `destruct` now introduces that eliminator-supplied IH and immediately discards it with a bare `intro.`, exposing `P (ctor ...)` for the case body. The resulting term is exactly what `induction` builds with the IH left unused — a full, Coq-checkable proof — so it stays within flag-never-guess. The `as` clause for `destruct` therefore names only the constructor arguments (`destruct l as [| x l]`), not the IH that `induction`'s names (`induction l as [| x l IHl]`). Demonstrated by reproving `sub_0_r` (n - 0 = n) with `destruct n` (the natural script, and it drops the spurious unused IH the `induction` workaround left). Verified on both nat and the list cons case (non-recursive head + recursive tail). README and PROOF_FIDELITY regenerated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Wires up the List `map`/`rev` theory — map_app, length_map, rev_app_distr,
rev_involutive — all kernel-checked convertible to their stdlib counterparts.
Getting there needed one kernel fix, one translator fix, and a fairness fix to
the timing baseline.
Kernel (src/kernel/expression.c): a match *branch* may now return the matched
parametric inductive. init_match_expression_wc seeded the match's result type
from the first branch *with that branch's pattern-var context*, then checked the
siblings against it; when the seed type names the inductive's parameter (a
`nil A` branch : list A) that context is not an ancestor of a sibling's, so the
sound `list A` == `list A` check spuriously failed ("Branch body types do not
match"). app/length escaped only because their base branch is a variable/`O`.
The seed type is now transported to the outer context by substituting away the
branch's parameter-slot pattern variables (each a delta-alias to a scrutinee
type arg — meaning-preserving). This lets `map`/`rev` be direct Fixpoints, which
stay folded under `simpl` so the rev proofs can `rewrite` a recursive call with
the IH (as the nat arithmetic proofs do). All 431 kernel tests + examples pass.
Translator (translate.py): parse_statement_leading_binder now matches the
binder's parentheses instead of a comma-naive regex, so it can peel a
function-typed leading binder (`f : A -> B`, printed `forall (_ : A), B`) to
reach `induction l` in map_app/length_map.
Fairness (stdlib_bench.py, report.py): Lists alone `Require`s Coq.Lists.List, so
its ~80 ms library load would inflate its startup-subtracted "proof" time
against the empty-.v floor. Added a per-module Rocq startup baseline — each
module's own Require/Import preamble, timed alone — so Lists is measured against
a List-loaded floor (~138 ms) and the load is subtracted, not charged to the
proof. Require-free modules are unchanged.
compat: `map`/`rev` as direct Fixpoints (match Rocq's List defs). Regenerated
mengine.me, manifest, stdlib_map, results, REPORT, scatter, PROOF_FIDELITY;
README documents kernel fix 9 and the per-module baseline.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The corpus proofs spelled out every step as a separate `.`-terminated tactic, while the real stdlib leans on `;` heavily (`induction l; simpl; f_equal; auto`, `split; assumption`, `destr_bool`). Adopt the same `;` idiom across all five modules: - Within-goal chains (`simpl; rewrite IHn; reflexivity`, `simpl; f_equal; exact IHl`, `constructor; constructor`) in Nat/Lists/Peano/Logic. - Boolean case-splits as `destruct b; simpl; reflexivity` (mirroring the stdlib's `destr_bool` = `destruct_all bool; simpl in *; trivial; ...`). translate.py: support a uniform semicolon tail on induction/destruct (`destruct b; t1; t2`). Rocq distributes the chain over every subgoal, but MEngine's cross-goal `;` normalizes the sibling case goals before either is closed, so `simpl`/`cbv` over the shared motive corrupts the not-yet-solved case. The translator instead replays the chain per case, sequentially — same proof term, no cross-goal hazard. Restricted to all-nullary inductives (bool), where no case needs per-case intros. kernel: fix fill_hole for MATCH_*/FIX_* parent uplinks (relations 8+). The switch only rewrote relations 0–7, so filling a hole that is a match scrutinee/branch or fix arg/body silently dropped the term (HoleExpression stores no fill term) and printed "todo: fill_hole for relation N". The Bool corpus alone emitted 20 such warnings. Branch/arg slots are array-indexed and the uplink carries no index, so locate the slot(s) still pointing at the hole and rebind them. make check (431), make examples, and stdlib_bench.py test (5/5) all pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
MEngine has `repeat` (the prelude is built on it: `intros := repeat intro`, `auto := repeat intro; ...`) — the gap was only that translate.py didn't translate it. Add `repeat <atom>` support to the translator (Rocq binds `repeat` tighter than `;`, so the body is a single atom after sentence-level `;` splitting) and adopt the idiom where the stdlib uses it: - Logic/and_intro3: `repeat split; assumption` (was the spelled-out `split. exact HA. split. exact HB. exact HC.`). - Peano le facts (le_succ_diag_r, le_1_2, le_2_4): `repeat constructor` (was `constructor; constructor; ...`). stdlib_bench.py test 5/5; manifest + PROOF_FIDELITY.md regenerated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The fidelity docs listed MEngine's combinators as `;`, `||`, `try`, `repeat`, `first […]`, `match Goal` — all implemented — but didn't note that the grammar also parses `… ; [ t1 | t2 | … ]` (dispatch) and `shelve`, which the interpreter leaves as unimplemented stubs (they raise `Unknown tactic expression`; tactic_interp.c:875-877). Spell out the implemented-vs-stubbed boundary in README.md and the PROOF_FIDELITY.md generator (proof_fidelity.py), and note neither stub is needed by the corpus — no case split closes its branches with different tactics. Regenerated PROOF_FIDELITY.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
… stdlib does A review of every corpus proof against its stdlib counterpart (per corpus/PROOF_FIDELITY.md) found one near-match lemma proved more heavily than the library does: `xorb_true_r` used `destruct b; simpl; reflexivity` while Stdlib.Bool.Bool proves it with a bare `reflexivity` (it is definitionally `negb b`). This was also inconsistent with `xorb_true_l` directly above it, which already uses plain `reflexivity`. The other xorb/bool lemmas keep their case split on purpose: the library proves *them* with `destr_bool`, so a case analysis (not reflexivity) is the faithful rendering even where reflexivity would also close them. - corpus/Bool/rocq.v: xorb_true_r -> `intro b. reflexivity.` - corpus/Bool/mengine.me: regenerated from rocq.v (translate.py). - manifest.json / PROOF_FIDELITY.md: regenerated. Both coqc and MEngine accept the new proof; stdlib_bench.py test (5/5), fidelity (68 convertible, 0 mismatch), and proof-fidelity all pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
…-> 88 lemmas) Expand the Tier-A corpus by 9 lemmas reachable with the existing translator: Nat (27 -> 34): - sub_succ (S n - S m = n - m) by reflexivity - max/min theory: max_0_l, max_0_r, min_0_l, min_0_r (the _0_r cases by destruct), max_id, min_id (by induction) — adds max/min Fixpoints to the compat prelude (nested single-scrutinee, extensionally identical to Nat.max/ Nat.min) and Nat.max/Nat.min to the translator's NAME_MAP. Lists (9 -> 11): - map_map (map g (map f l) = map (g . f) l) by f_equal down to the IH - rev_unit (rev (l ++ [a]) = a :: rev l) straight-line via rev_app_distr All mengine.me files are re-emitted by translate.py --elaborate (zero manual edits); the faithfulness gate, statement-fidelity (88/88 convertible to the installed stdlib), and proof-fidelity all pass, and the manifest/report/scatter are regenerated. No kernel changes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
…T, inline _Cursor - stdlib_bench: return best (None) instead of masking a never-finished run as 0.0 - translate: promote _THM_ALT to public THEOREM_ALT; reuse it in the faithfulness gate - translate: inline the single-use _Cursor base class into TermParser Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
- parse_term and parse_elab shared one grammar; drop parse_elab and the now-dead err_prefix machinery on TermParser - multi-name `intros a b` now expands to `intro a; intro b` (semicolon sequence) instead of period-separated statements, so it composes inside ';' chains naturally and no longer needs special-casing in translate_tactic_sentence Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Cleanups from a review of the stdlib benchmark scripts (no behavior change to the corpus output — Bool re-translates byte-identically, fidelity / proof-fidelity still pass): - Use translate.THEOREM_ALT in fidelity.py / proof_fidelity.py instead of re-joining THEOREM_KEYWORDS inline (the constant existed to be written once). - Centralize the proof-closer keyword set as translate.PROOF_CLOSERS / PROOF_CLOSER_ALT; derive PROOF_FRAMING from it and reuse the alternation in proof_fidelity's three closer regexes and translate_unit's closer check. - Merge translate_elab_type + translate_term into one render_term (they were identical: lex already skips whitespace, so the .strip() was a no-op). - Use clean_coqc_temp for the two baseline temp files instead of clean_coqc_byproducts + a manual os.remove in finally. - test_unit: run the translator in-process (rocq_elaborate -> translate_unit) instead of shelling out to translate.py. - Flag Set/SProp universes as Untranslatable rather than silently mapping them to Prop (flag, never guess). - report._succ_times: drop the pre-per-trial-array back-compat fallback. - time_command: record time_taken=None (not 0.0) for a trial that never ran. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Re-run the full stdlib pipeline against the current translator/engine: - Regenerate corpus mengine.me for Lists/Logic/Nat: the translator now sequences multi-name intros with ';' (`intro n; intro m.`) rather than as separate sentences, so these three were stale since 55a0954. Bool/Peano were already current. Faithfulness gate is now 5/5. - Refresh results/stdlib.json + results/REPORT.md + plots/stdlib_scatter.png from a fresh `run` (proof-only geomean 1.44×, median 1.80× over the 4 modules above the noise floor; Peano stays at/below startup jitter). - Regenerate corpus/PROOF_FIDELITY.md (embeds the corpus proof text, which changed with the intro sequencing). manifest.json unchanged — statement digests are stable, only proof bodies moved. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Previously, `floor is None` returned the raw total — silently reporting the whole-file time (process startup included) as the proof cost, the exact thing the startup subtraction exists to remove. With no baseline there is nothing to subtract, so the proof residual is undefined: return None. Downstream already renders None as `FAIL` in the proof column and drops it from the speedup, so a missing baseline now reads honestly instead of as a spuriously large proof time. (Current results carry valid floors, so REPORT.md and the plot are unchanged; this fixes the latent floor-missing path.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The report's math is now trivial to check by hand: every measurement is the minimum of its trials (best-of-N), and the only spread statistic is the sample standard deviation of the startup-floor trials. From those: proof = max(0, min(whole-file) − min(startup floor)) ~0 when proof <= that engine's floor stddev speedup = Rocq proof / MEngine proof (geomean + median summary) Removed the resampling/percentile machinery that existed only to draw error-bar whiskers: _baseline, _succ_times, _proof_time, _pct, _residual_dist, and the scatter's _axis_stat. The scatter now plots each module at exactly its (Rocq proof, MEngine proof) table values — no resampled median/percentile — so the plot can never disagree with the table; the two startup-noise-floor bands (each = a baseline's trial stddev) replace the per-point whiskers as the "don't trust below here" signal. All the concepts are preserved: per-engine startup subtraction, per-module Rocq floor (Lists' Require load), the noise floor, and the y=x parity scatter. Bumped baseline trials to 25 (cheap, measured once) and per-module trials to 10 so the single min/stddev is solid. Re-ran: proof-only speedup 1.79× geomean / 2.17× median over the 4 modules above the noise floor (Lists still ~2× slower; Peano stays at/below startup jitter). Updated the README scatter description to match (no error bars; noise-floor bands). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Comment-only; REPORT.md, the plot, stdlib.json, and the corpus regenerate
byte-identically.
- stdlib_bench: the baseline-key comment described report's *old* key discovery
("splits on the first '_'"); report now strips a single-underscore engine
prefix (documented at report.py:110). Rewrote the comment to match.
- stdlib_bench: the "Each unit is now a module file (Bool, Logic, Nat, Peano)"
note omitted Lists and used a stale "now"; list all five and drop "now".
- report._load: note that every value is re-derived from the raw per-trial
arrays, never the runner's stored time_taken — so the report is a
self-contained derivation an auditor can recheck.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
1. Single-source the proof-cost math. successful_times / sample_stddev / proof_time now live in stdlib_bench and are imported by report, so the `run` console summary and REPORT.md apply identical definitions. cmd_run's progress line now also applies the noise floor: a below-noise module (Peano) prints ~0 / — instead of a spurious 14.88x, matching the report. 2. Drop the vestigial `category` field from the manifest (== name, read by nothing since the scatter switched to `unit`). Regenerated manifest.json. 3. Add a manifest-staleness gate. compute_manifest (pure) backs both build_manifest and a new manifest_staleness check; `test` now flags corpus/manifest.json when a re-generated rocq.v/mengine.me would leave its digests stale, and fails the gate. Verified it catches drift (it flagged the pre-regen category mismatch) and passes when current. 4. load_config's trials default 5 -> 10 (matches config.json). Clarified the REPORT.md startup-floor prose: the shown Rocq ± is the global empty-.v floor, but each module subtracts its own Require/Import floor (Lists' ~2× larger) and the ~0 test uses that module's own floor ±. Re-ran: proof-only speedup 1.83× geomean / 2.24× median over the 4 modules above the noise floor; Lists still ~2× slower, Peano at/below startup jitter. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
- `clean` removes every generated file (the 5 auto-translated mengine.me, manifest.json, PROOF_FIDELITY.md, results/stdlib.json, results/REPORT.md, plots/stdlib_scatter.png) and keeps the hand-authored sources. - `regen` rebuilds them all from source in dependency order: re-translate each rocq.v -> mengine.me (in-process, same pipeline as translate.py's CLI) -> manifest -> proof-fidelity -> run -> report. Both are driven by a single `generated_files(cfg)` list, so "what is generated" has one source of truth. Verified a full clean+regen cycle: the deterministic generators (translator, manifest, proof-fidelity) reproduce byte-identical files; only the timing artifacts differ run-to-run. README usage updated. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
A function returning two unrelated statistics is poor form. `_geomean` now returns just the geometric mean; the median is `_median` (already separate); the call site computes both explicitly (`geo, med = _geomean(s), _median(s)`). REPORT.md and the plot regenerate byte-identically. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The MEngine (horizontal) and Rocq (vertical) startup-noise bands are the same concept on different axes, so they now render identically: - alpha unified to 0.10 (was 0.12 for the MEngine band, an arbitrary difference); - added a matching "Rocq noise floor" label (only the MEngine band was labeled). Cosmetic only — REPORT.md and the timing data are unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Restores per-point run-to-run uncertainty (dropped in the report simplification) without the old resampling/percentile machinery. Each dot is still exactly its REPORT.md proof value (best-of-N); it now carries a one-sided whisker on each axis up to the slowest of the N trials — length = that module's whole-file max − min, with the floor held at its min. Two numbers per whisker, nothing resampled, so the plot stays as auditable as the table. _load records mengine_total_max / rocq_total_max for the whisker ends; the axis upper bound accounts for whisker tops. Peano's whisker running deep into the noise band now visibly flags it as startup-dominated. README + title updated; REPORT.md and the timing data are unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Dropped the 45° rotation and repositioned it into the clear upper-left triangle below the legend, so it reads horizontally and mirrors the flat "MEngine faster" banner in the opposite half. Cosmetic only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Cut the module/function docstrings and inline comments down to short, code-focused notes, and collapse a few duplicated code paths, without changing behavior. The check still passes for all curated lemmas. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Drop proof_fidelity.py, the generated corpus/PROOF_FIDELITY.md, and the 'proof-fidelity' subcommand, along with its wiring in regen/clean and its docs. DESTR_BOOL_OBSTACLES.md is kept (it documents an engine limitation) with its dangling PROOF_FIDELITY.md link removed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Condense the ~420-line design dump to the operator essentials (corpus, layout, commands, the test/fidelity gates) plus the core rationale (Set-Printing-All translation, startup-subtracted proof timing, Tier A scope). Drop the per-fix kernel changelog and the repeated prose. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Delegate the sample standard deviation to the stdlib instead of reimplementing it; keep the 0.0-for-<2-points guard, where statistics.stdev would raise. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Drop the 0.0 guard so statistics.stdev's StatisticsError propagates. Baselines run >=25 trials, so a <2-point sample means the measurement is broken; masking it as a zero noise floor would make every proof residual read as real instead of ~0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Remove the one-line wrapper and its cross-module import; both stdlib_bench and report now call statistics.stdev at the use sites. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Drop the hand-rolled _median and _geomean (and the now-unused math import) in favor of the stdlib functions, same as the stddev change. REPORT.md and the plot regenerate byte-identically. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
The corpus is fixed, so the tier vocabulary (Tier A, Tier B, Tier-2) no longer carries meaning. Rephrase docs, comments, Untranslatable messages, and the manifest's tier/boundary fields to describe what is and isn't handled without the tier labels; regenerate manifest.json and REPORT.md. Also drop the stale 'list reasoning deferred' note (Lists is supported). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
regen and clean are the only pipeline entry points, so drop the standalone list/run/report/manifest subcommands and the unused units/modules selectors. Keep test and fidelity as by-hand correctness gates (now always over the whole corpus); keep run/report/manifest as internal steps regen calls. With no selectors left, no command reads argparse args, so dispatch on cfg alone and drop the args parameter throughout. fidelity.run loses its modules parameter. Update both READMEs. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Remove every quantitative figure that could fall out of sync with the real corpus/tests: the module/lemma counts and the Lemmas column, the startup/timing figures (~4/65/138 ms), the ~2x factor, the ~6 s fidelity cost, and the ~1/16 translate ratio; convert the test-gate ordered list to bullets. Kept: 'python3' (interpreter name) and the literal '~0' report marker, neither of which is a measurement. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Human review of the readme.
Contributor
Author
|
@triviajon I've reviewed everything but the C code to a sufficient extent to believe that the results are likely accurate. If you could confirm that the C bugfixes make sense, then this is ready to merge. |
triviajon
approved these changes
Jul 5, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Warning: the code in this PR was AI-generated and is not yet human-validated. It should be treated with suspicion until reviewed line-by-line or rewritten.
This is a draft PR to document progress. It is not suitable for merging.
This PR documents the work on translating standard library files to serve as a Rocq-Mengine benchmark. It depends on the bug fixes in #4 . It also includes code to fix some additional bugs, generated by LLM. That code definitely points to something useful, but may or may not itself be what we want.