A case study in proof based synthesis of algorithms on monotone lists

We apply the synthesis method introduced in our previous work in order to synthesize from proofs certain algorithms operating on sorted lists without duplications (“monotone lists”). The corresponding prover and algorithm extractor are implemented in the Theorema system. Three algorithms are automatically discovered from proofs: symmetrical difference, cartesian product and the cardinality. The larger context of this work is the manipulation of sets represented as monotone lists. This is a case study in which we demonstrate how to generate automatically the necessary functions, starting from properties from set theory. The properties of sets and of monotone lists which are necessary for the proofs are collected systematically in a knowledge base which extends the one presented in our previous work. This process of theory exploration is supported by a special prover which is able to prove automatically all the statements which are logical consequences of the axioms.