CoqHammer

CoqHammer is a general-purpose automated reasoning hammer tool for Coq. It combines learning from previous proofs with the translation of problems to the logics of automated systems and the reconstruction of successfully found proofs. A typical use is to prove relatively simple goals using available lemmas. The problem is to find appropriate lemmas in a large collection of all accessible lemmas and combine them to prove the goal. The advantage of a hammer is that it is a general system not depending on any domain-specific knowledge and not requiring configuration by the user. The hammer plugin may use all currently accessible lemmas, including those proven earlier in a given formalization, not only the lemmas from predefined libraries or hint databases. At present, however, best results are achieved for statements ”close to” first-order logic and lemmas from the standard library or similar.