ワンクリックでManusで任意のスキルを実行

domain-step-design

スター0

フォーク0

更新日2026年5月18日 20:34

Design domain-specific Step types and rewrite certificates in ComputationalPaths modules without confusing them with core Path.Step rewrite rules.

インストール

Codex または Claude でインストールこの Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。

Manusで実行

ソース

Arthur742Ramos

Arthur742Ramos/ComputationalPathsLean

GitHub リポジトリを開く Creator のリポジトリを見る

ダウンロード

Manusで実行

Domain Step Design

Use this skill when adding or reviewing domain-specific rewrite systems such as TQFTStep, KnotStep, SurfaceStep, or topology/algebra operation steps.

Core Distinction

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.

Domain Step Pattern

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

Guidelines

Use domain steps to name mathematical moves, not to hide missing proofs.
Include at least one concrete value-level Path, not only Path X.carrier X.carrier.
Prefer 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.
If a file also imports ComputationalPaths.Path.Rewrite.Step, avoid unqualified Step in ambiguous contexts.
Keep certificates small and composable; downstream modules can combine them with Path.trans and RwEq.trans.

Review Checklist

Does the domain step encode a real operation from the module narrative?
Does the certificate carry concrete data (Nat, Int, lists, words, counts)?
Is there at least one nontrivial Path.trans or RwEq witness?
Does the module still build independently with lake build <module>?

このリポジトリの他の Skills

同じリポジトリ

armada-review

Arthur742Ramos/ComputationalPathsLean

Review armada/fleet-generated Lean files for ComputationalPaths invariants, duplicate modules, shallow Path usage, and scaffold-heavy theorem stubs.

2026-05-180

deep-audit-certificates

Arthur742Ramos/ComputationalPathsLean

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.

2026-05-180

paper-companion-style

Arthur742Ramos/ComputationalPathsLean

Keep ComputationalPaths modules suitable as book/paper companion material with clear mathematical narrative, named constructions, and meaningful computational-path evidence.

2026-05-180

lean-module-compile-recovery

Arthur742Ramos/ComputationalPathsLean

Recover a broken Lean module with minimal safe edits by weakening non-derivable equalities while preserving declaration shape.

2026-03-040

aristotle

Arthur742Ramos/ComputationalPathsLean

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.

2026-01-280

lean-build

Arthur742Ramos/ComputationalPathsLean

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.

2026-01-280

Domain Step Design

Use this skill when adding or reviewing domain-specific rewrite systems such as TQFTStep, KnotStep, SurfaceStep, or topology/algebra operation steps.

Core Distinction

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.

Domain Step Pattern

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

Guidelines

Use domain steps to name mathematical moves, not to hide missing proofs.

Include at least one concrete value-level Path, not only Path X.carrier X.carrier.

Prefer 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.

If a file also imports ComputationalPaths.Path.Rewrite.Step, avoid unqualified Step in ambiguous contexts.

Keep certificates small and composable; downstream modules can combine them with Path.trans and RwEq.trans.

Review Checklist

Does the domain step encode a real operation from the module narrative?

Does the certificate carry concrete data (Nat, Int, lists, words, counts)?

Is there at least one nontrivial Path.trans or RwEq witness?

Does the module still build independently with lake build <module>?

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.