MCP-RoCQ (Coq Reasoning Server)

MCP-RoCQ（Coq 推理服务）

目前能显示工具，但 Claude 不知为何无法正常使用——问题通常似乎是语法无效，但也可能另有原因。

也许可以通过 coq cli 之类的方式更好地进行设置。 如果有懂行的人愿意尝试修复，那就太好了。

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

功能

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

安装

1. 安装 Coq Platform 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 .

Claude App 或 mcphost 配置的 JSON——请根据 Coq 和仓库的安装路径设置相应路径。

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

这也许能用——我是用 uv 配置成功的，但其中大部分内容可能是幻觉：

3. 安装依赖项：

pip install -r requirements.txt

用法

此服务提供三项主要功能：

1. 类型检查

{
    "tool": "type_check",
    "args": {
        "term": "<term to check>",
        "expected_type": "<type>",
        "context": ["relevant", "modules"] 
    }
}

2. 归纳类型

{
    "tool": "define_inductive",
    "args": {
        "name": "Tree",
        "constructors": [
            "Leaf : Tree",
            "Node : Tree -> Tree -> Tree"
        ],
        "verify": true
    }
}

3. 属性证明

{
    "tool": "prove_property",
    "args": {
        "property": "<statement>",
        "tactics": ["<tactic sequence>"],
        "use_automation": true
    }
}

许可证

本项目采用 MIT 许可证，详情请参阅 LICENSE 文件。