openmath-rocq-theorem

# 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](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](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 | 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](references/companions.md)** — When to use optional Rocq companion skills if they are already installed. - **[references/languages.md](references/languages.md)** — Rocq version, Stdlib prefix, libraries, and proof style. - **[references/proof_playbook.md](references/proof_playbook.md)** — Minimal standalone proving loop for downloaded OpenMath Rocq theorem workspaces.