Substitution: 无类型 λ-演算中的代换
module plfa.part2.Substitution where
引言
本章的主要目的是证明代换与自身可交换。Barendregt (1984) 将此称为代换引理：
M [x:=N] [y:=L] = M [y:=L] [x:= N[y:=L] ]在我们的环境中由于，使用了 de Bruijn 索引的变量，因此该引理的陈述变更为：
M [ N ] [ L ] ≡ M〔 L 〕[ N [ L ] ] (substitution)其中符号 M 〔 L 〕 表示用 L 代换 M 中的索引 1。此外，由于我们用平行代换来定义代换， 因此我们有以下推广，用任意平行代换 σ 替换掉了 L 的代换。
subst σ (M [ N ]) ≡ (subst (exts σ) M) [ subst σ N ] (subst-commute)代换的特例「重命名」也很有用：
rename ρ (M [ N ]) ≡ (rename (ext ρ) M) [ rename ρ N ]
(rename-subst-commute)本章的第二个目的是定义 Abadi、Cardelli、Curien 和 Levy (1991) 提出的平行代换的 σ-代数。这个代数方程不仅可以帮助我们证明代换引理， 而且还很有用。此外，当从左到右应用方程时，它们形成了一个重写系统， 以确定任意两个代换是否相等。
导入
import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; cong; cong₂; cong-app) open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎) open import Function.Base using (_∘_) open import plfa.part2.Untyped using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_; rename; subst; ext; exts; _[_]; subst-zero)
postulate extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) ----------------------- → f ≡ g
记法
我们引入了以下简写表示「将语境 Γ 中的变量重命名为语境 Δ 中的变量」的类型。
Rename : Context → Context → Set Rename Γ Δ = ∀{A} → Γ ∋ A → Δ ∋ A
与此类似，我们引入了以下简写表示「将语境 Γ 中的变量代换为语境 Δ 中的项」的类型。
Subst : Context → Context → Set Subst Γ Δ = ∀{A} → Γ ∋ A → Δ ⊢ A
我们用以下更简洁的记法表示 subst 代换函数。
⟪_⟫ : ∀{Γ Δ A} → Subst Γ Δ → Γ ⊢ A → Δ ⊢ A ⟪ σ ⟫ = λ M → subst σ M
代换的 σ-代数
代换将 de Bruijn 索引（自然数）映射为项，于是我们可以简单地将代换视作一系列项， 或者更精确地，将它视作项的有限序列。σ-代数由四个运算组成，用来构建这样的序列： 恒等 ids、抬升 ↑，构造 M • σ，以及序列 σ ⨟ τ。 序列 0, 1, 2, ... 由恒等代换构造：
ids : ∀{Γ} → Subst Γ Γ ids x = ` x
抬升运算 ↑ 用于构造序列
1, 2, 3, ...其定义如下：
↑ : ∀{Γ A} → Subst Γ (Γ , A) ↑ x = ` (S x)
给定项 M 和代换 σ，运算 M • σ 会构造序列
M , σ 0, σ 1, σ 2, ...以下运算类似 Lisp 中的 cons 构造运算。
infixr 6 _•_ _•_ : ∀{Γ Δ A} → (Δ ⊢ A) → Subst Γ Δ → Subst (Γ , A) Δ (M • σ) Z = M (M • σ) (S x) = σ x
给定两个代换 σ 和 τ，序列运算 σ ⨟ τ 会通过先应用代换 σ， 然后应用代换 τ 来将两个代换组合到一起，因此它会产生序列
⟪τ⟫(σ 0), ⟪τ⟫(σ 1), ⟪τ⟫(σ 2), ...下面是它的定义：
infixr 5 _⨟_ _⨟_ : ∀{Γ Δ Σ} → Subst Γ Δ → Subst Δ Σ → Subst Γ Σ σ ⨟ τ = ⟪ τ ⟫ ∘ σ
对于序列操作，Abadi 等人使用了函数复合的记法，将它记作 σ ∘ τ， 但 σ 仍然在 τ 之前被应用，这与标准的数学习惯相反。我们记作 σ ⨟ τ，因为分号是函数向右组合的标准记法。
σ-代数方程
σ-代数包含以下方程：
(sub-head) ⟪ M • σ ⟫ (` Z) ≡ M
(sub-tail) ↑ ⨟ (M • σ) ≡ σ
(sub-η) (⟪ σ ⟫ (` Z)) • (↑ ⨟ σ) ≡ σ
(Z-shift) (` Z) • ↑ ≡ ids
(sub-id) ⟪ ids ⟫ M ≡ M
(sub-app) ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M)
(sub-abs) ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N
(sub-sub) ⟪ τ ⟫ ⟪ σ ⟫ M ≡ ⟪ σ ⨟ τ ⟫ M
(sub-idL) ids ⨟ σ ≡ σ
(sub-idR) σ ⨟ ids ≡ σ
(sub-assoc) (σ ⨟ τ) ⨟ θ ≡ σ ⨟ (τ ⨟ θ)
(sub-dist) (M • σ) ⨟ τ ≡ (⟪ τ ⟫ M) • (σ ⨟ τ)第一组方程描述了 • 算子的行为类似于 cons。方程 sub-head 表示变量零 Z 返回序列的头部（它的行为类似于 Lisp 中的 car）。与此类似， sub-tail 表示对序列应用抬升运算 ↑ 后返回该序列的尾部（它的行为类似于 Lisp 中的 cdr）。sub-η 方程是序列的 η-展开规则，表示接受一个序列的头部和尾部， 将它们 cons 在一起产生原来的序列。Z-shift 方程表示将零 cons 到抬升的序列会得到恒等的序列。
接下来的四个方程涉及对项的代换。方程 sub-id 表示恒等代换返回的项保持不变。 方程 sub-app 和 sub-abs 表示代换对 λ-演算满足合同性。sub-sub 方程表示序列算子 ⨟ 的行为符合预期。
最后四个方程涉及代换的序列。前两个方程 sub-idL 和 sub-idR 表示 ids 是序列算子的左右单位元。sub-assoc 方程表示序列满足结合律。 最后，sub-dist 表示后面的序列对 cons 满足分配率。
关联 σ-代数和代换函数
代换的定义 N [ M ] 和平行代换 subst σ N 依赖于几个辅助函数：rename、 exts、ext 和 subst-zero。我们应当在 σ-代数中将这些函数与项关联起来。
首先，重命名可以用代换表示。我们有：
rename ρ M ≡ ⟪ ren ρ ⟫ M (rename-subst-ren)其中 ren 通过将 ρ 复合到恒等代换后面来将重命名 ρ 转换为一个代换：
ren : ∀{Γ Δ} → Rename Γ Δ → Subst Γ Δ ren ρ = ids ∘ ρ
当重命名为递增函数时，它等价于抬升。
ren S_ ≡ ↑ (ren-shift)
rename S_ M ≡ ⟪ ↑ ⟫ M (rename-shift)带恒等重命名的重命名会保持项不变：
rename (λ {A} x → x) M ≡ M (rename-id)接下来我们将 exts 函数关联到 σ-代数。回忆 exts 函数将代换扩展为以下形式：
exts σ = ` Z, rename S_ (σ 0), rename S_ (σ 1), rename S_ (σ 2), ...因此 exts 等价于将 Z cons 到应用 σ 所产生的序列上，之后再抬升它：
exts σ ≡ ` Z • (σ ⨟ ↑) (exts-cons-shift)ext 函数做的事情和 exts 一样，只不过用于重命名而非代换，因此将 ren 复合到 ext 等价于将 exts 复合到 ren：
ren (ext ρ) ≡ exts (ren ρ) (ren-ext)于是，我们可以将 exts-cons-shift 方程重新转换为重命名：
ren (ext ρ) ≡ ` Z • (ren ρ ⨟ ↑) (ext-cons-Z-shift)将 σ-代数的 sub-sub 方程特化为第一个代换是重命名的情况也很有用：
⟪ σ ⟫ (rename ρ M) ≡ ⟪ σ ∘ ρ ⟫ M (rename-subst)subst-zero M 代换等价于将 M cons 到恒等代换：
subst-zero M ≡ M • ids (subst-Z-cons-ids)最后，将 subst-zero M 列在 exts σ 之后等价于将 M cons 到 σ。
exts σ ⨟ subst-zero M ≡ (M • σ) (subst-zero-exts-cons)sub-head、sub-tail、sub-η、Z-shift、sub-idL、sub-dist 和 sub-app 的证明
我们直接从这些算子的定义就能得它们的证明：
sub-head : ∀ {Γ Δ} {A} {M : Δ ⊢ A}{σ : Subst Γ Δ} → ⟪ M • σ ⟫ (` Z) ≡ M sub-head = refl
sub-tail : ∀{Γ Δ} {A B} {M : Δ ⊢ A} {σ : Subst Γ Δ} → (↑ ⨟ M • σ) {A = B} ≡ σ sub-tail = 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
Z-shift : ∀{Γ}{A B} → ((` Z) • ↑) ≡ ids {Γ , A} {B} Z-shift {Γ}{A}{B} = extensionality lemma where lemma : (x : Γ , A ∋ B) → ((` Z) • ↑) x ≡ ids x lemma Z = refl lemma (S y) = refl
sub-idL : ∀{Γ Δ} {σ : Subst Γ Δ} {A} → ids ⨟ σ ≡ σ {A} sub-idL = extensionality λ x → refl
sub-dist : ∀{Γ Δ Σ : Context} {A B} {σ : Subst Γ Δ} {τ : Subst Δ Σ} {M : Δ ⊢ A} → ((M • σ) ⨟ τ) ≡ ((subst τ M) • (σ ⨟ τ)) {B} sub-dist {Γ}{Δ}{Σ}{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
sub-app : ∀{Γ Δ} {σ : Subst Γ Δ} {L : Γ ⊢ ★}{M : Γ ⊢ ★} → ⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M) sub-app = refl
插曲：合同性
在本节中，我们将为 σ-代数的算子 • 和 ⨟、subst 及其辅助函数 ext、 rename、exts 以及 subst-zero 建立合同律。这些合同律有助于后续章节的等式推理。
cong-ext : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B} → (∀{A} → ρ ≡ ρ′ {A}) --------------------------------- → ∀{A} → ext ρ {B = B} ≡ ext ρ′ {A} cong-ext{Γ}{Δ}{ρ}{ρ′}{B} rr {A} = extensionality λ x → lemma {x} where lemma : ∀{x : Γ , B ∋ A} → ext ρ x ≡ ext ρ′ x lemma {Z} = refl lemma {S y} = cong S_ (cong-app rr y)
cong-rename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}{M : Γ ⊢ B} → (∀{A} → ρ ≡ ρ′ {A}) ------------------------ → rename ρ M ≡ rename ρ′ M cong-rename {M = ` x} rr = cong `_ (cong-app rr x) cong-rename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr = cong ƛ_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr)) cong-rename {M = L · M} rr = cong₂ _·_ (cong-rename rr) (cong-rename rr)
cong-exts : ∀{Γ Δ}{σ σ′ : Subst Γ Δ}{B} → (∀{A} → σ ≡ σ′ {A}) ----------------------------------- → ∀{A} → exts σ {B = B} ≡ exts σ′ {A} cong-exts{Γ}{Δ}{σ}{σ′}{B} ss {A} = extensionality λ x → lemma {x} where lemma : ∀{x} → exts σ x ≡ exts σ′ x lemma {Z} = refl lemma {S x} = cong (rename S_) (cong-app (ss {A}) x)
cong-sub : ∀{Γ Δ}{σ σ′ : Subst Γ Δ}{A}{M M′ : Γ ⊢ A} → (∀{A} → σ ≡ σ′ {A}) → M ≡ M′ ------------------------------ → subst σ M ≡ subst σ′ M′ cong-sub {Γ} {Δ} {σ} {σ′} {A} {` x} ss refl = cong-app ss x cong-sub {Γ} {Δ} {σ} {σ′} {A} {ƛ M} ss refl = cong ƛ_ (cong-sub {σ = exts σ}{σ′ = exts σ′} {M = M} (cong-exts ss) refl) cong-sub {Γ} {Δ} {σ} {σ′} {A} {L · M} ss refl = cong₂ _·_ (cong-sub {M = L} ss refl) (cong-sub {M = M} ss refl)
cong-sub-zero : ∀{Γ}{B : Type}{M M′ : Γ ⊢ B} → M ≡ M′ ----------------------------------------- → ∀{A} → subst-zero M ≡ (subst-zero M′) {A} cong-sub-zero {Γ}{B}{M}{M′} mm' {A} = extensionality λ x → cong (λ z → subst-zero z x) mm'
cong-cons : ∀{Γ Δ}{A}{M N : Δ ⊢ A}{σ τ : Subst Γ Δ} → M ≡ N → (∀{A} → σ {A} ≡ τ {A}) -------------------------------- → ∀{A} → (M • σ) {A} ≡ (N • τ) {A} cong-cons{Γ}{Δ}{A}{M}{N}{σ}{τ} refl st {A′} = extensionality lemma where lemma : (x : Γ , A ∋ A′) → (M • σ) x ≡ (M • τ) x lemma Z = refl lemma (S x) = cong-app st x
cong-seq : ∀{Γ Δ Σ}{σ σ′ : Subst Γ Δ}{τ τ′ : Subst Δ Σ} → (∀{A} → σ {A} ≡ σ′ {A}) → (∀{A} → τ {A} ≡ τ′ {A}) → ∀{A} → (σ ⨟ τ) {A} ≡ (σ′ ⨟ τ′) {A} cong-seq {Γ}{Δ}{Σ}{σ}{σ′}{τ}{τ′} ss' tt' {A} = extensionality lemma where lemma : (x : Γ ∋ A) → (σ ⨟ τ) x ≡ (σ′ ⨟ τ′) x lemma x = begin (σ ⨟ τ) x ≡⟨⟩ subst τ (σ x) ≡⟨ cong (subst τ) (cong-app ss' x) ⟩ subst τ (σ′ x) ≡⟨ cong-sub{M = σ′ x} tt' refl ⟩ subst τ′ (σ′ x) ≡⟨⟩ (σ′ ⨟ τ′) x ∎
将 rename、exts、ext 和 subst-zero 关联到 σ-代数
本节中我们将为 σ-代数中的项与 subst 及其辅助函数（rename、exts、ext 和 subst-zero）建立关联方程。
我们要证明的第一个方程是
rename ρ M ≡ ⟪ ren ρ ⟫ M (rename-subst-ren)由于 subst 使用了 exts 函数，我们需要以下引理，它证明了 exts 和 ext 做的事情一样，只不过 ext 应用于重命名，而 exts 应用于代换。
ren-ext : ∀ {Γ Δ}{B C : Type} {ρ : Rename Γ Δ} → ren (ext ρ {B = B}) ≡ exts (ren ρ) {C} ren-ext {Γ}{Δ}{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
有了这条引理，我们只需对项 M 进行归纳即可：
rename-subst-ren : ∀ {Γ Δ}{A} {ρ : Rename Γ Δ}{M : Γ ⊢ A} → rename ρ M ≡ ⟪ ren ρ ⟫ M rename-subst-ren {M = ` x} = refl rename-subst-ren {ρ = ρ}{M = ƛ N} = begin rename ρ (ƛ N) ≡⟨⟩ ƛ rename (ext ρ) N ≡⟨ cong ƛ_ (rename-subst-ren {ρ = ext ρ}{M = N}) ⟩ ƛ ⟪ ren (ext ρ) ⟫ N ≡⟨ cong ƛ_ (cong-sub {M = N} ren-ext refl) ⟩ ƛ ⟪ exts (ren ρ) ⟫ N ≡⟨⟩ ⟪ ren ρ ⟫ (ƛ N) ∎ rename-subst-ren {M = L · M} = cong₂ _·_ rename-subst-ren rename-subst-ren
代换 ren S_ 等价于 ↑。
ren-shift : ∀{Γ}{A}{B} → ren S_ ≡ ↑ {A = B} {A} ren-shift {Γ}{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
代换 rename S_ M 等价于抬升：⟪ ↑ ⟫ M。
rename-shift : ∀{Γ} {A} {B} {M : Γ ⊢ A} → rename (S_{B = B}) M ≡ ⟪ ↑ ⟫ M rename-shift{Γ}{A}{B}{M} = begin rename S_ M ≡⟨ rename-subst-ren ⟩ ⟪ ren S_ ⟫ M ≡⟨ cong-sub{M = M} ren-shift refl ⟩ ⟪ ↑ ⟫ M ∎
接下来证明 exts-cons-shift，它陈述了 exts 等价于将 Z cons 到应用 σ 后抬升所产生的序列上。当 x = S y 时，使用 rename-subst-ren 对变量 x 进行情况分析即可证明。
exts-cons-shift : ∀{Γ Δ} {A B} {σ : Subst Γ Δ} → exts σ {A} {B} ≡ (` Z • (σ ⨟ ↑)) exts-cons-shift = 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} = rename-subst-ren
我们可以定义一个与 ren (ext ρ) 类似的函数作为辅助：
ext-cons-Z-shift : ∀{Γ Δ} {ρ : Rename Γ Δ}{A}{B} → ren (ext ρ {B = B}) ≡ (` Z • (ren ρ ⨟ ↑)) {A} ext-cons-Z-shift {Γ}{Δ}{ρ}{A}{B} = begin ren (ext ρ) ≡⟨ ren-ext ⟩ exts (ren ρ) ≡⟨ exts-cons-shift{σ = ren ρ} ⟩ ((` Z) • (ren ρ ⨟ ↑)) ∎
最后，代换 subst-zero M 等价于将 M cons 到恒等代换：
subst-Z-cons-ids : ∀{Γ}{A B : Type}{M : Γ ⊢ B} → subst-zero M ≡ (M • ids) {A} subst-Z-cons-ids = extensionality λ x → lemma {x = x} where lemma : ∀{Γ}{A B : Type}{M : Γ ⊢ B}{x : Γ , B ∋ A} → subst-zero M x ≡ (M • ids) x lemma {x = Z} = refl lemma {x = S x} = refl
sub-ab、sub-id 和 rename-id 的证明
方程 sub-abs 可直接从方程 exts-cons-shift 得出。
sub-abs : ∀{Γ Δ} {σ : Subst Γ Δ} {N : Γ , ★ ⊢ ★} → ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N sub-abs {σ = σ}{N = N} = begin ⟪ σ ⟫ (ƛ N) ≡⟨⟩ ƛ ⟪ exts σ ⟫ N ≡⟨ cong ƛ_ (cong-sub{M = N} exts-cons-shift refl) ⟩ ƛ ⟪ (` Z) • (σ ⨟ ↑) ⟫ N ∎
sub-id 的证明需要以下引理，它阐述了扩展一个恒等代换依旧会得到恒等代换：
exts-ids : ∀{Γ}{A B} → exts ids ≡ ids {Γ , B} {A} exts-ids {Γ}{A}{B} = extensionality lemma where lemma : (x : Γ , B ∋ A) → exts ids x ≡ ids x lemma Z = refl lemma (S x) = refl
⟪ ids ⟫ M ≡ M 的证明现在可以非常容易地对 M 进行归纳得出，只需在 M ≡ ƛ N 的情况中使用 exts-ids 即可。
sub-id : ∀{Γ} {A} {M : Γ ⊢ A} → ⟪ ids ⟫ M ≡ M sub-id {M = ` x} = refl sub-id {M = ƛ N} = begin ⟪ ids ⟫ (ƛ N) ≡⟨⟩ ƛ ⟪ exts ids ⟫ N ≡⟨ cong ƛ_ (cong-sub{M = N} exts-ids refl) ⟩ ƛ ⟪ ids ⟫ N ≡⟨ cong ƛ_ sub-id ⟩ ƛ N ∎ sub-id {M = L · M} = cong₂ _·_ sub-id sub-id
rename-id 方程是 sub-id 的对应函数。
rename-id : ∀ {Γ}{A} {M : Γ ⊢ A} → rename (λ {A} x → x) M ≡ M rename-id {M = M} = begin rename (λ {A} x → x) M ≡⟨ rename-subst-ren ⟩ ⟪ ren (λ {A} x → x) ⟫ M ≡⟨⟩ ⟪ ids ⟫ M ≡⟨ sub-id ⟩ M ∎
sub-idR 的证明
sub-idR 根据 sub-id 直接可得：
sub-idR : ∀{Γ Δ} {σ : Subst Γ Δ} {A} → (σ ⨟ ids) ≡ σ {A} sub-idR {Γ}{σ = σ}{A} = begin σ ⨟ ids ≡⟨⟩ ⟪ ids ⟫ ∘ σ ≡⟨ extensionality (λ x → sub-id) ⟩ σ ∎
sub-sub 的证明
sub-sub 方程陈述了代换序列 σ ⨟ τ 等价于先应用 σ 再应用 τ：
⟪ τ ⟫ ⟪ σ ⟫ M ≡ ⟪ σ ⨟ τ ⟫ M它的证明需要几条引理。首先，我们需要证明一个重命名的特化版本：
rename ρ (rename ρ′ M) ≡ rename (ρ ∘ ρ′) M而它需要以下关于 ext 的引理：
compose-ext : ∀{Γ Δ Σ}{ρ : Rename Δ Σ} {ρ′ : Rename Γ Δ} {A B} → ((ext ρ) ∘ (ext ρ′)) ≡ ext (ρ ∘ ρ′) {B} {A} compose-ext = 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
要证明复合重命名等价于用 rename 应用一个之后再应用另一个，我们需要通过在 M ≡ ƛ N 的情况中用 compose-ext 对项 M 进行归纳：
compose-rename : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A}{ρ : Rename Δ Σ}{ρ′ : Rename Γ Δ} → rename ρ (rename ρ′ M) ≡ rename (ρ ∘ ρ′) M compose-rename {M = ` x} = refl compose-rename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ′} = cong ƛ_ G where G : rename (ext ρ) (rename (ext ρ′) N) ≡ rename (ext (ρ ∘ ρ′)) N G = begin rename (ext ρ) (rename (ext ρ′) N) ≡⟨ compose-rename{ρ = ext ρ}{ρ′ = ext ρ′} ⟩ rename ((ext ρ) ∘ (ext ρ′)) N ≡⟨ cong-rename compose-ext ⟩ rename (ext (ρ ∘ ρ′)) N ∎ compose-rename {M = L · M} = cong₂ _·_ compose-rename compose-rename
下一条引理阐述了若重命名和代换对变量可交换，则它们对项也可交换。 我们在后面详细解释证明过程：
commute-subst-rename : ∀{Γ Δ}{M : Γ ⊢ ★}{σ : Subst Γ Δ} {ρ₁ : Rename Γ (Γ , ★)}{ρ₂ : Rename Δ (Δ , ★)} → (∀{x : Γ ∋ ★} → exts σ (ρ₁ x) ≡ rename ρ₂ (σ x)) → subst (exts σ) (rename ρ₁ M) ≡ rename ρ₂ (subst σ M) commute-subst-rename {M = ` x} H = H 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′ {Z} = refl H′ {S y} = begin exts (exts σ) (ext ρ₁ (S y)) ≡⟨⟩ rename S_ (exts σ (ρ₁ y)) ≡⟨ cong (rename S_) H ⟩ rename S_ (rename ρ₂ (σ y)) ≡⟨ compose-rename ⟩ rename (S_ ∘ ρ₂) (σ y) ≡⟨⟩ rename ((ext ρ₂) ∘ S_) (σ y) ≡⟨ sym compose-rename ⟩ rename (ext ρ₂) (rename S_ (σ y)) ≡⟨⟩ rename (ext ρ₂) (exts σ (S y)) ∎ commute-subst-rename {M = L · N} H = cong₂ _·_ (commute-subst-rename{M = L} H) (commute-subst-rename{M = N} H)
证明通过对项 M 进行归纳得出：
若
M为变量，则我们用前提可得结论。若
M ≡ ƛ N，我们对N应用归纳假设可出结论。然而，要使用归纳假设，我们必须证明exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)此方程可通过对
x进行情况分析证明：若
x = Z，则两边按照定义相等。若
x = S y，我们通过以下等式推理即可证得目标exts (exts σ) (ext ρ₁ (S y)) ≡ rename S_ (exts σ (ρ₁ y)) ≡ rename S_ (rename ρ₂ (σ y)) (by the premise) ≡ rename (S_ ∘ ρ₂) (σ y) (by compose-rename) ≡ rename ((ext ρ₂) ∘ S_) (σ y) ≡ rename (ext ρ₂) (rename S_ (σ y)) (by compose-rename) ≡ rename (ext ρ₂) (exts σ (S y))
- 若
M为应用，我们对每个子项使用归纳假设即可证得目标。
证明 sub-sub 所需的最后一个引理指出 exts 函数按对序列满足分配率。 它是 commute-subst-rename 的一个推论，如下所述。 （如果直接通过 σ-代数中的等式推理来证明这一点会更好，但这需要 sub-assoc 方程，其证明依赖于 sub-sub，而 sub-sub 又依赖于于此引理。）
exts-seq : ∀{Γ Δ Δ′} {σ₁ : Subst Γ Δ} {σ₂ : Subst Δ Δ′} → ∀ {A} → (exts σ₁ ⨟ exts σ₂) {A} ≡ exts (σ₁ ⨟ σ₂) exts-seq = 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)) ≡⟨ commute-subst-rename{M = σ₁ x}{σ = σ₂}{ρ₁ = S_}{ρ₂ = S_} refl ⟩ rename S_ (⟪ σ₂ ⟫ (σ₁ x)) ≡⟨⟩ rename S_ ((σ₁ ⨟ σ₂) x) ∎
通过对 x 进行情况分析来证明：
若
x = Z，则根据exts和序列的定义两边相等。若
x = S x，我们展开第一个exts和序列，之后应用引理commute-subst-rename。 根据序列的定义可得出结论。
现在我们来证明 sub-sub，它的解释如下：
sub-sub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ} → ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ M) ≡ ⟪ σ₁ ⨟ σ₂ ⟫ M sub-sub {M = ` x} = refl sub-sub {Γ}{Δ}{Σ}{A}{ƛ N}{σ₁}{σ₂} = begin ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ (ƛ N)) ≡⟨⟩ ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡⟨ cong ƛ_ (sub-sub{M = N}{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡⟨ cong ƛ_ (cong-sub{M = N} (λ {A} → exts-seq) refl) ⟩ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N ∎ sub-sub {M = L · M} = cong₂ _·_ (sub-sub{M = L}) (sub-sub{M = M})
我们通过对项 M 进行归纳来证明：
若
M = x，则两边都等于σ₂ (σ₁ x)。若
M = ƛ N，哦我们首先用归纳假设证明ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N之后用引理
exts-seq证明ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N若
M是一个应用，我们对两个子项应用归纳假设即可得证。
以下 sub-sub 的推论特化了重命名的第一个代换：
rename-subst : ∀{Γ Δ Δ′}{M : Γ ⊢ ★}{ρ : Rename Γ Δ}{σ : Subst Δ Δ′} → ⟪ σ ⟫ (rename ρ M) ≡ ⟪ σ ∘ ρ ⟫ M rename-subst {Γ}{Δ}{Δ′}{M}{ρ}{σ} = begin ⟪ σ ⟫ (rename ρ M) ≡⟨ cong ⟪ σ ⟫ (rename-subst-ren{M = M}) ⟩ ⟪ σ ⟫ (⟪ ren ρ ⟫ M) ≡⟨ sub-sub{M = M} ⟩ ⟪ ren ρ ⨟ σ ⟫ M ≡⟨⟩ ⟪ σ ∘ ρ ⟫ M ∎
sub-assoc 的证明
sub-assoc 的证明可直接从 sub-sub 以及序列的定义得出：
sub-assoc : ∀{Γ Δ Σ Ψ : Context} {σ : Subst Γ Δ} {τ : Subst Δ Σ} {θ : Subst Σ Ψ} → ∀{A} → (σ ⨟ τ) ⨟ θ ≡ (σ ⨟ τ ⨟ θ) {A} sub-assoc {Γ}{Δ}{Σ}{Ψ}{σ}{τ}{θ}{A} = extensionality λ x → lemma{x = x} where lemma : ∀ {x : Γ ∋ A} → ((σ ⨟ τ) ⨟ θ) x ≡ (σ ⨟ τ ⨟ θ) x lemma {x} = begin ((σ ⨟ τ) ⨟ θ) x ≡⟨⟩ ⟪ θ ⟫ (⟪ τ ⟫ (σ x)) ≡⟨ sub-sub{M = σ x} ⟩ ⟪ τ ⨟ θ ⟫ (σ x) ≡⟨⟩ (σ ⨟ τ ⨟ θ) x ∎
subst-zero-exts-cons 的证明
我们证明 subst-zero-exts-cons 需要的最后一个方程是 sub-assoc， 现在我们可以继续证明它。只需对 exts 和 subst-zero 应用方程，然后应用 σ-代数方程即可得到正规形式 M • σ。
subst-zero-exts-cons : ∀{Γ Δ}{σ : Subst Γ Δ}{B}{M : Δ ⊢ B}{A} → exts σ ⨟ subst-zero M ≡ (M • σ) {A} subst-zero-exts-cons {Γ}{Δ}{σ}{B}{M}{A} = begin exts σ ⨟ subst-zero M ≡⟨ cong-seq exts-cons-shift subst-Z-cons-ids ⟩ (` Z • (σ ⨟ ↑)) ⨟ (M • ids) ≡⟨ sub-dist ⟩ (⟪ M • ids ⟫ (` Z)) • ((σ ⨟ ↑) ⨟ (M • ids)) ≡⟨ cong-cons (sub-head{σ = ids}) refl ⟩ M • ((σ ⨟ ↑) ⨟ (M • ids)) ≡⟨ cong-cons refl (sub-assoc{σ = σ}) ⟩ M • (σ ⨟ (↑ ⨟ (M • ids))) ≡⟨ cong-cons refl (cong-seq{σ = σ} refl (sub-tail{M = M}{σ = ids})) ⟩ M • (σ ⨟ ids) ≡⟨ cong-cons refl (sub-idR{σ = σ}) ⟩ M • σ ∎
代换引理的证明
我们首先证明代换引理的推广形式，证明代换 σ 对在 N 中代换 M 满足交换律。
⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡ ⟪ σ ⟫ (N [ M ])这个证明是 σ-代数得到回报的地方。证明可通过直接得等式推理进项。 从方程左边开始，我们应用 σ-代数方程，从左到右，直到得到正规形式
⟪ ⟪ σ ⟫ M • σ ⟫ N之后我们对方程右边做同样的事情，直到得到同样的正规形式。
subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{σ : Subst Γ Δ } → ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡ ⟪ σ ⟫ (N [ M ]) subst-commute {Γ}{Δ}{N}{M}{σ} = begin ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡⟨⟩ ⟪ subst-zero (⟪ σ ⟫ M) ⟫ (⟪ exts σ ⟫ N) ≡⟨ cong-sub {M = ⟪ exts σ ⟫ N} subst-Z-cons-ids refl ⟩ ⟪ ⟪ σ ⟫ M • ids ⟫ (⟪ exts σ ⟫ N) ≡⟨ sub-sub {M = N} ⟩ ⟪ (exts σ) ⨟ ((⟪ σ ⟫ M) • ids) ⟫ N ≡⟨ cong-sub {M = N} (cong-seq exts-cons-shift refl) refl ⟩ ⟪ (` Z • (σ ⨟ ↑)) ⨟ (⟪ σ ⟫ M • ids) ⟫ N ≡⟨ cong-sub {M = N} (sub-dist {M = ` Z}) refl ⟩ ⟪ ⟪ ⟪ σ ⟫ M • ids ⟫ (` Z) • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N ≡⟨⟩ ⟪ ⟪ σ ⟫ M • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N ≡⟨ cong-sub{M = N} (cong-cons refl (sub-assoc{σ = σ})) refl ⟩ ⟪ ⟪ σ ⟫ M • (σ ⨟ ↑ ⨟ ⟪ σ ⟫ M • ids) ⟫ N ≡⟨ cong-sub{M = N} refl refl ⟩ ⟪ ⟪ σ ⟫ M • (σ ⨟ ids) ⟫ N ≡⟨ cong-sub{M = N} (cong-cons refl (sub-idR{σ = σ})) refl ⟩ ⟪ ⟪ σ ⟫ M • σ ⟫ N ≡⟨ cong-sub{M = N} (cong-cons refl (sub-idL{σ = σ})) refl ⟩ ⟪ ⟪ σ ⟫ M • (ids ⨟ σ) ⟫ N ≡⟨ cong-sub{M = N} (sym sub-dist) refl ⟩ ⟪ M • ids ⨟ σ ⟫ N ≡⟨ sym (sub-sub{M = N}) ⟩ ⟪ σ ⟫ (⟪ M • ids ⟫ N) ≡⟨ cong ⟪ σ ⟫ (sym (cong-sub{M = N} subst-Z-cons-ids refl)) ⟩ ⟪ σ ⟫ (N [ M ]) ∎
subst-commute 的一个推论是 rename 也对代换满足交换律。在下面的证明中， 我们首先为代换 ⟪ ren ρ ⟫ 交换了 rename ρ，然后应用 subst-commute， 之后转换回 rename ρ。
rename-subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{ρ : Rename Γ Δ } → (rename (ext ρ) N) [ rename ρ M ] ≡ rename ρ (N [ M ]) rename-subst-commute {Γ}{Δ}{N}{M}{ρ} = begin (rename (ext ρ) N) [ rename ρ M ] ≡⟨ cong-sub (cong-sub-zero (rename-subst-ren{M = M})) (rename-subst-ren{M = N}) ⟩ (⟪ ren (ext ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ] ≡⟨ cong-sub refl (cong-sub{M = N} ren-ext refl) ⟩ (⟪ exts (ren ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ] ≡⟨ subst-commute{N = N} ⟩ subst (ren ρ) (N [ M ]) ≡⟨ sym (rename-subst-ren) ⟩ rename ρ (N [ M ]) ∎
为了展示代换引理，我们为「用项 M 代换项 N 中的索引 1」引入了以下记法：
_〔_〕 : ∀ {Γ A B C} → Γ , B , C ⊢ A → Γ ⊢ B --------- → Γ , C ⊢ A _〔_〕 {Γ} {A} {B} {C} N M = subst {Γ , B , C} {Γ , C} (exts (subst-zero M)) {A} N
代换引理陈述如下，其证明是 subst-commute 引理的一个推论。
substitution : ∀{Γ}{M : Γ , ★ , ★ ⊢ ★}{N : Γ , ★ ⊢ ★}{L : Γ ⊢ ★} → (M [ N ]) [ L ] ≡ (M 〔 L 〕) [ (N [ L ]) ] substitution{M = M}{N = N}{L = L} = sym (subst-commute{N = M}{M = N}{σ = subst-zero L})
注记
本文件中的大部分属性和证明均基于 Schafer、Tebbi 和 Smolka 的论文 Autosubst: Reasoning with de BruijnTerms and Parallel Substitution (ITP 2015)。 该论文又基于 Abadi、Cardelli、Curien 和 Levy (1991) 定义 σ-代数的论文。
Unicode
本章使用了以下 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 (C-x 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)