ReactorJet/Coq-Stdlib

--- license: lgpl-2.1 task_categories: - text-generation - feature-extraction language: - en tags: - theorem-proving - formal-methods - coq - standard-library size_categories: - 1K<n<10K dataset_info: features: - name: fact dtype: string - name: type dtype: string - name: library dtype: string - name: imports list: string - name: filename dtype: string - name: symbolic_name dtype: string - name: docstring dtype: string splits: - name: train num_bytes: 692381 num_examples: 2364 download_size: 151271 dataset_size: 692381 configs: - config_name: default data_files: - split: train path: data/train-* --- # Coq-Stdlib Structured dataset of definitions and theorems from the Coq standard library. ## Dataset Description - **Source:** [coq/coq/theories](https://github.com/coq/coq/tree/master/theories) - **Entries:** 2,364 - **Files processed:** 106 - **License:** LGPL-2.1 (matches Coq) ## Schema | Column | Type | Description | |--------|------|-------------| | fact | string | Declaration body (without type keyword) | | type | string | Definition, Lemma, Theorem, Fixpoint, Inductive, Class, Instance, Ltac, Ltac2, etc. | | library | string | Top-level module (Corelib, Ltac2) | | imports | list | Require/Import statements | | filename | string | Source file path | | symbolic_name | string | Declaration identifier | ## Statistics ### By Type | Type | Count | |------|-------| | Definition | 688 | | Lemma | 553 | | Ltac2 | 550 | | Ltac | 124 | | Fixpoint | 75 | | Axiom | 74 | | Theorem | 62 | | Class | 48 | | Inductive | 48 | | Instance | 45 | ## Use Cases - Retrieval/RAG for Coq - Learning Coq standard library patterns - Training embeddings for formal proofs - Documentation exploration ## Related Datasets - [Coq-HoTT](https://huggingface.co/datasets/phanerozoic/Coq-HoTT) - [Coq-UniMath](https://huggingface.co/datasets/phanerozoic/Coq-UniMath) - [Coq-MetaCoq](https://huggingface.co/datasets/phanerozoic/Coq-MetaCoq)--- license: LGPL-2.1 task_categories: - 文本生成 - 特征抽取 language: - 英语 tags: - 定理证明 (theorem-proving) - 形式化方法 (formal-methods) - Coq - 标准库 size_categories: - 1K<n<10K dataset_info: features: - name: fact dtype: 字符串 - name: type dtype: 字符串 - name: library dtype: 字符串 - name: imports dtype: 字符串列表 - name: filename dtype: 字符串 - name: symbolic_name dtype: 字符串 - name: docstring dtype: 字符串 splits: - name: train num_bytes: 692381 num_examples: 2364 download_size: 151271 dataset_size: 692381 configs: - config_name: default data_files: - split: train path: data/train-* --- # Coq标准库 结构化数据集，收录了Coq标准库中的各类定义与定理。 ## 数据集说明 - **来源:** [coq/coq/theories](https://github.com/coq/coq/tree/master/theories) - **总条目数:** 2364 - **已处理文件数:** 106 - **许可证:** LGPL-2.1（与Coq许可证一致） ## 数据模式 | 列名 | 数据类型 | 描述 | |--------|------|-------------| | fact | 字符串 | 声明主体（不含type关键字） | | type | 字符串 | 声明类型，包括Definition、Lemma、Theorem、Fixpoint、Inductive、Class、Instance、Ltac、Ltac2等 | | library | 字符串 | 顶层模块（如Corelib、Ltac2） | | imports | 字符串列表 | Require/Import语句列表 | | filename | 字符串 | 源文件路径 | | symbolic_name | 字符串 | 声明标识符 | | docstring | 字符串 | 文档字符串 | ## 统计信息 ### 按声明类型统计 | 声明类型 | 数量 | |------|-------| | 定义 | 688 | | 引理 | 553 | | Ltac2 | 550 | | Ltac | 124 | | 不动点定义 | 75 | | 公理 | 74 | | 定理 | 62 | | 类 | 48 | | 归纳类型 | 48 | | 实例 | 45 | ## 应用场景 - 面向Coq的检索与检索增强生成（RAG, Retrieval-Augmented Generation） - 学习Coq标准库的编码范式 - 训练形式化证明相关的嵌入向量 - 文档探索与检索 ## 相关数据集 - [Coq-HoTT](https://huggingface.co/datasets/phanerozoic/Coq-HoTT) - [Coq-UniMath](https://huggingface.co/datasets/phanerozoic/Coq-UniMath) - [Coq-MetaCoq](https://huggingface.co/datasets/phanerozoic/Coq-MetaCoq)