逐次出现地处理常元

参数抽象需要公式常元的有限列表，但不能假设常元域上的相等可判定。因此本章逐次出现地计数并枚举常元，保留重复项，再建立把替代变量放在已有自由变量之后所需的指标算术。

公式的常元组成一列有序的出现。本章计数并枚举这些出现，给出抽象所需的序号算术，并处理该列为空的边界情形。

参数抽象把一条提及常元的公式改写为一条元数更高的无参公式，同时给出常元的列表，让新的变量逐个对应这些常元。构造需要这个列表是有限的，但不能假设常元域上的相等可判定，因此不能合并或去重条目。同一常元的两次出现因此保持为两个独立的位置，日后各自获得自己的替代变量。工作分三步：计数出现，按序枚举出现，再建立把新变量放在已有自由变量之后的序号算术。

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

module FOL.Manipulation.ConstantOccurrences where

open import Base.Prelude
open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

具体地说，公式的常元被读作一列有序的出现：常元每出现一次，无论在词项的何处或在任何量词之下，都占据列表的下一个位置。计数与枚举因此相伴而行。计数是一个自然数，记录出现了多少次；枚举是一个长度恰为该数的向量，按公式提及常元的次序存放它们。由于重复被保留而不被消解，全程不需要对常元作任何比较。本章最后处理出现列表为空的边界情形，证明这样的公式可以活在空的常元字母表上。

open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
open import Cubical.Data.Nat using ( _+_; snotz )
open import Cubical.Data.Vec using ( _++_; map )
import Cubical.Data.Empty as Empty

逐次出现地计数

countTm 与 countFo 逐次计数常元的每次出现，而 constantsTm 与 constantsFo 按相同顺序列出这些常元。因此，同一常元的重复出现仍占据不同位置。

本章的设计要点在此定下，先于任何语法上的挪动。一条公式的常元按出现计数，而非按取值：带 k 次常元出现的公式给出长度为 k 的向量，同一常元的两次出现就是该向量的两个条目，两处写的是同一个集合。

若读者期待的是公式所提及的常元之集，他会寻找一个可判定的相等关系，把同一常元的两次出现认作一次，却找不到这样的相等。本来就没有可找的：常元域是任意类型，其相等未必可判定；本书也不对预期使用的集合载体假设可判定相等。逐次出现地计数，正是使整章避开这一要求的关键。代价是抽象所得的元数高于严格必要的元数，多出的部分对应于同一取值被当作两个不同变量重复处理；下游分辨不出其中差别：参数向量仍是参数向量。

计数是对十个构造子的一次结构递归，其输入是词项各部分的计数：常元算作一次出现，变量算作零次。复合构造子的计数取其两部分之和，左部在先。

一个小例子定下约定。在 ∀̇∈ (con a) ((con a) ∈̇ (var f0)) 中，受限量词携带词项 con a，原子的左边重复 con a，右边是变元：共有两次出现，都是同一个常元，故计数必须是二，且按自左向右的阅读顺序。先数词项。常元 con c 是一次出现，变元 var i 是零次；词项只有这两种形式，且不检查自由变元的序号。两条原子关系再把各自两个词项的计数相加，左边的写在前面，例子的总和因此按阅读顺序得出。枚举将返回 [a, a]，即同一个常元被列出两次。

countTm : ∀ {ℓc} {K : Type ℓc} {n} → Term K n → ℕ
countTm (con c) = suc zero
countTm (var i) = zero

countFo : ∀ {ℓc} {K : Type ℓc} {n} → Formula K n → ℕ
countFo (t ∈̇ u)  = countTm t + countTm u

命题构造子按其作用分类，而不必逐个细读。组合分支的一类，即合取、析取与蕴涵，各把两个子公式的计数相加，仍是左边在先；假式不携带任何词项，贡献为零。于是整条公式的计数恰是对那些持有词项的节点求和：在二元节点处两个分支的计数相加，此外数字不再变动。

countFo (t ≐ u)  = countTm t + countTm u
countFo (φ ∧̇ ψ)  = countFo φ + countFo ψ
countFo (φ ∨̇ ψ)  = countFo φ + countFo ψ
countFo (φ ⇒̇ ψ)  = countFo φ + countFo ψ
countFo ⊥̇        = zero

