Syntax as sets

迄今为止的一切都把公式留在它们所谈论的集合之外：公式是宿主层的数据，集合是结构的点，满足关系是二者之间的桥。第四部需要相反的方向。要在模型内部说某个集合可定义，或者用模型看得见的序去比较两条公式，公式自身就必须是集合。本章把它们注入进去。

这套编码刻意平淡。没有算术化，没有哥德尔编号，没有递归花招：公式的码是一个带标签的对，标签是构造子的序号，载荷是各部分的码。递归留在它该在的地方，即宿主的归纳类型 Formula 上，而码是一种边界格式。唯一的优雅之处是：集合常量本来就是集合，故常量即自身的码。

本章取作参数的，恰是编码所需的东西：一个带单射性的配对运算，以及自然数的一个单射。关于结构的其余一切都无关紧要，故本章是泛型的，层级稍后才来实例化它。

关于最要紧的那件交付物说一句。除码函数之外，还有一个归纳关系 Codes，读作「这个集合编码那条公式」，其构造子在子码的位置上携带子推导。关于码的推理走这个关系，而不走码值之间的等式，理由是实际的：码值是深层嵌套的对，而两个码值之间的等式会迫使类型检查器把两边都展开。这个关系把形状变成构造子索引，于是匹配是句法的，而码值从不被归一化。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure )

module FOL.Coding {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ))
  (pr       : ZFStructure.S 𝒮 → ZFStructure.S 𝒮 → ZFStructure.S 𝒮)
  (pr-inj   : ∀ {a b c d} → pr a b ≡ pr c d → (a ≡ c) × (b ≡ d))
  (encℕ     : ℕ → ZFStructure.S 𝒮)
  (encℕ-inj : ∀ {j k} → encℕ j ≡ encℕ k → j ≡ k)
  where

open ZFStructure 𝒮 using ( S )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

import Cubical.Data.Empty as Empty
open import Cubical.Data.Nat using ( znots; snotz )
open import Cubical.Data.FinData using ( toℕ; inj-toℕ )

带标签的对

唯一的构造：构造子序号与载荷配成对。单射性直接来自那两个参数，而冲突模式把「两个不同构造子相比较」时反复出现的情形打包起来。

mkTag : ℕ → S → S
mkTag k x = pr (encℕ k) x

mkTag-inj : ∀ {j k x y} → mkTag j x ≡ mkTag k y → (j ≡ k) × (x ≡ y)
mkTag-inj p = encℕ-inj (pr-inj p .fst) , pr-inj p .snd

clash : ∀ {j k x y} {A : Type ℓ} → (j ≡ k → Empty.⊥) → mkTag j x ≡ mkTag k y → A
clash ne p = Empty.rec (ne (mkTag-inj p .fst))

码

先看项，承诺的那点优雅在此出现：集合常量无须编码，因为它本来就是集合，只有变元的序号要被注入。项的分隔足够清楚，其单射性立得。

⌜_⌝ᵗ : ∀ {n} → Term S n → S
⌜ con x ⌝ᵗ = mkTag 0 x
⌜ var i ⌝ᵗ = mkTag 1 (encℕ (toℕ i))

⌜⌝ᵗ-inj : ∀ {n} (t u : Term S n) → ⌜ t ⌝ᵗ ≡ ⌜ u ⌝ᵗ → t ≡ u
⌜⌝ᵗ-inj (con x) (con y) p = cong con (mkTag-inj p .snd)
⌜⌝ᵗ-inj (con x) (var j) p = clash znots p
⌜⌝ᵗ-inj (var i) (con y) p = clash snotz p
⌜⌝ᵗ-inj (var i) (var j) p = cong var (inj-toℕ (encℕ-inj (mkTag-inj p .snd)))

然后是公式：十二个构造子，十二个标签。二元构造子把两个子码配成对，一元的直接取子码，而两个常量取一个虚载荷，因为标签已经把它们区分开了。

