🚀 MCP - RoCQ（Coq 推理服务器）
MCP - RoCQ 是一个模型上下文协议服务器，它与 Coq 证明助手集成，能提供高级逻辑推理功能。可支持自动化依赖类型检查、归纳类型定义，还能使用自定义策略和自动化进行属性证明。
🚀 快速开始
目前显示工具但 Claude 无法正常使用，可能是因为语法错误或其他问题。或许有更好的方法使用 Coq CLI 设置。
✨ 主要特性
- 自动化依赖类型检查：可验证复杂依赖类型的项。
- 归纳类型定义：能够定义并自动验证自定义归纳数据类型。
- 属性证明：利用自定义策略和自动化证明逻辑属性。
- XML 协议集成：实现与 Coq 可靠的结构化通信。
- 丰富的错误处理：提供详细的类型错误和证明失败反馈。
📦 安装指南
-
安装 Coq 平台 8.19（2024.10） Coq 是一个形式证明管理系统。它提供了一个正式语言来编写数学定义、可执行算法和定理，并一起提供了一个用于半交互式开发机器检查证明的环境。 https://github.com/coq/platform
-
克隆此仓库：
git clone https://github.com/angrysky56/mcp-rocq.git
进入仓库目录
uv venv
./venv/Scripts/activate
uv pip install -e .
- 安装依赖
pip install -r requirements.txt
- JSON 配置示例（适用于 Claude 应用或 mcphost 配置）——请根据实际安装路径设置。
"mcp-rocq": {
"command": "uv",
"args": [
"--directory",
"F:/GithubRepos/mcp-rocq",
"run",
"mcp_rocq",
"--coq-path",
"F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe",
"--lib-path",
"F:/Coq-Platform~8.19~2024.10/lib/coq"
]
},
💻 使用示例
基础用法
该服务器提供三种主要功能，以下是具体的使用示例：
1. 类型检查
{
"tool": "type_check",
"args": {
"term": "<待检查的项>",
"expected_type": "<预期类型>",
"context": ["相关模块"]
}
}
2. 归纳类型定义
{
"tool": "define_inductive",
"args": {
"name": "Tree",
"constructors": [
"Leaf : Tree",
"Node : Tree -> Tree -> Tree"
],
"verify": true
}
}
3. 属性证明
{
"tool": "prove_property",
"args": {
"property": "<属性陈述>",
"tactics": ["<策略序列>"],
"use_automation": true
}
}
📄 许可证
该项目使用 MIT 许可证，详情请参阅 LICENSE 文件。