Proving Functional Program Equivalence via Directed Lemma Synthesis

TL;DR

Proving equivalence between functional programs over algebraic data types (ADTs) is essential for verification, but structural induction alone cannot prove many theorems. The paper presents directed lemma synthesis, introducing two induction-friendly forms and two tactics that synthesize lemmas to rewrite the goal into forms amenable to induction. These lemmas reduce to targeted program-synthesis problems, enabling efficient automatic proofs, and are implemented in AutoProof atop Cvc4Ind. Empirical results on extended benchmarks show substantial improvements over heuristic lemma enumeration, including a runtime reduction of $95.47%$ on average and solving 38 more tasks. The work advances automatic equivalence checking by providing principled, induction-aware lemma discovery and applying it to functional programs with ADTs.

Abstract

Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning about algebraic data types (ADTs) and compositions of structural recursions. Modern theorem provers address this problem by applying structural induction, which is insufficient for proving many equivalence theorems. In such cases, one has to invent a set of lemmas, prove these lemmas by additional induction, and use these lemmas to prove the original theorem. There is, however, a lack of systematic understanding of what lemmas are needed for inductive proofs and how these lemmas can be synthesized automatically. This paper presents directed lemma synthesis, an effective approach to automating equivalence proofs by discovering critical lemmas using program synthesis techniques. We first identify two induction-friendly forms of propositions that give formal guarantees to the progress of the proof. We then propose two tactics that synthesize and apply lemmas, thereby transforming the proof goal into induction-friendly forms. Both tactics reduce lemma synthesis to a specialized class of program synthesis problems with efficient algorithms. Experimental results demonstrate the effectiveness of our approach: Compared to state-of-the-art equivalence checkers employing heuristic-based lemma enumeration, directed lemma synthesis saves 95.47% runtime on average and solves 38 more tasks over an extended version of the standard benchmark set.

Figures (1)

• Figure 1: An algebraic data type and structurally recursive functions.