Automated theorem proving was one of the major motivations for the development
of the field of computer science, but it is only recently becoming a reality.
The goal of this project is to advance our understanding of Rocq, a powerful
and evolving proof assistant. In this project, we will perform an analysis of
an important library of “tactics” that Rocq uses to construct formal proofs.