diff options
| -rw-r--r-- | src/Data/Type/Properties.agda | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda index 8e862ed..e9d26ea 100644 --- a/src/Data/Type/Properties.agda +++ b/src/Data/Type/Properties.agda @@ -499,3 +499,33 @@ rename-congˡ A [ρs₁]≗[ρs₂] = Wf.All.wfRec (On.wellFounded size <-wellFounded) _ Rename.IH Rename.rename-helper A (Rename.do-congˡ [ρs₁]≗[ρs₂]) + +rename-congʳ : ∀ ρs → A ≈ B → rename ρs A ≈ rename ρs B +rename-congʳ ρs (var α) = var _ +rename-congʳ ρs unit = unit +rename-congʳ ρs (bin A≈C B≈D) = + bin (rename-congʳ ρs A≈C) (rename-congʳ ρs B≈D) +rename-congʳ ρs (all {α} {A} {β} {B} A≈B) = all (λ {γ} ∉₁ ∉₂ → begin + rename ((α′ , γ) ∷ []) (rename ((α , α′) ∷ ρs) A) + ≈⟨ rename-∘ ((α , α′) ∷ ρs) _ A ⟩ + rename ((α , α′) ∷ ρs ++ (α′ , γ) ∷ []) A + ≈˘⟨ rename-∘ ((α , α′) ∷ []) _ A ⟩ + rename (ρs ++ (α′ , γ) ∷ []) (rename ((α , α′) ∷ []) A) + ≈⟨ rename-congʳ ((ρs ++ (α′ , γ) ∷ [])) (A≈B α′∉∀α∙A α′∉∀β∙B) ⟩ + rename (ρs ++ (α′ , γ) ∷ []) (rename ((β , α′) ∷ []) B) + ≈⟨ rename-∘ (((β , α′) ∷ [])) _ B ⟩ + rename ((β , α′) ∷ ρs ++ (α′ , γ) ∷ []) B + ≡⟨ cong + ((λ δ → rename ((β , δ) ∷ ρs ++ (δ , γ) ∷ []) B) ∘ mkFresh ∘ (_++ _)) + (free-≈ (all A≈B)) ⟩ + rename ((β , β′) ∷ ρs ++ (β′ , γ) ∷ []) B + ≈˘⟨ rename-∘ ((β , β′) ∷ ρs) _ B ⟩ + rename ((β′ , γ) ∷ []) (rename ((β , β′) ∷ ρs) B) + ∎) + where + αs = free (all α A) ++ map Subst.from ρs ++ map Subst.to ρs + α′ = mkFresh αs + β′ = mkFresh (free (all β B) ++ map Subst.from ρs ++ map Subst.to ρs) + α′∉∀α∙A = isFresh .distinct αs ∘ ∈-++⁺ˡ + α′∉∀β∙B = P.subst (α′ ∉_) (free-≈ (all A≈B)) α′∉∀α∙A + open ≈-Reasoning |