Elpi: rule-based meta-languge for Rocq
summary
Elpi is a rule-based meta-language that implements new Rocq commands and tactics by manipulating open terms with binders and holes, using higher-order abstract syntax plus constraint handling rules to suspend and resume work on evars. It compiles tactics into small rules stored in a database of rules that can be extended at runtime, powers HB (algebraic-hierarchy growth after 2022), TR (transport via univalent parametricity), derive (code synthesis), and an algebra tactic that solves a 500-line polynomial in ~dozen seconds; performance is acceptable though not as fast as native reflexive tactics.
AI-written summary · about
chapters (12)
- 0:00Elpi introduction
- 1:04Elpi projects and features
- 9:13Elpi as CLP
- 13:53Open terms in Elpi
- 17:07Elpi with Coq and APIs
- 19:58Live proof transfer demo
- 26:11Extending tactics with DBs
- 34:13Programmatic rule synthesis
- 40:25Elpi vs MetaCoq Mtac2
- 44:40Elpi as Coq extension
- 46:25Future work: type classes analysis
- 47:51Q&A
related talks
15mImplementing parametricity in Rocq-ELPI
34mLanguage Design Where Paradigms Meet
19mCertified Compilers à la Carte
15mThe HOL-Light library of Multivariate real analysis in Rocq
30mA Mechanised Semantics of Erlang’s References
42mSession with the Rocq Development Team
21mNested Inductive Types for Rocq and Lean
16mEnhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)