npx claudepluginhub llm4rocq/rocq-skills --plugin rocq# Rocq Golf Improve Rocq proofs that already compile. Score candidates by: correctness → directness → clarity/inference burden → performance/determinism → length. **Prerequisite:** Code must compile. Verify via `rocq_compile` or `coqc` first. ## Usage ## Inputs | Arg | Required | Description | |-----|----------|-------------| | target | No | File or file:line to golf | | --dry-run | No | Preview only, no changes | | --search | No | `off`, `quick` (default), or `full` — MCP lemma replacement pass | | --max-delegates | No | `2` — max concurrent golfer subagents | ## Actions 1. **Veri...
/golfOptimizes compiling Lean4 proofs for directness, clarity, performance, and brevity. Supports file/line targets, --dry-run previews, --search modes, and --max-delegates.
Improve Rocq proofs that already compile. Score candidates by: correctness → directness → clarity/inference burden → performance/determinism → length.
Prerequisite: Code must compile. Verify via rocq_compile or coqc first.
/rocq:golf # Golf entire project
/rocq:golf File.v # Golf specific file
/rocq:golf File.v:42 # Golf proof at specific line
/rocq:golf --dry-run # Show opportunities without applying
/rocq:golf --search=full # Include lemma replacement pass
| Arg | Required | Description |
|---|---|---|
| target | No | File or file:line to golf |
| --dry-run | No | Preview only, no changes |
| --search | No | off, quick (default), or full — MCP lemma replacement pass |
| --max-delegates | No | 2 — max concurrent golfer subagents |
${ROCQ_PYTHON_BIN:-python3} "$ROCQ_SCRIPTS/find_golfable.py" [file]
rocq_step_multi + rocq_compile check--search=quick or full):
rocq_query("Search ...") → test with rocq_step_multirocq_compile verification after each; revert on failure| Before | After | Notes |
|---|---|---|
intros. reflexivity. | reflexivity. | When no intros needed |
apply H. exact H'. | exact (H H'). | Merge apply+exact |
split. exact H1. exact H2. | exact (conj H1 H2). | |
simpl. trivial. | trivial. | When trivial subsumes |
| Pattern | Condition |
|---|---|
Inline assert | Used once, simple term |
| Merge sequential rewrites | rewrite H1. rewrite H2. → rewrite H1, H2. |
Replace destruct chain | With decide or auto when applicable |
assert blocks used multiple timesQed vs Defined)Scoring order: directness → inference burden → performance → length. Length is a tiebreaker among acceptable proofs.
Tactic complexity ladder: reflexivity/exact < apply/rewrite < simpl/auto < eauto/intuition < broad lia/omega/ring/decide.
Hard reject if: moves UP the complexity ladder for only a 1-line win, removes meaningful names, changes Qed to Defined or vice versa.
## Golf Results
**Meaningful simplifications:** 3 (directness improvements)
**Performance cleanups:** 1
**Syntax cleanups:** 1
**Skipped:** 2 (safety / marginal)
**Build status:** passing
**Total savings:** 8 lines (~12%)
Optional next step: run `/rocq:checkpoint` to save progress.
Stop when success rate < 20% or last 3 attempts failed.
/rocq:checkpoint)/rocq:review - See opportunities (read-only)/rocq:refactor - Strategy-level simplification/rocq:checkpoint - Save after golfing