diff --git a/.gitignore b/.gitignore index e85c843..794b742 100644 --- a/.gitignore +++ b/.gitignore @@ -58,6 +58,10 @@ results/ !benchmarks/plots/** !benchmarks/results/ !benchmarks/results/** +!benchmarks/stdlib/plots/ +!benchmarks/stdlib/plots/** +!benchmarks/stdlib/results/ +!benchmarks/stdlib/results/** benchmarks/flame_trends/ # Local profiling and packaging artifacts. diff --git a/benchmarks/README.md b/benchmarks/README.md index c39a80d..aea5eec 100644 --- a/benchmarks/README.md +++ b/benchmarks/README.md @@ -53,3 +53,16 @@ python3 bench.py plot rewrite_nm --fixed m=3 ## Adding a Benchmark Create `benchmarks/my_benchmark.py` with a class extending `Benchmark`. The registry, CLI, and plotter pick it up automatically. + +## Rocq standard-library benchmark + +A separate, fixed-corpus suite comparing MEngine vs Rocq on auto-translated +stdlib lemmas lives under [`stdlib/`](stdlib/README.md). It is driven by its own +runner (it iterates a manifest rather than sweeping a parameter range): + +```bash +python3 stdlib/stdlib_bench.py regen # rebuild every generated file (translate, time, report) +python3 stdlib/stdlib_bench.py test # faithfulness gate +python3 stdlib/stdlib_bench.py fidelity # statement vs the real stdlib +python3 stdlib/stdlib_bench.py clean # remove generated files +``` diff --git a/benchmarks/config.json b/benchmarks/config.json index 8221494..e6c2d97 100644 --- a/benchmarks/config.json +++ b/benchmarks/config.json @@ -11,6 +11,14 @@ "max_consecutive_failures": 2, "trials": 2, "coq_timeout_multiplier": 1.5, + "stdlib": { + "corpus_dir": "stdlib/corpus", + "compat": "stdlib/compat/stdlib_compat.me", + "results": "stdlib/results/stdlib.json", + "plots_dir": "stdlib/plots", + "timeout": 20, + "trials": 10 + }, "mengine_variants": { "baseline": { "path": "~/mengine/build/ablations/mengine-baseline", diff --git a/benchmarks/stdlib/README.md b/benchmarks/stdlib/README.md new file mode 100644 index 0000000..932a553 --- /dev/null +++ b/benchmarks/stdlib/README.md @@ -0,0 +1,136 @@ +# Rocq standard-library benchmark for MEngine + +Per-module benchmark comparing **MEngine** against **Rocq** on a curated, +mechanically-translated subset of the Rocq standard library. Each unit is one +stdlib **module** — a `.v` file grouping that module's lemmas, mirroring the +library's own file structure. + +| Module | Source | +|---------|-----------------------------------------------------| +| `Bool` | `Coq.Bool.Bool` | +| `Lists` | `Coq.Lists.List` (app/length/map/rev over `list A`) | +| `Logic` | `Coq.Init.Logic` (eq, and/or, ex) | +| `Nat` | `Coq.Init.Nat` (inductive arithmetic, max/min) | +| `Peano` | `Coq.Init.Peano` (the `le` order) | + +## Layout + +``` +benchmarks/stdlib/ + translate.py Rocq .v -> MEngine .me translator (via Rocq `Set Printing All`) + stdlib_bench.py runner: test / fidelity / clean / regen + report.py markdown table + log-log scatter plot + fidelity.py statement-vs-stdlib correspondence check (via Rocq's kernel) + compat/stdlib_compat.me compat prelude: nat/bool/list/option + pred/max/min/le + emulated tactics + corpus/ + manifest.json locked corpus + per-statement digests + excluded boundary + stdlib_map.json each curated lemma -> its real stdlib counterpart + per-module file(s) + /rocq.v benchmarked Rocq source (hand-curated) + /mengine.me auto-translated MEngine source + results/ generated: stdlib.json (timings) + REPORT.md (table) + plots/stdlib_scatter.png generated scatter +``` + +## Usage + +```bash +cd benchmarks +python3 stdlib/stdlib_bench.py regen # rebuild every generated file, in dependency order +python3 stdlib/stdlib_bench.py clean # remove every generated file (keep sources) +python3 stdlib/stdlib_bench.py test # faithfulness gate (see below) +python3 stdlib/stdlib_bench.py fidelity # check each statement vs the real stdlib +``` + +`regen` rebuilds every generated file from source in order (mengine.me -> +manifest -> run -> report); `clean` removes them. Hand-authored sources +(`rocq.v`, `stdlib_map.json`, the compat prelude) are never touched. `test` and +`fidelity` check that the benchmarks are consistent between Rocq and MEngine +and relate to the actual standard library, respectively. + + +## Translation (`Set Printing All`) + +MEngine has no notation system and no elaboration, so notation, implicits, and +numeric literals must all be made explicit. Rather than re-implement Rocq's +elaborator, `translate.py` replays each unit through Rocq with `Set Printing All` +and translates the fully-explicit, notation-free form it prints (so a working +`coqc`/`rocq`, `--coq`, is required): + +``` +(* surface *) forall (A:Type) (l:list A), nil ++ l = l +(* Printing All *) forall (A : Type) (l : list A), @eq (list A) (@app A (@nil A) l) l +(* MEngine *) forall (A : Type), forall (l : (list A)), (((eq (list A)) (((app A) (nil A)) l)) l) +``` + +Every implicit is supplied by Rocq, so no type synthesis is needed. Terms inside +*tactics* are still translated from surface source. The guiding principle is +**flag, never guess**: any construct it cannot translate soundly is reported and +the unit excluded, never mistranslated (a wrong translation that happened to +compile would silently benchmark two *different* theorems). + +## Timing + +`run` times each unit end-to-end in both engines (whole process, best of N). +Both pay a fixed startup — MEngine loads `prelude/tactics.me` + compat, Rocq +loads its prelude — which at this problem size dominates the whole-file number. +To isolate proof cost, `run` also times each engine's preamble *alone* as a +startup floor: for Rocq, each module's Require/Import commands, +and for MEngine, the statements in the preamble. +`report` subtracts each module's floor (clamped at zero). +A residual at or below the floor's run-to-run jitter is reported `~0`. + +`plots/stdlib_scatter.png` plots each module's own-floor-subtracted proof +time (Rocq x vs MEngine y, log-log, parity `y = x`) — the same pair as its +REPORT.md row. Whole-file time would be dishonest: `Lists`' one-time `List` load +would drop it below any single parity line and read as an MEngine win, when on +proof cost MEngine is actually *slower* on `map`/`rev` induction. Whiskers run to +the slowest trial; shaded bands at each engine's startup-noise floor (the std-dev +of its baseline trials) mark where a residual stops being trustworthy. + +## `test` — faithfulness gate + +Per unit, before any timing: + +- `rocq.v` compiles under `coqc`. +- `mengine.me` runs clean under `mengine -q` (compat prelude prepended). +- `mengine.me` is exactly what `translate.py` re-emits from `rocq.v` (no drift), + with matching theorem names. + +Needs `coqc` on `PATH` (or `coq_path` in `config.json`). + +## `fidelity` — statement vs the real stdlib + +`test` checks that `.me` faithfully follows `.v`; it does **not** check that the +hand-curated `.v` statement matches the stdlib lemma it claims to be. +`fidelity` closes that gap with Rocq's own kernel: +`corpus/stdlib_map.json` records each module's source file(s) and +maps every lemma to a stdlib ref. The ref is qualified with the file (`andb_diag` +→ `Stdlib.Bool.Bool.andb_diag`) and checked by `Check (. : +).`, which passes iff the lemma both belongs to that file and +is convertible to the curated one. An unmapped lemma, a stale map entry, a +missing/absent ref, or a non-convertible match all fail (non-zero exit). Because +it shells out to `coqc` once per lemma it is slower than `test` and kept separate; +run it after editing any statement or the map. + +## Scope + +The computational/structural corner reachable by MEngine + the compat prelude: + +- **Bool** — identities by ground reduction and single-variable `destruct`. +- **Nat** — `add`/`mul`/`sub` reductions and computational induction over the + `add`/`mul` fixpoints (the full additive/multiplicative theory up to + `mul_assoc` and both distributive laws), plus the `max`/`min` identities. +- **Lists** — parametric `list` induction: `app`/`length` plus the `map`/`rev` + theory (`map_app`, `map_map`, `rev_app_distr`, `rev_involutive`, …). +- **`le` / order** — structural induction with a fixpoint-free motive. +- **Logic** — propositional introduction (`split`/`left`/`right`/`apply`). +- **Polymorphic `eq` / `ex`** — over an arbitrary type, unlocked by the + `Set Printing All` elaboration supplying the implicit type argument. + +## Why not verbatim stdlib files + +Running the translator over the installed stdlib per file, essentially none +translate whole, even in `Coq.Init`: real files are saturated with +`Notation`/`Ltac`/`Variant`/`Register`/multi-scrutinee `match`/qualified names. +Hence the corpus is curated lemmas drawn from stdlib content, grouped one file +per module to mirror the library's structure. diff --git a/benchmarks/stdlib/compat/stdlib_compat.me b/benchmarks/stdlib/compat/stdlib_compat.me new file mode 100644 index 0000000..fb01e9a --- /dev/null +++ b/benchmarks/stdlib/compat/stdlib_compat.me @@ -0,0 +1,215 @@ +(* stdlib_compat.me — compatibility prelude for the Rocq-stdlib benchmark. + + Loaded ahead of every translated unit (the translator prepends it). It + supplies the base datatypes and functions that the Rocq standard library + assumes but that MEngine's C core (src/runtime/core.c) does not provide + (core.c only defines eq/and/or/ex/Reflexive), plus a handful of emulated + tactics written in the tactic language. + + Each datatype/function mirrors the *semantics* of its Rocq counterpart so + that a translated theorem statement denotes the same proposition and ground + computation reduces identically. Function bodies use single-scrutinee + matches (MEngine has no multi-scrutinee match); this is extensionally equal + to Rocq's definitions, which is all the benchmark requires. + + Every emulated tactic carries a comment stating exactly how it differs from + Rocq's, so divergence is auditable in one place. *) + +(* ── Base datatypes ─────────────────────────────────────────────────── *) + +Inductive True : Prop := | I : True. + +Inductive bool : Type := | true : bool | false : bool. + +Inductive nat : Type := +| O : nat +| S : forall (n : nat), nat. + +(* list/option take A as a *parameter* (not an index): MEngine then generates the + Rocq-shaped parametric eliminator + list_ind : forall (A : Type) (P : list A -> Prop), + P (nil A) -> (forall x l, P l -> P (cons A x l)) -> forall l, P l + so `induction` on a list translates to `apply (list_ind A )`. The + constructor types are identical to the index form (the parameter is just a + leading forall), so every statement and the app/length fixpoints are unchanged. *) +Inductive list (A : Type) : Type := +| nil : list A +| cons : forall (x : A), forall (l : list A), list A. + +Inductive option (A : Type) : Type := +| None : option A +| Some : forall (x : A), option A. + +(* ── bool functions (Coq.Init.Datatypes) ───────────────────────────── *) + +Definition negb : forall (_ : bool), bool := + fun (b : bool) => match b with | true => false | false => true end. + +Definition andb : forall (_ : bool), forall (_ : bool), bool := + fun (b1 : bool) => fun (b2 : bool) => match b1 with | true => b2 | false => false end. + +Definition orb : forall (_ : bool), forall (_ : bool), bool := + fun (b1 : bool) => fun (b2 : bool) => match b1 with | true => true | false => b2 end. + +Definition implb : forall (_ : bool), forall (_ : bool), bool := + fun (b1 : bool) => fun (b2 : bool) => match b1 with | true => b2 | false => true end. + +Definition xorb : forall (_ : bool), forall (_ : bool), bool := + fun (b1 : bool) => fun (b2 : bool) => + match b1 with + | true => match b2 with | true => false | false => true end + | false => b2 + end. + +(* ── nat functions (Coq.Init.Nat) ──────────────────────────────────── *) + +Fixpoint add (n : nat) (m : nat) {struct n} : nat := + match n with | O => m | S p => S (add p m) end. + +Fixpoint mul (n : nat) (m : nat) {struct n} : nat := + match n with | O => O | S p => add m (mul p m) end. + +(* sub: Rocq matches on both n and m; here nested single-scrutinee matches. *) +Fixpoint sub (n : nat) (m : nat) {struct n} : nat := + match n with + | O => O + | S k => match m with | O => n | S l => sub k l end + end. + +Fixpoint eqb (n : nat) (m : nat) {struct n} : bool := + match n with + | O => match m with | O => true | S q => false end + | S p => match m with | O => false | S q => eqb p q end + end. + +Fixpoint leb (n : nat) (m : nat) {struct n} : bool := + match n with + | O => true + | S p => match m with | O => false | S q => leb p q end + end. + +Definition ltb : forall (_ : nat), forall (_ : nat), bool := + fun (n : nat) => fun (m : nat) => leb (S n) m. + +(* pred (Coq.Init.Nat): predecessor, with pred O = O. *) +Definition pred : forall (_ : nat), nat := + fun (n : nat) => match n with | O => O | S k => k end. + +(* max/min (Coq.Init.Nat): Rocq matches on both n and m; here nested + single-scrutinee matches, extensionally identical (the `S p, O` arm returns + the outer scrutinee `n` = `S p`, exactly as Nat.max/Nat.min do). *) +Fixpoint max (n : nat) (m : nat) {struct n} : nat := + match n with + | O => m + | S p => match m with | O => n | S q => S (max p q) end + end. + +Fixpoint min (n : nat) (m : nat) {struct n} : nat := + match n with + | O => O + | S p => match m with | O => O | S q => S (min p q) end + end. + +(* ── list functions (Coq.Lists.List / Coq.Init.Datatypes) ──────────── *) + +Fixpoint app (A : Type) (l : list A) (k : list A) {struct l} : list A := + match l with + | nil _ => k + | cons _ x xs => cons A x (app A xs k) + end. + +Fixpoint length (A : Type) (l : list A) {struct l} : nat := + match l with + | nil _ => O + | cons _ x xs => S (length A xs) + end. + +Fixpoint map (A : Type) (B : Type) (f : forall (_ : A), B) (l : list A) {struct l} : list B := + match l with + | nil _ => nil B + | cons _ x xs => cons B (f x) (map A B f xs) + end. + +(* rev: Coq.Lists.List's naive reverse, rev (x :: xs) = rev xs ++ (x :: nil). *) +Fixpoint rev (A : Type) (l : list A) {struct l} : list A := + match l with + | nil _ => nil A + | cons _ x xs => app A (rev A xs) (cons A x (nil A)) + end. + +(* ── Relational predicates (Coq.Init.Peano / Coq.Init.Datatypes) ───── *) + +(* le, as in Coq.Init.Peano: le n n and le n m -> le n (S m). *) +Inductive le : forall (_ : nat), forall (_ : nat), Prop := +| le_n : forall (n : nat), le n n +| le_S : forall (n : nat), forall (m : nat), forall (_ : le n m), le n (S m). + +(* ── Emulated tactics ──────────────────────────────────────────────── *) + +(* reflexivity (override): build `eq_refl A x` for a goal `eq A x y` and let + the kernel's conversion checker verify `x` converts to `y`. Differs from + the prelude's reflexivity, which matches `eq ?A ?x ?x` purely syntactically + (pointer equality) and so cannot close a goal whose two sides are equal only + up to computation, e.g. `eq nat (add (S O) O) (S O)`. Like Rocq's + `reflexivity`, it fails (cleanly) when the sides are not convertible. *) +Tactic reflexivity := match Goal with +| [ |- (((eq ?A) ?x) ?y) ] => exact ((eq_refl A) x) +end. + +(* symmetry := apply eq_sym. eq_sym : forall A x y, eq A x y -> eq A y x, so + applying it to `eq A y x` leaves the subgoal `eq A x y`. Identical to Rocq. *) +Tactic symmetry := apply eq_sym. + +(* simpl := cbv (full beta/delta/iota/fix normalization). Rocq's simpl is a + heuristic partial reduction that avoids unfolding some applications; cbv is + strictly more aggressive but agrees with simpl whenever simpl makes progress + on the closed/structural goals in this corpus. *) +Tactic simpl := cbv. + +(* trivial / easy / now : close trivial goals. Rocq's are stronger (trivial + runs a hint database; easy/now also discharge by `congruence`/`lia`-free + automation). Here: try reflexivity, then try assumption. *) +Tactic trivial := try reflexivity; try assumption. +Tactic easy := intros; try reflexivity; try assumption. +Tactic now := intros; try reflexivity; try assumption. + +(* constructor (sec. 6a): generalization of split/left/right. One arm per + inductive whose constructors this corpus uses. `first` tries them in + declaration order, exactly like Rocq's `constructor`. Each arm builds a + full proof term, so this stays sound under flag-never-guess. Witness-guessing + (constructor on `ex`, i.e. eexists) is intentionally excluded. *) +Tactic constructor := match Goal with +| [ |- True ] => exact I +| [ |- ((and ?A) ?B) ] => eapply ((conj A) B) +| [ |- ((or ?A) ?B) ] => first [ eapply ((or_introl A) B) | eapply ((or_intror A) B) ] +| [ |- ((le ?n) ?m) ] => first [ eapply (le_n n) | eapply (le_S n) ] +end. + +(* f_equal (approximation): reduce a goal `eq T (h .. a) (h .. b)` to its + differing-argument subgoals, discharging the unchanged layers by reflexivity. + Built on the kernel congruence `Bad_App_Congruence : forall A B (f g : A -> B) + (x y : A), f = g -> x = y -> f x = g y` — the *same* congruence the prelude's + `rewrite` is built on — so it adds no new trust. One application layer of the + goal becomes two subgoals, `eq (A -> T) f g` (the function) and `eq A x y` + (the argument); `try reflexivity` closes the layers that didn't change and the + recursive `try f_equal` peels nested applications, so `f_equal` on + `cons A a X = cons A a Y` leaves exactly `X = Y`. + + How it differs from Rocq's `f_equal`: it peels exactly one application layer + and reads the head `?f`/`?g` off the goal first-order (no higher-order + unification). `try reflexivity` discharges the function subgoal when the head + is unchanged (the common case — `cons A a`, `S`) and the argument subgoal when + the arguments are convertible, leaving any genuinely-different argument as the + single remaining goal. It deliberately does **not** recurse into that + argument subgoal: an argument that is itself a compound application (e.g. + `app A l (app A m n)`) is the proof obligation to discharge (here, by the + induction hypothesis), not a congruence to peel further — recursing there + would manufacture false subgoals. So this is a single-layer structural + congruence adequate for the `cons`/`S` goals an induction step produces, not a + general multi-argument `f_equal`. A bare `f_equal` on a non-application + equality fails (no match arm), as Rocq's does. *) +Tactic f_equal := match Goal with +| [ |- (((eq ?T) (?f ?x)) (?g ?y)) ] => + let A := type_of x in + apply ((((((Bad_App_Congruence A) T) f) g) x) y); try reflexivity +end. diff --git a/benchmarks/stdlib/corpus/Bool/mengine.me b/benchmarks/stdlib/corpus/Bool/mengine.me new file mode 100644 index 0000000..bbe2a94 --- /dev/null +++ b/benchmarks/stdlib/corpus/Bool/mengine.me @@ -0,0 +1,113 @@ +Theorem andb_true_l : forall (b : bool), (((eq bool) ((andb true) b)) b). +intro b. +reflexivity. + +Theorem andb_false_l : forall (b : bool), (((eq bool) ((andb false) b)) false). +intro b. +reflexivity. + +Theorem andb_true_r : forall (b : bool), (((eq bool) ((andb b) true)) b). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((andb b) true)) b))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem andb_false_r : forall (b : bool), (((eq bool) ((andb b) false)) false). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((andb b) false)) false))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem andb_b_b : forall (b : bool), (((eq bool) ((andb b) b)) b). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((andb b) b)) b))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem orb_true_l : forall (b : bool), (((eq bool) ((orb true) b)) true). +intro b. +reflexivity. + +Theorem orb_false_l : forall (b : bool), (((eq bool) ((orb false) b)) b). +intro b. +reflexivity. + +Theorem orb_true_r : forall (b : bool), (((eq bool) ((orb b) true)) true). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((orb b) true)) true))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem orb_false_r : forall (b : bool), (((eq bool) ((orb b) false)) b). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((orb b) false)) b))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem orb_b_b : forall (b : bool), (((eq bool) ((orb b) b)) b). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((orb b) b)) b))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem negb_involutive : forall (b : bool), (((eq bool) (negb (negb b))) b). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) (negb (negb b))) b))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem negb_involutive_reverse : forall (b : bool), (((eq bool) b) (negb (negb b))). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) b) (negb (negb b))))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem andb_negb_r : forall (b : bool), (((eq bool) ((andb b) (negb b))) false). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((andb b) (negb b))) false))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem orb_negb_r : forall (b : bool), (((eq bool) ((orb b) (negb b))) true). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((orb b) (negb b))) true))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem implb_true_l : forall (b : bool), (((eq bool) ((implb true) b)) b). +intro b. +reflexivity. + +Theorem implb_false_l : forall (b : bool), (((eq bool) ((implb false) b)) true). +intro b. +reflexivity. + +Theorem implb_b_b : forall (b : bool), (((eq bool) ((implb b) b)) true). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((implb b) b)) true))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem xorb_false_l : forall (b : bool), (((eq bool) ((xorb false) b)) b). +intro b. +reflexivity. + +Theorem xorb_false_r : forall (b : bool), (((eq bool) ((xorb b) false)) b). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((xorb b) false)) b))). +simpl; reflexivity. +simpl; reflexivity. + +Theorem xorb_true_l : forall (b : bool), (((eq bool) ((xorb true) b)) (negb b)). +intro b. +reflexivity. + +Theorem xorb_true_r : forall (b : bool), (((eq bool) ((xorb b) true)) (negb b)). +intro b. +reflexivity. + +Theorem xorb_b_b : forall (b : bool), (((eq bool) ((xorb b) b)) false). +intro b. +apply (bool_ind (fun (b : bool) => (((eq bool) ((xorb b) b)) false))). +simpl; reflexivity. +simpl; reflexivity. diff --git a/benchmarks/stdlib/corpus/Bool/rocq.v b/benchmarks/stdlib/corpus/Bool/rocq.v new file mode 100644 index 0000000..02d5da1 --- /dev/null +++ b/benchmarks/stdlib/corpus/Bool/rocq.v @@ -0,0 +1,71 @@ +(* Bool: Tier-A units from Coq.Init.Datatypes / Coq.Bool.Bool — decidable + identities closed by ground reduction or single boolean case analysis. The + case-analysis lemmas mirror the standard library's own `destr_bool` + (≈ `destruct_all bool; simpl in *; trivial; try discriminate`) with a uniform + semicolon tail: `destruct b; reflexivity`. *) + +Lemma andb_true_l : forall b : bool, andb true b = b. +Proof. intro b. reflexivity. Qed. + +Lemma andb_false_l : forall b : bool, andb false b = false. +Proof. intro b. reflexivity. Qed. + +Lemma andb_true_r : forall b : bool, andb b true = b. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma andb_false_r : forall b : bool, andb b false = false. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma andb_b_b : forall b : bool, andb b b = b. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma orb_true_l : forall b : bool, orb true b = true. +Proof. intro b. reflexivity. Qed. + +Lemma orb_false_l : forall b : bool, orb false b = b. +Proof. intro b. reflexivity. Qed. + +Lemma orb_true_r : forall b : bool, orb b true = true. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma orb_false_r : forall b : bool, orb b false = b. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma orb_b_b : forall b : bool, orb b b = b. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma negb_involutive : forall b : bool, negb (negb b) = b. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma negb_involutive_reverse : forall b : bool, b = negb (negb b). +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma andb_negb_r : forall b : bool, andb b (negb b) = false. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma orb_negb_r : forall b : bool, orb b (negb b) = true. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma implb_true_l : forall b : bool, implb true b = b. +Proof. intro b. reflexivity. Qed. + +Lemma implb_false_l : forall b : bool, implb false b = true. +Proof. intro b. reflexivity. Qed. + +Lemma implb_b_b : forall b : bool, implb b b = true. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma xorb_false_l : forall b : bool, xorb false b = b. +Proof. intro b. reflexivity. Qed. + +Lemma xorb_false_r : forall b : bool, xorb b false = b. +Proof. destruct b; simpl; reflexivity. Qed. + +Lemma xorb_true_l : forall b : bool, xorb true b = negb b. +Proof. intro b. reflexivity. Qed. + +Lemma xorb_true_r : forall b : bool, xorb b true = negb b. +Proof. intro b. reflexivity. Qed. + +Lemma xorb_b_b : forall b : bool, xorb b b = false. +Proof. destruct b; simpl; reflexivity. Qed. diff --git a/benchmarks/stdlib/corpus/Lists/mengine.me b/benchmarks/stdlib/corpus/Lists/mengine.me new file mode 100644 index 0000000..b180ae1 --- /dev/null +++ b/benchmarks/stdlib/corpus/Lists/mengine.me @@ -0,0 +1,125 @@ +Theorem app_nil_l : forall (A : Type), forall (l : (list A)), (((eq (list A)) (((app A) (nil A)) l)) l). +intro A; intro l. +reflexivity. + +Theorem app_nil_r : forall (A : Type), forall (l : (list A)), (((eq (list A)) (((app A) l) (nil A))) l). +intro A. +intro l. +apply (list_ind A (fun (l : (list A)) => (((eq (list A)) (((app A) l) (nil A))) l))). +simpl. +reflexivity. +intro x. +intro l. +intro IHl. +simpl. +simpl; f_equal; exact (IHl). + +Theorem app_comm_cons : forall (A : Type), forall (l : (list A)), forall (m : (list A)), forall (a : A), (((eq (list A)) (((cons A) a) (((app A) l) m))) (((app A) (((cons A) a) l)) m)). +intro A; intro l; intro m; intro a. +reflexivity. + +Theorem app_assoc : forall (A : Type), forall (l : (list A)), forall (m : (list A)), forall (n : (list A)), (((eq (list A)) (((app A) l) (((app A) m) n))) (((app A) (((app A) l) m)) n)). +intro A. +intro l. +apply (list_ind A (fun (l : (list A)) => forall (m : (list A)), forall (n : (list A)), (((eq (list A)) (((app A) l) (((app A) m) n))) (((app A) (((app A) l) m)) n)))). +simpl. +intro m. +intro n. +reflexivity. +intro x. +intro l. +intro IHl. +simpl. +intro m. +intro n. +simpl; f_equal; exact (((IHl m) n)). + +Theorem length_app : forall (A : Type), forall (l : (list A)), forall (m : (list A)), (((eq nat) ((length A) (((app A) l) m))) ((add ((length A) l)) ((length A) m))). +intro A. +intro l. +apply (list_ind A (fun (l : (list A)) => forall (m : (list A)), (((eq nat) ((length A) (((app A) l) m))) ((add ((length A) l)) ((length A) m))))). +simpl. +intro m. +reflexivity. +intro x. +intro l. +intro IHl. +simpl. +intro m. +simpl; f_equal; exact ((IHl m)). + +Theorem map_app : forall (A : Type), forall (B : Type), forall (f : forall (_ : A), B), forall (l : (list A)), forall (m : (list A)), (((eq (list B)) ((((map A) B) f) (((app A) l) m))) (((app B) ((((map A) B) f) l)) ((((map A) B) f) m))). +intro A. +intro B. +intro f. +intro l. +apply (list_ind A (fun (l : (list A)) => forall (m : (list A)), (((eq (list B)) ((((map A) B) f) (((app A) l) m))) (((app B) ((((map A) B) f) l)) ((((map A) B) f) m))))). +simpl. +intro m. +reflexivity. +intro x. +intro l. +intro IHl. +simpl. +intro m. +simpl; f_equal; exact ((IHl m)). + +Theorem length_map : forall (A : Type), forall (B : Type), forall (f : forall (_ : A), B), forall (l : (list A)), (((eq nat) ((length B) ((((map A) B) f) l))) ((length A) l)). +intro A. +intro B. +intro f. +intro l. +apply (list_ind A (fun (l : (list A)) => (((eq nat) ((length B) ((((map A) B) f) l))) ((length A) l)))). +simpl. +reflexivity. +intro x. +intro l. +intro IHl. +simpl. +simpl; f_equal; exact (IHl). + +Theorem rev_app_distr : forall (A : Type), forall (l : (list A)), forall (m : (list A)), (((eq (list A)) ((rev A) (((app A) l) m))) (((app A) ((rev A) m)) ((rev A) l))). +intro A. +intro l. +apply (list_ind A (fun (l : (list A)) => forall (m : (list A)), (((eq (list A)) ((rev A) (((app A) l) m))) (((app A) ((rev A) m)) ((rev A) l))))). +simpl. +intro m. +simpl; symmetry; rewrite app_nil_r with eq; reflexivity. +intro x. +intro l. +intro IHl. +simpl. +intro m. +simpl; rewrite IHl with eq; symmetry; rewrite app_assoc with eq; reflexivity. + +Theorem rev_involutive : forall (A : Type), forall (l : (list A)), (((eq (list A)) ((rev A) ((rev A) l))) l). +intro A. +intro l. +apply (list_ind A (fun (l : (list A)) => (((eq (list A)) ((rev A) ((rev A) l))) l))). +simpl. +reflexivity. +intro x. +intro l. +intro IHl. +simpl. +simpl; rewrite rev_app_distr with eq; simpl; rewrite IHl with eq; reflexivity. + +Theorem map_map : forall (A : Type), forall (B : Type), forall (C : Type), forall (f : forall (_ : A), B), forall (g : forall (_ : B), C), forall (l : (list A)), (((eq (list C)) ((((map B) C) g) ((((map A) B) f) l))) ((((map A) C) (fun (x : A) => (g (f x)))) l)). +intro A. +intro B. +intro C. +intro f. +intro g. +intro l. +apply (list_ind A (fun (l : (list A)) => (((eq (list C)) ((((map B) C) g) ((((map A) B) f) l))) ((((map A) C) (fun (x : A) => (g (f x)))) l)))). +simpl. +reflexivity. +intro x. +intro l. +intro IHl. +simpl. +simpl; f_equal; exact (IHl). + +Theorem rev_unit : forall (A : Type), forall (l : (list A)), forall (a : A), (((eq (list A)) ((rev A) (((app A) l) (((cons A) a) (nil A))))) (((cons A) a) ((rev A) l))). +intro A; intro l; intro a. +rewrite rev_app_distr with eq; simpl; reflexivity. diff --git a/benchmarks/stdlib/corpus/Lists/rocq.v b/benchmarks/stdlib/corpus/Lists/rocq.v new file mode 100644 index 0000000..3067002 --- /dev/null +++ b/benchmarks/stdlib/corpus/Lists/rocq.v @@ -0,0 +1,82 @@ +(* Lists: Tier-A structural-induction units over `list A` (Coq.Init.Datatypes / + Coq.Lists.List). These exercise parametric induction — `apply (list_ind A + )` — which is reachable now that the kernel reduces a fixpoint over a + parametric constructor (`app A (cons A x xs) k`) and preserves a match + parameter slot's delta alias under substitution. app/length are in + `Coq.Init.Datatypes` (auto-loaded), but `map`/`rev` live in `Coq.Lists.List`, + so this module (alone in the corpus) `Require`s it — and the benchmark times + that load against this module's *own* Require/Import preamble baseline, not + the empty-Prelude floor, so the library load is subtracted rather than charged + to the proof. + + `induction l` keeps any binder after `l` (here `m`, `n`) quantified in both the + goal and the induction hypothesis, so each case introduces them first. The + cons case then uses `f_equal` to peel the shared head (`cons x _`) / successor + (`S _`), mirroring the standard library's own proofs (`induction l; simpl; + f_equal; auto`); MEngine's compat prelude supplies a single-layer `f_equal` + (compat/stdlib_compat.me). Where the stdlib closes the peeled argument goal + with `auto`, here it is discharged explicitly with the induction hypothesis + (MEngine's `apply` cannot instantiate the quantified, redex-typed IH, so the + IH is applied by hand via `exact (IHl m n)`). *) + +From Stdlib Require Import Lists.List. +Import ListNotations. +Open Scope list_scope. + +Lemma app_nil_l : forall (A : Type) (l : list A), nil ++ l = l. +Proof. intros A l. reflexivity. Qed. + +Lemma app_nil_r : forall (A : Type) (l : list A), l ++ nil = l. +Proof. induction l as [| x l IHl]. + - reflexivity. + - simpl; f_equal; exact IHl. +Qed. + +Lemma app_comm_cons : forall (A : Type) (l m : list A) (a : A), a :: (l ++ m) = (a :: l) ++ m. +Proof. intros A l m a. reflexivity. Qed. + +Lemma app_assoc : forall (A : Type) (l m n : list A), l ++ (m ++ n) = (l ++ m) ++ n. +Proof. induction l as [| x l IHl]. + - intro m. intro n. reflexivity. + - intro m. intro n. simpl; f_equal; exact (IHl m n). +Qed. + +Lemma length_app : forall (A : Type) (l m : list A), length (l ++ m) = length l + length m. +Proof. induction l as [| x l IHl]. + - intro m. reflexivity. + - intro m. simpl; f_equal; exact (IHl m). +Qed. + +Lemma map_app : forall (A B : Type) (f : A -> B) (l m : list A), map f (l ++ m) = map f l ++ map f m. +Proof. induction l as [| x l IHl]. + - intro m. reflexivity. + - intro m. simpl; f_equal; exact (IHl m). +Qed. + +Lemma length_map : forall (A B : Type) (f : A -> B) (l : list A), length (map f l) = length l. +Proof. induction l as [| x l IHl]. + - reflexivity. + - simpl; f_equal; exact IHl. +Qed. + +Lemma rev_app_distr : forall (A : Type) (l m : list A), rev (l ++ m) = rev m ++ rev l. +Proof. induction l as [| x l IHl]. + - intro m. simpl; symmetry; rewrite app_nil_r; reflexivity. + - intro m. simpl; rewrite IHl; symmetry; rewrite app_assoc; reflexivity. +Qed. + +Lemma rev_involutive : forall (A : Type) (l : list A), rev (rev l) = l. +Proof. induction l as [| x l IHl]. + - reflexivity. + - simpl; rewrite rev_app_distr; simpl; rewrite IHl; reflexivity. +Qed. + +Lemma map_map : forall (A B C : Type) (f : A -> B) (g : B -> C) (l : list A), + map g (map f l) = map (fun x => g (f x)) l. +Proof. induction l as [| x l IHl]. + - reflexivity. + - simpl; f_equal; exact IHl. +Qed. + +Lemma rev_unit : forall (A : Type) (l : list A) (a : A), rev (l ++ a :: nil) = a :: rev l. +Proof. intros A l a. rewrite rev_app_distr; simpl; reflexivity. Qed. diff --git a/benchmarks/stdlib/corpus/Logic/mengine.me b/benchmarks/stdlib/corpus/Logic/mengine.me new file mode 100644 index 0000000..e906b03 --- /dev/null +++ b/benchmarks/stdlib/corpus/Logic/mengine.me @@ -0,0 +1,39 @@ +Theorem eq_refl_x : forall (A : Type), forall (x : A), (((eq A) x) x). +intro A; intro x. +reflexivity. + +Theorem eq_sym_ex : forall (A : Type), forall (x : A), forall (y : A), forall (_ : (((eq A) x) y)), (((eq A) y) x). +intro A; intro x; intro y; intro H. +symmetry; exact (H). + +Theorem eq_trans_ex : forall (A : Type), forall (x : A), forall (y : A), forall (z : A), forall (_ : (((eq A) x) y)), forall (_ : (((eq A) y) z)), (((eq A) x) z). +intro A; intro x; intro y; intro z; intro H1; intro H2. +rewrite H1 with eq; exact (H2). + +Theorem f_equal_ex : forall (A : Type), forall (B : Type), forall (f : forall (_ : A), B), forall (x : A), forall (y : A), forall (_ : (((eq A) x) y)), (((eq B) (f x)) (f y)). +intro A; intro B; intro f; intro x; intro y; intro H. +rewrite H with eq; reflexivity. + +Theorem f_equal2_ex : forall (A : Type), forall (B : Type), forall (C : Type), forall (f : forall (_ : A), forall (_ : B), C), forall (x1 : A), forall (y1 : A), forall (x2 : B), forall (y2 : B), forall (_ : (((eq A) x1) y1)), forall (_ : (((eq B) x2) y2)), (((eq C) ((f x1) x2)) ((f y1) y2)). +intro A; intro B; intro C; intro f; intro x1; intro y1; intro x2; intro y2; intro H1; intro H2. +rewrite H1 with eq; rewrite H2 with eq; reflexivity. + +Theorem f_equal3_ex : forall (A1 : Type), forall (A2 : Type), forall (A3 : Type), forall (B : Type), forall (f : forall (_ : A1), forall (_ : A2), forall (_ : A3), B), forall (x1 : A1), forall (y1 : A1), forall (x2 : A2), forall (y2 : A2), forall (x3 : A3), forall (y3 : A3), forall (_ : (((eq A1) x1) y1)), forall (_ : (((eq A2) x2) y2)), forall (_ : (((eq A3) x3) y3)), (((eq B) (((f x1) x2) x3)) (((f y1) y2) y3)). +intro A1; intro A2; intro A3; intro B; intro f; intro x1; intro y1; intro x2; intro y2; intro x3; intro y3; intro H1; intro H2; intro H3. +rewrite H1 with eq; rewrite H2 with eq; rewrite H3 with eq; reflexivity. + +Theorem and_intro : forall (A : Prop), forall (B : Prop), forall (_ : A), forall (_ : B), ((and A) B). +intro A; intro B; intro HA; intro HB. +split; assumption. + +Theorem or_introl_ex : forall (A : Prop), forall (B : Prop), forall (_ : A), ((or A) B). +intro A; intro B; intro HA. +left; assumption. + +Theorem or_intror_ex : forall (A : Prop), forall (B : Prop), forall (_ : B), ((or A) B). +intro A; intro B; intro HB. +right; assumption. + +Theorem ex_intro_ex : forall (A : Type), forall (P : forall (_ : A), Prop), forall (x : A), forall (_ : (P x)), ((ex A) (fun (y : A) => (P y))). +intro A; intro P; intro x; intro H. +exists (x); exact (H). diff --git a/benchmarks/stdlib/corpus/Logic/rocq.v b/benchmarks/stdlib/corpus/Logic/rocq.v new file mode 100644 index 0000000..835051a --- /dev/null +++ b/benchmarks/stdlib/corpus/Logic/rocq.v @@ -0,0 +1,31 @@ +(* Logic: Tier-A units drawn from Coq.Init.Logic. *) + +Lemma eq_refl_x : forall (A : Type) (x : A), x = x. +Proof. intros A x. reflexivity. Qed. + +Lemma eq_sym_ex : forall (A : Type) (x y : A), x = y -> y = x. +Proof. intros A x y H. symmetry; exact H. Qed. + +Lemma eq_trans_ex : forall (A : Type) (x y z : A), x = y -> y = z -> x = z. +Proof. intros A x y z H1 H2. rewrite H1; exact H2. Qed. + +Lemma f_equal_ex : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y. +Proof. intros A B f x y H. rewrite H; reflexivity. Qed. + +Lemma f_equal2_ex : forall (A B C : Type) (f : A -> B -> C) (x1 y1 : A) (x2 y2 : B), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2. +Proof. intros A B C f x1 y1 x2 y2 H1 H2. rewrite H1; rewrite H2; reflexivity. Qed. + +Lemma f_equal3_ex : forall (A1 A2 A3 B : Type) (f : A1 -> A2 -> A3 -> B) (x1 y1 : A1) (x2 y2 : A2) (x3 y3 : A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. +Proof. intros A1 A2 A3 B f x1 y1 x2 y2 x3 y3 H1 H2 H3. rewrite H1; rewrite H2; rewrite H3; reflexivity. Qed. + +Lemma and_intro : forall A B : Prop, A -> B -> A /\ B. +Proof. intros A B HA HB. split; assumption. Qed. + +Lemma or_introl_ex : forall A B : Prop, A -> A \/ B. +Proof. intros A B HA. left; assumption. Qed. + +Lemma or_intror_ex : forall A B : Prop, B -> A \/ B. +Proof. intros A B HB. right; assumption. Qed. + +Lemma ex_intro_ex : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists y, P y. +Proof. intros A P x H. exists x; exact H. Qed. diff --git a/benchmarks/stdlib/corpus/Nat/mengine.me b/benchmarks/stdlib/corpus/Nat/mengine.me new file mode 100644 index 0000000..039beef --- /dev/null +++ b/benchmarks/stdlib/corpus/Nat/mengine.me @@ -0,0 +1,257 @@ +Theorem add_0_l : forall (n : nat), (((eq nat) ((add O) n)) n). +intro n. +reflexivity. + +Theorem add_succ_l : forall (n : nat), forall (m : nat), (((eq nat) ((add (S n)) m)) (S ((add n) m))). +intro n; intro m. +reflexivity. + +Theorem add_1_l : forall (n : nat), (((eq nat) ((add (S O)) n)) (S n)). +intro n. +reflexivity. + +Theorem add_1_r : forall (n : nat), (((eq nat) ((add n) (S O))) (S n)). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((add n) (S O))) (S n)))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem add_0_r : forall (n : nat), (((eq nat) ((add n) O)) n). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((add n) O)) n))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem add_succ_r : forall (n : nat), forall (m : nat), (((eq nat) ((add n) (S m))) (S ((add n) m))). +intro n. +apply (nat_ind (fun (n : nat) => forall (m : nat), (((eq nat) ((add n) (S m))) (S ((add n) m))))). +simpl. +intro m. +reflexivity. +intro n. +intro IHn. +simpl. +intro m. +simpl; rewrite IHn with eq; reflexivity. + +Theorem add_comm : forall (n : nat), forall (m : nat), (((eq nat) ((add n) m)) ((add m) n)). +intro n. +apply (nat_ind (fun (n : nat) => forall (m : nat), (((eq nat) ((add n) m)) ((add m) n)))). +simpl. +intro m. +simpl; symmetry; rewrite add_0_r with eq; reflexivity. +intro n. +intro IHn. +simpl. +intro m. +simpl; rewrite IHn with eq; symmetry; rewrite add_succ_r with eq; reflexivity. + +Theorem add_assoc : forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((add n) ((add m) p))) ((add ((add n) m)) p)). +intro n. +apply (nat_ind (fun (n : nat) => forall (m : nat), forall (p : nat), (((eq nat) ((add n) ((add m) p))) ((add ((add n) m)) p)))). +simpl. +intro m. +intro p. +reflexivity. +intro n. +intro IHn. +simpl. +intro m. +intro p. +simpl; rewrite IHn with eq; reflexivity. + +Theorem mul_0_l : forall (n : nat), (((eq nat) ((mul O) n)) O). +intro n. +reflexivity. + +Theorem mul_0_r : forall (n : nat), (((eq nat) ((mul n) O)) O). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((mul n) O)) O))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem mul_succ_l : forall (n : nat), forall (m : nat), (((eq nat) ((mul (S n)) m)) ((add ((mul n) m)) m)). +intro n; intro m. +simpl; rewrite add_comm with eq; reflexivity. + +Theorem mul_succ_r : forall (n : nat), forall (m : nat), (((eq nat) ((mul n) (S m))) ((add ((mul n) m)) n)). +intro n. +apply (nat_ind (fun (n : nat) => forall (m : nat), (((eq nat) ((mul n) (S m))) ((add ((mul n) m)) n)))). +simpl. +intro m. +reflexivity. +intro n. +intro IHn. +simpl. +intro m. +simpl; rewrite IHn with eq; rewrite add_assoc with eq; symmetry; rewrite add_succ_r with eq; reflexivity. + +Theorem mul_comm : forall (n : nat), forall (m : nat), (((eq nat) ((mul n) m)) ((mul m) n)). +intro n. +apply (nat_ind (fun (n : nat) => forall (m : nat), (((eq nat) ((mul n) m)) ((mul m) n)))). +simpl. +intro m. +simpl; symmetry; rewrite mul_0_r with eq; reflexivity. +intro n. +intro IHn. +simpl. +intro m. +simpl; rewrite IHn with eq; symmetry; rewrite mul_succ_r with eq; rewrite add_comm with eq; reflexivity. + +Theorem mul_add_distr_r : forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((mul ((add n) m)) p)) ((add ((mul n) p)) ((mul m) p))). +intro n. +apply (nat_ind (fun (n : nat) => forall (m : nat), forall (p : nat), (((eq nat) ((mul ((add n) m)) p)) ((add ((mul n) p)) ((mul m) p))))). +simpl. +intro m. +intro p. +reflexivity. +intro n. +intro IHn. +simpl. +intro m. +intro p. +simpl; rewrite IHn with eq; rewrite add_assoc with eq; reflexivity. + +Theorem mul_add_distr_l : forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((mul n) ((add m) p))) ((add ((mul n) m)) ((mul n) p))). +intro n; intro m; intro p. +rewrite mul_comm with eq; rewrite mul_add_distr_r with eq; rewrite ((mul_comm m) n) with eq; rewrite ((mul_comm p) n) with eq; reflexivity. + +Theorem mul_assoc : forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((mul n) ((mul m) p))) ((mul ((mul n) m)) p)). +intro n. +apply (nat_ind (fun (n : nat) => forall (m : nat), forall (p : nat), (((eq nat) ((mul n) ((mul m) p))) ((mul ((mul n) m)) p)))). +simpl. +intro m. +intro p. +reflexivity. +intro n. +intro IHn. +simpl. +intro m. +intro p. +simpl; rewrite IHn with eq; symmetry; rewrite mul_add_distr_r with eq; reflexivity. + +Theorem mul_1_l : forall (n : nat), (((eq nat) ((mul (S O)) n)) n). +intro n. +simpl; rewrite add_0_r with eq; reflexivity. + +Theorem mul_1_r : forall (n : nat), (((eq nat) ((mul n) (S O))) n). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((mul n) (S O))) n))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem sub_0_l : forall (n : nat), (((eq nat) ((sub O) n)) O). +intro n. +reflexivity. + +Theorem sub_0_r : forall (n : nat), (((eq nat) ((sub n) O)) n). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((sub n) O)) n))). +simpl. +reflexivity. +intro n. +intro. +simpl. +reflexivity. + +Theorem sub_diag : forall (n : nat), (((eq nat) ((sub n) n)) O). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((sub n) n)) O))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem sub_succ : forall (n : nat), forall (m : nat), (((eq nat) ((sub (S n)) (S m))) ((sub n) m)). +intro n; intro m. +reflexivity. + +Theorem max_0_l : forall (n : nat), (((eq nat) ((max O) n)) n). +intro n. +reflexivity. + +Theorem max_0_r : forall (n : nat), (((eq nat) ((max n) O)) n). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((max n) O)) n))). +simpl. +reflexivity. +intro n. +intro. +simpl. +reflexivity. + +Theorem min_0_l : forall (n : nat), (((eq nat) ((min O) n)) O). +intro n. +reflexivity. + +Theorem min_0_r : forall (n : nat), (((eq nat) ((min n) O)) O). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((min n) O)) O))). +simpl. +reflexivity. +intro n. +intro. +simpl. +reflexivity. + +Theorem max_id : forall (n : nat), (((eq nat) ((max n) n)) n). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((max n) n)) n))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem min_id : forall (n : nat), (((eq nat) ((min n) n)) n). +intro n. +apply (nat_ind (fun (n : nat) => (((eq nat) ((min n) n)) n))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem pred_succ : forall (n : nat), (((eq nat) (pred (S n))) n). +intro n. +reflexivity. + +Theorem eqb_refl : forall (n : nat), (((eq bool) ((eqb n) n)) true). +intro n. +apply (nat_ind (fun (n : nat) => (((eq bool) ((eqb n) n)) true))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. + +Theorem leb_refl : forall (n : nat), (((eq bool) ((leb n) n)) true). +intro n. +apply (nat_ind (fun (n : nat) => (((eq bool) ((leb n) n)) true))). +simpl. +reflexivity. +intro n. +intro IHn. +simpl. +simpl; rewrite IHn with eq; reflexivity. diff --git a/benchmarks/stdlib/corpus/Nat/rocq.v b/benchmarks/stdlib/corpus/Nat/rocq.v new file mode 100644 index 0000000..26a6a91 --- /dev/null +++ b/benchmarks/stdlib/corpus/Nat/rocq.v @@ -0,0 +1,153 @@ +(* Nat: Tier-A units from Coq.Init.Nat / Coq.Arith. Computational induction over + the add/mul fixpoints, now reachable thanks to the symbolic-fixpoint reduction + fix and quantified-IH rewriting. *) + +Lemma add_0_l : forall n : nat, 0 + n = n. +Proof. intro n. reflexivity. Qed. + +Lemma add_succ_l : forall n m : nat, S n + m = S (n + m). +Proof. intros n m. reflexivity. Qed. + +Lemma add_1_l : forall n : nat, 1 + n = S n. +Proof. intro n. reflexivity. Qed. + +Lemma add_1_r : forall n : nat, n + 1 = S n. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma add_0_r : forall n : nat, n + 0 = n. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma add_succ_r : forall n m : nat, n + S m = S (n + m). +Proof. induction n. + - intro m. reflexivity. + - intro m. simpl; rewrite IHn; reflexivity. +Qed. + +Lemma add_comm : forall n m : nat, n + m = m + n. +Proof. induction n. + - intro m. simpl; symmetry; rewrite add_0_r; reflexivity. + - intro m. simpl; rewrite IHn; symmetry; rewrite add_succ_r; reflexivity. +Qed. + +Lemma add_assoc : forall n m p : nat, n + (m + p) = (n + m) + p. +Proof. induction n. + - intro m. intro p. reflexivity. + - intro m. intro p. simpl; rewrite IHn; reflexivity. +Qed. + +Lemma mul_0_l : forall n : nat, 0 * n = 0. +Proof. intro n. reflexivity. Qed. + +Lemma mul_0_r : forall n : nat, n * 0 = 0. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma mul_succ_l : forall n m : nat, S n * m = n * m + m. +Proof. intros n m. simpl; rewrite add_comm; reflexivity. Qed. + +Lemma mul_succ_r : forall n m : nat, n * S m = n * m + n. +Proof. induction n. + - intro m. reflexivity. + - intro m. simpl; rewrite IHn; rewrite add_assoc; symmetry; rewrite add_succ_r; reflexivity. +Qed. + +Lemma mul_comm : forall n m : nat, n * m = m * n. +Proof. induction n. + - intro m. simpl; symmetry; rewrite mul_0_r; reflexivity. + - intro m. simpl; rewrite IHn; symmetry; rewrite mul_succ_r; rewrite add_comm; reflexivity. +Qed. + +Lemma mul_add_distr_r : forall n m p : nat, (n + m) * p = n * p + m * p. +Proof. induction n. + - intro m. intro p. reflexivity. + - intro m. intro p. simpl; rewrite IHn; rewrite add_assoc; reflexivity. +Qed. + +Lemma mul_add_distr_l : forall n m p : nat, n * (m + p) = n * m + n * p. +Proof. intros n m p. rewrite mul_comm; rewrite mul_add_distr_r; rewrite (mul_comm m n); rewrite (mul_comm p n); reflexivity. Qed. + +Lemma mul_assoc : forall n m p : nat, n * (m * p) = n * m * p. +Proof. induction n. + - intro m. intro p. reflexivity. + - intro m. intro p. simpl; rewrite IHn; symmetry; rewrite mul_add_distr_r; reflexivity. +Qed. + +Lemma mul_1_l : forall n : nat, 1 * n = n. +Proof. intro n. simpl; rewrite add_0_r; reflexivity. Qed. + +Lemma mul_1_r : forall n : nat, n * 1 = n. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma sub_0_l : forall n : nat, 0 - n = 0. +Proof. intro n. reflexivity. Qed. + +Lemma sub_0_r : forall n : nat, n - 0 = n. +Proof. destruct n. + - reflexivity. + - reflexivity. +Qed. + +Lemma sub_diag : forall n : nat, n - n = 0. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma sub_succ : forall n m : nat, S n - S m = n - m. +Proof. intros n m. reflexivity. Qed. + +Lemma max_0_l : forall n : nat, Nat.max 0 n = n. +Proof. intro n. reflexivity. Qed. + +Lemma max_0_r : forall n : nat, Nat.max n 0 = n. +Proof. destruct n. + - reflexivity. + - reflexivity. +Qed. + +Lemma min_0_l : forall n : nat, Nat.min 0 n = 0. +Proof. intro n. reflexivity. Qed. + +Lemma min_0_r : forall n : nat, Nat.min n 0 = 0. +Proof. destruct n. + - reflexivity. + - reflexivity. +Qed. + +Lemma max_id : forall n : nat, Nat.max n n = n. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma min_id : forall n : nat, Nat.min n n = n. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma pred_succ : forall n : nat, Nat.pred (S n) = n. +Proof. intro n. reflexivity. Qed. + +Lemma eqb_refl : forall n : nat, Nat.eqb n n = true. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. + +Lemma leb_refl : forall n : nat, Nat.leb n n = true. +Proof. induction n. + - reflexivity. + - simpl; rewrite IHn; reflexivity. +Qed. diff --git a/benchmarks/stdlib/corpus/Peano/mengine.me b/benchmarks/stdlib/corpus/Peano/mengine.me new file mode 100644 index 0000000..9218d19 --- /dev/null +++ b/benchmarks/stdlib/corpus/Peano/mengine.me @@ -0,0 +1,17 @@ +Theorem le_refl_n : forall (n : nat), ((le n) n). +intro n. +constructor. + +Theorem le_0_n : forall (n : nat), ((le O) n). +intro n. +apply (nat_ind (fun (n : nat) => ((le O) n))). +simpl. +constructor. +intro n. +intro IHn. +simpl. +constructor; exact (IHn). + +Theorem le_succ_diag_r : forall (n : nat), ((le n) (S n)). +intro n. +repeat constructor. diff --git a/benchmarks/stdlib/corpus/Peano/rocq.v b/benchmarks/stdlib/corpus/Peano/rocq.v new file mode 100644 index 0000000..81e5737 --- /dev/null +++ b/benchmarks/stdlib/corpus/Peano/rocq.v @@ -0,0 +1,13 @@ +(* Peano: Tier-A units drawn from Coq.Init.Peano (the le order). *) + +Lemma le_refl_n : forall n : nat, n <= n. +Proof. intro n. constructor. Qed. + +Lemma le_0_n : forall n : nat, 0 <= n. +Proof. induction n. + - constructor. + - constructor; exact IHn. +Qed. + +Lemma le_succ_diag_r : forall n : nat, n <= S n. +Proof. intro n. repeat constructor. Qed. diff --git a/benchmarks/stdlib/corpus/manifest.json b/benchmarks/stdlib/corpus/manifest.json new file mode 100644 index 0000000..786a0c5 --- /dev/null +++ b/benchmarks/stdlib/corpus/manifest.json @@ -0,0 +1,361 @@ +{ + "description": "Rocq stdlib units auto-translated with zero manual edits and proved by MEngine + the compat prelude.", + "engine_note": "Requires the cbv applied-fix and GC-dedup kernel fixes (see benchmarks/stdlib/README.md).", + "units": [ + { + "name": "Bool", + "rocq_sha256": "e877d7ae98cfade8", + "statements": [ + { + "name": "andb_true_l", + "digest": "forall (b : bool), (((eq bool) ((andb true) b)) b)" + }, + { + "name": "andb_false_l", + "digest": "forall (b : bool), (((eq bool) ((andb false) b)) false)" + }, + { + "name": "andb_true_r", + "digest": "forall (b : bool), (((eq bool) ((andb b) true)) b)" + }, + { + "name": "andb_false_r", + "digest": "forall (b : bool), (((eq bool) ((andb b) false)) false)" + }, + { + "name": "andb_b_b", + "digest": "forall (b : bool), (((eq bool) ((andb b) b)) b)" + }, + { + "name": "orb_true_l", + "digest": "forall (b : bool), (((eq bool) ((orb true) b)) true)" + }, + { + "name": "orb_false_l", + "digest": "forall (b : bool), (((eq bool) ((orb false) b)) b)" + }, + { + "name": "orb_true_r", + "digest": "forall (b : bool), (((eq bool) ((orb b) true)) true)" + }, + { + "name": "orb_false_r", + "digest": "forall (b : bool), (((eq bool) ((orb b) false)) b)" + }, + { + "name": "orb_b_b", + "digest": "forall (b : bool), (((eq bool) ((orb b) b)) b)" + }, + { + "name": "negb_involutive", + "digest": "forall (b : bool), (((eq bool) (negb (negb b))) b)" + }, + { + "name": "negb_involutive_reverse", + "digest": "forall (b : bool), (((eq bool) b) (negb (negb b)))" + }, + { + "name": "andb_negb_r", + "digest": "forall (b : bool), (((eq bool) ((andb b) (negb b))) false)" + }, + { + "name": "orb_negb_r", + "digest": "forall (b : bool), (((eq bool) ((orb b) (negb b))) true)" + }, + { + "name": "implb_true_l", + "digest": "forall (b : bool), (((eq bool) ((implb true) b)) b)" + }, + { + "name": "implb_false_l", + "digest": "forall (b : bool), (((eq bool) ((implb false) b)) true)" + }, + { + "name": "implb_b_b", + "digest": "forall (b : bool), (((eq bool) ((implb b) b)) true)" + }, + { + "name": "xorb_false_l", + "digest": "forall (b : bool), (((eq bool) ((xorb false) b)) b)" + }, + { + "name": "xorb_false_r", + "digest": "forall (b : bool), (((eq bool) ((xorb b) false)) b)" + }, + { + "name": "xorb_true_l", + "digest": "forall (b : bool), (((eq bool) ((xorb true) b)) (negb b))" + }, + { + "name": "xorb_true_r", + "digest": "forall (b : bool), (((eq bool) ((xorb b) true)) (negb b))" + }, + { + "name": "xorb_b_b", + "digest": "forall (b : bool), (((eq bool) ((xorb b) b)) false)" + } + ], + "deps": "Coq.Init (auto-loaded)" + }, + { + "name": "Lists", + "rocq_sha256": "bf27ff9a508134f4", + "statements": [ + { + "name": "app_nil_l", + "digest": "forall (A : Type), forall (l : (list A)), (((eq (list A)) (((app A) (nil A)) l)) l)" + }, + { + "name": "app_nil_r", + "digest": "forall (A : Type), forall (l : (list A)), (((eq (list A)) (((app A) l) (nil A))) l)" + }, + { + "name": "app_comm_cons", + "digest": "forall (A : Type), forall (l : (list A)), forall (m : (list A)), forall (a : A), (((eq (list A)) (((cons A) a) (((app A) l) m))) (((app A) (((cons A) a) l)) m))" + }, + { + "name": "app_assoc", + "digest": "forall (A : Type), forall (l : (list A)), forall (m : (list A)), forall (n : (list A)), (((eq (list A)) (((app A) l) (((app A) m) n))) (((app A) (((app A) l) m)) n))" + }, + { + "name": "length_app", + "digest": "forall (A : Type), forall (l : (list A)), forall (m : (list A)), (((eq nat) ((length A) (((app A) l) m))) ((add ((length A) l)) ((length A) m)))" + }, + { + "name": "map_app", + "digest": "forall (A : Type), forall (B : Type), forall (f : forall (_ : A), B), forall (l : (list A)), forall (m : (list A)), (((eq (list B)) ((((map A) B) f) (((app A) l) m))) (((app B) ((((map A) B) f) l)) ((((map A) B) f) m)))" + }, + { + "name": "length_map", + "digest": "forall (A : Type), forall (B : Type), forall (f : forall (_ : A), B), forall (l : (list A)), (((eq nat) ((length B) ((((map A) B) f) l))) ((length A) l))" + }, + { + "name": "rev_app_distr", + "digest": "forall (A : Type), forall (l : (list A)), forall (m : (list A)), (((eq (list A)) ((rev A) (((app A) l) m))) (((app A) ((rev A) m)) ((rev A) l)))" + }, + { + "name": "rev_involutive", + "digest": "forall (A : Type), forall (l : (list A)), (((eq (list A)) ((rev A) ((rev A) l))) l)" + }, + { + "name": "map_map", + "digest": "forall (A : Type), forall (B : Type), forall (C : Type), forall (f : forall (_ : A), B), forall (g : forall (_ : B), C), forall (l : (list A)), (((eq (list C)) ((((map B) C) g) ((((map A) B) f) l))) ((((map A) C) (fun (x : A) => (g (f x)))) l))" + }, + { + "name": "rev_unit", + "digest": "forall (A : Type), forall (l : (list A)), forall (a : A), (((eq (list A)) ((rev A) (((app A) l) (((cons A) a) (nil A))))) (((cons A) a) ((rev A) l)))" + } + ], + "deps": "Coq.Init (auto-loaded)" + }, + { + "name": "Logic", + "rocq_sha256": "12d4dc897cb563e6", + "statements": [ + { + "name": "eq_refl_x", + "digest": "forall (A : Type), forall (x : A), (((eq A) x) x)" + }, + { + "name": "eq_sym_ex", + "digest": "forall (A : Type), forall (x : A), forall (y : A), forall (_ : (((eq A) x) y)), (((eq A) y) x)" + }, + { + "name": "eq_trans_ex", + "digest": "forall (A : Type), forall (x : A), forall (y : A), forall (z : A), forall (_ : (((eq A) x) y)), forall (_ : (((eq A) y) z)), (((eq A) x) z)" + }, + { + "name": "f_equal_ex", + "digest": "forall (A : Type), forall (B : Type), forall (f : forall (_ : A), B), forall (x : A), forall (y : A), forall (_ : (((eq A) x) y)), (((eq B) (f x)) (f y))" + }, + { + "name": "f_equal2_ex", + "digest": "forall (A : Type), forall (B : Type), forall (C : Type), forall (f : forall (_ : A), forall (_ : B), C), forall (x1 : A), forall (y1 : A), forall (x2 : B), forall (y2 : B), forall (_ : (((eq A) x1) y1)), forall (_ : (((eq B) x2) y2)), (((eq C) ((f x1) x2)) ((f y1) y2))" + }, + { + "name": "f_equal3_ex", + "digest": "forall (A1 : Type), forall (A2 : Type), forall (A3 : Type), forall (B : Type), forall (f : forall (_ : A1), forall (_ : A2), forall (_ : A3), B), forall (x1 : A1), forall (y1 : A1), forall (x2 : A2), forall (y2 : A2), forall (x3 : A3), forall (y3 : A3), forall (_ : (((eq A1) x1) y1)), forall (_ : (((eq A2) x2) y2)), forall (_ : (((eq A3) x3) y3)), (((eq B) (((f x1) x2) x3)) (((f y1) y2) y3))" + }, + { + "name": "and_intro", + "digest": "forall (A : Prop), forall (B : Prop), forall (_ : A), forall (_ : B), ((and A) B)" + }, + { + "name": "or_introl_ex", + "digest": "forall (A : Prop), forall (B : Prop), forall (_ : A), ((or A) B)" + }, + { + "name": "or_intror_ex", + "digest": "forall (A : Prop), forall (B : Prop), forall (_ : B), ((or A) B)" + }, + { + "name": "ex_intro_ex", + "digest": "forall (A : Type), forall (P : forall (_ : A), Prop), forall (x : A), forall (_ : (P x)), ((ex A) (fun (y : A) => (P y)))" + } + ], + "deps": "Coq.Init (auto-loaded)" + }, + { + "name": "Nat", + "rocq_sha256": "ec44b29f02532d33", + "statements": [ + { + "name": "add_0_l", + "digest": "forall (n : nat), (((eq nat) ((add O) n)) n)" + }, + { + "name": "add_succ_l", + "digest": "forall (n : nat), forall (m : nat), (((eq nat) ((add (S n)) m)) (S ((add n) m)))" + }, + { + "name": "add_1_l", + "digest": "forall (n : nat), (((eq nat) ((add (S O)) n)) (S n))" + }, + { + "name": "add_1_r", + "digest": "forall (n : nat), (((eq nat) ((add n) (S O))) (S n))" + }, + { + "name": "add_0_r", + "digest": "forall (n : nat), (((eq nat) ((add n) O)) n)" + }, + { + "name": "add_succ_r", + "digest": "forall (n : nat), forall (m : nat), (((eq nat) ((add n) (S m))) (S ((add n) m)))" + }, + { + "name": "add_comm", + "digest": "forall (n : nat), forall (m : nat), (((eq nat) ((add n) m)) ((add m) n))" + }, + { + "name": "add_assoc", + "digest": "forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((add n) ((add m) p))) ((add ((add n) m)) p))" + }, + { + "name": "mul_0_l", + "digest": "forall (n : nat), (((eq nat) ((mul O) n)) O)" + }, + { + "name": "mul_0_r", + "digest": "forall (n : nat), (((eq nat) ((mul n) O)) O)" + }, + { + "name": "mul_succ_l", + "digest": "forall (n : nat), forall (m : nat), (((eq nat) ((mul (S n)) m)) ((add ((mul n) m)) m))" + }, + { + "name": "mul_succ_r", + "digest": "forall (n : nat), forall (m : nat), (((eq nat) ((mul n) (S m))) ((add ((mul n) m)) n))" + }, + { + "name": "mul_comm", + "digest": "forall (n : nat), forall (m : nat), (((eq nat) ((mul n) m)) ((mul m) n))" + }, + { + "name": "mul_add_distr_r", + "digest": "forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((mul ((add n) m)) p)) ((add ((mul n) p)) ((mul m) p)))" + }, + { + "name": "mul_add_distr_l", + "digest": "forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((mul n) ((add m) p))) ((add ((mul n) m)) ((mul n) p)))" + }, + { + "name": "mul_assoc", + "digest": "forall (n : nat), forall (m : nat), forall (p : nat), (((eq nat) ((mul n) ((mul m) p))) ((mul ((mul n) m)) p))" + }, + { + "name": "mul_1_l", + "digest": "forall (n : nat), (((eq nat) ((mul (S O)) n)) n)" + }, + { + "name": "mul_1_r", + "digest": "forall (n : nat), (((eq nat) ((mul n) (S O))) n)" + }, + { + "name": "sub_0_l", + "digest": "forall (n : nat), (((eq nat) ((sub O) n)) O)" + }, + { + "name": "sub_0_r", + "digest": "forall (n : nat), (((eq nat) ((sub n) O)) n)" + }, + { + "name": "sub_diag", + "digest": "forall (n : nat), (((eq nat) ((sub n) n)) O)" + }, + { + "name": "sub_succ", + "digest": "forall (n : nat), forall (m : nat), (((eq nat) ((sub (S n)) (S m))) ((sub n) m))" + }, + { + "name": "max_0_l", + "digest": "forall (n : nat), (((eq nat) ((max O) n)) n)" + }, + { + "name": "max_0_r", + "digest": "forall (n : nat), (((eq nat) ((max n) O)) n)" + }, + { + "name": "min_0_l", + "digest": "forall (n : nat), (((eq nat) ((min O) n)) O)" + }, + { + "name": "min_0_r", + "digest": "forall (n : nat), (((eq nat) ((min n) O)) O)" + }, + { + "name": "max_id", + "digest": "forall (n : nat), (((eq nat) ((max n) n)) n)" + }, + { + "name": "min_id", + "digest": "forall (n : nat), (((eq nat) ((min n) n)) n)" + }, + { + "name": "pred_succ", + "digest": "forall (n : nat), (((eq nat) (pred (S n))) n)" + }, + { + "name": "eqb_refl", + "digest": "forall (n : nat), (((eq bool) ((eqb n) n)) true)" + }, + { + "name": "leb_refl", + "digest": "forall (n : nat), (((eq bool) ((leb n) n)) true)" + } + ], + "deps": "Coq.Init (auto-loaded)" + }, + { + "name": "Peano", + "rocq_sha256": "a73cc6210bdade3c", + "statements": [ + { + "name": "le_refl_n", + "digest": "forall (n : nat), ((le n) n)" + }, + { + "name": "le_0_n", + "digest": "forall (n : nat), ((le O) n)" + }, + { + "name": "le_succ_diag_r", + "digest": "forall (n : nat), ((le n) (S n))" + } + ], + "deps": "Coq.Init (auto-loaded)" + } + ], + "excluded": [ + { + "pattern": "multi-variable case analysis / nested induction (e.g. andb_comm, orb b1 b2 = orb b2 b1, de Morgan)", + "boundary": "nested", + "reason": "the translator emits one `apply (_ind motive)` per proof and segments a single level of cases; a second destruct inside a case (needed to decide a goal in two booleans) is not yet generated." + }, + { + "pattern": "induction over an inductive relation (e.g. le_trans, le_n_S via le_ind)", + "boundary": "relational", + "reason": "the eliminator has a dependent motive over the derivation; the translator only builds non-dependent `fun (x:T) => ` motives." + } + ] +} \ No newline at end of file diff --git a/benchmarks/stdlib/corpus/stdlib_map.json b/benchmarks/stdlib/corpus/stdlib_map.json new file mode 100644 index 0000000..5cffd0b --- /dev/null +++ b/benchmarks/stdlib/corpus/stdlib_map.json @@ -0,0 +1,272 @@ +{ + "description": "Maps each curated corpus lemma to its real Rocq standard-library counterpart, so `stdlib_bench.py fidelity` can verify (via Rocq's kernel) that the curated *statement* matches the library's. Every curated lemma MUST have a named stdlib counterpart: the benchmark deliberately contains no bespoke lemmas (ground computations, nested-conjunction intros, etc.) that do not exist in the standard library. Each entry is either {\"stdlib\": } (the curated type must be convertible to the stdlib lemma's type) or {\"stdlib\": , \"relation\": \"symmetry\"} (the curated type is the mirror of the stdlib lemma, verified by `intros; symmetry; apply `). `module_files` names, per module, the standard-library file(s) its lemmas are drawn from; `fidelity` qualifies each with those file(s) and checks `Check (. : ).`, so the ref must both live in the associated file AND be convertible. The mapping is hand-maintained: every curated lemma MUST appear here, and the stdlib refs / relations / files were each confirmed against the installed Rocq before being recorded (flag, never guess).", + "rocq_version": "9.0.1", + "preamble": [ + "From Stdlib Require Import Bool.Bool.", + "From Stdlib Require Import Arith.PeanoNat.", + "From Stdlib Require Import Lists.List.", + "Import ListNotations.", + "Open Scope list_scope." + ], + "module_files": { + "Bool": [ + "Stdlib.Bool.Bool" + ], + "Lists": [ + "Stdlib.Lists.List" + ], + "Logic": [ + "Corelib.Init.Logic" + ], + "Nat": [ + "Stdlib.Arith.PeanoNat" + ], + "Peano": [ + "Corelib.Init.Peano", + "Stdlib.Arith.PeanoNat" + ] + }, + "modules": { + "Bool": { + "andb_true_l": { + "stdlib": "andb_true_l" + }, + "andb_false_l": { + "stdlib": "andb_false_l" + }, + "andb_true_r": { + "stdlib": "andb_true_r" + }, + "andb_false_r": { + "stdlib": "andb_false_r" + }, + "andb_b_b": { + "stdlib": "andb_diag" + }, + "orb_true_l": { + "stdlib": "orb_true_l" + }, + "orb_false_l": { + "stdlib": "orb_false_l" + }, + "orb_true_r": { + "stdlib": "orb_true_r" + }, + "orb_false_r": { + "stdlib": "orb_false_r" + }, + "orb_b_b": { + "stdlib": "orb_diag" + }, + "negb_involutive": { + "stdlib": "negb_involutive" + }, + "negb_involutive_reverse": { + "stdlib": "negb_involutive_reverse" + }, + "andb_negb_r": { + "stdlib": "andb_negb_r" + }, + "orb_negb_r": { + "stdlib": "orb_negb_r" + }, + "implb_true_l": { + "stdlib": "implb_true_l" + }, + "implb_false_l": { + "stdlib": "implb_false_l" + }, + "implb_b_b": { + "stdlib": "implb_same" + }, + "xorb_false_l": { + "stdlib": "xorb_false_l" + }, + "xorb_false_r": { + "stdlib": "xorb_false_r" + }, + "xorb_true_l": { + "stdlib": "xorb_true_l" + }, + "xorb_true_r": { + "stdlib": "xorb_true_r" + }, + "xorb_b_b": { + "stdlib": "xorb_nilpotent" + } + }, + "Lists": { + "app_nil_l": { + "stdlib": "app_nil_l" + }, + "app_nil_r": { + "stdlib": "app_nil_r" + }, + "app_comm_cons": { + "stdlib": "app_comm_cons" + }, + "app_assoc": { + "stdlib": "app_assoc" + }, + "length_app": { + "stdlib": "length_app" + }, + "map_app": { + "stdlib": "map_app" + }, + "length_map": { + "stdlib": "length_map" + }, + "rev_app_distr": { + "stdlib": "rev_app_distr" + }, + "rev_involutive": { + "stdlib": "rev_involutive" + }, + "map_map": { + "stdlib": "map_map" + }, + "rev_unit": { + "stdlib": "rev_unit" + } + }, + "Logic": { + "eq_refl_x": { + "stdlib": "@eq_refl" + }, + "eq_sym_ex": { + "stdlib": "eq_sym" + }, + "eq_trans_ex": { + "stdlib": "eq_trans" + }, + "f_equal_ex": { + "stdlib": "f_equal" + }, + "f_equal2_ex": { + "stdlib": "f_equal2" + }, + "f_equal3_ex": { + "stdlib": "f_equal3" + }, + "and_intro": { + "stdlib": "@conj" + }, + "or_introl_ex": { + "stdlib": "@or_introl" + }, + "or_intror_ex": { + "stdlib": "@or_intror" + }, + "ex_intro_ex": { + "stdlib": "@ex_intro" + } + }, + "Nat": { + "add_0_l": { + "stdlib": "Nat.add_0_l" + }, + "add_0_r": { + "stdlib": "Nat.add_0_r" + }, + "add_succ_l": { + "stdlib": "Nat.add_succ_l" + }, + "add_succ_r": { + "stdlib": "Nat.add_succ_r" + }, + "add_1_l": { + "stdlib": "Nat.add_1_l" + }, + "add_1_r": { + "stdlib": "Nat.add_1_r" + }, + "add_comm": { + "stdlib": "Nat.add_comm" + }, + "add_assoc": { + "stdlib": "Nat.add_assoc" + }, + "mul_0_l": { + "stdlib": "Nat.mul_0_l" + }, + "mul_0_r": { + "stdlib": "Nat.mul_0_r" + }, + "mul_succ_l": { + "stdlib": "Nat.mul_succ_l" + }, + "mul_succ_r": { + "stdlib": "Nat.mul_succ_r" + }, + "mul_comm": { + "stdlib": "Nat.mul_comm" + }, + "mul_1_l": { + "stdlib": "Nat.mul_1_l" + }, + "mul_1_r": { + "stdlib": "Nat.mul_1_r" + }, + "mul_add_distr_r": { + "stdlib": "Nat.mul_add_distr_r" + }, + "mul_add_distr_l": { + "stdlib": "Nat.mul_add_distr_l" + }, + "mul_assoc": { + "stdlib": "Nat.mul_assoc" + }, + "sub_0_l": { + "stdlib": "Nat.sub_0_l" + }, + "sub_0_r": { + "stdlib": "Nat.sub_0_r" + }, + "sub_diag": { + "stdlib": "Nat.sub_diag" + }, + "sub_succ": { + "stdlib": "Nat.sub_succ" + }, + "max_0_l": { + "stdlib": "Nat.max_0_l" + }, + "max_0_r": { + "stdlib": "Nat.max_0_r" + }, + "min_0_l": { + "stdlib": "Nat.min_0_l" + }, + "min_0_r": { + "stdlib": "Nat.min_0_r" + }, + "max_id": { + "stdlib": "Nat.max_id" + }, + "min_id": { + "stdlib": "Nat.min_id" + }, + "pred_succ": { + "stdlib": "Nat.pred_succ" + }, + "eqb_refl": { + "stdlib": "Nat.eqb_refl" + }, + "leb_refl": { + "stdlib": "Nat.leb_refl" + } + }, + "Peano": { + "le_refl_n": { + "stdlib": "le_n" + }, + "le_0_n": { + "stdlib": "Nat.le_0_l" + }, + "le_succ_diag_r": { + "stdlib": "Nat.le_succ_diag_r" + } + } + } +} diff --git a/benchmarks/stdlib/fidelity.py b/benchmarks/stdlib/fidelity.py new file mode 100644 index 0000000..cdea21c --- /dev/null +++ b/benchmarks/stdlib/fidelity.py @@ -0,0 +1,187 @@ +#!/usr/bin/env python3 +"""Statement-level fidelity check: curated corpus lemma vs real Rocq stdlib. + +Corpus `rocq.v` files hand-restate stdlib lemmas. This check asks Rocq's own +kernel to confirm each restatement matches the library lemma it claims to be, +and that the lemma actually lives in the stdlib file its module points at. + +`stdlib_map.json` maps every curated lemma to a stdlib `ref` and each module to +the `module_files` its lemmas come from. We qualify the ref with a file +(`andb_diag` -> `Stdlib.Bool.Bool.andb_diag`) so one Rocq check proves both +membership and type-equality. Two relations: + convertible Check (. : ). -- types must be equal + symmetry prove via `symmetry; apply .` -- mirror lemma + +Every curated lemma must be mapped to a real stdlib ref; unmapped lemmas, stale +map entries, and refs absent from the module's files are all failures. +""" + +import os +import re +import subprocess +import sys +import tempfile + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +import translate # noqa: E402 (local; reuse its comment/sentence/paren splitters) + +# `Lemma foo (x : nat) : P x` -> name="foo", rest="(x : nat) : P x". +STMT_RE = re.compile(r"^(?:" + translate.THEOREM_ALT + + r")\s+([A-Za-z_][A-Za-z0-9_']*)\s*(.*)$", re.S) + + +def extract_statements(vpath): + """[(name, rocq_type)] for each theorem-like statement in a curated rocq.v. + Binders are folded into a `forall`; type text is left as verbatim Rocq.""" + with open(vpath) as f: + text = translate.strip_comments(f.read()) + out = [] + for s in translate.split_sentences(text): + m = STMT_RE.match(s.strip()) + if not m: + continue + name, rest = m.group(1), m.group(2) + parts = translate.split_top_level(rest, ":", maxsplit=1) # binders : type + if len(parts) != 2: + raise ValueError(f"{name}: statement has no top-level ':'") + binders, typ = (re.sub(r"\s+", " ", p).strip() for p in parts) + out.append((name, f"forall {binders}, {typ}" if binders else typ)) + return out + + +def _run_coqc(coq, preamble, body, workdir): + """Compile preamble+body as a temp .v; return (ok, one-line error message).""" + fd, path = tempfile.mkstemp(suffix=".v", prefix="fidelity_", dir=workdir) + with os.fdopen(fd, "w") as f: + f.write("\n".join(preamble) + "\n" + body + "\n") + try: + try: + proc = subprocess.run([coq, "-q", os.path.basename(path)], + capture_output=True, text=True, cwd=workdir) + except OSError as e: + return False, f"could not run '{coq}': {e}" + if proc.returncode == 0: + return True, "" + return False, re.sub(r"\s+", " ", (proc.stderr or proc.stdout).strip()) + finally: + translate.clean_coqc_temp(path) + + +def qualify_ref(ref, file): + """Prefix a stdlib ref with a library file, preserving any leading `@`: + ('andb_diag', 'Stdlib.Bool.Bool') -> 'Stdlib.Bool.Bool.andb_diag' + ('@conj', 'Corelib.Init.Logic') -> '@Corelib.Init.Logic.conj'.""" + at = ref.startswith("@") + return ("@" if at else "") + f"{file}.{ref[1:] if at else ref}" + + +def check_lemma(coq, preamble, entry, rocq_type, files, workdir): + """Check one curated lemma against its stdlib counterpart, trying each of the + module's `files` in turn. Returns (status, ref, detail): + match convertible to . (ref = qualified name) + symmetry mirror equivalence verified (ref = qualified name) + MISMATCH ref exists in a file but type differs + ABSENT ref exists in none of the files + NO_STDLIB map entry has no 'stdlib' ref + ERROR cannot run (no files / unknown relation)""" + ref = entry.get("stdlib") + if not ref: + return "NO_STDLIB", None, "map entry has no 'stdlib' ref" + if not files: + return "ERROR", ref, "module has no 'module_files' association in the map" + relation = entry.get("relation", "convertible") + if relation not in ("convertible", "symmetry"): + return "ERROR", ref, f"unknown relation '{relation}'" + + existed, last_msg = False, "" + for file in files: + qref = qualify_ref(ref, file) + if relation == "convertible": + body = f"Check ({qref} : {rocq_type})." + else: + body = f"Goal {rocq_type}.\nProof. intros; symmetry; apply {qref}. Qed." + ok, msg = _run_coqc(coq, preamble, body, workdir) + if ok: + return ("match" if relation == "convertible" else "symmetry"), qref, file + # Failed here: real MISMATCH if the name exists in this file, else keep looking. + found, _ = _run_coqc(coq, preamble, f"Check {qref}.", workdir) + if found: + existed, last_msg = True, msg + if existed: + return "MISMATCH", ref, last_msg + return "ABSENT", ref, f"'{ref}' is in none of the module's files ({', '.join(files)})" + + +def run(cfg): + """Check every curated lemma against its stdlib counterpart. Returns 0 if all + correspondences hold and every lemma is mapped; 1 on any failure.""" + corpus_dir, coq = cfg["corpus_dir"], cfg["coq_path"] + spec = translate.load_stdlib_map(corpus_dir) + preamble, mod_map = spec["preamble"], spec["modules"] + module_files = spec.get("module_files", {}) + sel = translate.corpus_modules(corpus_dir) + + tally = {k: 0 for k in ("match", "symmetry", "MISMATCH", "ABSENT", + "NO_STDLIB", "ERROR", "UNMAPPED", "STALE")} + failures = [] + workdir = tempfile.mkdtemp(prefix="fidelity_") + try: + for mod in sel: + vpath = os.path.join(corpus_dir, mod, "rocq.v") + if not os.path.exists(vpath): + print(f" ! no such module: {mod}", file=sys.stderr) + continue + stmts = extract_statements(vpath) + entries = mod_map.get(mod, {}) + files = module_files.get(mod, []) + if not files: + failures.append(f"{mod}: no 'module_files' entry in stdlib_map.json") + print(f"\n{mod} ({len(stmts)} lemmas, files: {', '.join(files) or '—'}):") + + seen = set() + for name, rocq_type in stmts: + seen.add(name) + if name not in entries: # curated lemma with no map entry + tally["UNMAPPED"] += 1 + failures.append(f"{mod}.{name}: not in stdlib_map.json") + print(f" [UNMAPPED] {name} (add it to stdlib_map.json)") + continue + status, ref, detail = check_lemma(coq, preamble, entries[name], + rocq_type, files, workdir) + tally[status] += 1 + if status == "match": + print(f" [match ] {name:18s} <- {ref}") + elif status == "symmetry": + print(f" [symmetry] {name:18s} <- {ref} (mirror, up to eq_sym)") + else: # MISMATCH / ABSENT / NO_STDLIB / ERROR + print(f" [{status:8s}] {name:18s}" + (f" <- {ref}" if ref else "")) + print(f" {detail[:240]}") + failures.append(f"{mod}.{name} ({status}): {detail[:160]}") + + for name in entries: # map entry with no curated lemma + if name not in seen: + tally["STALE"] += 1 + failures.append(f"{mod}.{name}: in stdlib_map.json but not in rocq.v") + print(f" [STALE ] {name} (in map, absent from rocq.v)") + finally: + try: + os.rmdir(workdir) + except OSError: + pass + + total = sum(tally.values()) - tally["STALE"] # STALE lemmas aren't curated + print(f"\n{total} curated lemmas: {tally['match']} convertible, " + f"{tally['symmetry']} symmetry-variant, " + f"{tally['MISMATCH']} mismatch, {tally['ABSENT']} absent-from-file, " + f"{tally['NO_STDLIB']} without-stdlib-counterpart, " + f"{tally['ERROR']} error, " + f"{tally['UNMAPPED']} unmapped, {tally['STALE']} stale.") + if failures: + print("\nFIDELITY FAILURES:") + for f in failures: + print(f" - {f}") + return 1 + print("\nAll curated statements correspond to their stdlib counterparts " + "and belong to their module's standard-library file.") + return 0 diff --git a/benchmarks/stdlib/plots/stdlib_scatter.png b/benchmarks/stdlib/plots/stdlib_scatter.png new file mode 100644 index 0000000..1979e89 Binary files /dev/null and b/benchmarks/stdlib/plots/stdlib_scatter.png differ diff --git a/benchmarks/stdlib/report.py b/benchmarks/stdlib/report.py new file mode 100644 index 0000000..4b9acfd --- /dev/null +++ b/benchmarks/stdlib/report.py @@ -0,0 +1,321 @@ +#!/usr/bin/env python3 +"""Reporting for the Rocq-stdlib benchmark: markdown table + scatter plot. + +Reads results/stdlib.json (written by stdlib_bench.py run) and emits: + - stdlib/results/REPORT.md : per-module table + geometric-mean summary + - stdlib/plots/stdlib_scatter.png : Rocq proof time (x) vs MEngine (y), log-log + +The whole report rests on two textbook numbers per measurement, so it is easy to +check by hand: + + * value = the *minimum* over its trials (best of N — the run least perturbed + by the OS, the standard wall-clock estimator); + * noise = the *sample standard deviation* of the startup-floor trials (the + jitter below which a difference is not meaningful). + +From those: proof = max(0, min(whole-file) - min(startup floor)); a proof at or +below its engine's noise is shown as `~0`; speedup = Rocq proof / MEngine proof. +There is no resampling, percentile, or error-bar math — the plot draws exactly +the table's proof numbers. +""" + +import json +import os +import statistics + +# Single source of truth for the results-file key scheme, so the writer +# (stdlib_bench) and this reader can never drift apart. stdlib_bench imports +# `report` only lazily (inside cmd_report), so this top-level import is not +# circular. +from stdlib_bench import (MENGINE_BASELINE_KEY, ROCQ_BASELINE_KEY, + proof_time, rocq_module_baseline_key, + successful_times) + + +# ─────────────────────────────── basic stats ───────────────────────────────── +# The proof-cost definitions (successful_times / proof_time) live in stdlib_bench +# and are imported above; the noise floor is statistics.stdev of the startup-floor +# trials. So this report and the `run` console summary compute proof time and the +# noise floor identically. Only the presentation-only helpers (median, geomean, +# formatting) are local. + +def _fmt_ms(t): + return f"{t*1000:.1f}" if t is not None else "FAIL" + + +# ─────────────────────────────── data loading ──────────────────────────────── + +def _lemma_counts(cfg): + """Map module name -> number of statements, read from the corpus manifest.""" + path = os.path.join(cfg.get("corpus_dir", ""), "manifest.json") + if not os.path.exists(path): + return {} + with open(path) as f: + manifest = json.load(f) + return {u["name"]: len(u.get("statements", [])) for u in manifest.get("units", [])} + + +def _load(cfg): + """Return (rows, meta): one row per module, plus the global startup floors. + + Each row's `*_proof` is the module's startup-subtracted proof time and each + `*_noise` is the jitter of the floor that was subtracted. MEngine has one + global floor; Rocq has one *per module* (its own Require/Import preamble — + e.g. Lists `Require`s List, so its floor is ~2× the others), falling back to + the global empty-.v floor when a module's own baseline wasn't recorded. + + Every value here is recomputed from the raw per-trial times (via + `successful_times`), never read from the runner's stored `time_taken` — so + the report is a self-contained derivation an auditor can recheck against the + trial arrays.""" + with open(cfg["results"]) as f: + results = json.load(f) + + m_floor_times = successful_times(results.get(MENGINE_BASELINE_KEY)) + r_floor_times = successful_times(results.get(ROCQ_BASELINE_KEY)) + counts = _lemma_counts(cfg) + + # Per-module keys are `mengine_` / `coq_`; baseline keys double the + # underscore after the engine prefix (`mengine__…`, `coq__…`). Strip a + # single-underscore prefix to recover the module name (keeps names that + # contain '_' intact, unlike splitting on the first '_'). + unit_keys = set() + for prefix in ("mengine_", "coq_"): + unit_keys |= {k[len(prefix):] for k in results + if k.startswith(prefix) and not k.startswith(prefix + "_")} + + rows = [] + for u in sorted(unit_keys): + m_total = successful_times(results.get(f"mengine_{u}")) + r_total = successful_times(results.get(f"coq_{u}")) + if not m_total or not r_total: + continue + r_mod_floor = successful_times(results.get(rocq_module_baseline_key(u))) or r_floor_times + rows.append({ + "unit": u, + "nlemmas": counts.get(u), + "mengine_total": min(m_total), + "rocq_total": min(r_total), + "mengine_total_max": max(m_total), # slowest run, for the scatter whisker + "rocq_total_max": max(r_total), + "mengine_proof": proof_time(m_total, m_floor_times), + "rocq_proof": proof_time(r_total, r_mod_floor), + "mengine_noise": statistics.stdev(m_floor_times), + "rocq_noise": statistics.stdev(r_mod_floor), + }) + meta = { + "mengine_floor": min(m_floor_times) if m_floor_times else None, + "rocq_floor": min(r_floor_times) if r_floor_times else None, + "mengine_noise": statistics.stdev(m_floor_times), + "rocq_noise": statistics.stdev(r_floor_times), + "nlemmas": sum(counts.values()) if counts else None, + } + return rows, meta + + +# ───────────────────────────────── report ──────────────────────────────────── + +def generate(cfg): + rows, meta = _load(cfg) + if not rows: + print("No results yet — run `stdlib_bench.py run` first.") + return + + m_floor, m_noise = meta["mengine_floor"], meta["mengine_noise"] + r_floor, r_noise = meta["rocq_floor"], meta["rocq_noise"] + # The proof columns subtract each engine's startup floor, which + # `stdlib_bench.py run` always records (see cmd_run) — so a results file + # without them is stale, not a supported mode. Bail with an actionable + # message rather than degrade to a whole-file table that buries proof cost + # under process startup. + if m_floor is None or r_floor is None: + print("No startup baseline in results — re-run `stdlib_bench.py run` " + "(it records each engine's startup floor, which the proof columns " + "subtract).") + return + + lines = [ + "# Rocq stdlib benchmark — MEngine vs Rocq\n", + "Whole-file wall-clock is dominated by fixed per-invocation cost — a " + "`coqc` process plus its auto-loaded `Prelude`, and an `mengine` " + "process plus `prelude/tactics.me` + the compat prelude — none of " + "which is the unit's proof. To compare *proof* cost fairly we time " + "each engine's preamble alone (an empty `.v`; the compat prelude with " + "no unit) and subtract it. Every number below is the **best (minimum) " + "of N trials**; **proof** columns are that whole-file minimum minus the " + "startup-floor minimum, clamped at 0.\n", + f"**Startup floor** (subtracted from each whole-file time): MEngine " + f"{_fmt_ms(m_floor)} ms (±{m_noise*1000:.1f}), one global floor; Rocq " + f"{_fmt_ms(r_floor)} ms (±{r_noise*1000:.1f}) for the `Require`-free " + "modules, but **each module subtracts its own Require/Import floor** " + "(Lists' is ~2× larger). The ± is that floor's trial standard deviation; " + "a proof at or below its own floor's ± is reported as `~0` — " + "indistinguishable from startup.\n", + "| Module | Lemmas | Rocq total (ms) | Rocq proof (ms) | " + "MEngine total (ms) | MEngine proof (ms) | Proof speedup |", + "|--------|--------|-----------------|-----------------|" + "--------------------|--------------------|---------------|", + ] + + speedups = [] + below_noise = 0 + for row in rows: + nl = row["nlemmas"] if row["nlemmas"] is not None else "?" + mp, rp = row["mengine_proof"], row["rocq_proof"] + m_below = mp is not None and mp <= row["mengine_noise"] + r_below = rp is not None and rp <= row["rocq_noise"] + mp_s = "~0" if m_below else _fmt_ms(mp) + rp_s = "~0" if r_below else _fmt_ms(rp) + if m_below or r_below: + below_noise += 1 + sp_s = "—" + elif mp and rp: + sp = rp / mp + speedups.append(sp) + sp_s = f"{sp:.2f}×" + else: + sp_s = "-" + lines.append(f"| `{row['unit']}` | {nl} | " + f"{_fmt_ms(row['rocq_total'])} | {rp_s} | " + f"{_fmt_ms(row['mengine_total'])} | {mp_s} | {sp_s} |") + + nlem = meta.get("nlemmas") + lem_s = f", {nlem} lemmas" if nlem else "" + lines.append("") + lines.append(f"**Modules:** {len(rows)}{lem_s} — one benchmark file " + "per stdlib module, matching the library's own file structure.") + lines.append(f"**Below startup-noise floor (proof time ~0 on either engine):** " + f"{below_noise} of {len(rows)}.") + if speedups: + geo, med = statistics.geometric_mean(speedups), statistics.median(speedups) + lines.append(f"**Proof-only speedup (Rocq/MEngine), over the " + f"{len(speedups)} module(s) above the noise floor:** " + f"{geo:.2f}× geomean (median {med:.2f}×).") + lines.append("") + if below_noise == len(rows): + lines.append("> Even grouped per module, these proofs are cheap " + "enough that their startup-subtracted cost stays at or below " + "measurement jitter on both engines — so the whole-file ratio " + "is still mostly a *process-startup* ratio. Heavier modules " + "(computational induction, list reasoning) are needed to " + "measure proof speed clearly above the noise floor.") + else: + lines.append("> Proof columns are startup-subtracted; modules above the " + "noise floor give a real proof-speed comparison, while the " + "whole-file columns still include each engine's fixed " + "per-invocation cost (which dominates the raw ratio).") + + out_md = os.path.join(os.path.dirname(cfg["results"]), "REPORT.md") + with open(out_md, "w") as f: + f.write("\n".join(lines) + "\n") + print(f"Wrote {os.path.relpath(out_md)}") + + _scatter(cfg, rows, meta) + + +# ─────────────────────────────── scatter plot ──────────────────────────────── + +def _scatter(cfg, rows, meta): + try: + import matplotlib + matplotlib.use("Agg") + import matplotlib.pyplot as plt + except Exception as e: # noqa: BLE001 + print(f"(skipping scatter plot: matplotlib unavailable: {e})") + return + + colors = {"Bool": "tab:blue", "Lists": "tab:purple", "Logic": "tab:red", + "Nat": "tab:green", "Peano": "tab:orange"} + m_noise, r_noise = meta["mengine_noise"], meta["rocq_noise"] + + # Each dot is exactly the table's (Rocq proof, MEngine proof) for a module — + # both startup-subtracted with that module's *own* floor. Subtracting the + # module's own floor is the one honest axis choice when floors differ: Lists + # `Require`s List, so its Rocq floor is ~2× the others, and a whole-file + # scatter would charge that library load to Lists' x-coordinate and make + # MEngine look ~2× better on Lists than it is. A module whose proof is 0 on + # either axis can't sit on a log scale, so it is dropped (and named). + pts, dropped = [], [] + for r in rows: + (pts if r["mengine_proof"] and r["rocq_proof"] else dropped).append(r) + if not pts: + names = ", ".join(r["unit"] for r in dropped) or "none" + print(f"(skipping scatter plot: no module has a measurable proof " + f"residual; all at/below startup: {names})") + return + if dropped: + names = ", ".join(r["unit"] for r in dropped) + print(f"(scatter: {names} omitted — proof residual 0 on an axis, " + "i.e. indistinguishable from startup)") + + xs = [r["rocq_proof"] * 1000 for r in pts] + ys = [r["mengine_proof"] * 1000 for r in pts] + # Upper whisker per axis = this module's whole-file trial spread (max − min); + # since the dot is the min-based residual, the slowest of N runs sits that far + # above it (the floor is held at its min, so it cancels out). + xtop = [x + (r["rocq_total_max"] - r["rocq_total"]) * 1000 for x, r in zip(xs, pts)] + ytop = [y + (r["mengine_total_max"] - r["mengine_total"]) * 1000 for y, r in zip(ys, pts)] + lo = min(xs + ys) * 0.5 + hi = max(xs + ys + xtop + ytop) * 1.4 + + fig, ax = plt.subplots(figsize=(6.4, 6.4)) + + # Parity: equal proof time on both engines is y = x (startup already removed + # per module). Shade the MEngine-faster half so the read is obvious. + ax.plot([lo, hi], [lo, hi], "k--", lw=1, label="parity (equal proof time)") + ax.fill_between([lo, hi], [lo, lo], [lo, hi], color="tab:green", alpha=0.05) + ax.text(hi * 0.85, lo * 2.4, "MEngine faster", fontsize=8, ha="right", + va="bottom", color="tab:green", style="italic") + ax.text(lo * 1.6, hi * 0.13, "MEngine slower", fontsize=8, ha="left", + va="center", color="tab:red", style="italic") + + # Noise floors: a proof at/below the startup measurement's own jitter (its + # trials' stddev) is not distinguishable from startup. Shade each engine's + # band so borderline points (e.g. Peano) are read with caution. Same concept + # on each axis, so identical weight (color/alpha) and a matching label. + if m_noise > 0: + ax.axhspan(lo, m_noise * 1000, color="tab:gray", alpha=0.10, zorder=0) + ax.text(hi * 0.96, m_noise * 1000, "MEngine noise floor", fontsize=6, + ha="right", va="bottom", color="dimgray") + if r_noise > 0: + ax.axvspan(lo, r_noise * 1000, color="tab:gray", alpha=0.10, zorder=0) + ax.text(r_noise * 1000, hi * 0.96, "Rocq noise floor", fontsize=6, + ha="right", va="top", color="dimgray", rotation=90) + + for r in pts: + col = colors.get(r["unit"], "gray") + x, y = r["rocq_proof"] * 1000, r["mengine_proof"] * 1000 + # One-sided whisker toward the slowest of N runs: the dot is the best-of-N + # residual (bottom end), the whisker length is just the whole-file min→max + # spread on that axis. No resampling — two numbers per whisker. + xerr = [[0.0], [(r["rocq_total_max"] - r["rocq_total"]) * 1000]] + yerr = [[0.0], [(r["mengine_total_max"] - r["mengine_total"]) * 1000]] + ax.errorbar(x, y, xerr=xerr, yerr=yerr, fmt="o", color=col, ecolor=col, + elinewidth=1.0, capsize=3, markersize=7, markeredgecolor="k", + markeredgewidth=0.5, zorder=3, label=r["unit"]) + ax.annotate(r["unit"], (x, y), textcoords="offset points", + xytext=(6, 4), fontsize=8) + + ax.set_xscale("log") + ax.set_yscale("log") + ax.set_xlim(lo, hi) + ax.set_ylim(lo, hi) + ax.set_aspect("equal") + ax.set_xlabel("Rocq proof time (ms, log) — startup-subtracted") + ax.set_ylabel("MEngine proof time (ms, log) — startup-subtracted") + ax.set_title("Rocq stdlib modules: proof cost (per-module startup removed)\n" + "dot = best-of-N proof; whisker = up to the slowest of N trials") + ax.legend(fontsize=8, loc="upper left") + ax.grid(True, which="both", ls=":", alpha=0.4) + os.makedirs(cfg["plots_dir"], exist_ok=True) + out = os.path.join(cfg["plots_dir"], "stdlib_scatter.png") + fig.tight_layout() + fig.savefig(out, dpi=120) + print(f"Wrote {os.path.relpath(out)}") + + +if __name__ == "__main__": + import sys + sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) + from stdlib_bench import load_config + generate(load_config()) diff --git a/benchmarks/stdlib/results/REPORT.md b/benchmarks/stdlib/results/REPORT.md new file mode 100644 index 0000000..f64e965 --- /dev/null +++ b/benchmarks/stdlib/results/REPORT.md @@ -0,0 +1,19 @@ +# Rocq stdlib benchmark — MEngine vs Rocq + +Whole-file wall-clock is dominated by fixed per-invocation cost — a `coqc` process plus its auto-loaded `Prelude`, and an `mengine` process plus `prelude/tactics.me` + the compat prelude — none of which is the unit's proof. To compare *proof* cost fairly we time each engine's preamble alone (an empty `.v`; the compat prelude with no unit) and subtract it. Every number below is the **best (minimum) of N trials**; **proof** columns are that whole-file minimum minus the startup-floor minimum, clamped at 0. + +**Startup floor** (subtracted from each whole-file time): MEngine 2.1 ms (±1.4), one global floor; Rocq 61.0 ms (±10.0) for the `Require`-free modules, but **each module subtracts its own Require/Import floor** (Lists' is ~2× larger). The ± is that floor's trial standard deviation; a proof at or below its own floor's ± is reported as `~0` — indistinguishable from startup. + +| Module | Lemmas | Rocq total (ms) | Rocq proof (ms) | MEngine total (ms) | MEngine proof (ms) | Proof speedup | +|--------|--------|-----------------|-----------------|--------------------|--------------------|---------------| +| `Bool` | 22 | 87.9 | 27.1 | 6.6 | 4.6 | 5.91× | +| `Lists` | 11 | 170.9 | 44.3 | 100.4 | 98.4 | 0.45× | +| `Logic` | 10 | 78.3 | 15.7 | 7.3 | 5.2 | 3.00× | +| `Nat` | 31 | 128.9 | 66.2 | 43.5 | 41.4 | 1.60× | +| `Peano` | 3 | 66.1 | ~0 | 2.2 | ~0 | — | + +**Modules:** 5, 77 lemmas — one benchmark file per stdlib module, matching the library's own file structure. +**Below startup-noise floor (proof time ~0 on either engine):** 1 of 5. +**Proof-only speedup (Rocq/MEngine), over the 4 module(s) above the noise floor:** 1.89× geomean (median 2.30×). + +> Proof columns are startup-subtracted; modules above the noise floor give a real proof-speed comparison, while the whole-file columns still include each engine's fixed per-invocation cost (which dominates the raw ratio). diff --git a/benchmarks/stdlib/results/stdlib.json b/benchmarks/stdlib/results/stdlib.json new file mode 100644 index 0000000..aab4ec2 --- /dev/null +++ b/benchmarks/stdlib/results/stdlib.json @@ -0,0 +1,1221 @@ +{ + "mengine__startup_baseline": { + "time_taken": 0.0020636506378650665, + "success": true, + "trials": [ + { + "time_taken": 0.0024679210036993027, + "success": true + }, + { + "time_taken": 0.002185574732720852, + "success": true + }, + { + "time_taken": 0.0022129472345113754, + "success": true + }, + { + "time_taken": 0.0051634348928928375, + "success": true + }, + { + "time_taken": 0.0050001488998532295, + "success": true + }, + { + "time_taken": 0.002161787822842598, + "success": true + }, + { + "time_taken": 0.0051955534145236015, + "success": true + }, + { + "time_taken": 0.0022914549335837364, + "success": true + }, + { + "time_taken": 0.0020945295691490173, + "success": true + }, + { + "time_taken": 0.005062682554125786, + "success": true + }, + { + "time_taken": 0.0022870581597089767, + "success": true + }, + { + "time_taken": 0.005120459944009781, + "success": true + }, + { + "time_taken": 0.0022054752334952354, + "success": true + }, + { + "time_taken": 0.005120419897139072, + "success": true + }, + { + "time_taken": 0.0021961499005556107, + "success": true + }, + { + "time_taken": 0.005244267173111439, + "success": true + }, + { + "time_taken": 0.00216714758425951, + "success": true + }, + { + "time_taken": 0.002220919355750084, + "success": true + }, + { + "time_taken": 0.005207140929996967, + "success": true + }, + { + "time_taken": 0.00220442283898592, + "success": true + }, + { + "time_taken": 0.002152395434677601, + "success": true + }, + { + "time_taken": 0.0052437568083405495, + "success": true + }, + { + "time_taken": 0.002208179794251919, + "success": true + }, + { + "time_taken": 0.0020636506378650665, + "success": true + }, + { + "time_taken": 0.0021195467561483383, + "success": true + } + ], + "error": "" + }, + "coq__startup_baseline": { + "time_taken": 0.061008233577013016, + "success": true, + "trials": [ + { + "time_taken": 0.08367697149515152, + "success": true + }, + { + "time_taken": 0.08289461117237806, + "success": true + }, + { + "time_taken": 0.06379095744341612, + "success": true + }, + { + "time_taken": 0.06561388727277517, + "success": true + }, + { + "time_taken": 0.08907206449657679, + "success": true + }, + { + "time_taken": 0.07897442113608122, + "success": true + }, + { + "time_taken": 0.061008233577013016, + "success": true + }, + { + "time_taken": 0.0627416567876935, + "success": true + }, + { + "time_taken": 0.062065787613391876, + "success": true + }, + { + "time_taken": 0.07237034291028976, + "success": true + }, + { + "time_taken": 0.06586936209350824, + "success": true + }, + { + "time_taken": 0.06246113404631615, + "success": true + }, + { + "time_taken": 0.062149773351848125, + "success": true + }, + { + "time_taken": 0.061743712052702904, + "success": true + }, + { + "time_taken": 0.06310193054378033, + "success": true + }, + { + "time_taken": 0.06287548877298832, + "success": true + }, + { + "time_taken": 0.0642940578982234, + "success": true + }, + { + "time_taken": 0.06667373608797789, + "success": true + }, + { + "time_taken": 0.08185073733329773, + "success": true + }, + { + "time_taken": 0.0905943512916565, + "success": true + }, + { + "time_taken": 0.06512828543782234, + "success": true + }, + { + "time_taken": 0.08747605048120022, + "success": true + }, + { + "time_taken": 0.06571552995592356, + "success": true + }, + { + "time_taken": 0.06524792592972517, + "success": true + }, + { + "time_taken": 0.06337571144104004, + "success": true + } + ], + "error": "" + }, + "coq__baseline__Bool": { + "time_taken": 0.0607640165835619, + "success": true, + "trials": [ + { + "time_taken": 0.06824701838195324, + "success": true + }, + { + "time_taken": 0.08944649063050747, + "success": true + }, + { + "time_taken": 0.06930828746408224, + "success": true + }, + { + "time_taken": 0.08403188548982143, + "success": true + }, + { + "time_taken": 0.0607640165835619, + "success": true + }, + { + "time_taken": 0.06257607694715261, + "success": true + }, + { + "time_taken": 0.09176560584455729, + "success": true + }, + { + "time_taken": 0.06506988778710365, + "success": true + }, + { + "time_taken": 0.0639596525579691, + "success": true + }, + { + "time_taken": 0.06176871992647648, + "success": true + }, + { + "time_taken": 0.0617895508185029, + "success": true + }, + { + "time_taken": 0.09048622660338879, + "success": true + }, + { + "time_taken": 0.09099030774086714, + "success": true + }, + { + "time_taken": 0.08996074460446835, + "success": true + }, + { + "time_taken": 0.0628806371241808, + "success": true + }, + { + "time_taken": 0.06267455592751503, + "success": true + }, + { + "time_taken": 0.07526143360882998, + "success": true + }, + { + "time_taken": 0.0621521882712841, + "success": true + }, + { + "time_taken": 0.062105217948555946, + "success": true + }, + { + "time_taken": 0.08631636016070843, + "success": true + }, + { + "time_taken": 0.08772744797170162, + "success": true + }, + { + "time_taken": 0.06820548512041569, + "success": true + }, + { + "time_taken": 0.08761277608573437, + "success": true + }, + { + "time_taken": 0.06550810765475035, + "success": true + }, + { + "time_taken": 0.09030592627823353, + "success": true + } + ], + "error": "" + }, + "mengine_Bool": { + "time_taken": 0.006648464128375053, + "success": true, + "trials": [ + { + "time_taken": 0.0071935877203941345, + "success": true + }, + { + "time_taken": 0.0069395629689097404, + "success": true + }, + { + "time_taken": 0.01698335539549589, + "success": true + }, + { + "time_taken": 0.006648464128375053, + "success": true + }, + { + "time_taken": 0.016685127280652523, + "success": true + }, + { + "time_taken": 0.006814975291490555, + "success": true + }, + { + "time_taken": 0.007026383653283119, + "success": true + }, + { + "time_taken": 0.007093565538525581, + "success": true + }, + { + "time_taken": 0.007035789079964161, + "success": true + }, + { + "time_taken": 0.019109241664409637, + "success": true + } + ], + "error": "" + }, + "coq_Bool": { + "time_taken": 0.08785024471580982, + "success": true, + "trials": [ + { + "time_taken": 0.08785024471580982, + "success": true + }, + { + "time_taken": 0.11576099507510662, + "success": true + }, + { + "time_taken": 0.09071752708405256, + "success": true + }, + { + "time_taken": 0.11294232401996851, + "success": true + }, + { + "time_taken": 0.11080336943268776, + "success": true + }, + { + "time_taken": 0.11695504561066628, + "success": true + }, + { + "time_taken": 0.11606174893677235, + "success": true + }, + { + "time_taken": 0.1221329215914011, + "success": true + }, + { + "time_taken": 0.11758558731526136, + "success": true + }, + { + "time_taken": 0.11464699544012547, + "success": true + } + ], + "error": "" + }, + "coq__baseline__Lists": { + "time_taken": 0.12655360903590918, + "success": true, + "trials": [ + { + "time_taken": 0.1519144745543599, + "success": true + }, + { + "time_taken": 0.13324865140020847, + "success": true + }, + { + "time_taken": 0.15813947934657335, + "success": true + }, + { + "time_taken": 0.1466888953000307, + "success": true + }, + { + "time_taken": 0.1550881415605545, + "success": true + }, + { + "time_taken": 0.1544969379901886, + "success": true + }, + { + "time_taken": 0.12936652917414904, + "success": true + }, + { + "time_taken": 0.1352119417861104, + "success": true + }, + { + "time_taken": 0.1575844343751669, + "success": true + }, + { + "time_taken": 0.12658885959535837, + "success": true + }, + { + "time_taken": 0.15586155652999878, + "success": true + }, + { + "time_taken": 0.15294427704066038, + "success": true + }, + { + "time_taken": 0.159058035351336, + "success": true + }, + { + "time_taken": 0.13901789113879204, + "success": true + }, + { + "time_taken": 0.15919591300189495, + "success": true + }, + { + "time_taken": 0.15849560871720314, + "success": true + }, + { + "time_taken": 0.15541995130479336, + "success": true + }, + { + "time_taken": 0.1573015870526433, + "success": true + }, + { + "time_taken": 0.12693273834884167, + "success": true + }, + { + "time_taken": 0.12655360903590918, + "success": true + }, + { + "time_taken": 0.1564568430185318, + "success": true + }, + { + "time_taken": 0.13432946242392063, + "success": true + }, + { + "time_taken": 0.12974059116095304, + "success": true + }, + { + "time_taken": 0.16695494204759598, + "success": true + }, + { + "time_taken": 0.1327393241226673, + "success": true + } + ], + "error": "" + }, + "mengine_Lists": { + "time_taken": 0.10042033717036247, + "success": true, + "trials": [ + { + "time_taken": 0.13687478937208652, + "success": true + }, + { + "time_taken": 0.12535923719406128, + "success": true + }, + { + "time_taken": 0.1341869169846177, + "success": true + }, + { + "time_taken": 0.1288621686398983, + "success": true + }, + { + "time_taken": 0.10159012954682112, + "success": true + }, + { + "time_taken": 0.13029523007571697, + "success": true + }, + { + "time_taken": 0.1203914973884821, + "success": true + }, + { + "time_taken": 0.1086914874613285, + "success": true + }, + { + "time_taken": 0.11112508550286293, + "success": true + }, + { + "time_taken": 0.10042033717036247, + "success": true + } + ], + "error": "" + }, + "coq_Lists": { + "time_taken": 0.17087356001138687, + "success": true, + "trials": [ + { + "time_taken": 0.1789044886827469, + "success": true + }, + { + "time_taken": 0.17561356723308563, + "success": true + }, + { + "time_taken": 0.18584307096898556, + "success": true + }, + { + "time_taken": 0.20499222166836262, + "success": true + }, + { + "time_taken": 0.17087356001138687, + "success": true + }, + { + "time_taken": 0.18039989285171032, + "success": true + }, + { + "time_taken": 0.20035299845039845, + "success": true + }, + { + "time_taken": 0.1792698698118329, + "success": true + }, + { + "time_taken": 0.20837020501494408, + "success": true + }, + { + "time_taken": 0.20267567038536072, + "success": true + } + ], + "error": "" + }, + "coq__baseline__Logic": { + "time_taken": 0.0625646598637104, + "success": true, + "trials": [ + { + "time_taken": 0.06275561731308699, + "success": true + }, + { + "time_taken": 0.06294884998351336, + "success": true + }, + { + "time_taken": 0.0625646598637104, + "success": true + }, + { + "time_taken": 0.08964517991989851, + "success": true + }, + { + "time_taken": 0.0633245874196291, + "success": true + }, + { + "time_taken": 0.06644233781844378, + "success": true + }, + { + "time_taken": 0.06577371805906296, + "success": true + }, + { + "time_taken": 0.07292455993592739, + "success": true + }, + { + "time_taken": 0.07178221736103296, + "success": true + }, + { + "time_taken": 0.07398183457553387, + "success": true + }, + { + "time_taken": 0.0709060886874795, + "success": true + }, + { + "time_taken": 0.06271498650312424, + "success": true + }, + { + "time_taken": 0.06308821868151426, + "success": true + }, + { + "time_taken": 0.06445624213665724, + "success": true + }, + { + "time_taken": 0.07049292512238026, + "success": true + }, + { + "time_taken": 0.06726467609405518, + "success": true + }, + { + "time_taken": 0.07200379204005003, + "success": true + }, + { + "time_taken": 0.07437705062329769, + "success": true + }, + { + "time_taken": 0.088324761018157, + "success": true + }, + { + "time_taken": 0.067588334903121, + "success": true + }, + { + "time_taken": 0.06281172391027212, + "success": true + }, + { + "time_taken": 0.06654542312026024, + "success": true + }, + { + "time_taken": 0.0640478665009141, + "success": true + }, + { + "time_taken": 0.06259696930646896, + "success": true + }, + { + "time_taken": 0.09370904788374901, + "success": true + } + ], + "error": "" + }, + "mengine_Logic": { + "time_taken": 0.007294178009033203, + "success": true, + "trials": [ + { + "time_taken": 0.0077179959043860435, + "success": true + }, + { + "time_taken": 0.0076314350590109825, + "success": true + }, + { + "time_taken": 0.007294178009033203, + "success": true + }, + { + "time_taken": 0.008480587042868137, + "success": true + }, + { + "time_taken": 0.020337232388556004, + "success": true + }, + { + "time_taken": 0.007664185017347336, + "success": true + }, + { + "time_taken": 0.016981842927634716, + "success": true + }, + { + "time_taken": 0.007925749756395817, + "success": true + }, + { + "time_taken": 0.014667203649878502, + "success": true + }, + { + "time_taken": 0.01212988793849945, + "success": true + } + ], + "error": "" + }, + "coq_Logic": { + "time_taken": 0.07825526874512434, + "success": true, + "trials": [ + { + "time_taken": 0.08237668219953775, + "success": true + }, + { + "time_taken": 0.0940405884757638, + "success": true + }, + { + "time_taken": 0.09487939160317183, + "success": true + }, + { + "time_taken": 0.08116703853011131, + "success": true + }, + { + "time_taken": 0.08042669203132391, + "success": true + }, + { + "time_taken": 0.07898687105625868, + "success": true + }, + { + "time_taken": 0.08306740317493677, + "success": true + }, + { + "time_taken": 0.08127483073621988, + "success": true + }, + { + "time_taken": 0.0786845050752163, + "success": true + }, + { + "time_taken": 0.07825526874512434, + "success": true + } + ], + "error": "" + }, + "coq__baseline__Nat": { + "time_taken": 0.06268912833184004, + "success": true, + "trials": [ + { + "time_taken": 0.06397353578358889, + "success": true + }, + { + "time_taken": 0.06364801339805126, + "success": true + }, + { + "time_taken": 0.06469013541936874, + "success": true + }, + { + "time_taken": 0.06300181057304144, + "success": true + }, + { + "time_taken": 0.06268912833184004, + "success": true + }, + { + "time_taken": 0.06313891615718603, + "success": true + }, + { + "time_taken": 0.06969328783452511, + "success": true + }, + { + "time_taken": 0.06388096511363983, + "success": true + }, + { + "time_taken": 0.06514392979443073, + "success": true + }, + { + "time_taken": 0.07090077921748161, + "success": true + }, + { + "time_taken": 0.06854472681879997, + "success": true + }, + { + "time_taken": 0.08869062270969152, + "success": true + }, + { + "time_taken": 0.06727894954383373, + "success": true + }, + { + "time_taken": 0.06657400634139776, + "success": true + }, + { + "time_taken": 0.0702693872153759, + "success": true + }, + { + "time_taken": 0.09553026501089334, + "success": true + }, + { + "time_taken": 0.06991490256041288, + "success": true + }, + { + "time_taken": 0.06773137953132391, + "success": true + }, + { + "time_taken": 0.0830736430361867, + "success": true + }, + { + "time_taken": 0.06502963695675135, + "success": true + }, + { + "time_taken": 0.06533340644091368, + "success": true + }, + { + "time_taken": 0.06361600570380688, + "success": true + }, + { + "time_taken": 0.06525762192904949, + "success": true + }, + { + "time_taken": 0.06554251071065664, + "success": true + }, + { + "time_taken": 0.08511576149612665, + "success": true + } + ], + "error": "" + }, + "mengine_Nat": { + "time_taken": 0.04349034186452627, + "success": true, + "trials": [ + { + "time_taken": 0.060421297326684, + "success": true + }, + { + "time_taken": 0.046960342675447464, + "success": true + }, + { + "time_taken": 0.059162271209061146, + "success": true + }, + { + "time_taken": 0.04493577219545841, + "success": true + }, + { + "time_taken": 0.04581351391971111, + "success": true + }, + { + "time_taken": 0.05012355372309685, + "success": true + }, + { + "time_taken": 0.044816700741648674, + "success": true + }, + { + "time_taken": 0.04431252088397741, + "success": true + }, + { + "time_taken": 0.04427569452673197, + "success": true + }, + { + "time_taken": 0.04349034186452627, + "success": true + } + ], + "error": "" + }, + "coq_Nat": { + "time_taken": 0.12892350181937218, + "success": true, + "trials": [ + { + "time_taken": 0.1298451228067279, + "success": true + }, + { + "time_taken": 0.12892350181937218, + "success": true + }, + { + "time_taken": 0.16004880145192146, + "success": true + }, + { + "time_taken": 0.16676206327974796, + "success": true + }, + { + "time_taken": 0.17252451181411743, + "success": true + }, + { + "time_taken": 0.13332939613610506, + "success": true + }, + { + "time_taken": 0.15855500847101212, + "success": true + }, + { + "time_taken": 0.13296729885041714, + "success": true + }, + { + "time_taken": 0.1426210356876254, + "success": true + }, + { + "time_taken": 0.16091108042746782, + "success": true + } + ], + "error": "" + }, + "coq__baseline__Peano": { + "time_taken": 0.06328690983355045, + "success": true, + "trials": [ + { + "time_taken": 0.07129685580730438, + "success": true + }, + { + "time_taken": 0.08647765591740608, + "success": true + }, + { + "time_taken": 0.08342824690043926, + "success": true + }, + { + "time_taken": 0.09383758064359426, + "success": true + }, + { + "time_taken": 0.09011065401136875, + "success": true + }, + { + "time_taken": 0.08220423199236393, + "success": true + }, + { + "time_taken": 0.06747900974005461, + "success": true + }, + { + "time_taken": 0.09064008109271526, + "success": true + }, + { + "time_taken": 0.06440906226634979, + "success": true + }, + { + "time_taken": 0.09550885204225779, + "success": true + }, + { + "time_taken": 0.06984950508922338, + "success": true + }, + { + "time_taken": 0.06328690983355045, + "success": true + }, + { + "time_taken": 0.07161639910191298, + "success": true + }, + { + "time_taken": 0.06470252480357885, + "success": true + }, + { + "time_taken": 0.06433051265776157, + "success": true + }, + { + "time_taken": 0.08608685620129108, + "success": true + }, + { + "time_taken": 0.07678560353815556, + "success": true + }, + { + "time_taken": 0.06389895360916853, + "success": true + }, + { + "time_taken": 0.06640479154884815, + "success": true + }, + { + "time_taken": 0.09816525690257549, + "success": true + }, + { + "time_taken": 0.06537804286926985, + "success": true + }, + { + "time_taken": 0.08680950570851564, + "success": true + }, + { + "time_taken": 0.07233402039855719, + "success": true + }, + { + "time_taken": 0.0787306958809495, + "success": true + }, + { + "time_taken": 0.07880871277302504, + "success": true + } + ], + "error": "" + }, + "mengine_Peano": { + "time_taken": 0.0022431109100580215, + "success": true, + "trials": [ + { + "time_taken": 0.0024305135011672974, + "success": true + }, + { + "time_taken": 0.007061737589538097, + "success": true + }, + { + "time_taken": 0.002353559248149395, + "success": true + }, + { + "time_taken": 0.0022431109100580215, + "success": true + }, + { + "time_taken": 0.00491412915289402, + "success": true + }, + { + "time_taken": 0.0025438861921429634, + "success": true + }, + { + "time_taken": 0.00311314407736063, + "success": true + }, + { + "time_taken": 0.0025501661002635956, + "success": true + }, + { + "time_taken": 0.00285286083817482, + "success": true + }, + { + "time_taken": 0.002516714856028557, + "success": true + } + ], + "error": "" + }, + "coq_Peano": { + "time_taken": 0.06609362363815308, + "success": true, + "trials": [ + { + "time_taken": 0.09270255174487829, + "success": true + }, + { + "time_taken": 0.06793548911809921, + "success": true + }, + { + "time_taken": 0.06769721023738384, + "success": true + }, + { + "time_taken": 0.08643151540309191, + "success": true + }, + { + "time_taken": 0.06609362363815308, + "success": true + }, + { + "time_taken": 0.06755499541759491, + "success": true + }, + { + "time_taken": 0.09435097593814135, + "success": true + }, + { + "time_taken": 0.06992846354842186, + "success": true + }, + { + "time_taken": 0.06915654055774212, + "success": true + }, + { + "time_taken": 0.06695622205734253, + "success": true + } + ], + "error": "" + } +} \ No newline at end of file diff --git a/benchmarks/stdlib/stdlib_bench.py b/benchmarks/stdlib/stdlib_bench.py new file mode 100644 index 0000000..02ba955 --- /dev/null +++ b/benchmarks/stdlib/stdlib_bench.py @@ -0,0 +1,607 @@ +#!/usr/bin/env python3 +"""Corpus runner for the Rocq-stdlib benchmark (MEngine vs Rocq). + +A sibling to ``benchmarks/bench.py``: instead of sweeping a parameter range it +iterates a fixed manifest of curated, auto-translated stdlib units. It reuses +the timing discipline of ``framework/runner.run_single`` (process-group kill on +timeout, N trials keeping the minimum) without subclassing ``Benchmark``. + +Subcommands: + test faithfulness gate: coqc compiles rocq.v, MEngine runs + mengine.me clean, and the statement digests correspond + fidelity verify each curated statement matches its real stdlib + counterpart (corpus/stdlib_map.json), via Rocq's kernel + clean remove every generated file (mengine.me, manifest, + results, plot); keep sources + regen rebuild every generated file from source, in dependency + order (mengine.me -> manifest -> run -> report) + +`regen` and `clean` are the primary entry points; `test` and `fidelity` are the +correctness gates, run by hand. The run/report/manifest steps are internal to +`regen` (no standalone subcommand). +""" + +import argparse +import hashlib +import json +import os +import re +import signal +import statistics +import subprocess +import sys +import tempfile +import time + +HERE = os.path.dirname(os.path.abspath(__file__)) +BENCH_ROOT = os.path.dirname(HERE) +sys.path.insert(0, HERE) +import translate # noqa: E402 (local module) + + +# ─────────────────────────────── config ────────────────────────────────────── + +def load_config(): + with open(os.path.join(BENCH_ROOT, "config.json")) as f: + cfg = json.load(f) + s = cfg.get("stdlib", {}) + def exp(p): + return os.path.expanduser(p) if p else p + return { + "mengine_path": exp(cfg["mengine_path"]), + "mengine_root": exp(cfg.get("mengine_root", "")), + "coq_path": exp(cfg.get("coq_path", "coqc")), + "corpus_dir": os.path.join(BENCH_ROOT, s.get("corpus_dir", "stdlib/corpus")), + "compat": os.path.join(BENCH_ROOT, s.get("compat", "stdlib/compat/stdlib_compat.me")), + "results": os.path.join(BENCH_ROOT, s.get("results", "stdlib/results/stdlib.json")), + "plots_dir": os.path.join(BENCH_ROOT, s.get("plots_dir", "stdlib/plots")), + "timeout": s.get("timeout", 20), + "trials": s.get("trials", 10), + "coq_timeout_multiplier": cfg.get("coq_timeout_multiplier", 1.5), + } + + +# ─────────────────────────── corpus discovery ──────────────────────────────── + +# Each unit is a whole stdlib *module* file — one per corpus// directory +# (Bool, Lists, Logic, Nat, Peano) — mirroring how the standard library is +# organized, not a one-lemma fragment. + + +def discover_units(cfg): + return translate.corpus_modules(cfg["corpus_dir"]) + + +def unit_paths(cfg, name): + d = os.path.join(cfg["corpus_dir"], name) + return os.path.join(d, "rocq.v"), os.path.join(d, "mengine.me"), d + + +def unit_statement_digests(mepath): + """(name, digest) pairs for each Theorem in a unit's mengine.me.""" + with open(mepath) as f: + return translate.statement_digests(f.read()) + + +# ───────────────────────────── timing core ─────────────────────────────────── +# Mirrors framework.runner.run_single: N trials, keep the min successful time, +# kill the whole process group on timeout. + +def time_command(cmd, cwd, timeout, trials): + best = None + success = False + all_trials = [] + last_err = "" + for _ in range(trials): + start = time.perf_counter() + try: + proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE, + text=True, cwd=cwd, start_new_session=True) + except OSError as e: + # Missing/unexecutable binary: record a failed trial and stop, like the + # sibling scripts (translate/fidelity) — don't crash the whole run. + last_err = f"could not run {cmd[0]!r}: {e}" + all_trials.append({"time_taken": None, "success": False}) + break + try: + out, err = proc.communicate(timeout=timeout) + elapsed = time.perf_counter() - start + ok = proc.returncode == 0 + all_trials.append({"time_taken": elapsed, "success": ok}) + if ok: + success = True + if best is None or elapsed < best: + best = elapsed + else: + last_err = (err or out)[:300] + break # don't repeat a failing point + except subprocess.TimeoutExpired: + elapsed = time.perf_counter() - start + # Mirror what subprocess.run(timeout=…) does on expiry — kill, then + # communicate() to reap — but across the whole process group, since + # start_new_session=True made the child a group leader. SIGKILL can't + # be caught, so a single killpg + communicate() reliably tears down the + # child and any grandchildren with no lingering pipe or zombie. + try: + os.killpg(proc.pid, signal.SIGKILL) + except ProcessLookupError: + pass # already exited between timeout and kill + proc.communicate() + all_trials.append({"time_taken": elapsed, "success": False, "timeout": True}) + last_err = f"timeout after {timeout}s" + break + return {"time_taken": best, + "success": success, "trials": all_trials, "error": last_err} + + +# ─────────────────────────── per-engine commands ───────────────────────────── + +def mengine_combined_file(cfg, mepath): + """Write compat-prelude + unit into a temp .me; return its path.""" + fd, path = tempfile.mkstemp(suffix=".me", prefix="stdlib_unit_") + with os.fdopen(fd, "w") as f: + with open(cfg["compat"]) as c: + f.write(c.read()) + f.write("\n") + with open(mepath) as m: + f.write(m.read()) + return path + + +def run_mengine(cfg, name, timeout, trials): + _v, mepath, _d = unit_paths(cfg, name) + combined = mengine_combined_file(cfg, mepath) + try: + cmd = [cfg["mengine_path"], "-q", combined] + res = time_command(cmd, cfg["mengine_root"] or None, timeout, trials) + finally: + os.remove(combined) + return res + + +def run_rocq(cfg, name, timeout, trials): + vpath, _m, d = unit_paths(cfg, name) + cmd = [cfg["coq_path"], "-q", vpath] + to = timeout * cfg["coq_timeout_multiplier"] + res = time_command(cmd, d, to, trials) + translate.clean_coqc_byproducts(vpath) # keep the corpus rocq.v, drop .vo/.aux/… + return res + + +# ─────────────────────────── startup baselines ─────────────────────────────── +# Whole-file wall-clock is dominated by fixed per-invocation cost: a coqc process +# plus its auto-loaded Prelude (~65 ms here), and an mengine process plus +# prelude/tactics.me + the compat prelude (~3-6 ms). None of that is the unit's +# proof. We time each engine's preamble *alone* — an empty .v for Rocq (same +# Prelude every unit auto-loads; the corpus has no `Require`), and the compat +# prelude with no unit appended for MEngine — and the report subtracts it to +# isolate the marginal statement+proof cost. Measured once and reused, so we +# spend extra trials to pin the floor down. + +def run_mengine_baseline(cfg, timeout, trials): + """Time the compat prelude with no unit: MEngine's per-invocation floor.""" + cmd = [cfg["mengine_path"], "-q", cfg["compat"]] + return time_command(cmd, cfg["mengine_root"] or None, timeout, trials) + + +def run_rocq_baseline(cfg, timeout, trials): + """Time an empty .v: coqc startup + auto-loaded Prelude, no statement.""" + fd, path = tempfile.mkstemp(suffix=".v", prefix="stdlib_baseline_") + os.close(fd) # empty file + try: + cmd = [cfg["coq_path"], "-q", path] + to = timeout * cfg["coq_timeout_multiplier"] + res = time_command(cmd, os.path.dirname(path), to, trials) + finally: + translate.clean_coqc_temp(path) # temp .v + its coqc byproducts + return res + + +def module_rocq_preamble(vpath): + """The leading directive sentences of a corpus rocq.v (everything the + translator drops before its first statement): its Require/Import/Open/Set + lines. Returns a .v source string, possibly empty (a Require-free module). + + Reuses ``translate.is_dropped`` — the translator's own drop-list — as the + single source of truth, so the *timed* preamble here and the preamble the + translator *discards* can never diverge (e.g. a leading ``#[...]`` attribute + or ``Declare Scope`` is recognized by both, or by neither).""" + with open(vpath) as f: + text = translate.strip_comments(f.read()) + out = [] + for s in translate.split_sentences(text): + s = s.strip() + if translate.is_dropped(s): + out.append(s + ".") + else: + break + return "\n".join(out) + + +def run_rocq_module_baseline(cfg, name, timeout, trials): + """Time a .v holding only this module's Require/Import preamble — the module's + own Rocq startup floor. A `Require`-free module yields an empty file, i.e. + the same Prelude-only floor as the global baseline; a module that loads a + library (Lists -> `Require Import List`) pays that load here, so the report + subtracts it instead of charging it to the proof. Run from the unit dir so + load paths resolve exactly as the unit's own compile does.""" + vpath, _m, d = unit_paths(cfg, name) + pre = module_rocq_preamble(vpath) + fd, path = tempfile.mkstemp(suffix=".v", prefix="stdlib_pre_", dir=d) + with os.fdopen(fd, "w") as f: + f.write(pre + "\n") + try: + cmd = [cfg["coq_path"], "-q", os.path.basename(path)] + to = timeout * cfg["coq_timeout_multiplier"] + res = time_command(cmd, d, to, trials) + finally: + translate.clean_coqc_temp(path) # temp .v + its coqc byproducts + return res + + +# Keys under which baselines are stored in results (alongside per-unit keys). +# Baseline keys double the underscore right after the engine prefix +# (`mengine__…`, `coq__…`) so report's per-unit key discovery — which strips a +# single-underscore engine prefix (`mengine_` / `coq_`) — skips them, keeping +# module names that themselves contain '_' intact. +MENGINE_BASELINE_KEY = "mengine__startup_baseline" +ROCQ_BASELINE_KEY = "coq__startup_baseline" + + +def rocq_module_baseline_key(name): + return f"coq__baseline__{name}" + + +# ─────────────────────── results interpretation ────────────────────────────── +# How a stored timing result becomes a proof-cost number. Imported by `report` +# and used by `cmd_run`'s progress line, so the console summary and REPORT.md +# apply the exact same definitions (best-of-N proof residual, stddev noise +# floor) and can never disagree. + +def successful_times(entry): + """Successful per-trial wall-clock times (seconds); [] if missing/failed.""" + if not entry or not entry.get("success"): + return [] + return [t["time_taken"] for t in entry.get("trials", []) if t.get("success")] + + +def proof_time(total_times, floor_times): + """Best-of-N proof-only cost: min(whole-file) − min(startup floor), clamped. + None when either measurement is missing (nothing to subtract → undefined, + never the raw total, which would count startup as proof cost).""" + if not total_times or not floor_times: + return None + return max(0.0, min(total_times) - min(floor_times)) + + +# ─────────────────────────── faithfulness gate ─────────────────────────────── + +def rocq_statement_names(vpath): + with open(vpath) as f: + text = translate.strip_comments(f.read()) + pat = r"\b(?:" + translate.THEOREM_ALT + \ + r")\s+([A-Za-z_][A-Za-z0-9_']*)" + return [m.group(1) for m in re.finditer(pat, text)] + + +def test_unit(cfg, name): + vpath, mepath, d = unit_paths(cfg, name) + problems = [] + + # 1. Rocq compiles. + rr = run_rocq(cfg, name, cfg["timeout"], 1) + if not rr["success"]: + problems.append(f"rocq.v fails coqc: {rr['error'][:120]}") + + # 2. MEngine runs clean. + mr = run_mengine(cfg, name, cfg["timeout"], 1) + if not mr["success"]: + problems.append(f"mengine.me fails: {mr['error'][:120]}") + + # 3. mengine.me re-derivable from rocq.v by the translator (no drift), and + # statement names correspond. Statement types are elaborated through Rocq + # (`Set Printing All`), so the gate runs the translator's own pipeline + # (rocq_elaborate -> translate_unit) directly, exactly as translate.py's + # CLI does. + try: + with open(vpath) as f: + vtext = f.read() + elab = translate.rocq_elaborate(vtext, vpath, cfg["coq_path"], + translate.statement_names(vtext)) + me_src = translate.translate_unit(vtext, translate.Report(), elab) + except translate.Untranslatable as e: + problems.append(f"translator flags rocq.v: {e.reason[:120]}") + else: + with open(mepath) as f: + on_disk = f.read() + if _norm(on_disk) != _norm(me_src): + problems.append("mengine.me is stale vs translate.py output (re-run manifest)") + me_names = set(dict(translate.statement_digests(me_src)).keys()) + rq_names = set(rocq_statement_names(vpath)) + if me_names != rq_names: + problems.append(f"statement names differ: rocq={rq_names} mengine={me_names}") + + return problems + + +def _norm(s): + return "\n".join(line.rstrip() for line in s.strip().splitlines()) + + +# ───────────────────────────── manifest ────────────────────────────────────── + +def sha256_file(path): + with open(path, "rb") as f: + return hashlib.sha256(f.read()).hexdigest()[:16] + + +def compute_manifest(cfg): + """The manifest dict for the current corpus (pure — no I/O), so callers can + either write it (`build_manifest`) or diff the on-disk copy against it to + detect drift (`manifest_staleness`).""" + units = [] + for name in discover_units(cfg): + vpath, mepath, _d = unit_paths(cfg, name) + digests = unit_statement_digests(mepath) + units.append({ + "name": name, + "rocq_sha256": sha256_file(vpath), + "statements": [{"name": n, "digest": dg} for n, dg in digests], + "deps": "Coq.Init (auto-loaded)", + }) + return { + "description": "Rocq stdlib units auto-translated with zero manual " + "edits and proved by MEngine + the compat prelude.", + "engine_note": "Requires the cbv applied-fix and GC-dedup kernel fixes " + "(see benchmarks/stdlib/README.md).", + "units": units, + "excluded": EXCLUDED_DOC, + } + + +def build_manifest(cfg): + manifest = compute_manifest(cfg) + out = os.path.join(cfg["corpus_dir"], "manifest.json") + with open(out, "w") as f: + json.dump(manifest, f, indent=2) + return out, len(manifest["units"]) + + +def manifest_staleness(cfg): + """Reason corpus/manifest.json differs from a freshly computed manifest, or + None if current. Guards against a corpus edit (a re-generated rocq.v / + mengine.me) that was not followed by `stdlib_bench.py manifest`, which would + otherwise leave stale statement digests and rocq.v hashes with no failing + check to catch it.""" + path = os.path.join(cfg["corpus_dir"], "manifest.json") + if not os.path.exists(path): + return "is missing (run: stdlib_bench.py manifest)" + with open(path) as f: + on_disk = json.load(f) + if on_disk != compute_manifest(cfg): + return "is out of date vs the corpus (rocq.v / mengine.me changed?)" + return None + + +# Constructs the translator deliberately does not handle; see README. +EXCLUDED_DOC = [ + {"pattern": "multi-variable case analysis / nested induction " + "(e.g. andb_comm, orb b1 b2 = orb b2 b1, de Morgan)", + "boundary": "nested", + "reason": "the translator emits one `apply (_ind motive)` per proof and " + "segments a single level of cases; a second destruct inside a case " + "(needed to decide a goal in two booleans) is not yet generated."}, + {"pattern": "induction over an inductive relation " + "(e.g. le_trans, le_n_S via le_ind)", + "boundary": "relational", + "reason": "the eliminator has a dependent motive over the derivation; the " + "translator only builds non-dependent `fun (x:T) => ` motives."}, +] + + +# ─────────────────────────────── subcommands ───────────────────────────────── + +def cmd_test(cfg): + units = discover_units(cfg) + npass = 0 + for u in units: + problems = test_unit(cfg, u) + if problems: + print(f" [FAIL] {u}") + for p in problems: + print(f" {p}") + else: + print(f" [ OK ] {u}") + npass += 1 + print(f"\n{npass}/{len(units)} units pass the faithfulness gate.") + print("(statement-vs-stdlib correspondence is a separate check: " + "stdlib_bench.py fidelity)") + # The manifest is a single global artifact (not per-unit), so verify it once: + # a re-generated rocq.v / mengine.me must not leave its digests stale. + stale = manifest_staleness(cfg) + if stale: + print(f"\n [STALE] corpus/manifest.json {stale}") + print(" re-run: stdlib_bench.py regen") + return 0 if npass == len(units) and not stale else 1 + + +def cmd_run(cfg): + units = discover_units(cfg) + results = load_results(cfg["results"]) + + # Measure each engine's fixed startup/preamble floor once (extra trials to + # pin its min and stddev down — the report subtracts the min from every + # unit's whole-file time and uses the stddev as the noise floor). Measured + # once and reused, so the extra trials are cheap. See run_*_baseline above. + base_trials = max(cfg["trials"], 25) + mb = run_mengine_baseline(cfg, cfg["timeout"], base_trials) + rb = run_rocq_baseline(cfg, cfg["timeout"], base_trials) + results[MENGINE_BASELINE_KEY] = mb + results[ROCQ_BASELINE_KEY] = rb + save_results(cfg["results"], results) + mb_t, rb_t = mb["time_taken"], rb["time_taken"] + print(f" {'startup baseline':24s} " + f"MEngine={mb_t*1000:8.1f}ms Rocq={rb_t*1000:8.1f}ms\n") + + m_floor = successful_times(mb) # MEngine's one global startup floor + m_noise = statistics.stdev(m_floor) + r_floor = successful_times(rb) # global fallback for a Require-free module + + for u in units: + # Each module's own Rocq startup floor: its Require/Import preamble timed + # alone. Require-free modules match the global empty-.v floor; Lists + # (`Require Import List`) pays the library load here so the report does + # not charge it to the proof. + rmb = run_rocq_module_baseline(cfg, u, cfg["timeout"], base_trials) + results[rocq_module_baseline_key(u)] = rmb + + mr = run_mengine(cfg, u, cfg["timeout"], cfg["trials"]) + rr = run_rocq(cfg, u, cfg["timeout"], cfg["trials"]) + results[f"mengine_{u}"] = mr + results[f"coq_{u}"] = rr + save_results(cfg["results"], results) + + # Interpret this module's timings with the *same* functions the report + # uses (proof_time / statistics.stdev), so this progress line and REPORT.md + # can never disagree: proof = min(whole-file) − min(startup floor); a + # residual at/below the startup floor's own stddev prints as `~0` + # (indistinguishable from startup) with speedup `—`, exactly as reported. + ru_floor = successful_times(rmb) or r_floor + mp = proof_time(successful_times(mr), m_floor) + rp = proof_time(successful_times(rr), ru_floor) + m_below = mp is not None and mp <= m_noise + r_below = rp is not None and rp <= statistics.stdev(ru_floor) + ms = f"{mr['time_taken']*1000:.1f}ms" if mr["success"] else "FAIL" + rs = f"{rr['time_taken']*1000:.1f}ms" if rr["success"] else "FAIL" + mps = "~0" if m_below else (f"{mp*1000:.1f}ms" if mp is not None else "FAIL") + rps = "~0" if r_below else (f"{rp*1000:.1f}ms" if rp is not None else "FAIL") + if m_below or r_below: + ratio = "—" + elif mp and rp: + ratio = f"{rp/mp:.2f}x" + else: + ratio = "-" + print(f" {u:24s} MEngine={ms:>9s}(proof {mps:>8s}) " + f"Rocq={rs:>9s}(proof {rps:>8s}) proof-speedup={ratio}") + print(f"\nResults written to {os.path.relpath(cfg['results'])}") + + +def cmd_report(cfg): + import report + report.generate(cfg) + + +def cmd_manifest(cfg): + out, n = build_manifest(cfg) + print(f"Wrote {os.path.relpath(out)} ({n} units).") + + +def cmd_fidelity(cfg): + import fidelity + return fidelity.run(cfg) + + +# ───────────────────────── generated artifacts ─────────────────────────────── +# The complete list of files the benchmark generates — the single source of +# truth for `clean` (remove them) and `regen` (rebuild them). Everything else +# in the tree is hand-authored source: rocq.v, stdlib_map.json, the compat +# prelude, the .py scripts, and the docs. + +def generated_files(cfg): + """Absolute paths of every file the benchmark generates.""" + paths = [] + for name in discover_units(cfg): + _v, mepath, _d = unit_paths(cfg, name) + paths.append(mepath) # corpus//mengine.me + results_dir = os.path.dirname(cfg["results"]) + paths += [ + os.path.join(cfg["corpus_dir"], "manifest.json"), + cfg["results"], # results/stdlib.json + os.path.join(results_dir, "REPORT.md"), + os.path.join(cfg["plots_dir"], "stdlib_scatter.png"), + ] + return paths + + +def regen_mengine_sources(cfg): + """Re-translate every corpus rocq.v to its mengine.me, in-process via the + translator's own pipeline (rocq_elaborate -> translate_unit) — byte-identical + to translate.py's CLI. Yields each module name as its file is written; + propagates translate.Untranslatable if a unit stops being translatable (a + real regression, surfaced rather than hidden).""" + for name in discover_units(cfg): + vpath, mepath, _d = unit_paths(cfg, name) + with open(vpath) as f: + vtext = f.read() + elab = translate.rocq_elaborate(vtext, vpath, cfg["coq_path"], + translate.statement_names(vtext)) + me_src = translate.translate_unit(vtext, translate.Report(), elab) + with open(mepath, "w") as f: + f.write(me_src) + yield name + + +def cmd_clean(cfg): + removed = 0 + for p in generated_files(cfg): + if os.path.exists(p): + os.remove(p) + print(f" removed {os.path.relpath(p)}") + removed += 1 + print(f"\n{removed} generated file(s) removed " + "(sources — rocq.v, stdlib_map.json, compat, docs — kept).") + + +def cmd_regen(cfg): + print("== 1/4 corpus mengine.me (re-translate each rocq.v) ==") + try: + for n in regen_mengine_sources(cfg): + print(f" [regen] {n}") + except translate.Untranslatable as e: + print(f" [FAIL ] translator flagged a unit: {e.reason}") + return 1 + print("\n== 2/4 corpus/manifest.json ==") + cmd_manifest(cfg) + print("\n== 3/4 results/stdlib.json (timing both engines) ==") + cmd_run(cfg) + print("\n== 4/4 results/REPORT.md + plots/stdlib_scatter.png ==") + cmd_report(cfg) + print("\nAll generated files rebuilt.") + return 0 + + +# ───────────────────────────── results io ──────────────────────────────────── + +def load_results(path): + if os.path.exists(path): + with open(path) as f: + return json.load(f) + return {} + + +def save_results(path, results): + os.makedirs(os.path.dirname(path), exist_ok=True) + with open(path, "w") as f: + json.dump(results, f, indent=2) + + +# ──────────────────────────────── main ─────────────────────────────────────── + +def main(): + cfg = load_config() + ap = argparse.ArgumentParser(description="Rocq-stdlib benchmark corpus runner") + sub = ap.add_subparsers(dest="command", required=True) + for name in ("test", "fidelity", "clean", "regen"): + sub.add_parser(name) + args = ap.parse_args() + + dispatch = { + "test": cmd_test, "fidelity": cmd_fidelity, + "clean": cmd_clean, "regen": cmd_regen, + } + rc = dispatch[args.command](cfg) + sys.exit(rc or 0) + + +if __name__ == "__main__": + main() diff --git a/benchmarks/stdlib/translate.py b/benchmarks/stdlib/translate.py new file mode 100644 index 0000000..a0ed8e4 --- /dev/null +++ b/benchmarks/stdlib/translate.py @@ -0,0 +1,1172 @@ +#!/usr/bin/env python3 +"""Mechanical Rocq (.v) -> MEngine (.me) translator for the stdlib benchmark. + +This is a *lightweight* sentence-aware rewriter with a small recursive-descent +parser for the term sublanguage, NOT a full Coq elaborator. Its guiding principle is +**flag, never guess**: any construct it cannot translate soundly raises +`Untranslatable` (surfaced as a `FLAG` in ``--report`` mode), so the unit is +excluded rather than mistranslated. A wrong translation that happened to compile +would silently corrupt the benchmark, which is the worst outcome. + +It covers the computational/structural corners reachable by MEngine + the compat +prelude — Bool, Nat arithmetic, parametric list reasoning, the `le` order, and +propositional logic. + +Statement and definition *types* are always elaborated through Rocq (`Set Printing +All`), so a working `coqc`/`rocq` binary (``--coq``) is required; see +``rocq_elaborate``. Terms inside definition bodies and proof tactics are still +translated from the surface source (they are not always elaborable). + +Usage: + translate.py unit.v # emit MEngine source on stdout + translate.py --report unit.v # print the handled-construct summary, or + # FLAG the first untranslatable construct +""" + +import argparse +import json +import os +import re +import subprocess +import sys +import tempfile + + +class Untranslatable(Exception): + def __init__(self, reason): + super().__init__(reason) + self.reason = reason + + +# The theorem-like statement keywords, shared by every benchmark script so the +# set stays in one place (the translator, the faithfulness gate, and both +# fidelity checks all recognize the same heads). +THEOREM_KEYWORDS = ("Lemma", "Theorem", "Example", "Corollary", "Fact", + "Remark", "Proposition") +# Regex alternation of the theorem heads, shared alongside THEOREM_KEYWORDS so +# the pattern is written once (used here and in the faithfulness gate). +THEOREM_ALT = "|".join(THEOREM_KEYWORDS) + + +# ───────────────────────────── comment / sentence split ────────────────────── + +def strip_comments(text): + """Remove (* ... *) comments (nested), keeping newlines for line numbers.""" + out = [] + depth = 0 + for token in re.split(r"(\(\*|\*\))", text): + if token == "(*": + depth += 1 + elif token == "*)": + if depth > 0: + depth -= 1 + else: + out.append(token) # stray close outside any comment + elif depth > 0: + out.append(re.sub(r"[^\n]", " ", token)) + else: + out.append(token) + return "".join(out) + + +# A '.' ends a sentence when followed by whitespace/EOF, unless it is itself +# preceded by another '.' (an ellipsis's trailing dot). A '.' between digits +# (e.g. '3.14') is never followed by whitespace, so it never qualifies either. +SENTENCE_END_RE = re.compile(r"(?.aux` beside it — but *not* the `.v` source itself.""" + base = os.path.splitext(vpath)[0] + aux = os.path.join(os.path.dirname(vpath), + "." + os.path.basename(base) + ".aux") + return [*(base + ext for ext in COQC_BYPRODUCT_EXTS), aux] + + +def _remove_all(paths): + for p in paths: + try: + os.remove(p) + except OSError: + pass + + +def clean_coqc_byproducts(vpath): + """Delete only the files `coqc` derives from `vpath`, keeping the `.v` source + itself — for cleaning up after compiling a *persistent* file (a corpus + `rocq.v`). Best-effort; missing files are ignored.""" + _remove_all(_coqc_byproducts(vpath)) + + +def clean_coqc_temp(vpath): + """Delete a temporary `.v` and every file `coqc` derives from it (the + compiled `.vo/.vok/.vos/.glob` and the hidden `..aux` beside it). + Best-effort — missing files are ignored.""" + _remove_all([vpath, *_coqc_byproducts(vpath)]) + + +def corpus_modules(corpus_dir): + """Sorted names of every corpus module directory (one holding a `rocq.v`).""" + return sorted(n for n in os.listdir(corpus_dir) + if os.path.isfile(os.path.join(corpus_dir, n, "rocq.v"))) + + +def load_stdlib_map(corpus_dir): + """The curated lemma -> stdlib correspondence map (`corpus/stdlib_map.json`).""" + with open(os.path.join(corpus_dir, "stdlib_map.json")) as f: + return json.load(f) + + +# ───────────────────────────────── term lexer ──────────────────────────────── + + +class Tok: + def __init__(self, kind, val): + self.kind = kind + self.val = val + + def __repr__(self): + return f"Tok({self.kind},{self.val!r})" + + +def _scan(regex, s, what): + """Yield (group_name, matched_text) for each non-whitespace token in ``s``.""" + i, n = 0, len(s) + while i < n: + m = regex.match(s, i) + if not m: + raise Untranslatable(f"unexpected character {s[i]!r} in {what}") + i = m.end() + if m.lastgroup != "ws": + yield m.lastgroup, m.group() + + +# ───────────────────────────────── AST ─────────────────────────────────────── +# Node forms (tuples): +# ("var", name) | ("app", f, a) | ("forall", var, ty, body) +# ("fun", var, ty, body) | ("arrow", a, b) | ("num", int) + + +# ────────────────────────────── term lexer + parser ────────────────────────── +# +# A single recursive-descent parser handles two closely related inputs: +# +# * statement/definition *types*, taken from Rocq's `Set Printing All` output +# (see ``rocq_elaborate``) — *notation-free and fully explicit*: every +# implicit argument is shown, `@head` marks an application with all implicits +# supplied, numerals are expanded to `O`/`S`, and the only qualified heads are +# the `Nat.*` arithmetic ops. This form needs no infix-notation table and no +# eq-type synthesis: every operator prints as a plain prefix application +# (`@eq T x y`, not `x = y`), and the implicit type arguments are already +# present — which is why statements and definition types are routed through +# Rocq first (see README). +# * surface *terms* from definition bodies and tactic arguments (e.g. `exists 2`, +# `apply (IHl m n)`), which are not elaborated because they may mention +# proof-local hypotheses. These share the elaborated grammar; they add only +# bare numerals (`2`), which the lexer/`parse_atom` accept and ``emit`` +# renders as `O`/`S`. +# +# The grammar is a superset of both: `@`/qualified heads appear only in elaborated +# input, numerals only in surface input, and everything else is common. + +# Qualified heads that `Set Printing All` emits, mapped to compat-prelude names. +# Any *other* dotted (qualified) head is flagged, never guessed. +NAME_MAP = { + "Nat.add": "add", "Nat.mul": "mul", "Nat.sub": "sub", + "Nat.eqb": "eqb", "Nat.leb": "leb", "Nat.ltb": "ltb", + "Nat.pred": "pred", "Nat.max": "max", "Nat.min": "min", +} + +TOKEN_RE = re.compile(r""" + (?P\s+) + | (?P->) + | (?P=>) + | (?P@) + | (?P[(),:]) + | (?P\d+) + | (?P[A-Za-z_][A-Za-z0-9_']*(?:\.[A-Za-z_][A-Za-z0-9_']*)*) +""", re.VERBOSE) + +KEYWORDS = {"forall", "fun", "fix", "match", "with", "end", "return", "in", + "let", "as", "Prop", "Type", "Set", "SProp"} + + +def lex(s, what): + toks = [] + for kind, val in _scan(TOKEN_RE, s, what): + if kind == "arrow": + toks.append(Tok("op", "->")) + elif kind == "fatarrow": + toks.append(Tok("=>", "=>")) + elif kind == "at": + toks.append(Tok("@", "@")) + elif kind == "num": + toks.append(Tok("num", val)) + elif kind == "sym": + toks.append(Tok(val, val)) + elif kind == "qident": + toks.append(Tok(val if val in KEYWORDS else "ident", val)) + return toks + + +def _map_name(name): + if name in NAME_MAP: + return NAME_MAP[name] + if "." in name: + raise Untranslatable(f"unmapped qualified name '{name}'") + return name + + +class TermParser: + """Recursive-descent parser for the (surface / `Set Printing All`) term + grammar. Emits the AST tuples (`var`/`app`/`forall`/`fun`/`arrow`/`num`) + that ``emit`` renders.""" + + def __init__(self, toks): + self.toks = toks + self.pos = 0 + + def peek(self): + return self.toks[self.pos] if self.pos < len(self.toks) else Tok("eof", None) + + def next(self): + t = self.peek() + self.pos += 1 + return t + + def expect(self, kind): + t = self.next() + if t.kind != kind: + raise Untranslatable(f"expected {kind}, got {t.kind} {t.val!r}") + return t + + def parse_binders(self): + """Parse `(x y : T) (z : U)` groups or a single bare `x : T`.""" + binders = [] + while True: + t = self.peek() + if t.kind == "(": + self.next() + names = [] + while self.peek().kind == "ident": + names.append(self.next().val) + if not names: + raise Untranslatable("empty binder group") + self.expect(":") + ty = self.parse_expr() + self.expect(")") + for nm in names: + binders.append((nm, ty)) + elif t.kind == "ident": + names = [] + while self.peek().kind == "ident": + names.append(self.next().val) + self.expect(":") + ty = self.parse_expr() + for nm in names: + binders.append((nm, ty)) + break + else: + break + return binders + + def parse_atom(self): + t = self.peek() + if t.kind == "@": + self.next() + return ("var", _map_name(self.expect("ident").val)) + if t.kind == "(": + self.next() + e = self.parse_expr() + self.expect(")") + return e + if t.kind == "ident": + self.next() + return ("var", _map_name(t.val)) + if t.kind == "num": + self.next() + return ("num", int(t.val)) + if t.kind in ("Prop", "Type"): + self.next() + return ("var", t.kind) + if t.kind in ("Set", "SProp"): + # `Set`/`SProp` are distinct universes, not `Prop`/`Type`; flag rather + # than silently collapse them (flag, never guess). + raise Untranslatable(f"universe '{t.kind}' has no MEngine equivalent") + if t.kind in ("match", "let", "fix"): + raise Untranslatable(f"'{t.kind}' in term") + raise Untranslatable(f"unexpected token {t.kind} {t.val!r}") + + def parse_app(self): + node = self.parse_atom() + while self.peek().kind in ("ident", "@", "(", "num", "Prop", "Type", "Set", "SProp"): + node = ("app", node, self.parse_atom()) + return node + + def parse_expr(self): + t = self.peek() + if t.kind == "forall": + self.next() + binders = self.parse_binders() + self.expect(",") + node = self.parse_expr() + for nm, ty in reversed(binders): + node = ("forall", nm, ty, node) + return node + if t.kind == "fun": + self.next() + binders = self.parse_binders() + self.expect("=>") + node = self.parse_expr() + for nm, ty in reversed(binders): + node = ("fun", nm, ty, node) + return node + left = self.parse_app() + if self.peek().kind == "op" and self.peek().val == "->": + self.next() + return ("arrow", left, self.parse_expr()) # '->' is right-associative + return left + + +def parse_term(s): + """Parse a term: a surface definition body / tactic argument, or a + `Set Printing All` type string (the two share one grammar).""" + p = TermParser(lex(s, "term")) + e = p.parse_expr() + if p.peek().kind != "eof": + raise Untranslatable(f"trailing tokens after term: {p.peek().val!r}") + return e + + +# ───────────────────────────── pretty printer ──────────────────────────────── + +def emit(node): + """Render an AST node as fully-parenthesized MEngine prefix syntax.""" + kind = node[0] + if kind == "var": + return node[1] + if kind == "num": + out = "O" + for _ in range(node[1]): + out = f"(S {out})" + return out + if kind == "app": + f = emit(node[1]) + a = emit(node[2]) + # A binder-headed argument (fun/forall/arrow) must be parenthesized: + # MEngine's parser will not accept a bare `fun …`/`forall …` as an + # application argument (e.g. the predicate of `ex A (fun y => …)`). + if node[2][0] in ("fun", "forall", "arrow"): + a = f"({a})" + return f"({f} {a})" + if kind == "arrow": + a = emit(node[1]) + b = emit(node[2]) + return f"forall (_ : {a}), {b}" + if kind == "forall": + nm, ty, body = node[1], node[2], node[3] + return f"forall ({nm} : {emit(ty)}), {emit(body)}" + if kind == "fun": + nm, ty, body = node[1], node[2], node[3] + return f"fun ({nm} : {emit(ty)}) => {emit(body)}" + raise Untranslatable(f"cannot emit node {kind}") + + +def render_term(src): + """Render a term as fully-parenthesized MEngine prefix syntax. + + One renderer for both inputs the parser accepts (see ``parse_term``): a + `Set Printing All` statement/definition *type*, and a surface definition + body / tactic argument. They share the grammar, so they share the emitter; + ``lex`` already skips surrounding whitespace, so no pre-strip is needed.""" + return emit(parse_term(src)) + + +# ──────────────────────────── command translation ──────────────────────────── + +DROP_PREFIXES = ("Require", "From", "Import", "Export", "Open", "Close", "Set", + "Unset", "Hint", "Arguments", "Local", "Global", "#[", "Scope", + "Declare", "Generalizable", "Print", "Check", "Search", + "Comments", "Section", "End", "Module", "Include") + +# Proof-closing keywords — everything that can terminate a `Proof … .` +# block. `PROOF_CLOSER_ALT` is the regex alternation of the same set. +PROOF_CLOSERS = ("Qed", "Defined", "Admitted", "Abort") +PROOF_CLOSER_ALT = "|".join(PROOF_CLOSERS) +PROOF_FRAMING = ("Proof",) + PROOF_CLOSERS + + +def translate_definition(sentence, report, elab): + """Definition/Lemma/Theorem/Example name [binders] : type [:= body]. + + Returns ``(rendered_line, type_out)`` — the emitted MEngine source line plus + the rendered statement type, so a caller (the proof translator) can use the + type directly rather than re-parsing it out of the emitted string. + + The statement type is always taken from ``elab`` — Rocq's `Set Printing All` + output — rather than parsed from the surface source; a Definition *body* is + still translated from the surface (terms are not always elaborable).""" + m = re.match(r"^(Definition|" + THEOREM_ALT + r")\s+" + r"([A-Za-z_][A-Za-z0-9_']*)\s*(.*)$", sentence, re.S) + if not m: + raise Untranslatable("unrecognized definition form") + kw, name, rest = m.group(1), m.group(2), m.group(3) + is_thm = kw in THEOREM_KEYWORDS + if name not in elab: + raise Untranslatable(f"no elaborated type for '{name}'") + + # Separate optional binders + ': type' + optional ':= body'. + body = None + if ":=" in rest: + head, body = rest.split(":=", 1) + else: + head = rest + + type_out = render_term(elab[name]) + + if is_thm: + report.add_handled(kw) + return f"Theorem {name} : {type_out}.", type_out + # Definition with a body. + if body is None: + report.add_handled("Definition(no body)") + return f"Axiom {name} : {type_out}.", type_out + # The elaborated type is fully explicit, but the body is not always elaborable, + # so it is translated from the surface source, wrapped in the surface binders. + # Split off the binders at the *top-level* ':' (the return-type ascription), not + # the first ':' — a naive split lands inside a typed binder group like `(x : T)`. + binders_src = split_top_level(head, ":", maxsplit=1)[0] + binders = _parse_binder_src(binders_src) if binders_src.strip() else [] + body_full = parse_term(body.strip()) + for nm, ty in reversed(binders): + body_full = ("fun", nm, ty, body_full) + report.add_handled("Definition") + return f"Definition {name} : {type_out} := {emit(body_full)}.", type_out + + +def _parse_binder_src(src): + src = src.strip() + if not src: + return [] + p = TermParser(lex(src, "definition binders")) + binders = p.parse_binders() + if p.peek().kind != "eof": + raise Untranslatable("could not parse definition binders") + return binders + + +def translate_axiom(sentence, report, elab): + m = re.match(r"^(Axiom|Parameter|Conjecture|Variable|Hypothesis)\s+" + r"([A-Za-z_][A-Za-z0-9_']*)\s*:\s*(.*)$", sentence, re.S) + if not m: + raise Untranslatable("unrecognized axiom form") + name = m.group(2) + if name not in elab: + raise Untranslatable(f"no elaborated type for '{name}'") + report.add_handled("Axiom") + return f"Axiom {name} : {render_term(elab[name])}." + + +def is_dropped(sentence): + return sentence.startswith(DROP_PREFIXES) + + +def is_framing(sentence): + word = re.match(r"^([A-Za-z]+)", sentence) + return bool(word and word.group(1) in PROOF_FRAMING) + + +# ──────────────────────────── tactic translation ───────────────────────────── +# +# Token-level mapping of a single Rocq tactic atom (no ';') to MEngine. Unknown +# tactics hard-stop (Untranslatable) so the unit is excluded. + +# Inductive data for the induction/destruct scaffold (compat-prelude types). +# `params` is the number of leading type parameters the eliminator takes (1 for +# `list A`, 0 for nat/bool); `cases` lists, per constructor in declaration order, +# the recursive flag of each *argument* (True = recursive occurrence, carrying an +# induction hypothesis in _ind; the parameter slot is not an argument here). +INDUCTIVES = { + "bool": {"ind": "bool_ind", "params": 0, "cases": [("true", []), ("false", [])]}, + "nat": {"ind": "nat_ind", "params": 0, "cases": [("O", []), ("S", [True])]}, + "list": {"ind": "list_ind", "params": 1, "cases": [("nil", []), ("cons", [False, True])]}, +} + +DIRECT_TACTICS = { + "reflexivity", "assumption", "split", "left", "right", "auto", + "constructor", "simpl", "symmetry", "trivial", "easy", "idtac", + # f_equal is emulated in the compat prelude (a single-layer structural + # congruence on Bad_App_Congruence — see compat/stdlib_compat.me); the + # translator passes it through like the other compat-prelude tactics. + "f_equal", +} + +UNSUPPORTED = { + "lia", "ring", "omega", "nia", "field", "auto with", "eauto", "inversion", + "congruence", "unfold", "fold", "replace", "generalize", + "revert", "case", "pose", "set", "specialize", "discriminate", "injection", + "contradiction", "exfalso", "cbn", "red", "change", "rename", "clear", + "remember", "induction'", "dependent", "functional", "decide", "destruct'", +} + + +def _has_in_clause(arg): + """True if `arg` carries an `in H` forward-reasoning clause, i.e. it contains + the `in` *keyword token* (already in ``KEYWORDS``). Detected by lexing rather + than substring-matching so an identifier such as `interp` or `in_range` never + trips it. A lex failure means the arg is malformed for other reasons, which + the subsequent `render_term` reports — so treat it as no `in` clause.""" + try: + return any(t.kind == "in" for t in lex(arg, "tactic argument")) + except Untranslatable: + return False + + +def translate_tactic_atom(atom, report): + atom = atom.strip() + if not atom: + return None + head = re.match(r"^([A-Za-z_][A-Za-z0-9_']*)", atom) + name = head.group(1) if head else None + + if name in UNSUPPORTED: + raise Untranslatable(f"unsupported tactic '{name}'") + + if name == "repeat": + # `repeat t` — MEngine has the same combinator (prelude `intros := repeat + # intro`). Rocq binds `repeat` tighter than `;`, so the body is a single + # atom (`repeat split; assumption` is `(repeat split); assumption`, split + # at the sentence level before this point). + inner = atom[len("repeat"):].strip() + if not inner: + raise Untranslatable("bare 'repeat'") + t = translate_tactic_atom(inner, report) + if t is None or "." in t or ";" in t: + raise Untranslatable("repeat of a non-atomic tactic") + report.add_handled("tac:repeat") + return f"repeat {t}" + + if name in DIRECT_TACTICS: + rest = atom[len(name):].strip() + if rest: + raise Untranslatable(f"tactic '{name}' with unexpected arguments") + report.add_handled(f"tac:{name}") + return name + + if name in ("intro", "intros"): + args = atom[len(name):].strip() + report.add_handled("tac:intro") + if not args: + return "intros" if name == "intros" else "intro" + names = args.split() + return "; ".join(f"intro {nm}" for nm in names) + + if name in ("apply", "eapply"): + arg = atom[len(name):].strip() + if _has_in_clause(arg): + raise Untranslatable("apply ... in H") + report.add_handled(f"tac:{name}") + return f"{name} ({render_term(arg)})" + + if name == "exact": + arg = atom[len("exact"):].strip() + report.add_handled("tac:exact") + return f"exact ({render_term(arg)})" + + if name in ("exists",): + arg = atom[len("exists"):].strip() + report.add_handled("tac:exists") + return f"exists ({render_term(arg)})" + + if name == "rewrite": + rest = atom[len("rewrite"):].strip() + if rest.startswith("<-"): + raise Untranslatable("rewrite <- (builtin rewrite is forward-only)") + if _has_in_clause(rest): + raise Untranslatable("rewrite ... in H") + report.add_handled("tac:rewrite") + # Builtin C rewrite (Leibniz eq). Routed through the kernel rewrite engine + # rather than the scripted `rewrite_s`, which cannot read the equality off an + # induction hypothesis whose type is the eliminator's beta-redex `(motive) x`. + return f"rewrite {render_term(rest)} with eq" + + if name in ("now",): + # now tac ≈ tac; easy. Bare 'now' is unusual; treat 'now' alone as easy. + rest = atom[len("now"):].strip() + report.add_handled("tac:now") + if not rest: + return "easy" + inner = translate_tactic_atom(rest, report) + if inner is None or "." in inner: + raise Untranslatable("now of a non-atomic tactic") + return f"{inner}; easy" + + raise Untranslatable(f"unknown tactic '{name or atom}'") + + +def translate_tactic_sentence(sentence, report): + """Translate one Rocq tactic sentence (may contain ';') -> MEngine, '.'-ended.""" + parts = _split_semicolons(sentence) + out = [] + for part in parts: + t = translate_tactic_atom(part, report) + if t is not None: + out.append(t) + if not out: + return "" + return "; ".join(out) + "." + + +def _split_semicolons(s): + """Top-level ';'-separated tactic atoms, trimmed and empties dropped.""" + return [p.strip() for p in split_top_level(s, ";") if p.strip()] + + +# ──────────────────────────── proof translation ────────────────────────────── + +def parse_statement_leading_binder(type_out): + """From an emitted 'forall (x : T), Body' string, return (x, T, Body) or None. + + The binder type T may itself contain commas / nested parentheses — e.g. a + function-typed binder `f : forall (_ : A), B` — so the binder's closing `)` + is found by matching parentheses from the `(` after `forall `, rather than + by a comma-naive regex (which would stop inside T).""" + prefix = "forall (" + if not type_out.startswith(prefix): + return None + depth = 0 + i = len("forall ") # index of the binder's opening '(' + start = i + while i < len(type_out): + c = type_out[i] + if c == "(": + depth += 1 + elif c == ")": + depth -= 1 + if depth == 0: + break + i += 1 + if depth != 0 or i >= len(type_out): + return None + inner = type_out[start + 1:i] # 'x : T' + rest = type_out[i + 1:] + if not rest.startswith(", "): + return None + body = rest[2:].strip() + ci = inner.find(" : ") + if ci < 0: + return None + name = inner[:ci].strip() + ty = inner[ci + 3:].strip() + if not re.match(r"^[A-Za-z_][A-Za-z0-9_']*$", name): + return None + return name, ty, body + + +def translate_proof(proof_sentences, stmt_type_out, report): + """Translate a list of Rocq proof tactic-sentences into MEngine proof lines. + + Handles two shapes: + (A) straight-line tactic sequence (no induction/destruct); + (B) a leading `induction x` / `destruct x` on the goal's leading binder, + with bullet- or position-segmented cases (nat/bool only). + Anything else is flagged (Untranslatable).""" + # Drop proof framing sentences. + body = [s for s in proof_sentences if not is_framing(s)] + if not body: + raise Untranslatable("empty proof") + + first = body[0].strip() + # The induction/destruct line may carry a uniform semicolon tail + # (`induction b; reflexivity`) — a chain applied to *every* resulting + # subgoal, the stdlib's idiom for case-splits all cases close the same way + # (e.g. `destr_bool` ≈ `destruct b; simpl; reflexivity`). It is only sound + # when no case needs per-case intros, so `_translate_induction` restricts it + # to all-nullary inductives (bool); anything else is flagged. + m = re.match(r"^(induction|destruct)\s+([A-Za-z_][A-Za-z0-9_']*)" + r"\s*(?:as\s+(\[.*?\]))?\s*(?:;\s*(.+))?$", first, re.S) + if m: + return _translate_induction(m.group(1), m.group(2), m.group(3), body[1:], + stmt_type_out, report, + uniform_tail=m.group(4)) + + # Shape (A): straight-line. Forbid any later induction/destruct. + for s in body: + if re.match(r"^(induction|destruct)\b", s.strip()): + raise Untranslatable("induction/destruct not as first tactic") + lines = [] + for s in body: + t = translate_tactic_sentence(s, report) + if t: + lines.append(t) + return lines + + +def _segment_cases(case_sentences, ncases): + """Segment proof remainder into per-case sentence lists, by '-' bullets or + (fallback) one sentence per case.""" + bulleted = any(s.lstrip().startswith(("-", "+", "*")) for s in case_sentences) + if bulleted: + cases = [] + cur = None + for s in case_sentences: + st = s.lstrip() + if st.startswith(("-", "+", "*")): + if cur is not None: + cases.append(cur) + cur = [st.lstrip("-+* ").strip()] + else: + if cur is None: + raise Untranslatable("proof text before first bullet") + cur.append(s) + if cur is not None: + cases.append(cur) + return cases + # Fallback: require exactly one sentence per case. + if len(case_sentences) != ncases: + raise Untranslatable( + f"cannot segment {len(case_sentences)} sentences into {ncases} cases " + "(use '-' bullets)") + return [[s] for s in case_sentences] + + +def _inductive_head_and_params(ty): + """Split an emitted inductive type like '(list A)' or 'nat' into + (head, params_string): ('list', 'A') or ('nat', '').""" + t = ty.strip() + if t.startswith("(") and t.endswith(")"): + inner = t[1:-1].strip() + depth = 0 + balanced = True + for ch in inner: + if ch == "(": + depth += 1 + elif ch == ")": + depth -= 1 + if depth < 0: + balanced = False + break + if balanced and depth == 0: + t = inner + parts = t.split(None, 1) + head = parts[0] + params = parts[1].strip() if len(parts) > 1 else "" + return head, params + + +def _parse_as_clause(as_clause, ncases): + """Parse `as [ | x l IHl ]` into a list of per-constructor name lists. + Returns e.g. [[], ['x', 'l', 'IHl']]; or None if no clause.""" + if as_clause is None: + return None + inner = as_clause.strip() + if not (inner.startswith("[") and inner.endswith("]")): + raise Untranslatable("malformed `as` intro-pattern") + inner = inner[1:-1] + groups = [g.split() for g in inner.split("|")] + if len(groups) != ncases: + raise Untranslatable( + f"`as` pattern has {len(groups)} cases, expected {ncases}") + return groups + + +def _case_intro_lines(kind, var, rec_flags, names): + """intro lines for one constructor case. + + The eliminator is always the *recursive* `_ind`, whose step case binds an + induction hypothesis (`P `) for every recursive argument. So each + case must introduce: every constructor argument in order, then one + hypothesis per recursive argument — for *both* `induction` and `destruct`, + because both go through `_ind` (MEngine generates no non-recursive + `_rec`/case principle). They differ only in how that hypothesis is + handled: + + - `induction` names it (from the `as` clause, else `IH`) so the case + body can use it. + - `destruct` has no induction hypothesis in Rocq; here it is an artifact + of emulating case analysis with `_ind`, so it is discarded with a + bare `intro.` (which still exposes `P (ctor ...)`), and the `as` clause + names only the constructor arguments. The resulting term is the same + proof `induction` would build with the IH left unused — a full, + Coq-checkable term — so this stays within flag-never-guess. + + With an explicit `as` group the argument names come verbatim; otherwise the + arguments default to Rocq's auto-naming (reuse the variable for the single + recursive argument), which is only well-defined when the constructor has no + non-recursive arguments.""" + n_rec = sum(1 for f in rec_flags if f) + if names is not None: + # induction `as` lists args + IHs; destruct `as` lists only the args. + n_named_ih = n_rec if kind == "induction" else 0 + if len(names) != len(rec_flags) + n_named_ih: + raise Untranslatable( + f"`as` case lists {len(names)} names, expected " + f"{len(rec_flags) + n_named_ih}") + lines = [f"intro {nm}." for nm in names] + if kind != "induction": + lines += ["intro." for _ in range(n_rec)] # discard the IH(s) + return lines + if any(not f for f in rec_flags): + raise Untranslatable( + "induction/destruct without `as` on a constructor with " + "non-recursive arguments (name them with `as [...]`)") + lines = [f"intro {var}." for _ in rec_flags] + if kind == "induction": + lines += [f"intro IH{var}." for f in rec_flags if f] + else: + lines += ["intro." for f in rec_flags if f] # discard the IH(s) + return lines + + +def _translate_induction(kind, var, as_clause, remainder, stmt_type_out, report, + uniform_tail=None): + # Peel leading binders, introducing each, until we reach the induction + # variable. Binders before it (e.g. the type parameter A of `list A`) are + # introduced and then supplied to the eliminator via the variable's own type. + rest = stmt_type_out + intros = [] + var_ty = None + body = None + while True: + lb = parse_statement_leading_binder(rest) + if lb is None: + raise Untranslatable( + f"{kind} variable '{var}' is not a leading forall binder") + name, ty, inner = lb + intros.append(name) + if name == var: + var_ty, body = ty, inner + break + rest = inner + + head, params = _inductive_head_and_params(var_ty) + if head not in INDUCTIVES: + raise Untranslatable(f"{kind} on type '{head}' not supported") + info = INDUCTIVES[head] + if info["params"] and not params: + raise Untranslatable(f"{kind} on '{head}' is missing its type parameter") + + motive = f"fun ({var} : {var_ty}) => {body}" + param_prefix = f"{params} " if params else "" + lines = [f"intro {b}." for b in intros] + + if uniform_tail is not None: + # `induction x; t1; t2` — Rocq runs the chain on every subgoal of the + # eliminator. MEngine has `;` too, but its cross-goal form + # (`apply (_ind ...); t1; t2`) normalizes the sibling case goals + # before either is closed, and `simpl`/`cbv` over the shared motive then + # corrupts the not-yet-solved case. So the chain is instead replayed + # *per case, sequentially* — `apply (...)`, then `t1; t2` once for each + # constructor — which yields the same proof term without the cross-goal + # hazard. Sound only when no case binds constructor arguments / an IH + # (otherwise the chain would hit an unintroduced `forall`), so restrict + # to all-nullary inductives (bool). + if as_clause is not None: + raise Untranslatable("uniform `;` tail with an `as` clause") + if remainder: + raise Untranslatable("uniform `;` tail followed by more tactics") + if any(rec_flags for _ctor, rec_flags in info["cases"]): + raise Untranslatable( + f"uniform `;` tail on '{head}' (a constructor takes arguments; " + "the chain cannot introduce them per case)") + report.add_handled(f"tac:{kind}") + tail_atoms = [] + for atom in _split_semicolons(uniform_tail): + t = translate_tactic_atom(atom, report) + if t is None: + continue + if "." in t: + raise Untranslatable( + f"uniform `;` tail step '{atom}' is not a single tactic") + tail_atoms.append(t) + lines.append(f"apply ({info['ind']} {param_prefix}({motive})).") + case_tail = "; ".join(tail_atoms) + "." + for _case in info["cases"]: + lines.append(case_tail) + return lines + + lines.append(f"apply ({info['ind']} {param_prefix}({motive})).") + + names_per_case = _parse_as_clause(as_clause, len(info["cases"])) + cases = _segment_cases(remainder, len(info["cases"])) + if len(cases) != len(info["cases"]): + raise Untranslatable( + f"{kind}: {len(cases)} cases provided, expected {len(info['cases'])}") + + report.add_handled(f"tac:{kind}") + for idx, ((ctor, rec_flags), case_body) in enumerate(zip(info["cases"], cases)): + names = names_per_case[idx] if names_per_case is not None else None + # The constructor args and IHs are introduced *first*; the `simpl` that + # reduces the eliminator's `motive (ctor ...)` redex (MEngine does not + # beta-reduce it automatically as Rocq does) must come after those intros. + case_lines = _case_intro_lines(kind, var, rec_flags, names) + case_lines.append("simpl.") + for s in case_body: + t = translate_tactic_sentence(s, report) + if t: + case_lines.append(t) + lines.extend(case_lines) + return lines + + +# ─────────────────────────────── report ────────────────────────────────────── + +class Report: + def __init__(self): + self.handled = {} + + def add_handled(self, key): + self.handled[key] = self.handled.get(key, 0) + 1 + + +# ─────────────────────────── unit-level translation ────────────────────────── + +def translate_unit(text, report, elab): + """Translate a whole .v unit to a MEngine source string, or raise. + + ``elab`` maps statement names to their `Set Printing All` types (see + ``rocq_elaborate``); statement types are taken from there rather than parsed + from the surface source.""" + text = strip_comments(text) + sentences = split_sentences(text) + + out_lines = [] + i = 0 + n = len(sentences) + while i < n: + s = sentences[i].strip() + if not s: + i += 1 + continue + word = re.match(r"^([A-Za-z_#\[]+)", s) + kw = word.group(1) if word else "" + + if is_dropped(s): + i += 1 + continue + if kw in ("Inductive", "Fixpoint", "CoFixpoint"): + raise Untranslatable(f"'{kw}' in unit (define it in the compat prelude)") + # Separate each top-level item (statement + proof) with a blank line. + if out_lines: + out_lines.append("") + if kw in ("Axiom", "Parameter", "Conjecture", "Variable", "Hypothesis"): + out_lines.append(translate_axiom(s, report, elab)) + i += 1 + continue + if kw == "Definition": + line, _type = translate_definition(s, report, elab) + out_lines.append(line) + i += 1 + continue + if kw in THEOREM_KEYWORDS: + stmt, type_out = translate_definition(s, report, elab) + out_lines.append(stmt) + # Collect the proof: subsequent sentences until Qed/Defined/Admitted/Abort. + proof = [] + i += 1 + while i < n: + ps = sentences[i].strip() + proof.append(ps) + w = re.match(r"^([A-Za-z]+)", ps) + if w and w.group(1) in PROOF_CLOSERS: + break + i += 1 + if any(re.match(r"^Admitted", p) or re.match(r"^Abort", p) for p in proof): + raise Untranslatable("proof is Admitted/Abort") + proof_lines = translate_proof(proof, type_out, report) + out_lines.extend(proof_lines) + i += 1 + continue + # Unknown command. + raise Untranslatable(f"unrecognized command '{kw}'") + + return "\n".join(out_lines) + "\n" + + +# ─────────────────────── Rocq elaboration (Set Printing All) ────────────────── +# +# Obtain the fully-explicit, notation-free type of each top-level statement by +# replaying the unit through Rocq with `Set Printing All` and a `Check` per name. +# This is what lets eq/list statements translate without surface type synthesis +# (the implicit type arguments are printed for us). Failure (the unit does not +# compile, or a name is missing) is reported as Untranslatable — never guessed. + +STMT_DECL_RE = re.compile( + r"^(Definition|" + THEOREM_ALT + r"|Axiom|Parameter|Conjecture)\s+" + r"([A-Za-z_][A-Za-z0-9_']*)") + + +def statement_names(text): + """Ordered, de-duplicated names of every elaboratable top-level statement.""" + names, seen = [], set() + for s in split_sentences(strip_comments(text)): + m = STMT_DECL_RE.match(s.strip()) + if m and m.group(2) not in seen: + seen.add(m.group(2)) + names.append(m.group(2)) + return names + + +def _parse_check_output(stdout, names): + """Parse `Check`/`Print` output into {name: type-string}. + + Each `Check name.` prints the name flush-left on its own line, then the type + on the following line(s) prefixed ` : ` (continuations are indented). We + set the print width effectively unbounded, so a forall/application/arrow type + lands on a single line; we still join any continuations defensively.""" + name_set = set(names) + out = {} + lines = stdout.splitlines() + i = 0 + while i < len(lines): + ln = lines[i] + if ln and not ln[0].isspace() and ln.strip() in name_set and ln.strip() not in out: + head = ln.strip() + buf, j = [], i + 1 + while j < len(lines): + cont = lines[j] + if cont.strip() == "" or (cont and not cont[0].isspace()): + break + buf.append(cont.strip()) + j += 1 + joined = " ".join(buf).strip() + if joined.startswith(":"): + joined = joined[1:].strip() + out[head] = joined + i = j + else: + i += 1 + missing = [n for n in names if n not in out] + if missing: + raise Untranslatable(f"rocq elaboration produced no type for {missing}") + return out + + +def rocq_elaborate(text, vpath, coq_path, names): + """Return {name: elaborated-type-string} via `coqc` + `Set Printing All`.""" + if not names: + return {} + unit_dir = os.path.dirname(os.path.abspath(vpath)) + appendix = ["", "Set Printing All.", + "Set Printing Width 2000000000.", + "Set Printing Depth 2000000000."] + appendix += [f"Check {nm}." for nm in names] + fd, tmp = tempfile.mkstemp(suffix=".v", prefix="elab_", dir=unit_dir) + try: + with os.fdopen(fd, "w") as f: + f.write(text.rstrip() + "\n" + "\n".join(appendix) + "\n") + try: + proc = subprocess.run([coq_path, "-q", os.path.basename(tmp)], + capture_output=True, text=True, cwd=unit_dir) + except OSError as e: + raise Untranslatable(f"could not run '{coq_path}': {e}") + if proc.returncode != 0: + msg = (proc.stderr or proc.stdout).strip().replace("\n", " ") + raise Untranslatable(f"rocq elaboration failed: {msg[:200]}") + return _parse_check_output(proc.stdout, names) + finally: + clean_coqc_temp(tmp) + + +# ─────────────────────────────── statement digest ──────────────────────────── + +def statement_digests(mengine_src): + """Normalized digest of each Theorem statement, for correspondence checking.""" + digs = [] + for line in mengine_src.splitlines(): + m = re.match(r"^Theorem\s+(\S+)\s*:\s*(.*)\.$", line) + if m: + norm = re.sub(r"\s+", " ", m.group(2)).strip() + digs.append((m.group(1), norm)) + return digs + + +# ─────────────────────────────────── main ──────────────────────────────────── + +def main(): + ap = argparse.ArgumentParser(description="Rocq .v -> MEngine .me translator") + ap.add_argument("input", help="input .v file") + ap.add_argument("--report", action="store_true", + help="print handled-construct counts, or FLAG the first " + "untranslatable construct") + ap.add_argument("--coq", default="coqc", + help="coqc/rocq binary for `Set Printing All` elaboration " + "(default: coqc)") + args = ap.parse_args() + + with open(args.input) as f: + text = f.read() + report = Report() + try: + elab = rocq_elaborate(text, args.input, args.coq, statement_names(text)) + src = translate_unit(text, report, elab) + except Untranslatable as e: + if args.report: + print(f"FLAG: {e.reason}") + sys.exit(2) + sys.stderr.write(f"Untranslatable: {e.reason}\n") + sys.exit(2) + + if args.report: + print(f"OK ({args.input})") + for k in sorted(report.handled): + print(f" handled {k}: {report.handled[k]}") + else: + sys.stdout.write(src) + + +if __name__ == "__main__": + main() diff --git a/src/commandlanguage/command_exec.c b/src/commandlanguage/command_exec.c index b8f05cf..af5d4f7 100644 --- a/src/commandlanguage/command_exec.c +++ b/src/commandlanguage/command_exec.c @@ -391,9 +391,8 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres return NULL; } - Expression *case_type = - _build_constructor_case_type(ctor_expr, motive_var, ind_var, params, param_count, - index_count, case_contexts[i]); + Expression *case_type = _build_constructor_case_type( + ctor_expr, motive_var, ind_var, params, param_count, index_count, case_contexts[i]); if (!case_type) { fprintf(stderr, ERROR "Failed to build case type for %s\n" CRESET, ctor->name); @@ -663,9 +662,9 @@ static Expression *_build_constructor_case_type(Expression *ctor_expr, Expressio // binders below because each hypothesis mentions its argument. for (size_t i = arg_count; i > 0; i--) { Expression *arg_var = (Expression *)dll_at(args, i - 1)->data; - Expression *hypothesis = _build_recursive_arg_hypothesis( - arg_var, kernel_expr_type(arg_var), ind_var, motive_var, param_count, index_count, - case_ctx); + Expression *hypothesis = + _build_recursive_arg_hypothesis(arg_var, kernel_expr_type(arg_var), ind_var, motive_var, + param_count, index_count, case_ctx); if (hypothesis) { case_type = kernel_arrow_create(hypothesis, case_type, case_ctx); } diff --git a/src/kernel/expression.c b/src/kernel/expression.c index 0ac1d6c..0e205bd 100644 --- a/src/kernel/expression.c +++ b/src/kernel/expression.c @@ -690,7 +690,31 @@ Expression *init_match_expression_wc(Expression *scrutinee, MatchBranch **branch // All branches must have the same type up to definitional equality. Expression *branch_body_type = get_expression_type(branch->body); if (match_type == NULL) { - match_type = branch_body_type; + // Transport the seed type out to the outer match `context` by + // substituting away this branch's parameter-slot pattern variables + // (each a delta-alias to one of the scrutinee's type arguments). + // Otherwise match_type keeps *this* branch's pattern-var context, + // which is not an ancestor of a sibling branch's context, so the + // (sound) convertibility check below spuriously rejects a valid + // non-dependent match whose branch type mentions the inductive's + // parameter -- e.g. a `nil A` branch, of type `list A`. (app/length + // escape only because their first branch is a variable/`O`, whose + // type already lives in the outer context.) Substituting a + // delta-alias for its body is meaning-preserving, so this only + // relocates the type, never changes it. + Expression *seed = branch_body_type; + for (int j = branch->pattern_var_count - 1; j >= 0; j--) { + Expression *pv = branch->pattern_variables[j]; + Expression *pv_body = get_var_body(pv); + if (pv_body != NULL) { + Expression *lowered = + new_subst(get_expression_context(seed), seed, pv, pv_body); + if (lowered != NULL) { + seed = lowered; + } + } + } + match_type = seed; } else if (!conversion_holds_in_context(get_expression_context(branch->body), branch_body_type, match_type)) { fprintf(stderr, ERROR "Branch body types do not match.\n" CRESET); @@ -1558,6 +1582,71 @@ bool fill_hole(Expression *hole, Expression *term) { SET_EXPR_TYPE(ptr, term); break; } + case (MATCH_SCRUTINEE): { + Expression *ptr = (Expression *)ul->ptr; + SET_MATCH_SCRUTINEE(ptr, term); + break; + } + // Branch/arg slots are array-indexed and the uplink carries no + // index, so locate the slot(s) still pointing at this hole and + // rebind them to term (the same hole may occupy more than one). + case (MATCH_BRANCH_BODY): { + Expression *ptr = (Expression *)ul->ptr; + for (int bi = 0; bi < ptr->as.match.branch_count; bi++) { + MatchBranch *br = ptr->as.match.branches[bi]; + if (br->body == hole) { + br->body = term; + br->body_uplink_node = add_to_parents(term, ptr, MATCH_BRANCH_BODY); + } + } + break; + } + case (MATCH_BRANCH_CONSTRUCTOR): { + Expression *ptr = (Expression *)ul->ptr; + for (int bi = 0; bi < ptr->as.match.branch_count; bi++) { + MatchBranch *br = ptr->as.match.branches[bi]; + if (br->constructor == hole) { + br->constructor = term; + br->constructor_uplink_node = + add_to_parents(term, ptr, MATCH_BRANCH_CONSTRUCTOR); + } + } + break; + } + case (MATCH_BRANCH_PATTERN_VAR): { + Expression *ptr = (Expression *)ul->ptr; + for (int bi = 0; bi < ptr->as.match.branch_count; bi++) { + MatchBranch *br = ptr->as.match.branches[bi]; + for (int pj = 0; pj < br->pattern_var_count; pj++) { + if (br->pattern_variables[pj] == hole) { + br->pattern_variables[pj] = term; + br->pattern_variables_uplink_nodes[pj] = + add_to_parents(term, ptr, MATCH_BRANCH_PATTERN_VAR); + } + } + } + break; + } + case (FIX_RECURSIVE_VAR): { + Expression *ptr = (Expression *)ul->ptr; + SET_FIX_RECURSIVE_VAR(ptr, term); + break; + } + case (FIX_ARG): { + Expression *ptr = (Expression *)ul->ptr; + for (int ai = 0; ai < ptr->as.fix.arg_count; ai++) { + if (ptr->as.fix.args[ai] == hole) { + ptr->as.fix.args[ai] = term; + ptr->as.fix.args_uplink_nodes[ai] = add_to_parents(term, ptr, FIX_ARG); + } + } + break; + } + case (FIX_BODY): { + Expression *ptr = (Expression *)ul->ptr; + SET_FIX_BODY(ptr, term); + break; + } default: fprintf(stderr, WARNING "todo: fill_hole for relation %d.\n" CRESET, ul->relation); diff --git a/tests/engine/test_integration.c b/tests/engine/test_integration.c index 5a8bad6..84dc060 100644 --- a/tests/engine/test_integration.c +++ b/tests/engine/test_integration.c @@ -442,14 +442,15 @@ static void test_fix_motive_apply(void) { /* Used to SIGSEGV type-checking the step case, where `add (S n) O` must convert * to `S (add n O)` under the `n` binder. */ static void test_fix_eliminator_exact(void) { - run_ok("fully explicit eliminator term over a fixpoint type-checks", - "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n" - "Fixpoint add (n : nat) (m : nat) {struct n} : nat :=\n" - " match n with | O => m | S p => S (add p m) end.\n" - "Axiom f_equal_S : forall (a : nat), forall (b : nat), forall (_: eq nat a b),\n" - " eq nat (S a) (S b).\n" - "Check (nat_ind (fun (k : nat) => eq nat (add k O) k) (eq_refl nat O)\n" - " (fun (n : nat) => fun (ih : eq nat (add n O) n) => f_equal_S (add n O) n ih)).\n"); + run_ok( + "fully explicit eliminator term over a fixpoint type-checks", + "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n" + "Fixpoint add (n : nat) (m : nat) {struct n} : nat :=\n" + " match n with | O => m | S p => S (add p m) end.\n" + "Axiom f_equal_S : forall (a : nat), forall (b : nat), forall (_: eq nat a b),\n" + " eq nat (S a) (S b).\n" + "Check (nat_ind (fun (k : nat) => eq nat (add k O) k) (eq_refl nat O)\n" + " (fun (n : nat) => fun (ih : eq nat (add n O) n) => f_equal_S (add n O) n ih)).\n"); } /* Used to fail cleanly with a type error: a Definition whose declared type is