⌜_⌝ : ∀ {n} → Formula S n → S
⌜ t ∈̇ u ⌝   = mkTag 0  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ t ≐ u ⌝   = mkTag 1  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ φ ∧̇ ψ ⌝   = mkTag 2  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ φ ∨̇ ψ ⌝   = mkTag 3  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ φ ⇒̇ ψ ⌝   = mkTag 4  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ ¬̇ φ ⌝     = mkTag 5  ⌜ φ ⌝
⌜ ⊤̇ ⌝       = mkTag 6  (encℕ 0)
⌜ ⊥̇ ⌝       = mkTag 7  (encℕ 0)
⌜ ∃̇ φ ⌝     = mkTag 8  ⌜ φ ⌝
⌜ ∀̇ φ ⌝     = mkTag 9  ⌜ φ ⌝
⌜ ∀̇∈ t φ ⌝  = mkTag 10 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)
⌜ ∃̇∈ t φ ⌝  = mkTag 11 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)

编码关系

然后是本章真正的接口。Codes s φ 说集合 s 编码公式 φ，是一个索引归纳族，其构造子恰在码函数作递归调用之处携带子推导。它与码函数携带同样的信息，只是呈现方式使得证明可以在编码的形状上匹配，而不必对码作计算。

data CodesT {n : ℕ} : S → Term S n → Type ℓ where
  c-con : (x : S)     → CodesT (mkTag 0 x) (con x)
  c-var : (i : Fin n) → CodesT (mkTag 1 (encℕ (toℕ i))) (var i)

data Codes : {n : ℕ} → S → Formula S n → Type ℓ where
  c-∈  : ∀ {n s s'} {t u : Term S n}
       → CodesT s t → CodesT s' u → Codes (mkTag 0 (pr s s')) (t ∈̇ u)
  c-≐  : ∀ {n s s'} {t u : Term S n}
       → CodesT s t → CodesT s' u → Codes (mkTag 1 (pr s s')) (t ≐ u)
  c-∧  : ∀ {n s s'} {φ ψ : Formula S n}
       → Codes s φ → Codes s' ψ → Codes (mkTag 2 (pr s s')) (φ ∧̇ ψ)
  c-∨  : ∀ {n s s'} {φ ψ : Formula S n}
       → Codes s φ → Codes s' ψ → Codes (mkTag 3 (pr s s')) (φ ∨̇ ψ)
  c-⇒  : ∀ {n s s'} {φ ψ : Formula S n}
       → Codes s φ → Codes s' ψ → Codes (mkTag 4 (pr s s')) (φ ⇒̇ ψ)
  c-¬  : ∀ {n s} {φ : Formula S n}
       → Codes s φ → Codes (mkTag 5 s) (¬̇ φ)
  c-⊤  : ∀ {n} → Codes {n} (mkTag 6 (encℕ 0)) ⊤̇
  c-⊥  : ∀ {n} → Codes {n} (mkTag 7 (encℕ 0)) ⊥̇
  c-∃  : ∀ {n s} {φ : Formula S (suc n)}
       → Codes s φ → Codes (mkTag 8 s) (∃̇ φ)
  c-∀  : ∀ {n s} {φ : Formula S (suc n)}
       → Codes s φ → Codes (mkTag 9 s) (∀̇ φ)
  c-∀∈ : ∀ {n s s'} {t : Term S n} {φ : Formula S (suc n)}
       → CodesT s t → Codes s' φ → Codes (mkTag 10 (pr s s')) (∀̇∈ t φ)
  c-∃∈ : ∀ {n s s'} {t : Term S n} {φ : Formula S (suc n)}
       → CodesT s t → Codes s' φ → Codes (mkTag 11 (pr s s')) (∃̇∈ t φ)

两个事实把关系与函数系在一起。每条公式都被它自己的码所编码，故该关系在该有的地方都有居民；而公式的任何一个码都就是那条公式的码，故该关系并不比函数多出什么。两者都是一次结构递归，而后者是后续诸章倚重的：它把推导 (匹配起来廉价) 换成等式 (归一化起来昂贵)，恰在等式终于被需要的那一点上。

codesT-complete : ∀ {n} (t : Term S n) → CodesT ⌜ t ⌝ᵗ t
codesT-complete (con x) = c-con x
codesT-complete (var i) = c-var i

