Substitution.commute-subst-rename is weird

[crisoagf]

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.

[jsiek]

I'm OK with this change as long as it doesn't break any of the uses of it, or as long as your PR fixes any downstream uses.