Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant

TL;DR

This paper presents a method to integrate an automated projective geometry prover, based on matroids, into the Coq proof assistant as a tactic, streamlining geometric proofs.

Contribution

It introduces a plugin architecture that embeds an external C-based prover into Coq, enabling automated proofs of projective geometry theorems as tactics.

Findings

Successfully embedded the prover as a Coq tactic

Automated proof generation for projective geometry theorems

Enhanced proof automation in Coq for geometric reasoning

Abstract

Recently, we developed an automated theorem prover for projective incidence geometry. This prover, based on a combinatorial approach using matroids, proceeds by saturation using the matroid rules. It is designed as an independent tool, implemented in C, which takes a geometric configuration as input and produces as output some Coq proof scripts: the statement of the expected theorem, a proof script proving the theorem and possibly some auxiliary lemmas. In this document, we show how to embed such an external tool as a plugin in Coq so that it can be used as a simple tactic.