The HOL-Light library of Multivariate real analysis in Rocq
summary
Coq-HOL-Light is a native Rocq library translated from HOL-Light that brings 20,000 theorems in real, complex, vector and algebraic analysis into Rocq via a two-step pipeline: HOL-Light → lambda-pi → Rocq using Altodeca and the LDAPI export, plus an extra alignment phase that maps HOL-Light types/functions to Rocq stdlib so most theorems are importable via opam and Require. An online LP search indexes lambda-pi files, uses a lambda-pi rewriting engine to erase encoding symbols and equate equivalent types (e.g. r vs R or n vs num), and returns Rocq-form theorems with provenance and selection rationale; core tooling and indexes are publicly available.
AI-written summary · about
chapters (11)
- 0:00Cocoite introduction
- 1:10Cocoite library structure
- 2:00HOL-Light to Rocq translation
- 3:49Type mapping alignment
- 5:16Expanding libraries
- 5:38Search tool design
- 7:26Rewriting rules
- 8:10Query language features
- 10:18Comparison with Rocq tools
- 11:04Future work
- 12:11Q&A
related talks
51mElpi: rule-based meta-languge for Rocq
31mA Coq Library of Undecidable Problems
22mComputing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
19mCertified Compilers à la Carte
24mCode Extraction from Coq to ML-like languages
11mExpanding the VOQC Toolkit
33mHolbert: Reading, Writing, Proving and Learning in the Browser
11mPOPLMark reloaded: Mechanizing proofs by logical relations