Generalize `commute-subst-rename`

[damhiya]

Hello! I generalized the statement of commute-subst-rename and added some definitions and lemmas in the Substitution appendix.

Here is the previous statement of commute-subst-rename:

commute-subst-rename : ∀{Γ Δ}{M : Γ ⊢ ★}{σ : Subst Γ Δ}
                        {ρ₁ : Rename Γ (Γ , ★)}{ρ₂ : Rename Δ (Δ , ★)}
                     → (∀{x : Γ ∋ ★} → exts σ (ρ₁ x) ≡ rename ρ₂ (σ x))
                     → subst (exts σ) (rename ρ₁ M) ≡ rename ρ₂ (subst σ M)

And suggested revision:

Commute : ∀ {Γ₁ Γ₂ Δ₁ Δ₂} → Subst Γ₂ Δ₂ → Rename Γ₁ Γ₂ → Subst Γ₁ Δ₁ → Rename Δ₁ Δ₂ → Set
Commute {Γ₁ = Γ₁} σ₁ ρ₁ σ₂ ρ₂ = ∀ (x : Γ₁ ∋ ★) → σ₁ (ρ₁ x) ≡ rename ρ₂ (σ₂ x)

commute-subst-rename : ∀ {Γ₁ Γ₂ Δ₁ Δ₂}
                         {σ₁ : Subst Γ₂ Δ₂} {ρ₁ : Rename Γ₁ Γ₂} {σ₂ : Subst Γ₁ Δ₁} {ρ₂ : Rename Δ₁ Δ₂}
                     → Commute σ₁ ρ₁ σ₂ ρ₂
                     → ∀ (M : Γ₁ ⊢ ★) → subst σ₁ (rename ρ₁ M) ≡ rename ρ₂ (subst σ₂ M)

Old statement is an instance of the new one, where σ₁ = exts σ and σ₂ = σ.

The motivation for this change is two folded. First, it is simply more general, so it has more applications in theory. Second and more importantly, the new proof can be naturally adapted to typed setting, while the older one is not. Consider the previous proof of commute-subst-rename for the ƛ_ case.

commute-subst-rename {Γ}{Δ}{ƛ N}{σ}{ρ₁}{ρ₂} H =
   cong ƛ_ (commute-subst-rename{Γ , ★}{Δ , ★}{N}
               {exts σ}{ext ρ₁}{ext ρ₂} (λ {x} → H′ {x}))
   where
   H′ : {x : Γ , ★ ∋ ★} → exts (exts σ) (ext ρ₁ x) ≡ rename (ext ρ₂) (exts σ x)
   H′ = ...

In the type of H′, exts σ on the LHS and exts σ on the RHS may seem equal, but each occurrence of exts operations are responsible for different variables. If we annotate ext/exts operations with relatedness, the type would be something like the following:

H′ : {x : Γ , ★ ∋ ★} → exts₂ (exts₁ σ) (ext₂ ρ₁ x) ≡ rename (ext₂ ρ₂) (exts₂ σ x)

However the use of H′ in commute-subst-rename{Γ , ★}{Δ , ★}{N}{exts σ}{ext ρ₁}{ext ρ₂} (λ {x} → H′ {x}) requires exts₁ σ and exts₂ σ to be judgementally equal. This is the case in our untyped setting, but it could be false in general, for instance in intrinsically typed setting. The generalized version does not have this problem.

I also fixed text according to changed proof structure.

[wadler]

Thanks, @damhiya . I'll leave @jsiek to comment. (Also, there are some failing checks @damhiya might want to look at.)

[damhiya]

Thank you for the quick reply!

I read the build error message, but it seems like that the error is irrelevant to change made in this PR. (https://github.com/plfa/plfa.github.io/pull/1129 also fails check with same error)

Error: cabal: Failed to build shoggoth-0.1.0.0 (which is required by
exe:builder from plfa-22.8). See the build log above for details.

[jsiek]

Thank you @damhiya for this PR. I like your generalization. I have one suggestion, which is to keep the old theorem as a corollary of the new generalized theorem. Then the uses of the old theorem do not need to change and don't need to use the Commute-S lemma.

[damhiya]

@jsiek Thank you, I recovered the original theorem as your suggestion!