{"id":"001930a6-c2eb-4b56-9f30-463ef3292acb","arxiv_id":"2504.19129","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"clone-finder detects alpha-equivalent proof goals in Rocq projects and estimates that real codebases hold an average of 27.73 such goal clones per project with a 5-line proof threshold.","lead":"A proof-engineering tool named clone-finder scans Rocq (Coq) projects and reports goal statements that are duplicates up to variable renaming. On 40 real-world projects it found such clones in 20, with a few large projects containing hundreds, pointing to reusable proof work.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Headline clone count rests on an unmeasured proof-tree reconstruction unsoundness conceded in §6; a filtering experiment would show whether the 27.73 average is an artifact.","rationale":"The reader's weakest assumption identifies exactly the load-bearing concern: Algorithm 1's proof-tree reconstruction is unsound under compound/multi-goal/focus-shifting tactics, and the empirical clone counts depend on the accuracy of this tree. The full text concedes this in §6 but does not quantify its impact. My analysis adds that the dismissal ('not harmful') is inconsistent with the paper's own metric, which counts pairs with proofs of at least 5 lines; any proof-boundary inaccuracy directly changes which pairs are counted. The proposed test (filtering out compound tactics and re-running) directly measures how much of the headline average depends on the unsound cases. The paper's other weaknesses—no precision/recall, no baseline, local-context-only comparison—are secondary to this core issue. Because the concern is real but addressable through a straightforward experiment, the reader's CONDITIONAL verdict remains appropriate, with no change needed.","tokens_in":19445,"tokens_out":3164,"duration_ms":36800,"concrete_test":"On the four projects with the largest clone counts (Chapar, HighSchoolGeometry, Subst, Stalmarck), run clone-finder twice: (1) as-is, reproducing Table 1; (2) with a preprocessing filter that rejects or splits any proof step whose tactic string contains ';', '||', 'all:', 'try', 'first', 'repeat', or ';[', so only linear atomic-tactic proofs are analyzed. Compare per-project clone counts and the resulting average. If the filtered average drops substantially (e.g., below 10) or the relative ordering of projects changes, the headline 27.73 figure is an artifact of the conceded proof-tree unsoundness. A complementary check: manually replay 20 randomly sampled reported clone pairs from these projects in stock Coq, verifying at each step that the reported goals actually appear and that the attached proof segment has the claimed length; if more than 10% of samples fail, the count is inflated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Algorithm 1 builds proof trees by pairing every disappeared goal with every newly introduced goal at the same tactic step (lines 19–29). With compound tactics, tactics that resolve multiple goals, or focus-shifting tactics, this pairing is invalid. The tree is then used to attach proofs to goals (GetProof via DFS) and to decide which goals become nodes; inaccurate boundaries mean the proof length attached to a goal may include tactics from other branches or omit some of its own. Since the reported clone count is the number of α-equivalent generalized goal pairs whose proofs have at least 5 lines of Ltac, misattributed tactics can both create spurious pairs and promote sub-threshold pairs into the count. The paper explicitly concedes this in §6 ('reporting inaccurate results when facing with compound tactics, tactics that resolves more than one goal, and focus-shifting tactics') but dismisses it as 'not harmful' because 'missing a few clone cases or reporting inaccurate proof boundaries for a goal is not harmful.' That dismissal is not valid for a quantitative headline: inaccurate boundaries directly alter the count being reported, not just recall. The central claim (27.73 average clones per project) therefore depends on an acknowledged unsoundness whose magnitude has never been measured. If many reported proofs are actually longer or shorter than the true sub-proofs, the average could be substantially inflated or deflated, and the qualitative conclusion about widespread redundancy would need re-examination.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces clone-finder, a Python tool that detects duplicate proof goals in Rocq (Coq) developments by comparing goals up to alpha-equivalence. The pipeline first reconstructs a proof tree for each theorem by executing the proof script step by step through Coq-LSP and matching goals that disappear with goals that appear (Algorithm 1). Each goal is then generalized by universally quantifying its free variables from the local context (Algorithm 3), and redundant goals whose generalizations are bodies of other goals are removed (Algorithm 2). Finally, all remaining goal pairs are checked for alpha-equivalence (Algorithm 4), and pairs whose attached proofs have at least a configurable number of Ltac lines (default 5) are reported as clones. The evaluation runs the tool on 40 Rocq projects from CoqGym, reporting that 20 of the 40 projects contain at least one clone, with an average of 27.73 clones per project, and that clones fall into three categories: identical proofs, generalized proofs, and entirely different proofs. The paper also reports runtime measurements, noting that most of the end-to-end time is spent in Coq-LSP/CoqPyt and that the pure analysis time averages 45.31 seconds per project.","tokens_in":19698,"tokens_out":4486,"duration_ms":48717,"significance":"If the empirical claims were established, this would be a useful contribution to proof engineering: the idea of detecting alpha-equivalent goals as reusable lemma candidates is natural, and the use of alpha-equivalence avoids the heuristics of token-based proof clone detectors. The paper ships an open-source implementation, contributes an extension to CoqPyt for physical-to-logical path mapping, and evaluates on an independent, real-world benchmark (CoqGym). The formal definitions of free variables, substitution, and alpha-equivalence are a strength, and the paper correctly identifies that the main cost is in the Coq-LSP interface rather than in the detection logic itself. However, the central quantitative claim---an average of 27.73 goal clones per project---is not yet supported because the proof-tree construction has an acknowledged unsoundness whose magnitude is unmeasured, and because the evaluation lacks precision/recall against ground truth or a baseline. The contribution is therefore at the stage of a promising tool with a plausible but unvalidated headline result.","major_comments":[{"comment":"The abstract's central claim, \"each project contains an average of 27.73 instances of goal clone,\" depends entirely on the proof trees built by Algorithm 1. That algorithm pairs every goal that disappears at a tactic step with every goal that appears at the same step. As the paper concedes in §6, this construction is inaccurate for compound tactics, tactics that resolve multiple goals, and focus-shifting tactics. The dismissal of this issue as \"not harmful\" is not valid for a quantitative headline: the clone count in Table 1 is gated on proofs having at least 5 lines of Ltac, so misattributed tactics can both create spurious clone pairs and move real pairs across the size threshold. The magnitude of this effect has not been measured. I request an experiment that either filters out proofs containing such tactics (as prior work cited in §6 does) or validates the reconstructed proof trees against ground-truth proof structure on a sample, and then reports how the 27.73 average changes.","section":"§6 and Algorithm 1 (lines 19–29)"},{"comment":"The implementation considers only local contexts when generalizing goals. The paper states in §4 that this \"could introduce unsoundness and false positives.\" Concretely, two goals that differ only in the global context, or in section variables that are not part of the local hypothesis list, would be treated as alpha-equivalent even though they may not be interchangeable proof obligations. Since the evaluation reports clone counts without any measurement of false positives, this acknowledged approximation directly threatens the validity of Table 1. The paper should quantify the false-positive rate, for example by manually inspecting a random sample of reported clones or by running a variant that includes the full context and comparing results.","section":"§4 and Algorithm 3"},{"comment":"The evaluation reports only raw clone counts; there is no precision, recall, or comparison against a ground-truth set of goal clones. The paper mentions \"manual review\" of clones but gives no methodology: how many clones were inspected, whether the review was independent, what the agreement rate was, or how many reported pairs were rejected as false positives. Without this, the reader cannot distinguish true redundancy from artifacts of the proof-tree reconstruction and the local-context approximation. I also note that the average of 27.73 is heavily influenced by a few projects (Chapar with 447, HighSchoolGeometry with 218, Stalmarck with 78, Subst with 82); the paper should report the distribution and the average over non-zero projects, not only the overall mean.","section":"§5.2 and Table 1"},{"comment":"The deduplication step removes any goal whose generalization is a body of another goal's generalization, using the prodBody predicate. This is a strong heuristic: a concrete instance of a more general goal may require a different proof or may be a separate genuinely duplicated development, and removing it before the alpha-equivalence comparison can lower the reported clone count. The paper does not evaluate the sensitivity of the reported 27.73 average to this deduplication step. I ask for an ablation that disables or varies the deduplication rule and reports the effect on the clone counts.","section":"Algorithm 2 (lines 11–17)"}],"minor_comments":[{"comment":"The phrase \"an average 45.31 seconds of run time, for a fresh run\" is ambiguous because §5.2 reports 45.31 seconds as the analysis time after type-checking, while the end-to-end average is 1,833.345 seconds; please state which average is being quoted in the introduction and abstract.","section":"§1 and §5.2"},{"comment":"The substitution definition has a case that appears redundant: the second clause for forall and other binders states a condition \"if x0∉FV(u)\" with the substitution not applied to the body, which seems to be the capture-avoidance case. Please clarify the intended conditions and check that all variable-capture cases are covered.","section":"§3, Definition 2"},{"comment":"The comment on line 8 of Algorithm 1 says \"file name and the the current theorem name pairs\"; please fix the duplicated \"the\".","section":"§3, Algorithm 1"},{"comment":"The runtime columns are labeled \"clone-finder Total\" and \"Analysis,\" but the text in §5.2 refers to the first of these as \"clone-finder Total\" and then says \"(2)\" twice when listing time measurements; please renumber the list and make the column names match the text.","section":"§5.2, Table 1"},{"comment":"The example clones are informative, but the proof scripts are typeset in a way that may be hard to read in print; consider using a monospaced font with lighter syntax highlighting or larger line spacing.","section":"Figures 3–5"}],"recommendation":"major_revision","confidential_remarks":"The paper's core idea is sound and the artifact appears to be real, but the headline empirical claim is currently under-supported by the evaluation. The author should be encouraged to add the validation experiments requested in the major comments: a sensitivity analysis around the proof-tree reconstruction, a false-positive sample, and an ablation of the deduplication step. The editor may also want to verify that the open-source repository is available and contains the described CoqPyt extension, since that is a listed contribution."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nShort version: this is the first goal-clone detector for Rocq/Coq I know of, and the core idea—alpha-equivalence over generalized goals—is sound and clearly implemented. But the paper's headline number, 27.73 clones per project, is not supported by the evaluation. The proof-tree construction has an acknowledged unsoundness that directly affects the count, and there is no ground truth or baseline to calibrate it.\n\nWhat's actually new: clone-finder detects alpha-equivalent goals across Coq developments, using local-context universal generalization and a Gallina parser, and it ships source code. Prior work on Isabelle/HOL script clones targets proof text, not goal obligations. The pipeline is reasonable: build proof trees via Coq-LSP, flatten, dedupe, generalize, compare with alpha-equivalence. The three observed categories—identical proofs, generalized proofs, different proofs—are a useful qualitative finding, and the runtime numbers suggest the tool is practical once dependencies are loaded.\n\nWhere it's soft: Algorithm 1 reconstructs proof trees by pairing disappeared goals with newly introduced goals at each tactic step. That fails for compound tactics, tactics that solve multiple goals, and focus-shifting tactics, as the paper admits in Section 6. The authors say missing a few clones or inaccurate proof boundaries is not harmful, but the reported clone count is defined as pairs whose proofs have at least five lines of Ltac. If proof boundaries are wrong, sub-threshold pairs can be promoted into the count and spurious pairs can appear. So the 27.73 average (median 0.5) is not a reliable estimate of real duplicate-goal frequency. The mean is also dragged up by two large projects (Chapar 447, HighSchoolGeometry 218). There is no precision or recall, no manual validation of all reported pairs beyond illustrative examples, and no comparison to a baseline or to the Isabelle/HOL clone detectors. The local-context-only comparison is another acknowledged source of false positives, though it is probably minor in practice.\n\nThat said, none of this is fatal to the technique. The weaknesses are empirical and fixable: a filtering experiment that excludes proofs containing compound or multi-goal tactics, plus a sample manual audit, would tell us whether the clones are real. The paper is honest about the limitations, and the open-source artifact is a real contribution.\n\nWho it's for: proof engineering and ITP researchers, and tool builders interested in Coq infrastructure. It deserves a serious referee—an editor should send it out, but reviewers should push for a much more careful evaluation before publication. I would condition acceptance on measured precision and a robustness check of the proof-tree assumptions.","headline":"First Coq goal-clone detector with a sound core idea, but the headline clone count rests on an unmeasured proof-tree reconstruction unsoundness the paper itself concedes.","tokens_in":20208,"tokens_out":1926,"would_cite":true,"duration_ms":19091,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Real Rocq projects contain, on average, 27.73 pairs of alpha-equivalent proof goals that are proved separately.","keywords":["goal clone detection","Rocq","Coq","alpha-equivalence","proof reuse","proof engineering","Gallina","Ltac"],"falsifier":"Re-run the 40-project evaluation with proof trees built from the prover's own goal stack instead of the disappeared-goal-is-parent heuristic, and compare the reported clone pairs; substantial disagreement on even one project would show that the 27.73 average reflects the reconstruction method rather than the projects themselves.","tokens_in":19236,"feed_emoji":"🔁","tokens_out":8972,"duration_ms":79391,"temperature":0.7,"pith_summary":"The paper introduces clone-finder, a tool that scans Rocq (formerly Coq) proof files for goal clones: pairs of proof obligations that are alpha-equivalent, meaning they are the same statement up to renaming of bound variables. To find them, clone-finder reconstructs the proof tree of every theorem, generalizes each goal by quantifying over the free variables from its local context, and compares the generalized goals. Evaluated on 40 real-world Rocq projects, the tool found at least one clone in 20 projects and an average of 27.73 clone pairs per project. The paper's point is that duplicated proof obligations are common enough that finding them automatically could let proof engineers factor shared subproofs into reusable lemmas and save real effort.","feed_headline":"Rocq re-proves the same goal 27.73 times per project on average","feed_subtitle":"A new clone-finder detects alpha-equivalent obligations so proof engineers can factor them into reusable lemmas.","key_machinery":"The load-bearing mechanism is the proof-tree reconstruction of Algorithm 1, which tracks the goals present at each step and treats every disappeared goal as the parent of the goals that appear in its place; the subproof of a goal is the depth-first accumulation of tactics under its node. Algorithm 3 then computes a goal's generalization by topologically sorting the free variables in its local context and prefixing universal quantifiers in dependency order, and Algorithm 2 prunes a generalized goal when it is the body of another product type via the prodBody check. Finally, Algorithm 4 compares every surviving pair of generalized goals for alpha-equivalence, with alpha-equivalence defined by the standard renaming and compatibility rules for the core Gallina syntax in Definitions 1-3. The proof-size threshold of five lines of Ltac is the filter that makes the output about duplicated effort worth recovering, rather than about trivial goals.","core_discovery":"The central claim is that real Rocq developments repeat themselves: the same goal, up to variable renaming, is proved from scratch in multiple places. clone-finder operationalizes this by executing every proof step through a language server, reconstructing a proof tree whose nodes are goals and whose edges are tactics, then replacing each goal by its generalization, a forall-prefixed form that makes context variables explicit. Two goals are reported as clones when their generalizations are alpha-equivalent under the standard rules for Gallina terms and each subproof contains at least five lines of Ltac. In the evaluation, 20 of 40 projects had at least one such clone, the per-project mean was 27.73, and manual inspection showed three patterns: identical or near-identical proofs, one proof that is a generalization of the other, and entirely different proofs of the same goal. The author argues these clones represent wasted proof effort that could be recovered by extracting the common goal as a lemma.","pith_inferences":["The 27.73 average is tied to the paper's measurement choices: it counts only pairs whose proofs have at least five lines of Ltac, only within the 40 projects that ran on one Coq version, and only syntactic alpha-equivalence; the true rate of redundant proof effort in other settings could be higher or lower.","Because the proof-tree reconstruction assumes a disappeared goal is the parent of newly appeared goals, a robustness check not run in the paper would be to rebuild proof trees from the prover's internal goal stack and see whether the reported clone pairs survive.","A natural extension of the same machinery would be to compare goals modulo eta-equivalence or after beta-normalization, which would catch a broader class of duplicated obligations; the paper lists eta-equivalence as future work.","The same alpha-equivalence checks could be used in reverse: instead of removing redundancies, mined pairs of entirely different proofs of the same goal could serve as training data for proof synthesis or as examples for teaching alternative proof strategies."],"forward_implications":["Proof engineers could run clone-finder on their own developments and obtain a list of goal pairs whose subproofs are candidates to be factored out as independent lemmas.","The three clone categories imply different refactoring costs: identical proofs are the cheapest to unify, generalized proofs should be preserved in their more general form, and entirely different proofs require choosing one proof before extraction.","Because the average pure-analysis time is 45.31 seconds per project and most end-to-end time is spent reloading dependencies, caching a project's compiled dependencies would make the tool practical for daily use and for IDE integration.","Finding clones in half of the sampled projects suggests that duplicated proof effort in Rocq is not a rare edge case, so tool support for proof reuse may benefit a broad range of formal verification projects."],"supporting_citations":[{"why":"supplies the corpus of real-world Rocq projects from which the 40-project benchmark and clone counts are drawn.","marker":"[42]"},{"why":"provides the language-server interface that Algorithm 1 drives to execute proof scripts step by step.","marker":"[9]"},{"why":"gives the Python API used to extract goals, hypotheses, and tactics from the prover during execution.","marker":"[7]"},{"why":"provides the foundational treatment of the calculus of inductive constructions and the alpha-equivalence notion underlying the clone definition.","marker":"[4]"},{"why":"defines proof engineering and proof reuse, the problem context that motivates detecting duplicated goals.","marker":"[33]"},{"why":"documents the scale and maintenance challenges of large verification projects, motivating automated detection of redundant proof effort.","marker":"[6]"},{"why":"is one of the lemma-extraction tools the paper says could turn detected goal clones into reusable lemmas.","marker":"[32]"},{"why":"is the other lemma-extraction IDE tool that could consume clone-finder's output for refactoring.","marker":"[35]"}],"fun_headline_variants":["27.73 goal clones per Rocq project","Rocq re-proves goals: clone-finder counts 27.73","Alpha-equivalent goals tackled by clone-finder","Spot duplicate Rocq goals with clone-finder","Rocq clone detection: 27.73 duplicates average"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The entire clone count depends on the reconstructed proof tree being accurate, and the reconstruction assumes that whenever a goal disappears and new goals appear, the disappeared goal is the parent of the new goals; compound tactics, tactics that solve several goals at once, and focus-shifting tactics violate that assumption.","fun_headline_variants_meta":{"raw":{"variants":["27.73 goal clones per Rocq project","Rocq re-proves goals: clone-finder counts 27.73","Alpha-equivalent goals tackled by clone-finder","Spot duplicate Rocq goals with clone-finder","Rocq clone detection: 27.73 duplicates average"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000272,"raw_usage":{"total_tokens":1620,"prompt_tokens":921,"completion_tokens":699,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":537,"completion_tokens_details":{"reasoning_tokens":618}},"tokens_in":537,"tokens_out":699,"duration_ms":6137,"temperature":1.0,"reasoning_tokens":618,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T06:00:30.106242+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Re-run the 40-project evaluation with proof trees built from the prover's own goal stack instead of the disappeared-goal-is-parent heuristic, and compare the reported clone pairs; substantial disagreement on even one project would show that the 27.73 average reflects the reconstruction method rather than the projects themselves.","supporting_citations":[],"review_version":1}