  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.
