MCP-RoCQ（Coq 推理服务器）

当前状态

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

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

功能

• 自动化依赖类型检查：验证复杂依赖类型的项
• 归纳类型定义：定义并自动验证自定义归纳数据类型
• 属性证明：使用自定义策略和自动化证明逻辑属性
• 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 .

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"
      ]
    },

安装依赖

pip install -r requirements.txt

使用方法

该服务器提供三种主要功能：

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