MCP Rocq

🚀 MCP - RoCQ（Coq 推理服务器）

MCP - RoCQ 是一个模型上下文协议服务器，它与 Coq 证明助手集成，能提供高级逻辑推理功能。可支持自动化依赖类型检查、归纳类型定义，还能使用自定义策略和自动化进行属性证明。

🚀 快速开始

目前显示工具但 Claude 无法正常使用，可能是因为语法错误或其他问题。或许有更好的方法使用 Coq CLI 设置。

✨ 主要特性

• 自动化依赖类型检查：可验证复杂依赖类型的项。
• 归纳类型定义：能够定义并自动验证自定义归纳数据类型。
• 属性证明：利用自定义策略和自动化证明逻辑属性。
• XML 协议集成：实现与 Coq 可靠的结构化通信。
• 丰富的错误处理：提供详细的类型错误和证明失败反馈。

📦 安装指南

1. 安装 Coq 平台 8.19（2024.10） Coq 是一个形式证明管理系统。它提供了一个正式语言来编写数学定义、可执行算法和定理，并一起提供了一个用于半交互式开发机器检查证明的环境。 https://github.com/coq/platform

2. 克隆此仓库：

git clone https://github.com/angrysky56/mcp-rocq.git

进入仓库目录

uv venv
./venv/Scripts/activate
uv pip install -e .

3. 安装依赖

pip install -r requirements.txt

4. 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 文件。