Prove renaming is left congruent.

1 files changed, 221 insertions, 0 deletions

diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda
index 0ef018f..8e862ed 100644
--- a/src/Data/Type/Properties.agda
+++ b/src/Data/Type/Properties.agda
@@ -278,3 +278,224 @@ open IsEquivalence ≈-isEquivalence public
 ≈-setoid = record { isEquivalence = ≈-isEquivalence }
 
 module ≈-Reasoning = Reasoning ≈-setoid
+
+-- More Properties of rename---------------------------------------------------
+
+private
+  module Rename where
+    data Case (A : Type) : Set where
+      do-∘     : (ρs ρs₁ : List Renaming) → Case A
+      do-congˡ :
+        ∀ {ρs ρs₁} →
+        ([ρs]≗[ρs₁] :
+          ∀ {α} → α ∈ free A → applyRenaming ρs α ≡ applyRenaming ρs₁ α) →
+        Case A
+
+    Result : Case A → Set
+    Result {A} (do-∘ ρs ρs₁)                    =
+      rename ρs₁ (rename ρs A) ≈ rename (ρs ++ ρs₁) A
+    Result {A} (do-congˡ {ρs} {ρs₁} [ρs]≗[ρs₁]) = rename ρs A ≈ rename ρs₁ A
+
+    IH : Type → Set
+    IH A = (case : Case A) → Result case
+
+    lemma₁ : ∀ A ρs →
+      let α = mkFresh (free A ++ map Subst.from ρs ++ map Subst.to ρs) in
+      α ≡ applyRenaming ρs α
+    lemma₁ A ρs =
+      fromInj₁
+        (⊥-elim ∘
+         isFresh .distinct (free A ++ map Subst.from ρs ++ map Subst.to ρs) ∘
+         ∈-++⁺ʳ (free A) ∘
+         ∈-++⁺ˡ)
+        (applyRenaming⁻¹ ρs refl)
+
+    lemma₂ : ∀ A ρs {α} →
+      let β = mkFresh (free A ++ map Subst.from ρs ++ map Subst.to ρs) in
+      α ∈ free A → β ≢ applyRenaming ρs α
+    lemma₂ A ρs α∈A β≡[ρs]α =
+      [ β∉αs ∘ ∈-++⁺ˡ ∘ flip (P.subst (_∈ _)) α∈A
+      , β∉αs ∘
+        ∈-++⁺ʳ (free A) ∘
+        ∈-++⁺ʳ (map Subst.from ρs) ∘
+        P.subst (_∈ _) (sym β≡[ρs]α) ∘
+        applyRenaming-lookup ρs
+      ] (applyRenaming⁻¹ ρs (sym β≡[ρs]α))
+      where
+      αs = free A ++ map Subst.from ρs ++ map Subst.to ρs
+      β∉αs = isFresh .distinct αs
+
+    rename-helper :
+      ∀ A → WfRec (_<_ on size) IH A → IH A
+    rename-helper (var α)     hyp (do-∘ ρs ρs₁)                      =
+      ≈-reflexive (cong var (applyRenaming-++ ρs ρs₁ α))
+    rename-helper (var α)     hyp (do-congˡ [ρs]≗[ρs₁])              =
+      ≈-reflexive (cong var ([ρs]≗[ρs₁] (here refl)))
+    rename-helper unit        hyp (do-∘ ρs ρs₁)                      = unit
+    rename-helper unit        hyp (do-congˡ [ρs]≗[ρs₁])              = unit
+    rename-helper (bin ⊗ A B) hyp (do-∘ ρs ρs₁)                      =
+      bin (hyp A (m≤m+n _ _) (do-∘ ρs ρs₁))
+          (hyp B (m<n+m _ 0<1+n) (do-∘ ρs ρs₁))
+    rename-helper (bin ⊗ A B) hyp (do-congˡ [ρs]≗[ρs₁])              =
+      bin (hyp A (m≤m+n _ _) (do-congˡ ([ρs]≗[ρs₁] ∘ ∈-++⁺ˡ)))
+          (hyp B (m<n+m _ 0<1+n) (do-congˡ ([ρs]≗[ρs₁] ∘ ∈-++⁺ʳ _)))
+    rename-helper (all α A)   hyp (do-∘ ρs ρs₁)                      =
+      all (λ {γ} ∉₁ ∉₂ → begin
+        rename ((β₂ , γ) ∷ []) (rename ((β₁ , β₂) ∷ ρs₁) (rename ((α , β₁) ∷ ρs) A))
+          ≈⟨  hyp (rename ((α , β₁) ∷ ρs) A)
+                (P.subst (_< _) (sym (size-rename _ A)) (n<1+n _))
+                (do-∘ _ _) ⟩
+        rename ((β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) (rename ((α , β₁) ∷ ρs) A)
+          ≈⟨  hyp A (n<1+n _) (do-∘ _ _) ⟩
+        rename ((α , β₁) ∷ ρs ++ (β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) A
+          ≈⟨  hyp A (n<1+n _) (do-congˡ (lemma₃ ∉₁ ∉₂)) ⟩
+        rename ((α , β₁₂) ∷ (ρs ++ ρs₁) ++ (β₁₂ , γ) ∷ []) A
+          ≈˘⟨ hyp A (n<1+n _) (do-∘ _ _) ⟩
+        rename ((β₁₂ , γ) ∷ []) (rename ((α , β₁₂) ∷ ρs ++ ρs₁) A)
+          ∎)
+      where
+      β₁ = mkFresh (free (all α A) ++ map Subst.from ρs ++ map Subst.to ρs)
+      β₂ =
+        mkFresh
+          (free (rename ρs (all α A)) ++
+           map Subst.from ρs₁ ++
+           map Subst.to ρs₁)
+      β₁₂ =
+        mkFresh
+          (free (all α A) ++
+           map Subst.from (ρs ++ ρs₁) ++
+           map Subst.to (ρs ++ ρs₁))
+
+      lemma₃ :
+        ∀ {γ} →
+        γ ∉ free (rename ρs₁ (rename ρs (all α A))) →
+        γ ∉ free (rename (ρs ++ ρs₁) (all α A)) →
+        ∀ {δ} → δ ∈ free A →
+        applyRenaming ((α , β₁) ∷ ρs ++ (β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) δ ≡
+        applyRenaming ((α , β₁₂) ∷ (ρs ++ ρs₁) ++ (β₁₂ , γ) ∷ []) δ
+      lemma₃ {γ} ∉₁ ∉₂ {δ} δ∈A with α ≟ δ
+      ... | true because _ = begin
+        applyRenaming (ρs ++ (β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) β₁
+          ≡˘⟨ applyRenaming-++ ρs _ β₁ ⟩
+        applyRenaming ((β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) (applyRenaming ρs β₁)
+          ≡˘⟨ cong (applyRenaming ((β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []))
+                (lemma₁ (all α A) ρs) ⟩
+        applyRenaming ((β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) β₁
+          ≡˘⟨ applyRenaming-++ ((β₁ , β₂) ∷ ρs₁) _ β₁ ⟩
+        applyRenaming ((β₂ , γ) ∷ []) (applyRenaming ((β₁ , β₂) ∷ ρs₁) β₁)
+          ≡⟨  cong (applyRenaming ((β₂ , γ) ∷ [])) (begin
+            applyRenaming ((β₁ , β₂) ∷ ρs₁) β₁
+              ≡⟨  applyRenaming-step β₁ β₂ ρs₁ ⟩
+            applyRenaming ρs₁ β₂
+              ≡˘⟨ lemma₁ (rename ρs (all α A)) ρs₁ ⟩
+            β₂
+              ∎) ⟩
+        applyRenaming ((β₂ , γ) ∷ []) β₂
+          ≡⟨  applyRenaming-step β₂ γ [] ⟩
+        γ
+          ≡˘⟨ applyRenaming-step β₁₂ γ [] ⟩
+        applyRenaming ((β₁₂ , γ) ∷ []) β₁₂
+          ≡⟨  cong (applyRenaming ((β₁₂ , γ) ∷ []))
+                (lemma₁ (all α A) (ρs ++ ρs₁)) ⟩
+        applyRenaming ((β₁₂ , γ) ∷ []) (applyRenaming ((ρs ++ ρs₁)) β₁₂)
+          ≡⟨  applyRenaming-++ (ρs ++ ρs₁) _ β₁₂ ⟩
+        applyRenaming ((ρs ++ ρs₁) ++ (β₁₂ , γ) ∷ []) β₁₂
+          ∎
+        where open ≡-Reasoning
+      ... | no α≢δ         = begin
+        applyRenaming (ρs ++ (β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) δ
+          ≡˘⟨ applyRenaming-++ ρs _ δ ⟩
+        applyRenaming ((β₁ , β₂) ∷ ρs₁ ++ (β₂ , γ) ∷ []) (applyRenaming ρs δ)
+          ≡⟨  applyRenaming-skip β₂ (ρs₁ ++ (β₂ , γ) ∷ [])
+                (lemma₂ (all α A) ρs δ∈∀α∙A) ⟩
+        applyRenaming (ρs₁ ++ (β₂ , γ) ∷ []) (applyRenaming ρs δ)
+          ≡˘⟨ applyRenaming-++ ρs₁ _ _ ⟩
+        applyRenaming ((β₂ , γ) ∷ []) (applyRenaming ρs₁ (applyRenaming ρs δ))
+          ≡⟨  applyRenaming-skip γ []
+                (lemma₂ (rename ρs (all α A)) ρs₁ [ρs]δ∈[ρs]∀α∙A) ⟩
+        applyRenaming ρs₁ (applyRenaming ρs δ)
+          ≡⟨  applyRenaming-++ ρs ρs₁ δ ⟩
+        applyRenaming (ρs ++ ρs₁) δ
+          ≡˘⟨ applyRenaming-skip γ [] (lemma₂ (all α A) (ρs ++ ρs₁) δ∈∀α∙A) ⟩
+        applyRenaming ((β₁₂ , γ) ∷ []) (applyRenaming (ρs ++ ρs₁) δ)
+          ≡⟨  applyRenaming-++ (ρs ++ ρs₁) _ δ ⟩
+        applyRenaming ((ρs ++ ρs₁) ++ (β₁₂ , γ) ∷ []) δ
+          ∎
+        where
+        open ≡-Reasoning
+        δ∈∀α∙A = ∈-filter⁺ (¬? ∘ (α ≟_)) δ∈A α≢δ
+        [ρs]δ∈[ρs]∀α∙A =
+          P.subst (_ ∈_) (sym (free-rename ρs (all α A))) (∈-map⁺ _ δ∈∀α∙A)
+
+      open ≈-Reasoning
+    rename-helper (all α A)   hyp (do-congˡ {ρs₁} {ρs₂} [ρs₁]≗[ρs₂]) =
+      all (λ {γ} ∉₁ ∉₂ → begin
+        rename ((β₁ , γ) ∷ []) (rename ((α , β₁) ∷ ρs₁) A)
+          ≈⟨  hyp A (n<1+n _) (do-∘ _ _) ⟩
+        rename ((α , β₁) ∷ ρs₁ ++ (β₁ , γ) ∷ []) A
+          ≈⟨  hyp A (n<1+n _) (do-congˡ (lemma₃ ∉₁ ∉₂)) ⟩
+        rename ((α , β₂) ∷ ρs₂ ++ (β₂ , γ) ∷ []) A
+          ≈˘⟨ hyp A (n<1+n _) (do-∘ _ _) ⟩
+        rename ((β₂ , γ) ∷ []) (rename ((α , β₂) ∷ ρs₂) A)
+          ∎)
+      where
+      β₁ = mkFresh (free (all α A) ++ map Subst.from ρs₁ ++ map Subst.to ρs₁)
+      β₂ = mkFresh (free (all α A) ++ map Subst.from ρs₂ ++ map Subst.to ρs₂)
+
+      lemma₃ :
+        ∀ {γ} →
+        γ ∉ free (rename ρs₁ (all α A)) →
+        γ ∉ free (rename ρs₂ (all α A)) →
+        ∀ {δ} → δ ∈ free A →
+        applyRenaming ((α , β₁) ∷ ρs₁ ++ (β₁ , γ) ∷ []) δ ≡
+        applyRenaming ((α , β₂) ∷ ρs₂ ++ (β₂ , γ) ∷ []) δ
+      lemma₃ {γ} ∉₁ ∉₂ {δ} δ∈A with α ≟ δ
+      ... | yes α≡δ = begin
+        applyRenaming (ρs₁ ++ (β₁ , γ) ∷ []) β₁
+          ≡˘⟨ applyRenaming-++ ρs₁ _ β₁ ⟩
+        applyRenaming ((β₁ , γ) ∷ []) (applyRenaming ρs₁ β₁)
+          ≡˘⟨ cong (applyRenaming ((β₁ , γ) ∷ [])) (lemma₁ (all α A) ρs₁) ⟩
+        applyRenaming ((β₁ , γ) ∷ []) β₁
+          ≡⟨  applyRenaming-step β₁ γ [] ⟩
+        γ
+          ≡˘⟨ applyRenaming-step β₂ γ [] ⟩
+        applyRenaming ((β₂ , γ) ∷ []) β₂
+          ≡⟨  cong (applyRenaming ((β₂ , γ) ∷ [])) (lemma₁ (all α A) ρs₂) ⟩
+        applyRenaming ((β₂ , γ) ∷ []) (applyRenaming ρs₂ β₂)
+          ≡⟨  applyRenaming-++ ρs₂ _ β₂ ⟩
+        applyRenaming (ρs₂ ++ (β₂ , γ) ∷ []) β₂
+          ∎
+        where open ≡-Reasoning
+      ... | no α≢δ  = begin
+        applyRenaming (ρs₁ ++ (β₁ , γ) ∷ []) δ
+          ≡˘⟨ applyRenaming-++ ρs₁ _ δ ⟩
+        applyRenaming ((β₁ , γ) ∷ []) (applyRenaming ρs₁ δ)
+          ≡⟨  applyRenaming-skip γ [] (lemma₂ (all α A) ρs₁ δ∈∀α∙A) ⟩
+        applyRenaming ρs₁ δ
+          ≡⟨  [ρs₁]≗[ρs₂] δ∈∀α∙A ⟩
+        applyRenaming ρs₂ δ
+          ≡˘⟨ applyRenaming-skip γ [] (lemma₂ (all α A) ρs₂ δ∈∀α∙A) ⟩
+        applyRenaming ((β₂ , γ) ∷ []) (applyRenaming ρs₂ δ)
+          ≡⟨  applyRenaming-++ ρs₂ _ δ ⟩
+        applyRenaming (ρs₂ ++ (β₂ , γ) ∷ []) δ
+          ∎
+        where
+        open ≡-Reasoning
+        δ∈∀α∙A = ∈-filter⁺ (¬? ∘ (α ≟_)) δ∈A α≢δ
+
+      open ≈-Reasoning
+
+rename-∘ : ∀ ρs ρs₁ A → rename ρs₁ (rename ρs A) ≈ rename (ρs ++ ρs₁) A
+rename-∘ ρs ρs₁ A =
+  Wf.All.wfRec (On.wellFounded size <-wellFounded) _
+    Rename.IH Rename.rename-helper
+    A (Rename.do-∘ ρs ρs₁)
+
+rename-congˡ :
+  ∀ {ρs₁ ρs₂} A →
+  (∀ {α} → α ∈ free A → applyRenaming ρs₁ α ≡ applyRenaming ρs₂ α) →
+  rename ρs₁ A ≈ rename ρs₂ A
+rename-congˡ A [ρs₁]≗[ρs₂] =
+  Wf.All.wfRec (On.wellFounded size <-wellFounded) _
+    Rename.IH Rename.rename-helper
+    A (Rename.do-congˡ [ρs₁]≗[ρs₂])