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
