  Coding conventions for naming, spacing, and other essentially stylistic
properties are necessary for developers to effectively understand, review, and
modify source code in large software projects. Consistent conventions in
verification projects based on proof assistants, such as Coq, increase in
importance as projects grow in size and scope. While conventions can be
documented and enforced manually at high cost, emerging approaches
automatically learn and suggest idiomatic names in Java-like languages by
applying statistical language models on large code corpora. However, due to its
powerful language extension facilities and fusion of type checking and
computation, Coq is a challenging target for automated learning techniques. We
present novel generation models for learning and suggesting lemma names for Coq
projects. Our models, based on multi-input neural networks, are the first to
leverage syntactic and semantic information from Coq's lexer (tokens in lemma
statements), parser (syntax trees), and kernel (elaborated terms) for naming;
the key insight is that learning from elaborated terms can substantially boost
model performance. We implemented our models in a toolchain, dubbed Roosterize,
and applied it on a large corpus of code derived from the Mathematical
Components family of projects, known for its stringent coding conventions. Our
results show that Roosterize substantially outperforms baselines for suggesting
lemma names, highlighting the importance of using multi-input models and
elaborated terms.