量词按是否携带词项而分。无界的 ∃̇ 与 ∀̇ 约束一个变元而不含常元，因此直接沿用主体的计数；约束变元不产生出现。有界的 ∀̇∈ 与 ∃̇∈ 则携带一个词项，如上例所示，其计数是在主体计数之前加上 countTm t。这保持了自左向右的阅读顺序，后面的枚举将逐词项地复现这一顺序。

countFo (∃̇ φ)    = countFo φ
countFo (∀̇ φ)    = countFo φ
countFo (∀̇∈ t φ) = countTm t + countFo φ
countFo (∃̇∈ t φ) = countTm t + countFo φ

收集是对同一结构进行的第二次递归，而且必须与计数分成两次，不能在一次递归中同时给出两个结果：返回向量的长度恰是第一次递归算出的数，因此必须先算出计数，收集函数的返回类型才得以确定。每条子句都对应上面的计数子句，只把 + 换成 ++；于是常元按照公式提及它们的次序，自左向右依次排列。

收集与计数由一条不变式绑定：这里的递归是依赖的，结果类型 Vec K (countTm t) 要求返回向量的长度按定义就是该词项自身的出现计数，且条目按自左向右的次序排列。常元给出单条目向量 c ∷ []，变元给出空向量；公式情形拼接两个词项向量，左边的在先。

constantsTm : ∀ {ℓc} {K : Type ℓc} {n} (t : Term K n) → Vec K (countTm t)
constantsTm (con c) = c ∷ []
constantsTm (var i) = []

constantsFo : ∀ {ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Vec K (countFo φ)
constantsFo (t ∈̇ u)  = constantsTm t ++ constantsTm u

同一条不变式贯穿命题构造子：每条二元公式恰在计数把两个加数相加的节点处拼接两个子列表，假式在计数贡献零之处贡献空向量。由于拼接逐节点地取代加法，结果的长度按定义计算就是计数，无需另行记账。

constantsFo (t ≐ u)  = constantsTm t ++ constantsTm u
constantsFo (φ ∧̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ∨̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ⇒̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo ⊥̇        = []

量词子句结束递归并确定次序：无界量词直接传递主体的列表，受限量词把词项的列表接在主体列表之前，与计数所用的阅读顺序一致。对上面的例子，结果是 [a, a]，其长度就是该公式的计数，而这个向量恰是参数抽象将要消费的输入。

constantsFo (∃̇ φ)    = constantsFo φ
constantsFo (∀̇ φ)    = constantsFo φ
constantsFo (∀̇∈ t φ) = constantsTm t ++ constantsFo φ
constantsFo (∃̇∈ t φ) = constantsTm t ++ constantsFo φ

安置新的参数变元

参数抽象在元数为 n 的环境后增加 k 个位置，分别对应常元的出现。原有变元占据前 n 个位置，参数占据随后的 k 个位置。两个索引嵌入及其查值定律保证，环境连接后，两部分都保持原有的值。

两件安置装置承担序号算术，各占三行。padRight b 读 a + b 中头 a 个位的序号，padLeft a 读末 b 个位的序号。二者互为镜像，参数的不对称正是递归的不对称：padRight 对序号递归，padLeft 对它跨过的位数递归。

一个数值例子说明嵌入必须做什么：取 a = 2、b = 3，五元环境分成前两元 (存放原有变元) 与后三元 (存放参数)。padRight 把 Fin a 嵌入 Fin (a + b)，方式是让序号保持原位，因为拼接的前 a 个位正是原来的 a 个位：前一半的序号在五个位置中位置不变。界 b 是隐式的且全程固定，故每个递归步骤只是给序号再包一层 suc：零仍是零，suc i 变为 suc (padRight b i)。

padRight : ∀ {a} b → Fin a → Fin (a + b)
padRight b zero    = zero
padRight b (suc i) = suc (padRight b i)

padLeft : ∀ a {b} → Fin b → Fin (a + b)
padLeft zero    j = j

padLeft 把 Fin b 嵌入 Fin (a + b)，方式是把序号移过前 a 个位，因此这里显式的界是 a，递归也在它上进行。在例子中，padLeft 2 把参数序号 0 送到位置 2，即原有变元之后的第一个位置。当 a 为零时，拼接就是后半段，j 已指向正确位置；每多前缀一个位，就多包一层 suc，从而把后半段放在前半段之后。

padLeft (suc a) j = suc (padLeft a j)

每件安置装置各有一条定律，而这条定律正是环境所遵守的那一条：在拼接向量中查一个被安置过的序号，就是在对应的那一半中查原来的序号。与它们并列的还有第三条同形的定律，即查值可以穿过 map；正是这条定律使常元的解释得以穿过收集出的出现向量。三条定律都对向量与序号同时作结构递归，每个基例或步例都化归为 refl 或归纳假设，不涉及任何其他等价装置。

要记住的图景是一个写作拼接 p ++ q 的环境：p 存放原有自由变元的值，q 存放分配给常元出现的值。两个嵌入回答的是同一个问题：在接合后的环境中查值，是否仍读到接合前读到的值。对带有指向前一半的序号 i : Fin a 的原有变元，第一条定律陈述 lookup (padRight b i) (p ++ q) ≡ lookup i p：padRight b i 在拼接中指名同一个位置，因此读到的条目不变。

lookup-padRight : ∀ {ℓa} {A : Type ℓa} {a b} (p : Vec A a) (q : Vec A b) (i : Fin a)
                → lookup (padRight b i) (p ++ q) ≡ lookup i p
lookup-padRight []      q ()
lookup-padRight (x ∷ p) q zero    = refl
lookup-padRight (x ∷ p) q (suc i) = lookup-padRight p q i

第二条定律处理带有指向后一半的自然序号 j : Fin b 的参数：lookup (padLeft a j) (p ++ q) ≡ lookup j q，即被移动后的序号读到的，恰是 lookup j q 在 q 中读到的值。两条定律合起来说的正是环境必须说的：拼接环境的每一半都保持自己单独存在时的值。两个证明都沿向量与序号一同下降，每步剥去一个条目和一层构造子，直到抵达基例。

lookup-padLeft : ∀ {ℓa} {A : Type ℓa} a {b} (p : Vec A a) (q : Vec A b) (j : Fin b)
               → lookup (padLeft a j) (p ++ q) ≡ lookup j q
lookup-padLeft zero    []      q j = refl
lookup-padLeft (suc a) (x ∷ p) q j = lookup-padLeft a p q j

lookup-map : ∀ {ℓa ℓb} {A : Type ℓa} {B : Type ℓb} {n}

第三条定律关于被改名的向量：lookup j (map f v) ≡ f (lookup j v)。读取被映射的向量再施加 f，与先施加 f 再读取一致。在参数抽象中，正是这条定律让常元的解释随出现一同前进：若 f 给每个常元指派其替代变量应取的值，v 是从公式收集出的出现向量，则查 map f v 的任一位置，都计算出该位置上常元的 f 像。证明与两条安置定律同形，沿向量与序号一同下降。

             (f : A → B) (v : Vec A n) (j : Fin n)
           → lookup j (map f v) ≡ f (lookup j v)
lookup-map f []      ()
lookup-map f (x ∷ v) zero    = refl
lookup-map f (x ∷ v) (suc j) = lookup-map f v j

无常元出现的公式

计数与收集装置为每条公式附上一份有限的出现数据。本节发展这一接口的边界情形：当计数为零时，公式中任何地方都不出现常元，于是它所含的每个词项都是变元。这样的公式可以在空的常元字母表 ⊥* 上表达，也就是写成同一元数的无参公式。模块 ZeroOccurrences 以原常元域 K 为参数，其中首先给出把 countFo φ ≡ 0 的证明按和式两侧拆开的算术，然后是两个映射：消去常元域的 erase，以及证明映回 K 后恰好恢复原公式的 erase-inv。

出现接口的边界问题是：计数为零对语法强制了什么？本节对任意常元类型 K 回答这一问题，输入是一条公式 φ 连同其出现计数为零的证明。由于答案不得依赖 K 究竟是哪个类型，尤其不得使用 K 上的可判定相等，这一论证只发展一次，对层级 ℓ 上所有这样的 K 一致成立。

module ZeroOccurrences {ℓ : Level} (K : Type ℓ) where

本节把边界情形形式化。输入是一条公式 φ 连同证明 p : countFo φ ≡ 0；构造先从 p 为每个子词项、子公式提取其自身计数为零的证明，并在此基础上在空常元字母表上重建同一语法。映射 eraseTm 与 erase 从 K 走向 ⊥*；映射 eraseTm-inv 与 erase-inv 则证明，沿 Empty.rec*(从空类型读出一个定元的消去子) 改名后，作为路径返回原来的词项或公式。二者合起来说：在 K 上，无常元出现的公式恰是无参公式的像，且对 K 无任何可判定性假设。

第一个要素是算术的：和为零，仅当两个加数都为零。由于复合公式的计数总是各部分计数之和，countFo φ ≡ 0 的证明必须拆分为各部分计数为零的证明，plus-zero-l 与 plus-zero-r 执行的正是这一拆分，从 a + b ≡ 0 分别提取 a ≡ 0 与 b ≡ 0。拆分得以进行，是因为非零的左加数按定义计算为后继：suc a + b 就是 suc (a + b)，引理 snotz 把后继等于 0 的等式变成矛盾，从矛盾可得任意结论。当左加数为 zero 时，zero + b 计算为 b，两个命题都是立即的。

  plus-zero-l : {a b : ℕ} → a + b ≡  → a ≡ 
  plus-zero-l {zero} {b} p = refl
  plus-zero-l {suc a} {b} p = Empty.rec (snotz p)

  plus-zero-r : {a b : ℕ} → a + b ≡  → b ≡ 
  plus-zero-r {zero} {b} p = p

计数为零是关于语法的一条定理：常元构造子不可能出现。对词项而言，这已是直接的陈述。词项的计数为零恰当它是变元，eraseTm 把这一点变成一个映射：从 t 连同 p : countTm t ≡ 0 出发，得到空字母表 ⊥* 上同一元数 n 的词项。常元情形被排除，因为 countTm (con a) 计算为 1，使 p 成为 suc _ ≡ 0 的证明；这一矛盾给出所需的词项。变元情形保留序号，给出 var i：自由变元原样不动，空字母表只禁绝常元。

  plus-zero-r {suc a} {b} p = Empty.rec (snotz p)

  eraseTm : {n : ℕ} (t : Term K n) → countTm t ≡  → Term (⊥* {ℓ}) n
  eraseTm (con a) p = Empty.rec {A = Term (⊥* {ℓ}) _} (snotz p)
  eraseTm (var i) _ = var i

  erase : {n : ℕ} (φ : Formula K n) → countFo φ ≡  → Formula (⊥* {ℓ}) n

同一重建贯穿整个 erase，原子关系以其最简形式展示该模式。取 t ∈̇ u：其计数是 countTm t + countTm u，于是 plus-zero-l 与 plus-zero-r 把 p 拆成 t 与 u 各自计数为零的证明，erase 对两侧各自递归，在 ⊥* 上重建该关系。相等原子 ≐ 的处理完全相同。全程中自由变元的元数 n 从未被改动：消去常元只改变常元域，不改变自由变元的结构。

  erase (t ∈̇ u) p = eraseTm t (plus-zero-l p) ∈̇ eraseTm u (plus-zero-r p)
  erase (t ≐ u) p = eraseTm t (plus-zero-l p) ≐ eraseTm u (plus-zero-r p)
  erase (φ ∧̇ ψ) p = erase φ (plus-zero-l p) ∧̇ erase ψ (plus-zero-r p)
  erase (φ ∨̇ ψ) p = erase φ (plus-zero-l p) ∨̇ erase ψ (plus-zero-r p)
  erase (φ ⇒̇ ψ) p = erase φ (plus-zero-l p) ⇒̇ erase ψ (plus-zero-r p)

一个量词情形展示了约束如何与计数互动。对无界量词如 ∃̇ φ，整体的计数等于主体的计数，于是同一个 p 直接带入递归调用，结果就是把 ∃̇ 施于消去后的主体；假式没有部分也没有出现，消去后仍是自身。有界量词 ∀̇∈ 与 ∃̇∈ 组合一个词项与一个公式，这里像原子情形一样拆分和式：词项经 eraseTm，主体经递归的 erase。每条子句都保持原公式的形状，只替换其中的常元。

  erase ⊥̇ _ = ⊥̇
  erase (∃̇ φ) p = ∃̇ erase φ p
  erase (∀̇ φ) p = ∀̇ erase φ p
  erase (∀̇∈ t φ) p = ∀̇∈ (eraseTm t (plus-zero-l p)) (erase φ (plus-zero-r p))
  erase (∃̇∈ t φ) p = ∃̇∈ (eraseTm t (plus-zero-l p)) (erase φ (plus-zero-r p))

往返才是这一构造超出翻译之处：映回 K 必须返回原公式。词项层面的陈述 eraseTm-inv 先行。若 t 计数为零，则沿 Empty.rec* 改名 eraseTm t p 便按路径返回 t 本身，即 K 上词项之间的一条路径。改名函数 Empty.rec* : ⊥* → K 是空类型的消去子：要它给出一个 K 的常元，它就索要 ⊥* 的一个元素；而由 eraseTm 建出的词项不含常元节点，该函数实际上从未被调用。于是归纳只剩一个矛盾情形和一个变元情形，后者由 mapTm 的计算规则关闭，它从 var i 重建出 var i。

  eraseTm-inv : {n : ℕ} (t : Term K n) (p : countTm t ≡ )
              → mapTm Empty.rec* (eraseTm t p) ≡ t
  eraseTm-inv (con a) p = Empty.rec (snotz p)
  eraseTm-inv (var i) _ = refl

  erase-inv : {n : ℕ} (φ : Formula K n) (p : countFo φ ≡ )

在公式层面，逆定律 erase-inv 由对语法树的结构归纳证明，把词项层面的逆与自身递归地结合起来。两条原子关系以两个子部分展示了基例模式：由于 mapFo 把改名分配到两个被消去的词项中，目标是同一构造子的两次应用之间的路径，cong₂ 把词项层面的两条路径 eraseTm-inv t _ 与 eraseTm-inv u _ 提升为该路径。子词项的计数为零的证明由 plus-zero-l 与 plus-zero-r 作用于 p 得到，与 erase 自身完全一致。

            → mapFo Empty.rec* (erase φ p) ≡ φ
  erase-inv (t ∈̇ u) p =
    cong₂ _∈̇_ (eraseTm-inv t (plus-zero-l p)) (eraseTm-inv u (plus-zero-r p))
  erase-inv (t ≐ u) p =
    cong₂ _≐_ (eraseTm-inv t (plus-zero-l p)) (eraseTm-inv u (plus-zero-r p))

由于 erase 在每个节点都保持公式的形状，每个节点可用的归纳假设已经恰是该处逆定律所需的形式。三条二元连接词重复双部分模式：对 ∧̇、∨̇ 与 ⇒̇，整体的计数在两个子公式之间拆分，cong₂ 把一对归纳假设提升为重建后的连接词之间的路径。这种一致性是结构性的而非偶然：逆定律是语法树的性质，一次核查一个节点。

  erase-inv (φ ∧̇ ψ) p =
    cong₂ _∧̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
  erase-inv (φ ∨̇ ψ) p =
    cong₂ _∨̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
  erase-inv (φ ⇒̇ ψ) p =

单子部分的情形相应地更轻。假式只需 refl，因为两边都化归为构造子 ⊥̇ 本身。两条无界量词使用 cong 而非 cong₂，因为它们只携带一个子公式：在 mapFo 的计算规则展开后，目标是 ∃̇_ 之下的一条路径，cong ∃̇_ (erase-inv φ p) 给出的恰是它，同一个 p 原样传入。

    cong₂ _⇒̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
  erase-inv ⊥̇ _ = refl
  erase-inv (∃̇ φ) p = cong ∃̇_ (erase-inv φ p)
  erase-inv (∀̇ φ) p = cong ∀̇_ (erase-inv φ p)
  erase-inv (∀̇∈ t φ) p =

有界量词结束了这次归纳，与原子一样混合一个词项与一个公式：cong₂ 提升由词项层面的路径 eraseTm-inv t (plus-zero-l p) 与公式层面的路径 erase-inv φ (plus-zero-r p) 组成的对。到这一条款，定理完成。每条计数为零的公式都是其消去后的无参形式在相差一条路径意义下的精确像。于是出现接口的边界情形得到完整交代：在 K 上，无常元的公式恰是无参公式，且全程没有任何可判定性假设。

    cong₂ ∀̇∈ (eraseTm-inv t (plus-zero-l p)) (erase-inv φ (plus-zero-r p))
  erase-inv (∃̇∈ t φ) p =
    cong₂ ∃̇∈ (eraseTm-inv t (plus-zero-l p)) (erase-inv φ (plus-zero-r p))

小结

出现为公式的常元提供了一个有限接口，它从不追问常元域中两个符号是否相等。计数 countFo 既是出现之枚举的指标，也是此后参数抽象的指标：每次出现各得一个替代变量；安置装置及其查值定律为拼接环境补足所需的序号算术。当计数为零时，ZeroOccurrences 证明该公式恰是某条无参公式的精确像，于是可以采用空常元域而不损失任何语法。