CycleQ: An Efficient Basis for Cyclic Equational Reasoning

TL;DR

CycleQ introduces a cyclic proof system for equational reasoning in functional programs, combining cyclic proofs with contextual substitution, enabling efficient, incremental correctness verification and promising benchmark results.

Contribution

The paper presents a novel cyclic proof system, CycleQ, that unifies various implicit induction methods and enables efficient proof search through incremental correctness verification.

Findings

CycleQ subsumes multiple implicit induction approaches.

Incremental correctness verification improves proof search efficiency.

The CycleQ tool performs well on standard benchmarks.

Abstract

We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proof and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as "inductionless induction", "rewriting induction", and "proof by consistency". By restricting the form of the traces, we show that global correctness in our system can be verified incrementally, taking advantage of the well-known size-change principle, which leads to an efficient implementation of proof search. Our CycleQ tool, accessible as a GHC plugin, shows promising results on a number of standard benchmarks.