Automatic Goal Clone Detection in Rocq

Ali Ghanbari

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 clonin…