メニュー
Guides adding new computational-path constructions to the ComputationalPaths library. Use when defining new spaces, π₁ calculations, encode-decode proofs, or adding new topological constructions.
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 | lean-hit-development |
| description | Guides adding new computational-path constructions to the ComputationalPaths library. Use when defining new spaces, π₁ calculations, encode-decode proofs, or adding new topological constructions. |
Add new computational-path constructions to the ComputationalPaths library.
ComputationalPaths/Path/CompPath/YourSpace.lean
import ComputationalPaths.Path.Basic
import ComputationalPaths.Path.Rewrite.SimpleEquiv
import ComputationalPaths.Path.Homotopy.FundamentalGroup
namespace ComputationalPaths.Path.CompPath
/-! ## Point type and basepoint -/
inductive YourSpace : Type u
| base : YourSpace
@[simp] def yourSpaceBase : YourSpace := YourSpace.base
/-! ## Path expressions with generators -/
inductive YourSpaceExpr : YourSpace → YourSpace → Type u
| loop : YourSpaceExpr yourSpaceBase yourSpaceBase
| refl (a : YourSpace) : YourSpaceExpr a a
| symm {a b} (p : YourSpaceExpr a b) : YourSpaceExpr b a
| trans {a b c} (p : YourSpaceExpr a b) (q : YourSpaceExpr b c) : YourSpaceExpr a c
/-! ## Relation, quotient, and encode/decode -/
def yourSpaceRel : YourSpaceExpr yourSpaceBase yourSpaceBase →
YourSpaceExpr yourSpaceBase yourSpaceBase → Prop := ...
def yourSpaceSetoid : Setoid (YourSpaceExpr yourSpaceBase yourSpaceBase) := ...
abbrev yourSpacePiOne : Type u := Quot yourSpaceSetoid.r
noncomputable def encode : yourSpacePiOne → Presentation := ...
noncomputable def decode : Presentation → yourSpacePiOne := ...
theorem decode_encode : decode (encode x) = x := by
-- quotient induction
...
theorem encode_decode : encode (decode y) = y := by
-- quotient induction
...
noncomputable def piOneEquiv : SimpleEquiv yourSpacePiOne Presentation := ...
end ComputationalPaths.Path.CompPath
ComputationalPaths/Path.lean| Space | Computational-path model |
|---|---|
| Circle (S¹) | One basepoint, one loop generator |
| Torus (T²) | Product of circle constructions |
| Sphere (S²) | Suspension/pushout-based loop triviality |
| Wedge (A ∨ B) | Pushout of basepoints, free product on π₁ |