Discovering conditional properties of recursive functions in a proof assistant

Theory exploration is a bottom-up approach to automatically discovering a collection of theorems in a given mathematical theory. It is especially important for the verification of programs, since the correctness property are often proved by induction, and such inductive proof essentially requires plenty of lemmas. In theory exploration, it is hard to find syntactically complex properties. Especially, there have been not so much investigation on exploration of conditional properties. In this paper, we study how the top-down approach based on generalization can be used in theory exploration to find complex conditional properties through an example.