Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant
This work provides a tool for mathematicians and formal verification practitioners to automate proofs in projective geometry within Coq, though it is incremental as it embeds an existing prover.
The authors integrated an automated theorem prover for projective geometry into Coq as a plugin, enabling it to be used as a tactic to generate proof scripts for geometric configurations.
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.