MCP Rocq

🚀 MCP-RoCQ (Coq Inference Server)

MCP-RoCQ is a model context protocol server that provides advanced logical reasoning capabilities through integration with the Coq proof assistant. It supports automated dependent type checking, inductive type definition, and property proof using custom tactics and automation.

🚀 Quick Start

Currently, the display tool is available, but Claude cannot be used properly. This might be due to syntax errors or other issues. There might be a better way to set up using the Coq CLI.

✨ Features

• Automated Dependent Type Checking: Validate terms of complex dependent types.
• Inductive Type Definition: Define and automatically validate custom inductive data types.
• Property Proof: Prove logical properties using custom tactics and automation.
• XML Protocol Integration: Reliable structured communication with Coq.
• Comprehensive Error Handling: Detailed feedback on type errors and proof failures.

📦 Installation

1. Install Coq Platform 8.19 (2024.10). Coq is a formal proof management system. It provides a formal language for writing mathematical definitions, executable algorithms, and theorems, along with an environment for semi-interactive development of machine-checked proofs. https://github.com/coq/platform

2. Clone this repository:

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

Enter the repository directory:

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

JSON Configuration Example (for Claude application or mcphost configuration) - Please set according to the actual installation path.

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

Install Dependencies

pip install -r requirements.txt

💻 Usage Examples

Basic Usage

The server provides three main functions:

1. Type Checking

{
    "tool": "type_check",
    "args": {
        "term": "<term to be checked>",
        "expected_type": "<expected type>",
        "context": ["related modules"]
    }
}

2. Inductive Type Definition

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

3. Property Proof

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

📄 License

This project is licensed under the MIT License. Please refer to the LICENSE file for details.