Recycling Proof Patterns in Coq: Case Studies

TL;DR

This paper presents case studies on recycling proof patterns in Coq, evaluating a machine-learning tool that helps users identify reusable proof strategies within large libraries.

Contribution

It introduces a novel approach using ML4PG to data-mine proof libraries for pattern reuse, aiding non-expert users across domains.

Findings

ML4PG effectively identifies reusable proof patterns

Proof pattern reuse improves library accessibility

Case studies demonstrate practical benefits of pattern mining

Abstract

Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries.