القائمة
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