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.

翻译：证明函数式程序之间的等价性是程序验证中的一个基本问题，通常涉及对代数数据类型（ADT）及结构化递归组合的推理。现代定理证明器通过结构归纳法解决此问题，但该方法对于证明许多等价定理而言并不充分。在此类情形下，研究人员需要构思一组引理，通过额外的归纳法证明这些引理，并利用它们来证明原始定理。然而，目前对归纳证明需要哪些引理以及如何自动合成这些引理缺乏系统性的理解。本文提出有向引理合成（Directed Lemma Synthesis），一种通过程序合成技术发现关键引理，从而有效自动完成等价证明的方法。我们首先识别出两种有利于归纳的命题形式，它们能为证明的进展提供形式化保证。接着提出两种策略，通过合成并应用引理，将证明目标转化为归纳友好形式。这两种策略将引理合成归约为一类具有高效算法的专门程序合成问题。实验结果表明了我们方法的有效性：与采用基于启发式的引理枚举的现有等价性检查器相比，有向引理合成在标准基准测试的扩展版上平均节省95.47%的运行时间，并额外解决了38个任务。