菜单
Use ComputationalPaths path tactics to automate common RwEq goals (path_simp/path_auto/path_normalize), and structure calc-based proofs cleanly.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Review armada/fleet-generated Lean files for ComputationalPaths invariants, duplicate modules, shallow Path usage, and scaffold-heavy theorem stubs.
Design domain-specific Step types and rewrite certificates in ComputationalPaths modules without confusing them with core Path.Step rewrite rules.
Audit and harden scaffold-heavy ComputationalPaths Lean modules by replacing selected True/trivial/rfl placeholders with typed Path/RwEq certificate records while preserving public APIs.
Keep ComputationalPaths modules suitable as book/paper companion material with clear mathematical narrative, named constructions, and meaningful computational-path evidence.
Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape.
Run Aristotle automated theorem prover on Lean files to fill sorry placeholders. Use when you have a file with sorries that needs automated proof search. Handles API setup, axiom import checks, and result verification.
| name | path-tactics |
| description | Use ComputationalPaths path tactics to automate common RwEq goals (path_simp/path_auto/path_normalize), and structure calc-based proofs cleanly. |
Automated tactics for RwEq proofs.
import ComputationalPaths.Path.Rewrite.PathTactic
| Tactic | Use Case |
|---|---|
path_auto | Try first for any RwEq goal |
path_simp | Unit elimination, inverse cancellation |
path_normalize | Convert to right-associative form |
path_rfl | Close reflexive goals p ≈ p |
| Tactic | Description |
|---|---|
path_symm | Apply symmetry to goal |
path_congr_left h | RwEq (trans p q₁) (trans p q₂) from h : RwEq q₁ q₂ |
path_congr_right h | RwEq (trans p₁ q) (trans p₂ q) from h : RwEq p₁ p₂ |
path_cancel_left | Close RwEq (trans (symm p) p) refl |
path_cancel_right | Close RwEq (trans p (symm p)) refl |
| Goal | Tactic |
|---|---|
RwEq (trans refl p) p | path_simp |
RwEq (trans p refl) p | path_simp |
RwEq (trans (symm p) p) refl | path_cancel_left |
RwEq (symm (symm p)) p | path_simp |
Use calc with ≈ notation:
calc p
_ ≈ p' := rweq_cmpA_refl_left
_ ≈ q := rweq_symm rweq_tt