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: bash

  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 or Admitted. remains: bash

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

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

Scripts#

ActionCommandUse whenCheck Rocq versionrocq --versionVerify the active opam switch has the expected Rocq release.Verify stdlib loadsrocq -e 'From Stdlib Require Import Arith. Check Nat.add_comm.'Confirm the standard library is reachable before proving.Build projectdune buildAfter each proof attempt; must exit 0 with no errors.Compile single filerocq compile <file>.vQuick check on a single .v file without a full dune build.Check for admitsgrep -rn 'admit|Admitted\.' *.vBefore submitting; must return no matches.Install opam depsopam install . --deps-onlyAfter 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.