Extraction and Search in Rocq: Theorems, Definitions and Their dependencies

Jian Fang, Yingfei Xiong

Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven t…