While in the process of using the Substitution chapter for a personal project, I realized that commute-subst-rename, as it is written, does not translate to Contexts with variable names.
To understand why, just look at the implementation:
commute-subst-rename : ∀{Γ Δ}{M : Γ ⊢ ★}{σ : Subst Γ Δ}
{ρ : ∀{Γ} → Rename Γ (Γ , ★)}
→ (∀{x : Γ ∋ ★} → exts σ {B = ★} (ρ x) ≡ rename ρ (σ x))
→ subst (exts σ {B = ★}) (rename ρ M) ≡ rename ρ (subst σ M)
commute-subst-rename {M = ` x} r = r
commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r =
cong ƛ_ (commute-subst-rename{Γ , ★}{Δ , ★}{N}
{exts σ}{ρ = ρ′} (λ {x} → H {x}))
where
ρ′ : ∀ {Γ} → Rename Γ (Γ , ★)
ρ′ {∅} = λ ()
ρ′ {Γ , ★} = ext ρ
H : {x : Γ , ★ ∋ ★} → exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
H {Z} = refl
H {S y} =
begin
exts (exts σ) (ext ρ (S y))
≡⟨⟩
rename S_ (exts σ (ρ y))
≡⟨ cong (rename S_) r ⟩
rename S_ (rename ρ (σ y))
≡⟨ compose-rename ⟩
rename (S_ ∘ ρ) (σ y)
≡⟨ cong-rename refl ⟩
rename ((ext ρ) ∘ S_) (σ y)
≡⟨ sym compose-rename ⟩
rename (ext ρ) (rename S_ (σ y))
≡⟨⟩
rename (ext ρ) (exts σ (S y))
∎
commute-subst-rename {M = L · M}{ρ = ρ} r =
cong₂ _·_ (commute-subst-rename{M = L}{ρ = ρ} r)
(commute-subst-rename{M = M}{ρ = ρ} r)The ρ′ used in the lambda case can only be written because the context does not care about variable names. We're using the "wrong" variable. If you try to implement this with Context as below you'll see.
data Context = data Context : Set where
∅ : Context
_:_,_ : Context → Id -> Type → Context
However, this is not needed, there is a simpler (and I think stronger, but I haven't proven this hypothesis) version of commute-subst-rename that also works for what we need and is quite less weird in its implementation (and arguments).
commute-subst-rename : ∀{Γ Δ Δ' Θ}{M : Γ ⊢ ★}
{ρ : Rename Γ Δ }{σ : Subst Δ Θ}
{σ' : Subst Γ Δ'}{ρ' : Rename Δ' Θ}
→ (∀{x : Γ ∋ ★} → σ (ρ x) ≡ rename ρ' (σ' x))
→ subst σ (rename ρ M) ≡ rename ρ' (subst σ' M)
commute-subst-rename {M = ` x} r = r
commute-subst-rename{Γ}{Δ}{M = ƛ N}{ρ}{σ}{σ'}{ρ'} r =
cong ƛ_ (commute-subst-rename{M = N} (\ {x} -> H {x}))
where
H : {x : Γ , ★ ∋ ★} → exts σ (ext ρ x) ≡ rename (ext ρ') (exts σ' x)
H {Z} = refl
H {S y} =
begin
exts σ (ext ρ (S y))
≡⟨⟩
rename S_ (σ (ρ y))
≡⟨ cong (rename S_) r ⟩
rename S_ (rename ρ' (σ' y))
≡⟨ compose-rename ⟩
rename (S_ ∘ ρ') (σ' y)
≡⟨ cong-rename refl ⟩
rename ((ext ρ') ∘ S_) (σ' y)
≡⟨ sym compose-rename ⟩
rename (ext ρ') (rename S_ (σ' y))
≡⟨⟩
rename (ext ρ') (exts σ' (S y))
∎
commute-subst-rename {M = L · M}{ρ = ρ} r =
cong₂ _·_ (commute-subst-rename{M = L}{ρ = ρ} r)
(commute-subst-rename{M = M}{ρ = ρ} r)I propose changing to this version. I have a branch ready, now building, let me know if I can submit a PR.
While in the process of using the Substitution chapter for a personal project, I realized that
commute-subst-rename, as it is written, does not translate to Contexts with variable names.To understand why, just look at the implementation:
The
ρ′used in the lambda case can only be written because the context does not care about variable names. We're using the "wrong" variable. If you try to implement this withContextas below you'll see.However, this is not needed, there is a simpler (and I think stronger, but I haven't proven this hypothesis) version of
commute-subst-renamethat also works for what we need and is quite less weird in its implementation (and arguments).I propose changing to this version. I have a branch ready, now building, let me know if I can submit a PR.