path-tactics

Arthur742Ramos's avatarfrom Arthur742Ramos

Use ComputationalPaths path tactics to automate common RwEq goals (path_simp/path_auto/path_normalize), and structure calc-based proofs cleanly.

⭐0stars🔀0forks📁View on GitHub🕐Updated Jan 1, 2026⬇️1downloads
[Developer Tools]

When & Why to Use This Skill

The path-tactics skill is designed to automate and streamline formal verification workflows within the Lean theorem prover. It provides specialized tactics—path_auto, path_simp, and path_normalize—to handle complex rewrite equality (RwEq) goals, manage groupoid laws, and reduce boilerplate code in mathematical proofs, ensuring cleaner and more maintainable formal specifications.

Use Cases

  • Automating routine algebraic proofs: Use path_auto to resolve standalone goals involving groupoid laws, cancellations, and associativity reshaping without manual intervention.
  • Proof cleanup and optimization: Apply path_simp as a final step in long proofs to automatically handle unit laws and trivial cancellations, keeping the proof script concise.
  • Normalizing path expressions: Utilize path_normalize to resolve goals where both sides are definitionally equivalent but differ in parenthesization, unblocking complex verification steps.
  • Structuring readable calc-based proofs: Integrate these tactics within 'calc' chains to create highly readable, structured formal proofs that are easy for other developers to audit and maintain.
namepath-tactics
descriptionUse ComputationalPaths path tactics to automate common RwEq goals (path_simp/path_auto/path_normalize), and structure calc-based proofs cleanly.

Path Tactics (RwEq automation)

This skill focuses on reducing boilerplate in RwEq proofs by using the project’s path tactics and a few repeatable proof shapes.

Import

Most automation lives in:

import ComputationalPaths.Path.Rewrite.PathTactic

What to try first

1) path_auto

Use for “standalone” goals that are mostly groupoid laws, cancellation, associativity reshaping, etc.

theorem t : RwEq (trans (symm p) p) refl := by
  path_auto

2) path_simp

Use inside longer proofs to close the last “cleanup” step (unit laws, trivial cancellations).

-- ... after rewriting/congruence steps
path_simp

3) path_normalize

Use when the goal is blocked because both sides are definitionally different parenthesizations.

path_normalize

Proof structuring patterns

Prefer calc chains for readability

This project commonly uses a calc chain with the ÷ notation for RwEq:

theorem my_rweq : RwEq p q := by
  calc p
    _ ÷ p' := h1
    _ ÷ p'' := h2
    _ ÷ q := by
      path_simp

Combine tactics with targeted lemmas

When you need one key lemma application (e.g. associativity or congruence) and the rest is routine:

  1. apply the key lemma(s) with apply / exact
  2. finish with path_simp / path_auto

Troubleshooting

  • If path_auto fails, normalize both sides (path_normalize) and retry.
  • If the goal is “almost solved” but has extra trans refl _ / trans _ refl, use path_simp.
  • For congruence-heavy goals, apply the project lemmas (e.g. rweq_trans_congr_left/right) to reduce the goal, then finish with tactics.