Performing Implicit Induction Reasoning with Certifying Proof Environments

TL;DR

This paper introduces a new tactic for Coq that automates implicit induction reasoning by integrating Spike, enabling automatic proof generation and certification within the proof assistant.

Contribution

It presents a novel approach to perform implicit induction in Coq through an automatic black-box method using Spike, enhancing proof automation and certification.

Findings

Automated implicit induction proofs in Coq using Spike

Proofs are translated into certified Coq scripts

Improves proof automation in theorem proving environments

Abstract

Largely adopted by proof assistants, the conventional induction methods based on explicit induction schemas are non-reductive and local, at schema level. On the other hand, the implicit induction methods used by automated theorem provers allow for lazy and mutual induction reasoning. In this paper, we present a new tactic for the Coq proof assistant able to perform automatically implicit induction reasoning. By using an automatic black-box approach, conjectures intended to be manually proved by the certifying proof environment that integrates Coq are proved instead by the Spike implicit induction theorem prover. The resulting proofs are translated afterwards into certified Coq scripts.