OpenMath Rocq Theorem

---

name: openmath-rocq-theorem

description: Configures Rocq environments, runs preflight checks, and guides the proving workflow for OpenMath Rocq theorems. Use when the user wants to set up Rocq tooling, prove a downloaded OpenMath theorem in Rocq/Coq, or verify and submit a Rocq proof.

version: v1.0.2

requirements:

commands:

- rocq or coqc

- dune

- opam

side_effects:

- Runs local Rocq, dune, and opam commands in the theorem workspace

---

# OpenMath Rocq Theorem

Instructions

Set up the Rocq proving environment, validate opam switches, and prove downloaded OpenMath theorems. Assumes the theorem workspace was already created by the `openmath-open-theorem` skill.

This skill package is self-contained: it consists of this `SKILL.md` plus the local `references/` files in this directory. It does not bundle or install sibling `rocq-*` companion skills.

Workflow checklist

```bash

rocq --version

rocq -e 'From Stdlib Require Import Arith. Check Nat.add_comm.'

dune --version

opam list rocq-prover

```

```bash

dune build

grep -rn 'admit\|Admitted\.' *.v

```

Scripts

| Action | Command | Use when |

|--------|---------|----------|

| Check Rocq version | `rocq --version` | Verify the active opam switch has the expected Rocq release. |

| Verify stdlib loads | `rocq -e 'From Stdlib Require Import Arith. Check Nat.add_comm.'` | Confirm the standard library is reachable before proving. |

| Build project | `dune build` | After each proof attempt; must exit 0 with no errors. |

| Compile single file | `rocq compile <file>.v` | Quick check on a single `.v` file without a full dune build. |

| Check for admits | `grep -rn 'admit\|Admitted\.' *.v` | Before submitting; must return no matches. |

| Install opam deps | `opam install . --deps-only` | After cloning or changing the project `opam` file. |

Notes

References

Load when needed (one level from this file):