REVIEW 4 major objections 5 minor 29 references
Automatic Goal Clone Detection in Rocq
T0 review · 4 major / 5 minor · reviewed 2026-08-16 · deepseek-v4-flash
Pith's one-line read Real Rocq projects contain, on average, 27.73 pairs of alpha-equivalent proof goals that are proved separately.
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (4)
- [§6 and Algorithm 1 (lines 19–29)] 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.
- [§4 and Algorithm 3] 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.
- [§5.2 and Table 1] 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.
- [Algorithm 2 (lines 11–17)] 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.
minor comments (5)
- [§1 and §5.2] 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.
- [§3, Definition 2] 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.
- [§3, Algorithm 1] The comment on line 8 of Algorithm 1 says "file name and the the current theorem name pairs"; please fix the duplicated "the".
- [§5.2, Table 1] 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.
- [Figures 3–5] 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.
Circularity Check
No circularity: the clone counts are direct measurements under a standard α-equivalence definition, and the §6 proof-tree caveat is a validity threat, not a circular step.
full rationale
The paper's central empirical claim is that 40 CoqGym projects contain an average of 27.73 goal clones. This is a measurement: clone-finder extracts generalized goals, checks α-equivalence using the standard recursive definition in Definitions 1–3, and counts pairs in Algorithm 4. The notion of goal clone is explicitly defined as α-equivalent goals, so the detector operationalizes its own definition, but the paper does not derive the count from a separate quantity that was defined in terms of the count. There is no fitted parameter, no self-citation chain, and no imported uniqueness theorem. The only author-affiliated reference is the open-source repository URL [17], which is not load-bearing. The §6 limitation about compound tactics and focus-shifting tactics concedes that proof-tree reconstruction may attach inaccurate proof boundaries, which could affect the reported counts; however, that is a threat to the correctness or validity of the measurement, not circularity, because the result does not reduce by construction to the assumptions of Algorithm 1. The benchmark is an independent external dataset (CoqGym [42]) created by other authors, and the minimum proof-size threshold of 5 Ltac lines is a fixed user-set parameter rather than a value fitted to the data. Therefore no circular step is present.
Assumptions & free parameters
free parameters (1)
- minimum proof size threshold =
5 (default, lines of Ltac)
assumptions (5)
- domain assumption Goal-tracking through Coq-LSP step execution correctly reconstructs proof trees.
- standard math Generalizing a goal by quantifying its context variables in reverse topological order preserves type well-formedness.
- ad hoc to paper The global context can be ignored when comparing goals.
- domain assumption The filtered CoqGym subset represents real-world Rocq proof development.
- domain assumption The Python Gallina parser computes alpha-equivalence correctly for the core language.
Cite this review
Pith. "Pith review of Automatic Goal Clone Detection in Rocq." pith.science (2026). https://pith.science/paper/A625SP52
@misc{pith2026250419129,
author = {Pith},
title = {Pith review of: Automatic Goal Clone Detection in Rocq},
year = {2026},
howpublished = {\url{https://pith.science/paper/A625SP52}},
note = {Machine review of arXiv:2504.19129}
}
read the original abstract
Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving {\alpha}-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of {\alpha}-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or {\alpha}-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.
Reference graph
Works this paper leans on
-
[8]
doi:10.1145/3421473.3421477. 14 Emily First and Yuriy Brun. Diversity-driven automated formal verification. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022, pages 1–13. ACM, 2022.doi:10.1145/3510003.3510138. 15 Emily First, Yuriy Brun, and Arjun Guha. Tactok: semantics-aware proof syn...
arXiv 2022
-
[9]
doi:10.1145/3428299. 16 Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Satish Chandra, Kelly Blincoe, and Paolo Tonella, editors, Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE ...
-
[16]
28 Micheline Bénédicte Moumoula, Abdoul Kader Kaboré, Jacques Klein, and Tegawendé F
doi:10.1145/1538788.1538814. 28 Micheline Bénédicte Moumoula, Abdoul Kader Kaboré, Jacques Klein, and Tegawendé F. Bis- syandé. Large language models for cross-language code clone detection.CoRR, abs/2408.04430,
-
[17]
URL: https://doi.org/10.48550/arXiv.2408.04430, arXiv:2408.04430, doi:10. 48550/ARXIV.2408.04430. 29 Morteza Zakeri Nasrabadi, Saeed Parsa, Mohammad Ramezani, Chanchal Roy, and Masoud Ekhtiarzadeh. A systematic literature review on source code similarity measurement and clone detection: Techniques, applications, and challenges.J. Syst. Softw., 204:111796,
-
[22]
URL: https://arxiv.org/abs/2003.06458, arXiv:2003.06458. A. Ghanbari 23:19 34 Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for proof reuse in coq. In John Harrison, John O’Leary, and Andrew Tolmach, editors,10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 ...
work page Pith review arXiv 2003
-
[24]
36 Chanchal Kumar Roy and James R Cordy
doi:10.1007/978-3-319-43144-4\_32. 36 Chanchal Kumar Roy and James R Cordy. A survey on software clone detection research. Queen’s School of computing TR, 541(115):64–68,
-
[26]
doi:10.1145/3593374. 39 Paula Severi and Erik Poll. Pure type systems with definitions. In Anil Nerode and Yuri V. Matiyasevich, editors,Logical Foundations of Computer Science, Third International Sympo- sium, LFCS’94, St. Petersburg, Russia, July 11-14, 1994, Proceedings, volume 813 ofLecture Notes in Computer Science, pages 316–328. Springer, 1994.doi:...
-
[27]
Deep learning code fragments for code clone detection
41 Martin White, Michele Tufano, Christopher Vendome, and Denys Poshyvanyk. Deep learning code fragments for code clone detection. In David Lo, Sven Apel, and Sarfraz Khurshid, editors, Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pages 87–98. ACM,
work page 2016
Show all 29 references
-
[28]
42 Kaiyu Yang and Jia Deng
doi: 10.1145/2970276.2970326. 42 Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors,Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, ...
-
[29]
43 Dongjin Yu, Jie Wang, Qing Wu, Jiazha Yang, Jiaojiao Wang, Wei Yang, and Wei Yan
URL: http://proceedings.mlr.press/v97/yang19a.html. 43 Dongjin Yu, Jie Wang, Qing Wu, Jiazha Yang, Jiaojiao Wang, Wei Yang, and Wei Yan. Detecting java code clones with multi-granularities based on bytecode. In Sorel Reisman, Sheikh Iqbal Ahamed, Claudio Demartini, Thomas M. C...
2017
-
[1992]
The coq proof assistant documentation,
ECOOP 2025 23:18 Automatic Goal Clone Detection in Rocq 20 Inria. The coq proof assistant documentation,
2025
-
[1993]
32 Clément Pit-Claudel and Pierre Courtieu
URL:https://doi.org/10.1007/BFb0037116, doi: 10.1007/BFB0037116. 32 Clément Pit-Claudel and Pierre Courtieu. Company-coq: Taking proof general one step closer to a real ide. InCoqPL’16: The Second International Workshop on Coq for PL, January
-
[1995]
12 David Delahaye
URL:https://hal.univ-lorraine.fr/tel-01748604. 12 David Delahaye. A tactic language for the system coq. In Michel Parigot and Andrei Voronkov, editors, Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-1...
-
[2001]
4 Yves Bertot and Pierre Castéran.Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions
doi:10.1007/3-540-45315-6\_4. 4 Yves Bertot and Pierre Castéran.Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.doi:10.1007/978-3-662-07964-5. A. Ghan...
-
[2002]
31 Christine Paulin-Mohring
doi:10.1007/3-540-45949-9. 31 Christine Paulin-Mohring. Inductive definitions in the system coq - rules and properties. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’...
-
[2004]
22 Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer
doi:10.1007/978-3-540-30142-4\_12. 22 Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28:e20,
-
[2007]
Generatingcorrectness proofs with neural networks
37 AlexSanchez-Stern, YousefAlhessi, LawrenceK.Saul, andSorinLerner. Generatingcorrectness proofs with neural networks. In Koushik Sen and Mayur Naik, editors, Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL@PLDI 20...
2020
-
[2008]
25 Iman Keivanloo, Chanchal K
URL: https: //doi.org/10.1007/s10664-008-9076-6, doi:10.1007/S10664-008-9076-6. 25 Iman Keivanloo, Chanchal K. Roy, and Juergen Rilling. Java bytecode clone detection via relaxation on code fingerprint and semantic web reasoning. In James R. Cordy, Katsuro Inoue, Rainer Koschk...
-
[2009]
2 Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
doi:10.1007/s10817-009-9123-z. 2 Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. Concert: a smart contract certification framework in coq. In Jasmin Blanchette and Catalin Hritcu, editors, Pro- ceedings of the 9th ACM SIGPLAN International Conference on Certified Progr...
-
[2010]
27 Xavier Leroy
doi:10.1145/1743546.1743574. 27 Xavier Leroy. Formal verification of a realistic compiler.Commun. ACM, 52(7):107–115,
-
[2012]
7 Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F
doi:10.1007/978-3-642-31374-5\_3. 7 Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, and Emily First. Coqpyt: Proof navigation in python in the era of llms. In Marcelo d’Amorim, editor, Companion Proceedings of the 32nd ACM International Conference ...
-
[2017]
IEEE Computer Society, 2017.doi:10.1109/COMPSAC
Volume 1, pages 317–326. IEEE Computer Society, 2017.doi:10.1109/COMPSAC. 2017.104. ECOOP 2025
2017 doi
-
[2018]
cloning considered harmful
doi:10.1017/S0956796818000151. 23 Elmar Jürgens, Florian Deissenboeck, Benjamin Hummel, and Stefan Wagner. Do code clones matter? In 31st International Conference on Software Engineering, ICSE 2009, May 16-24, 2009, Vancouver, Canada, Proceedings, pages 485–495. IEEE, 2009.doi...
2009 doi
-
[2019]
35 Kenneth Roe and Scott F
URL:https://doi.org/10.4230/LIPIcs.ITP.2019.26, doi:10.4230/ LIPICS.ITP.2019.26. 35 Kenneth Roe and Scott F. Smith. Coqpie: An IDE aimed at improving proof development productivity - (rough diamond). In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem...
2019 doi
-
[2020]
3 Gilles Barthe and Olivier Pons
doi:10.1145/3372885.3373829. 3 Gilles Barthe and Olivier Pons. Type isomorphisms and proof reuse in dependent type theory. In Furio Honsell and Marino Miculan, editors,Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held a...
-
[2021]
6 Timothy Bourke, Matthias Daum, Gerwin Klein, and Rafal Kolanski
URL:https://ceur-ws.org/Vol-3377/fmm12.pdf. 6 Timothy Bourke, Matthias Daum, Gerwin Klein, and Rafal Kolanski. Challenges and ex- periences in managing large-scale proofs. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and V...
2012
-
[2023]
30 Tobias Nipkow, Lawrence C
URL: https://doi.org/10.1016/j.jss.2023.111796, doi:10.1016/J.JSS.2023.111796. 30 Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 ofLecture Notes in Computer Science. Springer,
2023
-
[2024]
8 Coq-Elpi Team
doi:10.1145/3663529.3663814. 8 Coq-Elpi Team. Coq-Elpi: Coq plugin embedding elpi,
-
[2025]
URL: https:// rocq-prover.org/doc/V9.0.0/refman/index.html
Accessed: 04/22. URL: https:// rocq-prover.org/doc/V9.0.0/refman/index.html. 21 Einar Broch Johnsen and Christoph Lüth. Theorem reuse by proof term transformation. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors,Theorem Proving in Higher Order Logics, 17th ...
2004
Reviewed August 16, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.