主要观点：此仓库包含关于带前瞻的正则表达式匹配的 Coq 形式化内容，将在 CPP 2025 上展示，基于 2024 年发表于 POPL 的先前工作。
关键信息：

• 包含多种关于正则表达式的定义和算法文件，如LRegex.v等。
• 介绍了检查证明的方法，需 Coq 8.19 并可通过make或在容器中运行。
• 详细说明了各 Coq 文件与预印本的对应关系，涵盖各种正则表达式相关概念及操作。
  重要细节：
• LRegex.v定义了带前瞻的正则表达式的语法和语义等。
• llmatch函数在Layerwise.v中用于找到最左最长匹配并证明其正确性。
• 各文件中的函数和定义分别处理不同方面，如列表引理、正则表达式等价等。
• 与预印本的对应关系明确了各个概念在 Coq 文件中的具体位置和定义。
• 如scanMatch等算法在Layerwise.v中，且有相关定理证明其正确性等。