codes-complete : ∀ {n} (φ : Formula S n) → Codes ⌜ φ ⌝ φ
codes-complete (t ∈̇ u)  = c-∈  (codesT-complete t) (codesT-complete u)
codes-complete (t ≐ u)  = c-≐  (codesT-complete t) (codesT-complete u)
codes-complete (φ ∧̇ ψ)  = c-∧  (codes-complete φ)  (codes-complete ψ)
codes-complete (φ ∨̇ ψ)  = c-∨  (codes-complete φ)  (codes-complete ψ)
codes-complete (φ ⇒̇ ψ)  = c-⇒  (codes-complete φ)  (codes-complete ψ)
codes-complete (¬̇ φ)    = c-¬  (codes-complete φ)
codes-complete ⊤̇        = c-⊤
codes-complete ⊥̇        = c-⊥
codes-complete (∃̇ φ)    = c-∃  (codes-complete φ)
codes-complete (∀̇ φ)    = c-∀  (codes-complete φ)
codes-complete (∀̇∈ t φ) = c-∀∈ (codesT-complete t) (codes-complete φ)
codes-complete (∃̇∈ t φ) = c-∃∈ (codesT-complete t) (codes-complete φ)

codesT-canon : ∀ {n s} {t : Term S n} → CodesT s t → s ≡ ⌜ t ⌝ᵗ
codesT-canon (c-con x) = refl
codesT-canon (c-var i) = refl

codes-canon : ∀ {n s} {φ : Formula S n} → Codes s φ → s ≡ ⌜ φ ⌝
codes-canon (c-∈ ct cu) =
  cong (mkTag 0)  (cong₂ pr (codesT-canon ct) (codesT-canon cu))
codes-canon (c-≐ ct cu) =
  cong (mkTag 1)  (cong₂ pr (codesT-canon ct) (codesT-canon cu))
codes-canon (c-∧ c d)   = cong (mkTag 2)  (cong₂ pr (codes-canon c) (codes-canon d))
codes-canon (c-∨ c d)   = cong (mkTag 3)  (cong₂ pr (codes-canon c) (codes-canon d))
codes-canon (c-⇒ c d)   = cong (mkTag 4)  (cong₂ pr (codes-canon c) (codes-canon d))
codes-canon (c-¬ c)     = cong (mkTag 5)  (codes-canon c)
codes-canon c-⊤         = refl
codes-canon c-⊥         = refl
codes-canon (c-∃ c)     = cong (mkTag 8)  (codes-canon c)
codes-canon (c-∀ c)     = cong (mkTag 9)  (codes-canon c)
codes-canon (c-∀∈ ct c) =
  cong (mkTag 10) (cong₂ pr (codesT-canon ct) (codes-canon c))
codes-canon (c-∃∈ ct c) =
  cong (mkTag 11) (cong₂ pr (codesT-canon ct) (codes-canon c))

典范性已经给出了「码决定公式」通常要陈述的内容：同一个码上的两份推导，迫使两条公式拥有相同的码；而一个手里握着推导、据以从码还原公式的论证，不再要求任何更多的东西。它们是绝大多数，而上面那个关系正是它们所围绕设计的接口。

但不是全部。有一个消费方要的是那条等式本身，理由是任何关系都答不了的，而本章最后一节把它证出来。当初把它挡在外面的那条反对意见是一个成本估计，而成本最终并不是那个估计所设想的样子。

小结

公式如今是集合了：⌜_⌝ 把构造子序号贴在各部分的码上，而常量编码自身。下游的接口是关系 Codes，它完备 (codes-complete) 且典范 (codes-canon)，使码值不出现在类型检查器必须归一化的等式里。一切都对结构泛型，只需一个单射的配对与自然数的一个单射；层级把二者都供上。

码决定公式

同一元数、同一码的两条公式是同一条公式。这条陈述曾被丢掉，理由是它的自然证明是一张十二乘十二的网格，其中一百三十二条子句不含数学，而每个消费方当初都是围绕 Codes 关系设计的。如今来了一个要等式而非要关系的消费方，而它要的理由是任何关系都答不了的：递归的表是一个集合，故若两处不同子公式共用一个码，那张表就真的多值，垮掉的将是它的存在性，而不只是它的证明。

那张网格不必写。构造子可从标签还原，而标签是一个数，故一条公式的构造子是什么可以从标签算出来：一个以标签为索引的类型族，说出「带那个标签」长什么样；一个函数把它造出来；而配对的单射性所给出的那条标签等式把后者搬到前者上。两者各十二条子句，再加十二条作情形分析，取代一百四十四条。

这与可构造性那一章「把十二个构造子对上八项要求」所用的是同一个动作，而它值得一般地说一次：当一次情形分析由两样东西索引、而某个标签已经把它们关联起来时，就从标签算出一侧，不要两侧都匹配。

