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 |