Substitution: Substitution in the untyped lambda calculus
module plfa.part2.Substitution where
Introduction
The primary purpose of this chapter is to prove that substitution commutes with itself. Barendgredt (1984) refers to this as the substitution lemma:
M [x:=N] [y:=L] = M [y:=L] [x:= N[y:=L] ]
In our setting, with de Bruijn indices for variables, the statement of the lemma becomes:
M [ N ] [ L ] ≡ M〔 L 〕[ N [ L ] ] (substitution)
where the notation M 〔 L 〕
is for substituting L for index 1 inside
M. In addition, because we define substitution in terms of parallel
substitution, we have the following generalization, replacing the
substitution of L with an arbitrary parallel substitution σ.
subst σ (M [ N ]) ≡ (subst (exts σ) M) [ subst σ N ] (substcommute)
The special case for renamings is also useful.
rename ρ (M [ N ]) ≡ (rename (ext ρ) M) [ rename ρ N ]
(renamesubstcommute)
The secondary purpose of this chapter is to define the σ algebra of parallel substitution due to Abadi, Cardelli, Curien, and Levy (1991). The equations of this algebra not only help us prove the substitution lemma, but they are generally useful. Furthermore, when the equations are applied from left to right, they form a rewrite system that decides whether any two substitutions are equal.
Imports
import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; cong; cong₂; congapp) open Eq.≡Reasoning using (begin_; _≡⟨⟩_; step≡; _∎) open import Function using (_∘_) open import plfa.part2.Untyped using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_; rename; subst; ext; exts; _[_]; substzero)
postulate extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x)  → f ≡ g
Notation
We introduce the following shorthand for the type of a renaming from
variables in context Γ
to variables in context Δ
.
Rename : Context → Context → Set Rename Γ Δ = ∀{A} → Γ ∋ A → Δ ∋ A
Similarly, we introduce the following shorthand for the type of a
substitution from variables in context Γ
to terms in context Δ
.
Subst : Context → Context → Set Subst Γ Δ = ∀{A} → Γ ∋ A → Δ ⊢ A
We use the following more succinct notation the subst
function.
⟪_⟫ : ∀{Γ Δ A} → Subst Γ Δ → Γ ⊢ A → Δ ⊢ A ⟪ σ ⟫ = λ M → subst σ M
The σ algebra of substitution
Substitutions map de Bruijn indices (natural numbers) to terms, so we
can view a substitution simply as a sequence of terms, or more
precisely, as an infinite sequence of terms. The σ algebra consists of
four operations for building such sequences: identity ids
, shift
↑
, cons M • σ
, and sequencing σ ⨟ τ
. The sequence 0, 1, 2, ...
is constructed by the identity substitution.
ids : ∀{Γ} → Subst Γ Γ ids x = ` x
The shift operation ↑
constructs the sequence
1, 2, 3, ...
and is defined as follows.
↑ : ∀{Γ A} → Subst Γ (Γ , A) ↑ x = ` (S x)
Given a term M
and substitution σ
, the operation
M • σ
constructs the sequence
M , σ 0, σ 1, σ 2, ...
This operation is analogous to the cons
operation of Lisp.
infixr 6 _•_ _•_ : ∀{Γ Δ A} → (Δ ⊢ A) → Subst Γ Δ → Subst (Γ , A) Δ (M • σ) Z = M (M • σ) (S x) = σ x
Given two substitutions σ
and τ
, the sequencing operation σ ⨟ τ
produces the sequence
⟪τ⟫(σ 0), ⟪τ⟫(σ 1), ⟪τ⟫(σ 2), ...
That is, it composes the two substitutions by first applying
σ
and then applying τ
.
infixr 5 _⨟_ _⨟_ : ∀{Γ Δ Σ} → Subst Γ Δ → Subst Δ Σ → Subst Γ Σ σ ⨟ τ = ⟪ τ ⟫ ∘ σ
For the sequencing operation, Abadi et al. use the notation of
function composition, writing σ ∘ τ
, but still with σ
applied
before τ
, which is the opposite of standard mathematical
practice. We instead write σ ⨟ τ
, because semicolon is
the standard notation for forward function composition.
The σ algebra equations
The σ algebra includes the following equations.
(subhead) ⟪ M • σ ⟫ (` Z) ≡ M
(subtail) ↑ ⨟ (M • σ) ≡ σ
(subη) (⟪ σ ⟫ (` Z)) • (↑ ⨟ σ) ≡ σ
(Zshift) (` Z) • ↑ ≡ ids
(subid) ⟪ ids ⟫ M ≡ M
(subapp) ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M)
(subabs) ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ σ ⟫ N
(subsub) ⟪ τ ⟫ ⟪ σ ⟫ M ≡ ⟪ σ ⨟ τ ⟫ M
(subidL) ids ⨟ σ ≡ σ
(subidR) σ ⨟ ids ≡ σ
(subassoc) (σ ⨟ τ) ⨟ θ ≡ σ ⨟ (τ ⨟ θ)
(subdist) (M • σ) ⨟ τ ≡ (⟪ τ ⟫ M) • (σ ⨟ τ)
The first group of equations describe how the •
operator acts like cons.
The equation subhead
says that the variable zero Z
returns the
head of the sequence (it acts like the car
of Lisp). Similarly,
subtail
says that sequencing with shift ↑
returns the tail of the
sequence (it acts like cdr
of Lisp). The subη
equation is the
ηexpansion rule for sequences, saying that taking the head and tail
of a sequence, and then cons’ing them together yields the original
sequence. The Zshift
equation says that cons’ing zero onto the
shifted sequence produces the identity sequence.
The next four equations involve applying substitutions to terms. The
equation subid
says that the identity substitution returns the term
unchanged. The equations subapp
and subabs
says that
substitution is a congruence for the lambda calculus. The subsub
equation says that the sequence operator ⨟
behaves as intended.
The last four equations concern the sequencing of substitutions.
The first two equations, subidL
and subidR
, say that
ids
is the left and right unit of the sequencing operator.
The subassoc
equation says that sequencing is associative.
Finally, subdist
says that postsequencing distributes through cons.
Relating the σ algebra and substitution functions
The definitions of substitution N [ M ]
and parallel substitution
subst σ N
depend on several auxiliary functions: rename
, exts
,
ext
, and substzero
. We shall relate those functions to terms in
the σ algebra.
To begin with, renaming can be expressed in terms of substitution. We have
rename ρ M ≡ ⟪ ren ρ ⟫ M (renamesubstren)
where ren
turns a renaming ρ
into a substitution by postcomposing
ρ
with the identity substitution.
ren : ∀{Γ Δ} → Rename Γ Δ → Subst Γ Δ ren ρ = ids ∘ ρ
When the renaming is the increment function, then it is equivalent to shift.
ren S_ ≡ ↑ (renshift)
rename S_ M ≡ ⟪ ↑ ⟫ M (renameshift)
Renaming with the identity renaming leaves the term unchanged.
rename (λ {A} x → x) M ≡ M (renameid)
Next we relate the exts
function to the σ algebra. Recall that the
exts
function extends a substitution as follows:
exts σ = ` Z, rename S_ (σ 0), rename S_ (σ 1), rename S_ (σ 2), ...
So exts
is equivalent to cons’ing Z onto the sequence formed
by applying σ
and then shifting.
exts σ ≡ ` Z • (σ ⨟ ↑) (extsconsshift)
The ext
function does the same job as exts
but for renamings
instead of substitutions. So composing ext
with ren
is the same as
composing ren
with exts
.
ren (ext ρ) ≡ exts (ren ρ) (renext)
Thus, we can recast the extsconsshift
equation in terms of
renamings.
ren (ext ρ) ≡ ` Z • (ren ρ ⨟ ↑) (extconsZshift)
It is also useful to specialize the subsub
equation of the σ
algebra to the situation where the first substitution is a renaming.
⟪ σ ⟫ (rename ρ M) ≡ ⟪ σ ∘ ρ ⟫ M (renamesubst)
The substzero M
substitution is equivalent to cons’ing
M
onto the identity substitution.
substzero M ≡ M • ids (substZconsids)
Finally, sequencing exts σ
with substzero M
is equivalent to
cons’ing M
onto σ
.
exts σ ⨟ substzero M ≡ (M • σ) (substzeroextscons)
Proofs of subhead, subtail, subη, Zshift, subidL, subdist, and subapp
We start with the proofs that are immediate from the definitions of the operators.
subhead : ∀ {Γ Δ} {A} {M : Δ ⊢ A}{σ : Subst Γ Δ} → ⟪ M • σ ⟫ (` Z) ≡ M subhead = refl
subtail : ∀{Γ Δ} {A B} {M : Δ ⊢ A} {σ : Subst Γ Δ} → (↑ ⨟ M • σ) {A = B} ≡ σ subtail = extensionality λ x → refl
subη : ∀{Γ Δ} {A B} {σ : Subst (Γ , A) Δ} → (⟪ σ ⟫ (` Z) • (↑ ⨟ σ)) {A = B} ≡ σ subη {Γ}{Δ}{A}{B}{σ} = extensionality λ x → lemma where lemma : ∀ {x} → ((⟪ σ ⟫ (` Z)) • (↑ ⨟ σ)) x ≡ σ x lemma {x = Z} = refl lemma {x = S x} = refl
Zshift : ∀{Γ}{A B} → ((` Z) • ↑) ≡ ids {Γ , A} {B} Zshift {Γ}{A}{B} = extensionality lemma where lemma : (x : Γ , A ∋ B) → ((` Z) • ↑) x ≡ ids x lemma Z = refl lemma (S y) = refl
subidL : ∀{Γ Δ} {σ : Subst Γ Δ} {A} → ids ⨟ σ ≡ σ {A} subidL = extensionality λ x → refl
subdist : ∀{Γ Δ Σ : Context} {A B} {σ : Subst Γ Δ} {τ : Subst Δ Σ} {M : Δ ⊢ A} → ((M • σ) ⨟ τ) ≡ ((subst τ M) • (σ ⨟ τ)) {B} subdist {Γ}{Δ}{Σ}{A}{B}{σ}{τ}{M} = extensionality λ x → lemma {x = x} where lemma : ∀ {x : Γ , A ∋ B} → ((M • σ) ⨟ τ) x ≡ ((subst τ M) • (σ ⨟ τ)) x lemma {x = Z} = refl lemma {x = S x} = refl
subapp : ∀{Γ Δ} {σ : Subst Γ Δ} {L : Γ ⊢ ★}{M : Γ ⊢ ★} → ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M) subapp = refl
Interlude: congruences
In this section we establish congruence rules for the σ algebra
operators •
and ⨟
and for subst
and its helper functions ext
,
rename
, exts
, and substzero
. These congruence rules help with
the equational reasoning in the later sections of this chapter.
[JGS: I would have liked to prove all of these via cong and cong₂, but I have not yet found a way to make that work. It seems that various implicit parameters get in the way.]
congext : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B} → (∀{A} → ρ ≡ ρ′ {A})  → ∀{A} → ext ρ {B = B} ≡ ext ρ′ {A} congext{Γ}{Δ}{ρ}{ρ′}{B} rr {A} = extensionality λ x → lemma {x} where lemma : ∀{x : Γ , B ∋ A} → ext ρ x ≡ ext ρ′ x lemma {Z} = refl lemma {S y} = cong S_ (congapp rr y)
congrename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}{M : Γ ⊢ B} → (∀{A} → ρ ≡ ρ′ {A})  → rename ρ M ≡ rename ρ′ M congrename {M = ` x} rr = cong `_ (congapp rr x) congrename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr = cong ƛ_ (congrename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (congext rr)) congrename {M = L · M} rr = cong₂ _·_ (congrename rr) (congrename rr)
congexts : ∀{Γ Δ}{σ σ′ : Subst Γ Δ}{B} → (∀{A} → σ ≡ σ′ {A})  → ∀{A} → exts σ {B = B} ≡ exts σ′ {A} congexts{Γ}{Δ}{σ}{σ′}{B} ss {A} = extensionality λ x → lemma {x} where lemma : ∀{x} → exts σ x ≡ exts σ′ x lemma {Z} = refl lemma {S x} = cong (rename S_) (congapp (ss {A}) x)
congsub : ∀{Γ Δ}{σ σ′ : Subst Γ Δ}{A}{M M′ : Γ ⊢ A} → (∀{A} → σ ≡ σ′ {A}) → M ≡ M′  → subst σ M ≡ subst σ′ M′ congsub {Γ} {Δ} {σ} {σ′} {A} {` x} ss refl = congapp ss x congsub {Γ} {Δ} {σ} {σ′} {A} {ƛ M} ss refl = cong ƛ_ (congsub {σ = exts σ}{σ′ = exts σ′} {M = M} (congexts ss) refl) congsub {Γ} {Δ} {σ} {σ′} {A} {L · M} ss refl = cong₂ _·_ (congsub {M = L} ss refl) (congsub {M = M} ss refl)
congsubzero : ∀{Γ}{B : Type}{M M′ : Γ ⊢ B} → M ≡ M′  → ∀{A} → substzero M ≡ (substzero M′) {A} congsubzero {Γ}{B}{M}{M′} mm' {A} = extensionality λ x → cong (λ z → substzero z x) mm'
congcons : ∀{Γ Δ}{A}{M N : Δ ⊢ A}{σ τ : Subst Γ Δ} → M ≡ N → (∀{A} → σ {A} ≡ τ {A})  → ∀{A} → (M • σ) {A} ≡ (N • τ) {A} congcons{Γ}{Δ}{A}{M}{N}{σ}{τ} refl st {A′} = extensionality lemma where lemma : (x : Γ , A ∋ A′) → (M • σ) x ≡ (M • τ) x lemma Z = refl lemma (S x) = congapp st x
congseq : ∀{Γ Δ Σ}{σ σ′ : Subst Γ Δ}{τ τ′ : Subst Δ Σ} → (∀{A} → σ {A} ≡ σ′ {A}) → (∀{A} → τ {A} ≡ τ′ {A}) → ∀{A} → (σ ⨟ τ) {A} ≡ (σ′ ⨟ τ′) {A} congseq {Γ}{Δ}{Σ}{σ}{σ′}{τ}{τ′} ss' tt' {A} = extensionality lemma where lemma : (x : Γ ∋ A) → (σ ⨟ τ) x ≡ (σ′ ⨟ τ′) x lemma x = begin (σ ⨟ τ) x ≡⟨⟩ subst τ (σ x) ≡⟨ cong (subst τ) (congapp ss' x) ⟩ subst τ (σ′ x) ≡⟨ congsub{M = σ′ x} tt' refl ⟩ subst τ′ (σ′ x) ≡⟨⟩ (σ′ ⨟ τ′) x ∎
Relating rename
, exts
, ext
, and substzero
to the σ algebra
In this section we establish equations that relate subst
and its
helper functions (rename
, exts
, ext
, and substzero
) to terms
in the σ algebra.
The first equation we prove is
rename ρ M ≡ ⟪ ren ρ ⟫ M (renamesubstren)
Because subst
uses the exts
function, we need the following lemma
which says that exts
and ext
do the same thing except that ext
works on renamings and exts
works on substitutions.
renext : ∀ {Γ Δ}{B C : Type} {ρ : Rename Γ Δ} → ren (ext ρ {B = B}) ≡ exts (ren ρ) {C} renext {Γ}{Δ}{B}{C}{ρ} = extensionality λ x → lemma {x = x} where lemma : ∀ {x : Γ , B ∋ C} → (ren (ext ρ)) x ≡ exts (ren ρ) x lemma {x = Z} = refl lemma {x = S x} = refl
With this lemma in hand, the proof is a straightforward induction on
the term M
.
renamesubstren : ∀ {Γ Δ}{A} {ρ : Rename Γ Δ}{M : Γ ⊢ A} → rename ρ M ≡ ⟪ ren ρ ⟫ M renamesubstren {M = ` x} = refl renamesubstren {ρ = ρ}{M = ƛ N} = begin rename ρ (ƛ N) ≡⟨⟩ ƛ rename (ext ρ) N ≡⟨ cong ƛ_ (renamesubstren {ρ = ext ρ}{M = N}) ⟩ ƛ ⟪ ren (ext ρ) ⟫ N ≡⟨ cong ƛ_ (congsub {M = N} renext refl) ⟩ ƛ ⟪ exts (ren ρ) ⟫ N ≡⟨⟩ ⟪ ren ρ ⟫ (ƛ N) ∎ renamesubstren {M = L · M} = cong₂ _·_ renamesubstren renamesubstren
The substitution ren S_
is equivalent to ↑
.
renshift : ∀{Γ}{A}{B} → ren S_ ≡ ↑ {A = B} {A} renshift {Γ}{A}{B} = extensionality λ x → lemma {x = x} where lemma : ∀ {x : Γ ∋ A} → ren (S_{B = B}) x ≡ ↑ {A = B} x lemma {x = Z} = refl lemma {x = S x} = refl
The substitution rename S_ M
is equivalent to shifting: ⟪ ↑ ⟫ M
.
renameshift : ∀{Γ} {A} {B} {M : Γ ⊢ A} → rename (S_{B = B}) M ≡ ⟪ ↑ ⟫ M renameshift{Γ}{A}{B}{M} = begin rename S_ M ≡⟨ renamesubstren ⟩ ⟪ ren S_ ⟫ M ≡⟨ congsub{M = M} renshift refl ⟩ ⟪ ↑ ⟫ M ∎
Next we prove the equation extsconsshift
, which states that exts
is equivalent to cons’ing Z onto the sequence formed by applying σ
and then shifting. The proof is by case analysis on the variable x
,
using renamesubstren
for when x = S y
.
extsconsshift : ∀{Γ Δ} {A B} {σ : Subst Γ Δ} → exts σ {A} {B} ≡ (` Z • (σ ⨟ ↑)) extsconsshift = extensionality λ x → lemma{x = x} where lemma : ∀{Γ Δ} {A B} {σ : Subst Γ Δ} {x : Γ , B ∋ A} → exts σ x ≡ (` Z • (σ ⨟ ↑)) x lemma {x = Z} = refl lemma {x = S y} = renamesubstren
As a corollary, we have a similar correspondence for ren (ext ρ)
.
extconsZshift : ∀{Γ Δ} {ρ : Rename Γ Δ}{A}{B} → ren (ext ρ {B = B}) ≡ (` Z • (ren ρ ⨟ ↑)) {A} extconsZshift {Γ}{Δ}{ρ}{A}{B} = begin ren (ext ρ) ≡⟨ renext ⟩ exts (ren ρ) ≡⟨ extsconsshift{σ = ren ρ} ⟩ ((` Z) • (ren ρ ⨟ ↑)) ∎
Finally, the substzero M
substitution is equivalent to cons’ing M
onto the identity substitution.
substZconsids : ∀{Γ}{A B : Type}{M : Γ ⊢ B} → substzero M ≡ (M • ids) {A} substZconsids = extensionality λ x → lemma {x = x} where lemma : ∀{Γ}{A B : Type}{M : Γ ⊢ B}{x : Γ , B ∋ A} → substzero M x ≡ (M • ids) x lemma {x = Z} = refl lemma {x = S x} = refl
Proofs of subabs, subid, and renameid
The equation subabs
follows immediately from the equation
extsconsshift
.
subabs : ∀{Γ Δ} {σ : Subst Γ Δ} {N : Γ , ★ ⊢ ★} → ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N subabs {σ = σ}{N = N} = begin ⟪ σ ⟫ (ƛ N) ≡⟨⟩ ƛ ⟪ exts σ ⟫ N ≡⟨ cong ƛ_ (congsub{M = N} extsconsshift refl) ⟩ ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N ∎
The proof of subid
requires the following lemma which says that
extending the identity substitution produces the identity
substitution.
extsids : ∀{Γ}{A B} → exts ids ≡ ids {Γ , B} {A} extsids {Γ}{A}{B} = extensionality lemma where lemma : (x : Γ , B ∋ A) → exts ids x ≡ ids x lemma Z = refl lemma (S x) = refl
The proof of ⟪ ids ⟫ M ≡ M
now follows easily by induction on M
,
using extsids
in the case for M ≡ ƛ N
.
subid : ∀{Γ} {A} {M : Γ ⊢ A} → ⟪ ids ⟫ M ≡ M subid {M = ` x} = refl subid {M = ƛ N} = begin ⟪ ids ⟫ (ƛ N) ≡⟨⟩ ƛ ⟪ exts ids ⟫ N ≡⟨ cong ƛ_ (congsub{M = N} extsids refl) ⟩ ƛ ⟪ ids ⟫ N ≡⟨ cong ƛ_ subid ⟩ ƛ N ∎ subid {M = L · M} = cong₂ _·_ subid subid
The renameid
equation is a corollary is subid
.
renameid : ∀ {Γ}{A} {M : Γ ⊢ A} → rename (λ {A} x → x) M ≡ M renameid {M = M} = begin rename (λ {A} x → x) M ≡⟨ renamesubstren ⟩ ⟪ ren (λ {A} x → x) ⟫ M ≡⟨⟩ ⟪ ids ⟫ M ≡⟨ subid ⟩ M ∎
Proof of subidR
The proof of subidR
follows directly from subid
.
subidR : ∀{Γ Δ} {σ : Subst Γ Δ} {A} → (σ ⨟ ids) ≡ σ {A} subidR {Γ}{σ = σ}{A} = begin σ ⨟ ids ≡⟨⟩ ⟪ ids ⟫ ∘ σ ≡⟨ extensionality (λ x → subid) ⟩ σ ∎
Proof of subsub
The subsub
equation states that sequenced substitutions σ ⨟ τ
are equivalent to first applying σ
then applying τ
.
⟪ τ ⟫ ⟪ σ ⟫ M ≡ ⟪ σ ⨟ τ ⟫ M
The proof requires several lemmas. First, we need to prove the specialization for renaming.
rename ρ (rename ρ′ M) ≡ rename (ρ ∘ ρ′) M
This in turn requires the following lemma about ext
.
composeext : ∀{Γ Δ Σ}{ρ : Rename Δ Σ} {ρ′ : Rename Γ Δ} {A B} → ((ext ρ) ∘ (ext ρ′)) ≡ ext (ρ ∘ ρ′) {B} {A} composeext = extensionality λ x → lemma {x = x} where lemma : ∀{Γ Δ Σ}{ρ : Rename Δ Σ} {ρ′ : Rename Γ Δ} {A B} {x : Γ , B ∋ A} → ((ext ρ) ∘ (ext ρ′)) x ≡ ext (ρ ∘ ρ′) x lemma {x = Z} = refl lemma {x = S x} = refl
To prove that composing renamings is equivalent to applying one after
the other using rename
, we proceed by induction on the term M
,
using the composeext
lemma in the case for M ≡ ƛ N
.
composerename : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A}{ρ : Rename Δ Σ}{ρ′ : Rename Γ Δ} → rename ρ (rename ρ′ M) ≡ rename (ρ ∘ ρ′) M composerename {M = ` x} = refl composerename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ′} = cong ƛ_ G where G : rename (ext ρ) (rename (ext ρ′) N) ≡ rename (ext (ρ ∘ ρ′)) N G = begin rename (ext ρ) (rename (ext ρ′) N) ≡⟨ composerename{ρ = ext ρ}{ρ′ = ext ρ′} ⟩ rename ((ext ρ) ∘ (ext ρ′)) N ≡⟨ congrename composeext ⟩ rename (ext (ρ ∘ ρ′)) N ∎ composerename {M = L · M} = cong₂ _·_ composerename composerename
The next lemma states that if a renaming and substitution commute on variables, then they also commute on terms. We explain the proof in detail below.
commutesubstrename : ∀{Γ Δ}{M : Γ ⊢ ★}{σ : Subst Γ Δ} {ρ : ∀{Γ} → Rename Γ (Γ , ★)} → (∀{x : Γ ∋ ★} → exts σ {B = ★} (ρ x) ≡ rename ρ (σ x)) → subst (exts σ {B = ★}) (rename ρ M) ≡ rename ρ (subst σ M) commutesubstrename {M = ` x} r = r commutesubstrename{Γ}{Δ}{ƛ N}{σ}{ρ} r = cong ƛ_ (commutesubstrename{Γ , ★}{Δ , ★}{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)) ≡⟨ composerename ⟩ rename (S_ ∘ ρ) (σ y) ≡⟨ congrename refl ⟩ rename ((ext ρ) ∘ S_) (σ y) ≡⟨ sym composerename ⟩ rename (ext ρ) (rename S_ (σ y)) ≡⟨⟩ rename (ext ρ) (exts σ (S y)) ∎ commutesubstrename {M = L · M}{ρ = ρ} r = cong₂ _·_ (commutesubstrename{M = L}{ρ = ρ} r) (commutesubstrename{M = M}{ρ = ρ} r)
The proof is by induction on the term M
.

If
M
is a variable, then we use the premise to conclude. 
If
M ≡ ƛ N
, we conclude using the induction hypothesis forN
. However, to use the induction hypothesis, we must show thatexts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
We prove this equation by cases on x.

If
x = Z
, the two sides are equal by definition. 
If
x = S y
, we obtain the goal by the following equational reasoning.exts (exts σ) (ext ρ (S y)) ≡ rename S_ (exts σ (ρ y)) ≡ rename S_ (rename S_ (σ (ρ y) (by the premise) ≡ rename (ext ρ) (exts σ (S y)) (by composerename) ≡ rename ((ext ρ) ∘ S_) (σ y) ≡ rename (ext ρ) (rename S_ (σ y)) (by composerename) ≡ rename (ext ρ) (exts σ (S y))


If
M
is an application, we obtain the goal using the induction hypothesis for each subterm.
The last lemma needed to prove subsub
states that the exts
function distributes with sequencing. It is a corollary of
commutesubstrename
as described below. (It would have been nicer
to prove this directly by equational reasoning in the σ algebra, but
that would require the subassoc
equation, whose proof depends on
subsub
, which in turn depends on this lemma.)
extsseq : ∀{Γ Δ Δ′} {σ₁ : Subst Γ Δ} {σ₂ : Subst Δ Δ′} → ∀ {A} → (exts σ₁ ⨟ exts σ₂) {A} ≡ exts (σ₁ ⨟ σ₂) extsseq = extensionality λ x → lemma {x = x} where lemma : ∀{Γ Δ Δ′}{A}{x : Γ , ★ ∋ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Δ′} → (exts σ₁ ⨟ exts σ₂) x ≡ exts (σ₁ ⨟ σ₂) x lemma {x = Z} = refl lemma {A = ★}{x = S x}{σ₁}{σ₂} = begin (exts σ₁ ⨟ exts σ₂) (S x) ≡⟨⟩ ⟪ exts σ₂ ⟫ (rename S_ (σ₁ x)) ≡⟨ commutesubstrename{M = σ₁ x}{σ = σ₂}{ρ = S_} refl ⟩ rename S_ (⟪ σ₂ ⟫ (σ₁ x)) ≡⟨⟩ rename S_ ((σ₁ ⨟ σ₂) x) ∎
The proof proceed by cases on x
.

If
x = Z
, the two sides are equal by the definition ofexts
and sequencing. 
If
x = S x
, we unfold the first use ofexts
and sequencing, then apply the lemmacommutesubstrename
. We conclude by the definition of sequencing.
Now we come to the proof of subsub
, which we explain below.
subsub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ} → ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ M) ≡ ⟪ σ₁ ⨟ σ₂ ⟫ M subsub {M = ` x} = refl subsub {Γ}{Δ}{Σ}{A}{ƛ N}{σ₁}{σ₂} = begin ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ (ƛ N)) ≡⟨⟩ ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡⟨ cong ƛ_ (subsub{M = N}{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡⟨ cong ƛ_ (congsub{M = N} (λ {A} → extsseq) refl) ⟩ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N ∎ subsub {M = L · M} = cong₂ _·_ (subsub{M = L}) (subsub{M = M})
We proceed by induction on the term M
.

If
M = x
, then both sides are equal toσ₂ (σ₁ x)
. 
If
M = ƛ N
, we first use the induction hypothesis to show thatƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N
and then use the lemma
extsseq
to showƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N

If
M
is an application, we use the induction hypothesis for both subterms.
The following corollary of subsub
specializes the first
substitution to a renaming.
renamesubst : ∀{Γ Δ Δ′}{M : Γ ⊢ ★}{ρ : Rename Γ Δ}{σ : Subst Δ Δ′} → ⟪ σ ⟫ (rename ρ M) ≡ ⟪ σ ∘ ρ ⟫ M renamesubst {Γ}{Δ}{Δ′}{M}{ρ}{σ} = begin ⟪ σ ⟫ (rename ρ M) ≡⟨ cong ⟪ σ ⟫ (renamesubstren{M = M}) ⟩ ⟪ σ ⟫ (⟪ ren ρ ⟫ M) ≡⟨ subsub{M = M} ⟩ ⟪ ren ρ ⨟ σ ⟫ M ≡⟨⟩ ⟪ σ ∘ ρ ⟫ M ∎
Proof of subassoc
The proof of subassoc
follows directly from subsub
and the
definition of sequencing.
subassoc : ∀{Γ Δ Σ Ψ : Context} {σ : Subst Γ Δ} {τ : Subst Δ Σ} {θ : Subst Σ Ψ} → ∀{A} → (σ ⨟ τ) ⨟ θ ≡ (σ ⨟ τ ⨟ θ) {A} subassoc {Γ}{Δ}{Σ}{Ψ}{σ}{τ}{θ}{A} = extensionality λ x → lemma{x = x} where lemma : ∀ {x : Γ ∋ A} → ((σ ⨟ τ) ⨟ θ) x ≡ (σ ⨟ τ ⨟ θ) x lemma {x} = begin ((σ ⨟ τ) ⨟ θ) x ≡⟨⟩ ⟪ θ ⟫ (⟪ τ ⟫ (σ x)) ≡⟨ subsub{M = σ x} ⟩ ⟪ τ ⨟ θ ⟫ (σ x) ≡⟨⟩ (σ ⨟ τ ⨟ θ) x ∎
Proof of substzeroextscons
The last equation we needed to prove substzeroextscons
was
subassoc
, so we can now go ahead with its proof. We simply apply
the equations for exts
and substzero
and then apply the σ algebra
equation to arrive at the normal form M • σ
.
substzeroextscons : ∀{Γ Δ}{σ : Subst Γ Δ}{B}{M : Δ ⊢ B}{A} → exts σ ⨟ substzero M ≡ (M • σ) {A} substzeroextscons {Γ}{Δ}{σ}{B}{M}{A} = begin exts σ ⨟ substzero M ≡⟨ congseq extsconsshift substZconsids ⟩ (` Z • (σ ⨟ ↑)) ⨟ (M • ids) ≡⟨ subdist ⟩ (⟪ M • ids ⟫ (` Z)) • ((σ ⨟ ↑) ⨟ (M • ids)) ≡⟨ congcons (subhead{σ = ids}) refl ⟩ M • ((σ ⨟ ↑) ⨟ (M • ids)) ≡⟨ congcons refl (subassoc{σ = σ}) ⟩ M • (σ ⨟ (↑ ⨟ (M • ids))) ≡⟨ congcons refl (congseq{σ = σ} refl (subtail{M = M}{σ = ids})) ⟩ M • (σ ⨟ ids) ≡⟨ congcons refl (subidR{σ = σ}) ⟩ M • σ ∎
Proof of the substitution lemma
We first prove the generalized form of the substitution lemma, showing
that a substitution σ
commutes with the substitution of M
into
N
.
⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡ ⟪ σ ⟫ (N [ M ])
This proof is where the σ algebra pays off. The proof is by direct equational reasoning. Starting with the lefthand side, we apply σ algebra equations, oriented lefttoright, until we arrive at the normal form
⟪ ⟪ σ ⟫ M • σ ⟫ N
We then do the same with the righthand side, arriving at the same normal form.
substcommute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{σ : Subst Γ Δ } → ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡ ⟪ σ ⟫ (N [ M ]) substcommute {Γ}{Δ}{N}{M}{σ} = begin ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡⟨⟩ ⟪ substzero (⟪ σ ⟫ M) ⟫ (⟪ exts σ ⟫ N) ≡⟨ congsub {M = ⟪ exts σ ⟫ N} substZconsids refl ⟩ ⟪ ⟪ σ ⟫ M • ids ⟫ (⟪ exts σ ⟫ N) ≡⟨ subsub {M = N} ⟩ ⟪ (exts σ) ⨟ ((⟪ σ ⟫ M) • ids) ⟫ N ≡⟨ congsub {M = N} (congseq extsconsshift refl) refl ⟩ ⟪ (` Z • (σ ⨟ ↑)) ⨟ (⟪ σ ⟫ M • ids) ⟫ N ≡⟨ congsub {M = N} (subdist {M = ` Z}) refl ⟩ ⟪ ⟪ ⟪ σ ⟫ M • ids ⟫ (` Z) • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N ≡⟨⟩ ⟪ ⟪ σ ⟫ M • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N ≡⟨ congsub{M = N} (congcons refl (subassoc{σ = σ})) refl ⟩ ⟪ ⟪ σ ⟫ M • (σ ⨟ ↑ ⨟ ⟪ σ ⟫ M • ids) ⟫ N ≡⟨ congsub{M = N} refl refl ⟩ ⟪ ⟪ σ ⟫ M • (σ ⨟ ids) ⟫ N ≡⟨ congsub{M = N} (congcons refl (subidR{σ = σ})) refl ⟩ ⟪ ⟪ σ ⟫ M • σ ⟫ N ≡⟨ congsub{M = N} (congcons refl (subidL{σ = σ})) refl ⟩ ⟪ ⟪ σ ⟫ M • (ids ⨟ σ) ⟫ N ≡⟨ congsub{M = N} (sym subdist) refl ⟩ ⟪ M • ids ⨟ σ ⟫ N ≡⟨ sym (subsub{M = N}) ⟩ ⟪ σ ⟫ (⟪ M • ids ⟫ N) ≡⟨ cong ⟪ σ ⟫ (sym (congsub{M = N} substZconsids refl)) ⟩ ⟪ σ ⟫ (N [ M ]) ∎
A corollary of substcommute
is that rename
also commutes with
substitution. In the proof below, we first exchange rename ρ
for
the substitution ⟪ ren ρ ⟫
, and apply substcommute
, and
then convert back to rename ρ
.
renamesubstcommute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{ρ : Rename Γ Δ } → (rename (ext ρ) N) [ rename ρ M ] ≡ rename ρ (N [ M ]) renamesubstcommute {Γ}{Δ}{N}{M}{ρ} = begin (rename (ext ρ) N) [ rename ρ M ] ≡⟨ congsub (congsubzero (renamesubstren{M = M})) (renamesubstren{M = N}) ⟩ (⟪ ren (ext ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ] ≡⟨ congsub refl (congsub{M = N} renext refl) ⟩ (⟪ exts (ren ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ] ≡⟨ substcommute{N = N} ⟩ subst (ren ρ) (N [ M ]) ≡⟨ sym (renamesubstren) ⟩ rename ρ (N [ M ]) ∎
To present the substitution lemma, we introduce the following notation
for substituting a term M
for index 1 within term N
.
_〔_〕 : ∀ {Γ A B C} → Γ , B , C ⊢ A → Γ ⊢ B  → Γ , C ⊢ A _〔_〕 {Γ} {A} {B} {C} N M = subst {Γ , B , C} {Γ , C} (exts (substzero M)) {A} N
The substitution lemma is stated as follows and proved as a corollary
of the substcommute
lemma.
substitution : ∀{Γ}{M : Γ , ★ , ★ ⊢ ★}{N : Γ , ★ ⊢ ★}{L : Γ ⊢ ★} → (M [ N ]) [ L ] ≡ (M 〔 L 〕) [ (N [ L ]) ] substitution{M = M}{N = N}{L = L} = sym (substcommute{N = M}{M = N}{σ = substzero L})
Notes
Most of the properties and proofs in this file are based on the paper Autosubst: Reasoning with de Bruijn Terms and Parallel Substitution by Schafer, Tebbi, and Smolka (ITP 2015). That paper, in turn, is based on the paper of Abadi, Cardelli, Curien, and Levy (1991) that defines the σ algebra.
Unicode
This chapter uses the following unicode:
⟪ U+27EA MATHEMATICAL LEFT DOUBLE ANGLE BRACKET (\<<)
⟫ U+27EA MATHEMATICAL RIGHT DOUBLE ANGLE BRACKET (\>>)
↑ U+2191 UPWARDS ARROW (\u)
• U+2022 BULLET (\bub)
⨟ U+2A1F Z NOTATION SCHEMA COMPOSITION (Cx 8 RET Z NOTATION SCHEMA COMPOSITION)
〔 U+3014 LEFT TORTOISE SHELL BRACKET (\( option 9 on page 2)
〕 U+3015 RIGHT TORTOISE SHELL BRACKET (\) option 9 on page 2)