rocq-simulate-author
Create or update Rocq simulate files in this repository, including imports, executable definitions, and corresponding _eq lemmas with the project’s proof/admission conventions.
来源信息
- 仓库
- formal-land/rocq-of-rust
- 最近来源活动
- 2026年2月8日 21:10
- 检测到的 SKILL.md 语言
- 英语
- 星标
- 1,165
- 分支
- 43
安装方式
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
检查来源文件
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
正在显示 SKILL.md
SKILL.md
来源说明 · 只读预览- name
- rocq-simulate-author
- description
- Create or update Rocq simulate files in this repository, including imports, executable definitions, and corresponding _eq lemmas with the project’s proof/admission conventions.
# Rocq Simulate Author
Use this skill when asked to create or complete files under `**/simulate/**/*.v`.
## Goals
- Add a simulate `Definition` that mirrors the links/run behavior at the right abstraction level.
- Add the matching `_eq` lemma connecting `run_*` and the simulate definition.
- Keep the file compiling with project flags.
## Repository Conventions
- Compile with:
```sh
coqc -R . RocqOfRust -impredicative-set path/to/file.v
```
- Prefer explicit imports; do not assume aggregator modules exist.
- In this repo, many `_eq` lemmas are intentionally `Admitted` during iteration.
- Use `id` instead of `(fun interpreter => interpreter)`.
- Prefer record notation when clearer (for example `Range` records).
## Procedure
1. Locate links source and nearby simulate examples.
- Read corresponding links file (`.../links/...`) to extract `run_*` signature and parameter order.
- Read one neighboring simulate file in same folder for style.
2. Build imports explicitly.
- `Require Import simulate.RocqOfRust.` first.
- Add links/simulate imports used by the definition.
- Add missing imports only when compile errors require them.
3. Write the simulate definition.
- Keep shape close to Rust intent and existing sibling files.
- Use existing macros (`gas_macro`, `push_macro`, etc.) consistently.
- Avoid overfitting proofs in the definition.
4. Write `_eq` lemma.
- Match argument order of `run_*` exactly.
- Prefer class-level `Run` assumptions in Eq-style files.
- If proof is not ready, keep `Admitted` unless user asked no admitted.
5. Compile and iterate.
- Compile touched file first.
- Fix minimal issues (imports, type annotations, argument order).
## Starter Skeleton
```coq
Require Import simulate.RocqOfRust.
(* other explicit imports *)
Definition <name>
{A ... : Set} `{Link ...}
...
(x : ...) : ... :=
... .
Lemma <name>_eq
{A ... : Set} `{Link ...}
...
(x : ...) :
...
.
Proof.
Admitted.
```
## Common Failure Fixes
- `module-not-found`: add explicit `Require Import ...` for split per-function links/simulate files.
- Type mismatch in `run_*`: compare with links instance signature and reorder args.
- Numeric inference to `Z`: use typed literals like `(0 : usize)`.
- Missing class projections in Eq files: add appropriate class-level `*.Run` assumption.
在 GitHub 查看