Bedrock使编码槽位对七种构造闭合
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图在 L 内部，每条公式都被编码为载体的元素，且每条公式都有一个键：以元数数码居前、公式编码居后的有序对。某个界处的槽位收集一条公式及其全部子公式的键，因此槽位是一棵键树，而界只是相关引理的接口参数。本章证明槽位是闭合的：凡复合公式的键位于槽位中，其直接子公式的键也位于其中；这对带子公式的七种构造子逐一成立。
抽象的闭合原理在这里落实到具体对象：由公式语法树生成的诸键满足 closedAt。这正是沿这些键递归定义图时所需的闭合前提。
语言的构造子中有七个带子公式，其余三个不带，对后者无可闭合。七条子句各是四个动作：把槽位的成员求逆回「它是谁的键」的那条公式、从子句的标签算出那条公式的构造子、把部件的键放回复合公式自己的槽位、再把它们提升到整体的槽位。
本章围绕三个数学对象展开。元数为 j 的公式 χ 的键 keyʟ χ 是数码 j 与 χ 的编码构成的有序对，而编码本身是编码模块的编码 LCode.⌜ χ ⌝。槽位 slot B φ 是由这类键组成的集合，即 φ 及其整棵子公式树的键。closedAt 则陈述：一个槽位对七个构造子闭合，即合取、析取、蕴含、两个量词与两个有界量词。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Coding.SlotClosure {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
公式即对象语言的公式，其满足在可构造结构中读取：下文的满足符号一律指那里的满足。外围层级提供键与槽位所由构成的底层元素。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; Formula; _∧̇_; _∨̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
有序对编码键，且分量可恢复，因此一个键可以拆开为元数分量与编码分量。可构造结构承载诸编码；编码模块定义公式的编码 ⌜_⌝ 与码上的配对运算；闭包模块则逐形状陈述七条闭合子句及其引入形式。
open import V.Coding {ℓ} using ( pr; pr-inj ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( module LCode; prʟ; prʟ-fst ) open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt )
满足表一章是三个核心对象的出处。它定义了公式的键 keyʟ、按构造子标签分解公式的形状引理 keyʟ-shape、挂在公式与某个界上的槽位 slot、把槽位成员求逆回其键所属公式的 slot-inv，以及关于键树的部件引理 Parts。
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Coding.SatisfactionTable {ℓ} lem using ( keyʟ; keyʟ-shape; slot; satTable; slot-inv; module Parts )
槽位成员只能在命题截断下求逆，因此每条子句都把该截断消去到一个命题。保持元数的二元情形以两个隶属命题的合取为目标；一元情形与有界情形的目标则各是一个隶属命题。
import Cubical.HITs.PropositionalTruncation as PT open import Cubical.Foundations.HLevels using ( isProp× ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
元数以数码记录，而抬升元数的构造子记录的是数码的后继；二者都取自外围的无穷集合。
open InfinitySet using ( #_; sucV )
可构造结构的载体是本章一切码、键与槽位所居的类型。
open hPropStructure 𝒮ʟ
这里的 S ^ n 表示长度为 n 的环境向量；重命名为 _⊨_ 的关系，则是在这种环境下读取限制可构造结构中的满足。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
把部件的键放回去
键树由部件引理支配。Parts.self 说公式自己的键在自己的槽位中；Parts.left、Parts.right 与 Parts.only 说复合公式的槽位包含其直接部件槽位中的键：这是沿构造子树的子树包含，由部件引理与求逆给出，从不来自界的任何序或向下的闭合。界 B 在其中只是作为接口参数传递。于是闭合子句所需做的，是把子句所读的对认作某个部件的键；下面两条引理恰完成此事。
module _ (B : S) where private Sl : ∀ {n} → Formula S n → S Sl = slot B
键的计算，就元数为 j 的公式 χ 陈述：凡第一分量为元数数码 # j、第二分量为 ⌜ χ ⌝ 的编码分量的对，都等于键 fst (keyʟ χ)。注意三个量互不相同：⌜ χ ⌝ 是公式的编码，其第一分量才是进入键的那个量，而键是数码居前的有序对。
key≡ : ∀ {j} (χ : Formula S j) (ar p : V ℓ) → # j ≡ ar → p ≡ fst LCode.⌜ χ ⌝ → pr ar p ≡ fst (keyʟ χ)
两条假设都必须用到：元数等式与编码分量等式。证明是穿过两条计算法则的短链：j 的数码的第一分量是 # j，而编码对的第一分量是第一分量的对。
key≡ {j} χ ar p qa qp = cong₂ pr (sym qa) qp ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst j)) ∙ sym (prʟ-fst (numeralL j) LCode.⌜ χ ⌝)
抬升形式对元数为 suc j 的公式 χ 陈述同一事实：此时键的第一分量是元数数码的后继，而这恰是构造子抬升元数时子句所读取的量。
keyS≡ : ∀ {j} (χ : Formula S (suc j)) (ar p : V ℓ) → # j ≡ ar → p ≡ fst LCode.⌜ χ ⌝ → pr (sucV ar) p ≡ fst (keyʟ χ)
链是同一条，只是把后继沿元数等式推过去：suc j 的数码的第一分量是 suc (# j)，而子句的抬升读法与之相合。
keyS≡ {j} χ ar p qa qp = cong₂ pr (cong sucV (sym qa)) qp ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst (suc j))) ∙ sym (prʟ-fst (numeralL (suc j)) LCode.⌜ χ ⌝)
七条子句
子句按各构造子所要求的闭合形状组织。共证明四个主体，每种形状一个：保持元数的二元构造子、保持元数的一元构造子、抬升元数的一元构造子、把项与抬升元数公式配对的二元构造子。同一主体下两条子句的不同只在构造子的标签与其交还的部件，而两者都是参数。每条子句经四个动作运行：把槽位成员求逆成一条公式、按标签读出其构造子、把部件的键放回该公式自己的槽位、再提升到整体的槽位。
module _ {n : ℕ} (φ : Formula S n) {k : ℕ} (γ : S ^ k) where private δ : S ^ (suc (suc (suc k))) δ = B ∷ satTable B φ ∷ Sl φ ∷ γ
被证明闭合的递归以固定公式 φ 的槽位为索引，其环境携带三个具名条目：界、φ 处的满足表，以及该槽位。环境的其余槽位留给具体实例。
Ci : Fin (suc (suc (suc k)))
Ci = suc (suc zero)
位置 Ci 是槽位在此环境中的索引；每条子句都恰在这个位置读取槽位。
binSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∈ Formula S m ] (Σ[ b' ∈ Formula S m ] (ψ ≡ op a' b')))
→ (∀ {m} (a' b' : Formula S m)
→ LCode.payOf (op a' b') ≡ prʟ LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
第一个主体覆盖保持元数的二元构造子，即合取、析取、蕴含的形状。其假设描述标签 k'：一条公式与该标签匹配，当且仅当它由同元数的两条公式 op a' b' 构成，且这种复合的载荷是两个部件编码构成的有序对。
→ (∀ {m} (a' b' : Formula S m) (z : V ℓ) → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩) → (∀ {m} (a' b' : Formula S m) (z : V ℓ) → ⟨ z ∈ fst (Sl b') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩) → ⟨ δ ⊨ binShapeAt Ci k' (bothSameAt Ci) ⟩
两条闭合方向分别是部件引理给出的左、右子树包含；结论即子句自身：槽位对标签 k' 以「交还两个部件的键」的形状闭合。
binSame k' op get payOp inL inR = binSameClosed-in Ci k' δ (λ c ar a b c∈ sh → PT.rec (isProp× (snd (pr (fst ar) (fst a) ∈ fst (Sl φ))) (snd (pr (fst ar) (fst b) ∈ fst (Sl φ)))) (λ { (m , ψ , (q , incl)) →
第一步对槽位成员 c 求逆。它仅仅地是某条元数为 m 的公式 ψ 的键，求逆同时返回该键属于 φ 的槽位。目标是两个隶属的合取，由 isProp× 是命题，这使截断消去合法。
let r = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh) g = get ψ (r .fst) a' = g .fst b' = g .snd .fst eψ = g .snd .snd
第二步计算构造子。形状引理以子句的形状证明把 ψ 对上标签 k'，随同匹配返回元数等式与载荷等式；分解假设进而把 ψ 写成两个直接子公式的 op a' b'。
pay = sym (prʟ-fst LCode.⌜ a' ⌝ LCode.⌜ b' ⌝) ∙ cong fst (sym (payOp a' b')) ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
第三步是关于载荷的共享计算。成员 c 是键形的对，其载荷分量记录着两个部件的编码分量；链条证明这些被记录的分量按分量分别是编码 ⌜ a' ⌝ 与 ⌜ b' ⌝：由构造子自身的载荷法则，ψ 的载荷是两个部件编码构成的对，而形状引理的载荷等式把它与从 c 读出的对连接起来。此处切莫混淆三个量：整条公式的编码 ⌜ ψ ⌝、位于其中的载荷分量，以及第一槽携带元数的最终的键。
inψ : (χ : Formula S m) → ⟨ fst (keyʟ χ) ∈ fst (Sl ψ) ⟩ → ⟨ fst (keyʟ χ) ∈ fst (Sl φ) ⟩ inψ χ h = incl (fst (keyʟ χ)) h in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩) (sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym (pr-inj pay .fst))))
第四个动作把键送回。先由辅助函数借求逆返回的包含，把任一同元数公式的键从其槽位提升到 φ 的槽位；再由形状引理的元数等式与编码单射性供给的第一分量等式喂给 key≡，把子句所读对的隶属改写为 a' 的键的隶属。
(inψ a' (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inL a' b' _ (Parts.self B keyʟ a')))) , subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩) (sym (key≡ b' (fst ar) (fst b) (r .snd .fst) (sym (pr-inj pay .snd))))
右分量以右侧闭合方向与单射性供给的第二分量等式重复同一组装，改写为含 b' 那个对的隶属。两半合拢，子句证毕。
(inψ b' (subst (λ w → ⟨ fst (keyʟ b') ∈ fst (Sl w) ⟩) (sym eψ) (inR a' b' _ (Parts.self B keyʟ b')))) }) (slot-inv B φ (fst c) c∈))
消去由求逆供给，那条包含正是从那里来的。两侧分量组装完毕，子句即告证成。
andC : ⟨ δ ⊨ binShapeAt Ci 2 (bothSameAt Ci) ⟩
andC = binSame 2 _∧̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ∧̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ∧̇ b') a' b')
合取是第一个实例：a' ∧̇ b' 的槽位包含两个合取支槽位的键。
orC : ⟨ δ ⊨ binShapeAt Ci 3 (bothSameAt Ci) ⟩
orC = binSame 3 _∨̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ∨̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ∨̇ b') a' b')
析取是形状相同的第二个实例，带自己的标签与自己的部件引理。
impC : ⟨ δ ⊨ binShapeAt Ci 4 (bothSameAt Ci) ⟩
impC = binSame 4 _⇒̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ⇒̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ⇒̇ b') a' b')
蕴含是第三个：a' ⇒̇ b' 的槽位包含前件槽位的键与后件槽位的键，子句由同样四个动作证得。
unSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∈ Formula S m ] (ψ ≡ op a'))
→ (∀ {m} (a' : Formula S m) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
辅助引理 unSame 证明了一个假想的、保持元数的一元运算所满足的相应闭合原理。本语言的十个构造子都不具有这种形状，因此 closedAt 不使用这一辅助引理。
→ (∀ {m} (a' : Formula S m) (z : V ℓ) → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩) → ⟨ δ ⊨ unShapeAt Ci k' (oneSameAt Ci) ⟩
闭合方向与结论都是单部件形状：被要求交还的只有那唯一子公式的键。
unSame k' op get payOp inA = unSameClosed-in Ci k' δ (λ c ar a c∈ sh → PT.rec (snd (pr (fst ar) (fst a) ∈ fst (Sl φ))) (λ { (m , ψ , (q , incl)) → let r = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh) g = get ψ (r .fst)
证明以一个分量运行同样的四个动作。求逆产出 ψ 及其到 φ 槽位的包含，形状引理按标签分解它，而此处的读取只涉及元数与那唯一的编码。
a' = g .fst eψ = g .snd pay = cong fst (sym (payOp a')) ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
这里的共享计算更短：op a' 的载荷就是 a' 自己的编码，故链条把成员 c 中记录的编码分量直接认同为 a' 的编码分量，无须拆分任何对。
(sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay))) (incl (fst (keyʟ a')) (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inA a' _ (Parts.self B keyʟ a')))) }) (slot-inv B φ (fst c) c∈))
第四个动作一次性组装该情形：a' 的键在自己的槽位中，inA 把它移入 op a' 的槽位，incl 提升到 φ 的槽位，key≡ 完成改写，元数等式包含在内。
unSucc : (k' : ℕ) (op : ∀ {m} → Formula S (suc m) → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∈ Formula S (suc m) ] (ψ ≡ op a'))
→ (∀ {m} (a' : Formula S (suc m)) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
→ (∀ {m} (a' : Formula S (suc m)) (z : V ℓ)
第三个主体覆盖抬升元数的一元构造子，即两个量词的形状。其假设是抬升版本：标签恰与由抬升元数公式经 op 构成的公式匹配，载荷就是该公式自己的编码，且唯一一条闭合方向把它的键送入复合槽位。
→ ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩) → ⟨ δ ⊨ unShapeAt Ci k' (oneSuccAt Ci) ⟩
读取与结论使用抬升形式：子句读取的对以元数数码的后继居首，并要求子公式的键以单部件形状交还。
unSucc k' op get payOp inA = unSuccClosed-in Ci k' δ (λ c ar a c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst a) ∈ fst (Sl φ))) (λ { (m , ψ , (q , incl)) → let r = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh) g = get ψ (r .fst)
前两个动作照旧：把成员求逆成公式，再按标签分解出唯一的、元数抬升的子公式。
a' = g .fst eψ = g .snd pay = cong fst (sym (payOp a')) ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
载荷计算把被记录的编码分量认同为子公式的编码。另一方面，形状等式给出 # m ≡ fst ar；只有 keyS≡ 对该等式施加 sucV 时，后继才被引入。
(sym (keyS≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay))) (incl (fst (keyʟ a')) (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inA a' _ (Parts.self B keyʟ a')))) }) (slot-inv B φ (fst c) c∈))
改写经由 keyS≡ 完成：它对 # m ≡ fst ar 施加 sucV，再与编码分量等式合并，从而把子句所读的对认同为 a' 的键。
binSucc : (k' : ℕ)
→ (op : ∀ {m} → Term S m → Formula S (suc m) → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ t ∈ Term S m ] (Σ[ a' ∈ Formula S (suc m) ] (ψ ≡ op t a')))
→ (∀ {m} (t : Term S m) (a' : Formula S (suc m))
第四个主体覆盖有界量词，其构造子把一个项与一个元数抬升的公式配对。这种复合的载荷按次序编码项与子公式，而只有子公式本身是公式，故被要求交回的只有它的键。
→ LCode.payOf (op t a') ≡ prʟ LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝) → (∀ {m} (t : Term S m) (a' : Formula S (suc m)) (z : V ℓ) → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op t a')) ⟩) → ⟨ δ ⊨ binShapeAt Ci k' (succSndAt Ci) ⟩
结论是第二分量形状：子句读取的对以抬升的元数居前、公式的编码分量居后，并要求交回子公式的键。
binSucc k' op get payOp inA = binSuccClosed-in Ci k' δ (λ c ar a b c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst b) ∈ fst (Sl φ))) (λ { (m , ψ , (q , incl)) → let r = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh) g = get ψ (r .fst)
成员 c 是键形的对，其载荷携带两个分量：居前的项 t 的编码分量，与居后的子公式 a' 的编码分量。子句读取的是抬升元数连同第二分量。
t = g .fst a' = g .snd .fst eψ = g .snd .snd pay = sym (prʟ-fst LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝) ∙ cong fst (sym (payOp t a'))
共享计算把成员中记录的载荷按分量认同为 ⌜ t ⌝ᵗ 与 ⌜ a' ⌝ 的编码对。改写所消耗的是由编码单射性供给的第二分量等式；项乘坐在第一分量里，随后退出。
∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩) (sym (keyS≡ a' (fst ar) (fst b) (r .snd .fst) (sym (pr-inj pay .snd)))) (incl (fst (keyʟ a'))
keyS≡ 的改写使用元数等式与第二分量等式，落定为子句所读对的隶属。第四个动作随后把 a' 的键经它自己的槽位与闭合方向提升到 φ 的槽位，而求逆供给那条包含。
(subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inA t a' _ (Parts.self B keyʟ a')))) }) (slot-inv B φ (fst c) c∈))
两个量词例示第三个主体。各自供给标签、分解、定义性成立的载荷等式，以及唯一一条闭合方向：∃̇ a' 的槽位包含 a' 槽位的键，全称量词亦然。
exC : ⟨ δ ⊨ unShapeAt Ci 6 (oneSuccAt Ci) ⟩
exC = unSucc 6 ∃̇_ (λ _ m → m) (λ _ → refl)
(λ a' → Parts.only B keyʟ (∃̇ a') a')
全称量词是同一主体的第二个实例，带标签七与自己的部件引理。
allC : ⟨ δ ⊨ unShapeAt Ci 7 (oneSuccAt Ci) ⟩
allC = unSucc 7 ∀̇_ (λ _ m → m) (λ _ → refl)
(λ a' → Parts.only B keyʟ (∀̇ a') a')
两个有界量词以标签八与九例示第四个主体：∀̇∈ t a' 的槽位包含 a' 槽位的键，存在有界量词亦然。
allInC : ⟨ δ ⊨ binShapeAt Ci 8 (succSndAt Ci) ⟩
allInC = binSucc 8 ∀̇∈ (λ _ m → m) (λ _ _ → refl)
(λ t a' → Parts.only B keyʟ (∀̇∈ t a') a')
存在有界量词是七条子句中的最后一条。
exInC : ⟨ δ ⊨ binShapeAt Ci 9 (succSndAt Ci) ⟩
exInC = binSucc 9 ∃̇∈ (λ _ m → m) (λ _ _ → refl)
(λ t a' → Parts.only B keyʟ (∃̇∈ t a') a')
七条子句组装成闭合陈述 closedAt：φ 在该界处的槽位对每个带子公式的构造子闭合。这就消解了对编码的递归对其索引集陈述的假设；也正因如此，这样的递归才能在每个复合码处求助于直接子公式键处记录的取值。本章的三个对象各尽其用：键识别了子句所读的对，槽位树供给了闭合方向，closedAt 汇集了结果。
slotClosed : ⟨ δ ⊨ closedAt Ci ⟩
slotClosed = andC , (orC , (impC
, (exC , (allC , (allInC , exInC)))))