Rocq에서의 추출 및 검색: 정리, 정의 및 그 의존성

Rocq (Coq)는 현재 소프트웨어 검증 (software verification) 및 수학적 증명 (mathematical proofs)을 포함한 다양한 분야에서 널리 사용되고 있습니다. 새로운 정리 (theorem)를 증명할 때, 사용자들은 현재의 증명 과정을 돕기 위해 이미 증명된 정리들을 검색하고 적용해야 하는 경우가 많습니다. 그러나 현재의 검색 명령은 임포트된 모듈 (imported modules) 환경으로 제한되어 있어, 이 범위를 벗어난 정리들은 검색할 수 없습니다. 또한, 도구 개발자와 연구자들은 정리의 이름, 문장 (statements), 의존성 (dependencies)과 같은 정리에 대한 상세한 정보를 얻고자 할 수 있습니다. 하지만 현재 Rocq 프로젝트로부터 포괄적인 정보를 추출할 수 있는 사용자 친화적이고 효율적인 도구는 존재하지 않습니다. 우리는 파싱 단계 (parsing phase)와 런타임 (runtime) 모두에서 정리의 구성 (composition)을 분석하고 정리, 의존성, 정의 (definitions)를 추출할 수 있는 Rocq 정리 추출 및 분석 도구인 TheoremExtr를 소개합니다. 우리는 Rocq 커뮤니티의 32개 오픈 소스 프로젝트로부터 71,795개의 정리와 그 의존성을 추출했습니다. 또한, 이 프로젝트들 사이에서 27,481개의 정의와 그 타입 (types)을 추출했습니다. 우리는 또한 정리와 정의에 대한 프로젝트 간 유사도 검색 (cross-project similarity search)을 지원하는 웹사이트를 개발했습니다. 해당 도구는 https://github.com/Rw1nd/TheoremExtr 에서 이용 가능하며, 검색 웹사이트는 https://lemmasearch.com 에서 이용 가능합니다.