Menu
Design domain-specific Step types and rewrite certificates in ComputationalPaths modules without confusing them with core Path.Step rewrite rules.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
Based on SOC occupation classification
Review armada/fleet-generated Lean files for ComputationalPaths invariants, duplicate modules, shallow Path usage, and scaffold-heavy theorem stubs.
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.
Build, test, and debug Lean 4 projects using Lake. Use when building the ComputationalPaths project, checking for errors, running tests, cleaning artifacts, or debugging Lean 4 compilation issues.
| name | domain-step-design |
| description | Design domain-specific Step types and rewrite certificates in ComputationalPaths modules without confusing them with core Path.Step rewrite rules. |
Use this skill when adding or reviewing domain-specific rewrite systems such as
TQFTStep, KnotStep, SurfaceStep, or topology/algebra operation steps.
There are two common notions of step:
ComputationalPaths.Step A: base equality steps used by Path.ComputationalPaths.Path.Step p q: rewrite steps between computational paths.When names may collide, qualify the base-level step as
ComputationalPaths.Step or _root_.ComputationalPaths.Step.
Use a domain-specific inductive type when the file models named mathematical operations:
inductive FooStep : FooObject โ FooObject โ Type
| normalize (x : FooObject) : FooStep x x
| compose (x : FooObject) (n : Nat) : FooStep x x
Then expose path-level certificates:
structure FooRewriteCertificate (x : FooObject) where
before : Nat
after : Nat
trace : Path before after
stable : RwEq (Path.trans trace (Path.refl after)) trace
Path, not only Path X.carrier X.carrier.rweq_of_step (Path.Step.trans_refl_right _) or the path tactics for
unit cleanup after a substantive domain trace; if Path.Step is not in scope,
state explicitly that the core rewrite step is intended.ComputationalPaths.Path.Rewrite.Step, avoid unqualified
Step in ambiguous contexts.Path.trans and RwEq.trans.Nat, Int, lists, words, counts)?Path.trans or RwEq witness?lake build <module>?