When Agda met Vampire

TL;DR

This paper presents a method to integrate Agda with the ATP Vampire by translating between constructive and classical logic, enabling automated proofs while maintaining correctness guarantees.

Contribution

It introduces an expressive fragment for sound translation between Agda and Vampire, creating a prototype system that automates proof obligations in dependent type theory.

Findings

Automated proofs were generated for complex algebraic properties.

The approach simplifies proof automation in dependently-typed systems.

The prototype required modest engineering effort.

Abstract

Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in implementation. We aim to improve the situation by integrating proof assistants with automated theorem provers (ATPs) in a simple way, while preserving the correctness guarantees of the former. A central difficulty arises from the fact that most ATPs operate in classical first-order logic, whereas these proof assistants are grounded in constructive dependent type theory. We identify an expressive fragment of both languages -- essentially equational Horn -- that admits sound, straightforward translations in both directions. The approach produces a prototype system for Agda forwarding proof obligations to the ATP Vampire, then transforming the resulting classical proof into a constructive proof term that Agda can type-check. The prototype automatically derives proofs concerning the properties of a complex field equipped with roots of unity, which took professional Agda developers two full days to complete. The required engineering effort is modest, and we anticipate that the methodology will extend readily to other ATPs and proof assistants.