Skills openmath-rocq-theorem

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.

install

source · Clone the upstream repo

git clone https://github.com/openclaw/skills

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/openclaw/skills "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/bennyzhe/openmath-rocq-theorem" ~/.claude/skills/clawdbot-skills-openmath-rocq-theorem && rm -rf "$T"

manifest: skills/bennyzhe/openmath-rocq-theorem/SKILL.md

source content

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

Environment: Verify
```
rocq
```
(or
```
coqc
```
),
```
dune
```
, and
```
opam
```
are installed and the active opam switch matches the project's
```
.opam-switch
```
or
```
opam
```
file. See the
```
rocq-setup
```
skill for installation and switch management.
Companion skills: If companion Rocq skills such as
```
rocq-proof
```
,
```
rocq-ssreflect
```
,
```
rocq-setup
```
, or
```
rocq-dune
```
are already installed in the active agent, use them. See references/companions.md for when each one is useful. This isolated package does not include their code and does not install them for you.

Preflight: Confirm the environment is healthy before proving:

rocq --version
rocq -e 'From Stdlib Require Import Arith. Check Nat.add_comm.'
dune --version
opam list rocq-prover

Prove: Follow the minimal Rocq proving loop in references/proof_playbook.md. If
```
rocq-proof
```
or
```
rocq-ssreflect
```
is already installed, use them as companion guidance; otherwise continue with the local workflow in this skill.

Verify: Confirm

dune build

(or

rocq compile <file>.v

) passes and no

admit

Admitted.

remains:

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

Submit: Use the
```
openmath-submit-theorem
```
skill to hash and submit the proof.

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

Rocq version: OpenMath Rocq workspaces target Rocq 9.1.0 (current stable, September 2025) with Platform 2025.08.2.
Companion skills:
```
rocq-proof
```
(proving methodology, tactic reference, Ltac2),
```
rocq-ssreflect
```
(SSReflect / MathComp style),
```
rocq-setup
```
(opam, toolchain, editor), and
```
rocq-dune
```
(build system,
```
_CoqProject
```
, dune stanzas) are useful companions when already installed. Optional companions:
```
rocq-mwe
```
,
```
rocq-bisect
```
,
```
rocq-extraction
```
,
```
rocq-mathcomp-build
```
.
Install boundary: This isolated skill should not instruct copying unseen
```
rocq-*
```
directories into
```
~/.agents/skills
```
or any other global skills directory. If you are installing from the full repository, review the companion skill folders there and copy them only into a deliberate project-local skills directory such as
```
.codex/skills
```
or
```
.claude/skills
```
.
Stdlib prefix: Use
```
From Stdlib Require Import
```
for Rocq 9.x. The legacy
```
From Coq Require Import
```
still works with a deprecation warning; prefer
```
From Stdlib
```
for all new proofs.
Verification status: A proof is complete only when
```
dune build
```
exits 0, no
```
admit
```
or
```
Admitted.
```
remains, and the LSP panel shows no errors or warnings.

References

Load when needed (one level from this file):

references/companions.md — When to use optional Rocq companion skills if they are already installed.
references/languages.md — Rocq version, Stdlib prefix, libraries, and proof style.
references/proof_playbook.md — Minimal standalone proving loop for downloaded OpenMath Rocq theorem workspaces.