Automatic Goal Clone Detection in Rocq

TL;DR

The paper tackles redundant proof engineering in Rocq by introducing clone-finder, a tool that detects goal clones through formal $\alpha$-equivalence of Gallina terms. It builds proof trees, generalizes goals, and identifies $\alpha$-equivalent generalized goals across large Rocq codebases, enabling potential proof reuse. Evaluation on 40 CoqGym Rocq projects reveals frequent cloning (average 27.73 clones per project) and categorizes clones into exact duplication, generalized proofs, and entirely different proofs, highlighting tangible opportunities to factor out reusable lemmas. The work demonstrates a lightweight, end-to-end approach with substantial integration time overhead primarily from Coq-LSP, and it includes open-source enhancements to CoqPyt and a Gallina parser, laying groundwork for future improvements such as semantic cloning, plugin integration, and η-equivalence detection.

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 α-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 α-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 α-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.

Figures (5)

• Figure 1: A simple Rocq theorem and its proof in Ltac. The proof process starts with the theorem statement as the current goal. Each valid Ltac command transforms the state of the proof assistant, prompting it to generate zero or more new goals. This amounts to creating a proof tree, where nodes corresponds to goals and the edges are labeled with the Ltac command that generated the child nodes. A depth-first search on each node of the tree to accumulate the tactics at the edges constitute the sub-proof for the goal at each node. This figure also illustrates how Algorithm \ref{['alg:proof_tree_algo']} constructs proof trees by executing proofs line by line, while tracking the goals that are created and eliminated as a result of running each tactic
• Figure 2: Abstract syntax of a core subset of Gallina terms.
• Figure 3: Duplicate proofs example: Example of two goals from Rocq project Chapar where $\alpha$-equivalent goals show up in two different theorems KVSAlg1CauseObl.algrec_step and KVSAlg1CauseObl.cause_rec and identical proofs have been used.
• Figure 4: More general proof reinvented: Example of two goals from Rocq project GroupTheory where $\alpha$-equivalent goals show up in two different theorems T_1_6_3 and T_1_6_4. The second proof is a more general form of the first one, and the proofs seem to be reinvented for each goal.
• Figure 5: Reinvented proofs example: Example of two goals from Rocq project HighschoolGeometry where $\alpha$-equivalent goals show up in two different theorems intersection_cercle_droite and intersection2_cercle_droite, different proofs seem to be reinvented.

Theorems & Definitions (4)

• Definition 1: Free Variables
• Definition 2: Substitution
• Definition 3: $\alpha$-equivalence
• Definition 4: prodBody Function