菜单
Helps construct RwEq (rewrite equivalence) proofs using transitivity, congruence, and canonical lemmas from the LND_EQ-TRS system. Use when proving path equalities, working with quotients, or establishing rewrite equivalences in the ComputationalPaths library.
用 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 | rweq-proofs |
| description | Helps construct RwEq (rewrite equivalence) proofs using transitivity, congruence, and canonical lemmas from the LND_EQ-TRS system. Use when proving path equalities, working with quotients, or establishing rewrite equivalences in the ComputationalPaths library. |
Construct proofs of rewrite equivalence (RwEq).
Step p q -- single rewrite step
↓
Rw p q -- multi-step (reflexive-transitive)
↓
RwEq p q -- equivalence (symmetric-transitive)
rweq_refl : RwEq p p
rweq_symm : RwEq p q → RwEq q p
rweq_trans : RwEq p q → RwEq q r → RwEq p r
rweq_cmpA_refl_left : RwEq (trans refl p) p
rweq_cmpA_refl_right : RwEq (trans p refl) p
rweq_cmpA_inv_left : RwEq (trans (symm p) p) refl
rweq_cmpA_inv_right : RwEq (trans p (symm p)) refl
rweq_tt : RwEq (trans (trans p q) r) (trans p (trans q r))
rweq_trans_congr_left : RwEq q₁ q₂ → RwEq (trans p q₁) (trans p q₂)
rweq_trans_congr_right : RwEq p₁ p₂ → RwEq (trans p₁ q) (trans p₂ q)
rweq_symm_congr : RwEq p q → RwEq (symm p) (symm q)
theorem my_proof : RwEq p q := by
calc p
_ ≈ p' := rweq_cmpA_refl_left
_ ≈ q := rweq_symm rweq_tt
theorem my_proof : RwEq p q := by
apply rweq_trans h₁
exact h₂
-- Goal: RwEq (trans p₁ q) (trans p₂ q)
exact rweq_trans_congr_right h -- where h : RwEq p₁ p₂
| Goal | Lemma / Tactic |
|---|---|
RwEq (trans refl p) p | rweq_cmpA_refl_left or path_simp |
RwEq (trans p refl) p | rweq_cmpA_refl_right or path_simp |
RwEq (trans (symm p) p) refl | rweq_cmpA_inv_left |
RwEq (symm (symm p)) p | rweq_ss or path_simp |
RwEq p p | rweq_refl or path_rfl |