SKILL.md

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.

Path Tactics

Automated tactics for RwEq proofs.

Import

import ComputationalPaths.Path.Rewrite.PathTactic

Primary Tactics

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`

Structural Tactics

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`

Quick Reference

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`

Preferred Style

Use calc with ≈ notation:

calc p
  _ ≈ p' := rweq_cmpA_refl_left
  _ ≈ q := rweq_symm rweq_tt

スコア

総合スコア

60/100

リポジトリの品質指標に基づく評価

✓SKILL.md

SKILL.mdファイルが含まれている

+20

✓LICENSE

ライセンスが設定されている

+10

○説明文

100文字以上の説明がある

0/10

○人気

GitHub Stars 100以上

0/15

○最近の活動

3ヶ月以内に更新がある

0/10

○フォーク

10回以上フォークされている

0/5

✓Issue管理

オープンIssueが50未満

✓言語

プログラミング言語が設定されている

○タグ

1つ以上のタグが設定されている

0/5

path-tactics