tagOf : ∀ {n} → Formula S n → ℕ
tagOf (t ∈̇ u)  = 0
tagOf (t ≐ u)  = 1
tagOf (a ∧̇ b)  = 2
tagOf (a ∨̇ b)  = 3
tagOf (a ⇒̇ b)  = 4
tagOf (¬̇ a)    = 5
tagOf ⊤̇        = 6
tagOf ⊥̇        = 7
tagOf (∃̇ a)    = 8
tagOf (∀̇ a)    = 9
tagOf (∀̇∈ t a) = 10
tagOf (∃̇∈ t a) = 11

payOf : ∀ {n} → Formula S n → S
payOf (t ∈̇ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (t ≐ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (a ∧̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (a ∨̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (a ⇒̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (¬̇ a)    = ⌜ a ⌝
payOf ⊤̇        = encℕ 0
payOf ⊥̇        = encℕ 0
payOf (∃̇ a)    = ⌜ a ⌝
payOf (∀̇ a)    = ⌜ a ⌝
payOf (∀̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝
payOf (∃̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝

shape : ∀ {n} (φ : Formula S n) → ⌜ φ ⌝ ≡ mkTag (tagOf φ) (payOf φ)
shape (t ∈̇ u)  = refl
shape (t ≐ u)  = refl
shape (a ∧̇ b)  = refl
shape (a ∨̇ b)  = refl
shape (a ⇒̇ b)  = refl
shape (¬̇ a)    = refl
shape ⊤̇        = refl
shape ⊥̇        = refl
shape (∃̇ a)    = refl
shape (∀̇ a)    = refl
shape (∀̇∈ t a) = refl
shape (∃̇∈ t a) = refl

Match : ∀ {n} → ℕ → Formula S n → Type ℓ
Match {n} 0  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ∈̇ u)))
Match {n} 1  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ≐ u)))
Match {n} 2  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∧̇ b)))
Match {n} 3  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∨̇ b)))
Match {n} 4  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ⇒̇ b)))
Match {n} 5  φ = Σ[ a ∈ Formula S n ] (φ ≡ (¬̇ a))
Match     6  φ = φ ≡ ⊤̇
Match     7  φ = φ ≡ ⊥̇
Match {n} 8  φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∃̇ a))
Match {n} 9  φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∀̇ a))
Match {n} 10 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∀̇∈ t a))
Match {n} 11 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∃̇∈ t a))
Match     _  _ = Empty.⊥*

matches : ∀ {n} (φ : Formula S n) → Match (tagOf φ) φ
matches (t ∈̇ u)  = t , (u , refl)
matches (t ≐ u)  = t , (u , refl)
matches (a ∧̇ b)  = a , (b , refl)
matches (a ∨̇ b)  = a , (b , refl)
matches (a ⇒̇ b)  = a , (b , refl)
matches (¬̇ a)    = a , refl
matches ⊤̇        = refl
matches ⊥̇        = refl
matches (∃̇ a)    = a , refl
matches (∀̇ a)    = a , refl
matches (∀̇∈ t a) = t , (a , refl)
matches (∃̇∈ t a) = t , (a , refl)

⌜⌝-inj : ∀ {n} (φ ψ : Formula S n) → ⌜ φ ⌝ ≡ ⌜ ψ ⌝ → φ ≡ ψ

private
  go : ∀ {n} (φ ψ : Formula S n) → Match (tagOf φ) ψ → payOf φ ≡ payOf ψ → φ ≡ ψ
  go (t ∈̇ u) ψ (t' , (u' , q)) p =
    cong₂ _∈̇_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (t ≐ u) ψ (t' , (u' , q)) p =
    cong₂ _≐_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ∧̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∧̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ∨̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∨̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ⇒̇ b) ψ (a' , (b' , q)) p =
    cong₂ _⇒̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (¬̇ a) ψ (a' , q) p = cong ¬̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go ⊤̇ ψ q p = sym q
  go ⊥̇ ψ q p = sym q
  go (∃̇ a) ψ (a' , q) p = cong ∃̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇ a) ψ (a' , q) p = cong ∀̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∀̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (∃̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∃̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q

⌜⌝-inj φ ψ e = go φ ψ
  (subst (λ k → Match k ψ) (sym (tp .fst)) (matches ψ)) (tp .snd)
  where
  tp = mkTag-inj (sym (shape φ) ∙ e ∙ shape ψ)