Quantifiers: 全称量词与存在量词
module plfa.part1.Quantifiers where
本章节介绍全称量化（Universal Quantification）和存在量化（Existential Quantification）。
导入
import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_) open import Relation.Nullary.Negation using (¬_) open import Data.Product.Base using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality) open import Function.Base using (_∘_)
全称量化
我们用依赖函数类型（Dependent Function Type）来形式化全称量化， 这样的形式在书中贯穿始终。例如，在归纳一章中，我们证明了加法满足结合律：
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)它断言对于所有的自然数 m、n 和 p，(m + n) + p ≡ m + (n + p) 成立。 它是一个依赖函数，给出 m、n 和 p 的值，它会返回与该等式对应的证据。
通常给定一个 A 类型的变量 x 和一个带有 x 自由变量的命题 B x，全称量化 的命题 ∀ (x : A) → B x 当对于所有类型为 A 的项 M，命题 B M 成立时成立。 在这里，B M 代表了将 B x 中自由出现的变量 x 替换成 M 后的命题。 变量 x 在 B x 中以自由变量的形式出现，但是在 ∀ (x : A) → B x 中是约束的。
∀ (x : A) → B x 成立的证明由以下形式构成：
λ (x : A) → N x其中 N x 是一个 B x 类型的项，N x 和 B x 都包含了一个 A 类型的自由变量 x。 给定一个项 L， 其提供 ∀ (x : A) → B x 成立的证明，和一个类型为 A 的项 M， L M 这一项则是 B M 成立的证明。换句话说，∀ (x : A) → B x 成立的证明是一个函数， 将类型为 A 的项 M 转换成 B M 成立的证明。
再换句话说，如果我们知道 ∀ (x : A) → B x 成立，又知道 M 是一个类型为 A 的项， 那么我们可以推导出 B M 成立：
∀-elim : ∀ {A : Set} {B : A → Set} → (L : ∀ (x : A) → B x) → (M : A) ----------------- → B M ∀-elim L M = L M
如 →-elim 那样，这条规则对应了函数应用。
函数是依赖函数的一种特殊形式，其值域不取决于定义域中的变量。当一个函数被视为 蕴涵的证明时，它的参数和结果都是证明，而当一个依赖函数被视为全称量词的证明时， 它的参数被视为数据类型中的一个元素，而结果是一个依赖于参数的命题的证明。因为在 Agda 中，一个数据类型中的一个值和一个命题的证明是无法区别的，这样的区别很大程度上 取决于如何来诠释。
依赖函数类型也被叫做依赖积（Dependent Product），因为如果 A 是一个有限的数据类型， 有值 x₁ , ⋯ , xₙ，如果每个类型 B x₁ , ⋯ , B xₙ 有 m₁ , ⋯ , mₙ 个不同的成员， 那么 ∀ (x : A) → B x 有 m₁ * ⋯ * mₙ 个成员。的确，∀ (x : A) → B x 的记法有时 也被 Π[ x ∈ A ] (B x) 取代，其中 Π 代表积。然而，我们还是使用依赖函数这个名称， 因为依赖积这个名称是有歧义的，我们后续会体会到歧义所在。
练习 ∀-distrib-× （推荐）
证明全称量词对于合取满足分配律：
postulate ∀-distrib-× : ∀ {A : Set} {B C : A → Set} → (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
将这个结果与 Connectives 章节中的 (→-distrib-×) 结果对比。
提示：你需要 ∀-extensionality。
练习 ⊎∀-implies-∀⊎（实践）
证明全称命题的析取蕴涵了析取的全称命题：
postulate ⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} → (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
逆命题成立么？如果成立，给出证明。如果不成立，解释为什么。
练习 ∀-×（实践）
参考下面的类型：
data Tri : Set where aa : Tri bb : Tri cc : Tri
令 B 作为由 Tri 索引的一个类型，也就是说 B : Tri → Set。 证明 ∀ (x : Tri) → B x 和 B aa × B bb × B cc 是同构的。
Hint: you will need to use ∀-extensionality.
提示：你需要 ∀-extensionality。
存在量化
给定一个 A 类型的变量 x 和一个带有 x 自由变量的命题 B x，存在量化 的命题 Σ[ x ∈ A ] B x 当对于一些类型为 A 的项 M，命题 B M 成立时成立。 在这里，B M 代表了将 B x 中自由出现的变量 x 替换成 M 以后的命题。 变量 x 在 B x 中以自由变量形式出现，但是在 Σ[ x ∈ A ] B x 中是约束的。
我们定义一个合适的归纳数据类型来形式化存在量化：
data Σ (A : Set) (B : A → Set) : Set where ⟨_,_⟩ : (x : A) → B x → Σ A B
我们为存在量词定义一个方便的语法：
Σ-syntax = Σ infix 2 Σ-syntax syntax Σ-syntax A (λ x → Bx) = Σ[ x ∈ A ] Bx
这是我们第一次使用语法声明，其表示左手边的项可以以右手边的语法来书写。 这种特殊语法只有在标识符 Σ-syntax 被导入时可用。
Σ[ x ∈ A ] B x 成立的证明由 ⟨ M , N ⟩ 组成，其中 M 是类型为 A 的项， N 是 B M 成立的证明。
我们也可以用记录类型来等价地定义存在量化。
record Σ′ (A : Set) (B : A → Set) : Set where field proj₁′ : A proj₂′ : B proj₁′
这里的记录构造
record
{ proj₁′ = M
; proj₂′ = N
}对应了项
⟨ M , N ⟩其中 M 是类型为 A 的项，N 是类型为 B M 的项。
积是存在量词的一种特殊形式，其第二分量不取决于第一分量中的变量。当一个积被视为 合取的证明时，它的两个分量都是证明，而当一个依赖积被视为存在量词的证明时， 它的第一分量被视为数据类型中的一个元素，而第二分量是一个依赖于第一分量的命题的证明。因为在 Agda 中，一个数据类型中的一个值一个命题的证明是无法区别的，这样的区别很大程度上 取决于如何来诠释。
存在量化也被叫做依赖和（Dependent Sum），因为如果 A 是一个有限的数据类型， 有值 x₁ , ⋯ , xₙ，如果每个类型 B x₁ , ⋯ , B xₙ 有 m₁ , ⋯ , mₙ 个不同的成员， 那么 Σ[ x ∈ A ] B x 有 m₁ + ⋯ + mₙ 个成员，这也解释了选择使用这个记法的原因—— Σ 代表和。
存在量化有时也被叫做依赖积（Dependent Product），因为积是其中的一种特殊形式。但是， 这样的叫法非常让人困扰，因为全程量化也被叫做依赖积，而存在量化已经有依赖和的叫法。
存在量词的普通记法是 ∃ （与全程量词的 ∀ 记法相类似）。我们使用 Agda 标准库中的惯例， 使用一种隐式申明约束变量定义域的记法。
∃ : ∀ {A : Set} (B : A → Set) → Set ∃ {A} B = Σ A B ∃-syntax = ∃ syntax ∃-syntax (λ x → B) = ∃[ x ] B
这种特殊的语法只有在 ∃-syntax 标识符被导入时可用。我们将倾向于使用这种语法，因为它更短， 而且看上去更熟悉。
给定 ∀ x → B x → C 成立的证明，其中 C 不包括自由变量 x，给定 ∃[ x ] B x 成立的 证明，我们可以推导出 C 成立。
∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} → (∀ x → B x → C) → ∃[ x ] B x --------------- → C ∃-elim f ⟨ x , y ⟩ = f x y
换句话说，如果我们知道对于任何 A 类型的 x，B x 蕴涵了 C，还知道对于某个类型 A 的 x，B x 成立，那么我们可以推导出 C 成立。这是因为我们可以先将 ∀ x → B x → C 的证明对于 A 类型的 x 和 B x 类型的 y 实例化，而这样的值恰好可以由 ∃[ x ] B x 的证明来提供。
的确，逆命题也成立，两者合起来构成一个同构：
∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set} → (∀ x → B x → C) ≃ (∃[ x ] B x → C) ∀∃-currying = record { to = λ{ f → λ{ ⟨ x , y ⟩ → f x y }} ; from = λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}} ; from∘to = λ{ f → refl } ; to∘from = λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl }} }
这可以被看做是将柯里化推广的结果。的确，建立这两者同构的证明与之前我们讨论 蕴涵时给出的证明是一样的。
练习 ∃-distrib-⊎ （推荐）
证明存在量词对于析取满足分配律：
postulate ∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} → ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
练习 ∃×-implies-×∃（实践）
证明合取的存在命题蕴涵了存在命题的合取：
postulate ∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} → ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
逆命题成立么？如果成立，给出证明。如果不成立，解释为什么。
练习 ∃-⊎（实践）
沿用练习 ∀-× 中的 Tri 和 B 。 证明 ∃[ x ] B x 与 B aa ⊎ B bb ⊎ B cc 是同构的。
一个存在量化的例子
回忆我们在 Relations 章节中定义的 even 和 odd：
data even : ℕ → Set data odd : ℕ → Set data even where even-zero : even zero even-suc : ∀ {n : ℕ} → odd n ------------ → even (suc n) data odd where odd-suc : ∀ {n : ℕ} → even n ----------- → odd (suc n)
如果一个数是 0 或者它是奇数的后继，那么这个数是偶数。如果一个数是偶数的后继，那么这个数是奇数。
我们接下来要证明，一个数是偶数当且仅当这个数是一个数的两倍，一个数是奇数当且仅当这个数 是一个数的两倍多一。换句话说，我们要证明的是：
even n 当且仅当 ∃[ m ] ( m * 2 ≡ n)
odd n 当且仅当 ∃[ m ] (1 + m * 2 ≡ n)
惯例来说，我们往往将常数因子写在前面、将和里的常数项写在后面。但是这里我们没有按照惯例， 而是反了过来，因为这样可以让证明更简单：
这是向前方向的证明：
even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] ( m * 2 ≡ n) odd-∃ : ∀ {n : ℕ} → odd n → ∃[ m ] (1 + m * 2 ≡ n) even-∃ even-zero = ⟨ zero , refl ⟩ even-∃ (even-suc o) with odd-∃ o ... | ⟨ m , refl ⟩ = ⟨ suc m , refl ⟩ odd-∃ (odd-suc e) with even-∃ e ... | ⟨ m , refl ⟩ = ⟨ m , refl ⟩
我们定义两个相互递归的函数。给定 n 是奇数或者是偶数的证明，我们返回一个数 m，以及 m * 2 ≡ n 或者 1 + m * 2 ≡ n 的证明。我们根据 n 是奇数 或者是偶数的证明进行归纳：
如果这个数是偶数，因为它是 0，那么我们返回数据对 0 ，以及 0 的两倍是 0 的证明。
如果这个数是偶数，因为它是比一个奇数多 1，那么我们可以使用归纳假设，来获得一个数
m和1 + m * 2 ≡ n的证明。我们返回数据对suc m以及suc m * 2 ≡ suc n的证明—— 我们可以直接通过替换n来得到证明。如果这个数是奇数，因为它是一个偶数的后继，那么我们可以使用归纳假设，来获得一个数
m和m * 2 ≡ n的证明。我们返回数据对m以及1 + m * 2 ≡ suc n的证明—— 我们可以直接通过替换n来得到证明。
这样，我们就完成了正方向的证明。
接下来是反方向的证明：
∃-even : ∀ {n : ℕ} → ∃[ m ] ( m * 2 ≡ n) → even n ∃-odd : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) → odd n ∃-even ⟨ zero , refl ⟩ = even-zero ∃-even ⟨ suc m , refl ⟩ = even-suc (∃-odd ⟨ m , refl ⟩) ∃-odd ⟨ m , refl ⟩ = odd-suc (∃-even ⟨ m , refl ⟩)
给定一个是另一个数两倍的数，我们需要证明这个数是偶数。给定一个是另一个数两倍多一的数， 我们需要证明这个数是奇数。我们对于存在量化的证明进行归纳。在偶数的情况，我们也需要考虑两种 一个数是另一个数两倍的情况。
在偶数是
zero的情况中，我们需要证明zero * 2是偶数，由even-zero可得。在偶数是
suc n的情况中，我们需要证明suc m * 2是偶数。归纳假设告诉我们，1 + m * 2是奇数，那么所求证的结果由even-suc可得。在偶数的情况中，我们需要证明
1 + m * 2是奇数。归纳假设告诉我们，m * 2是偶数， 那么所求证的结果由odd-suc可得。
这样，我们就完成了向后方向的证明。
练习 ∃-even-odd（实践）
如果我们用 2 * m 代替 m * 2，2 * m + 1 代替 1 + m * 2，上述证明会变得复杂多少呢？ 用这种方法来重写 ∃-even 和 ∃-odd。
-- 请将代码写在此处
练习 ∃-+-≤（实践）
证明当且仅当存在一个 x 使得 x + y ≡ z 成立时 y ≤ z 成立。
-- 请将代码写在此处
存在量化、全称量化和否定
存在量化的否定与否定的全称量化是同构的。考虑到存在量化是解构的推广，全称量化是合构的推广， 这样的结果与解构的否定与否定的合构是同构的结果相似。
¬∃≃∀¬ : ∀ {A : Set} {B : A → Set} → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x ¬∃≃∀¬ = record { to = λ{ ¬∃xy x y → ¬∃xy ⟨ x , y ⟩ } ; from = λ{ ∀¬xy ⟨ x , y ⟩ → ∀¬xy x y } ; from∘to = λ{ ¬∃xy → extensionality λ{ ⟨ x , y ⟩ → refl } } ; to∘from = λ{ ∀¬xy → refl } }
在 to 的方向，给定了一个 ¬ ∃[ x ] B x 类型的值 ¬∃xy，需要证明给定一个 x 的值， 可以推导出 ¬ B x。换句话说，给定一个 B x 类型的值 y，我们可以推导出假。将 x 和 y 合并起来我们就得到了 ∃[ x ] B x 类型的值 ⟨ x , y ⟩，对其使用 ¬∃xy 即可获得矛盾。
在 from 的方向，给定了一个 ∀ x → ¬ B x 类型的值 ∀¬xy，需要证明从一个类型为 ∃[ x ] B x 类型的值 ⟨ x , y ⟩ ，我们可以推导出假。将 ∀¬xy 使用于 x 之上， 可以得到类型为 ¬ B x 的值，对其使用 y 即可获得矛盾。
两个逆的证明很直接，其中有一个方向需要外延性。
练习 ∃¬-implies-¬∀ （推荐）
证明否定的存在量化蕴涵了全称量化的否定：
postulate ∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set} → ∃[ x ] (¬ B x) -------------- → ¬ (∀ x → B x)
逆命题成立吗？如果成立，给出证明。如果不成立，解释为什么。
练习 Bin-isomorphism （延伸）
回忆在练习 Bin、 Bin-laws 和 Bin-predicates 中， 我们定义了比特串数据类型 Bin 来表示自然数，并要求你定义了下列函数和谓词：
to : ℕ → Bin
from : Bin → ℕ
Can : Bin → Set以及证明了下列性质：
from (to n) ≡ n
----------
Can (to n)
Can b
---------------
to (from b) ≡ b使用上述，证明 ℕ 与 ∃[ b ](Can b) 之间存在同构。
我们建议证明以下引理，它描述了对于给定的二进制数 b，One b 只有一个证明， Can b，也是如此。
≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
≡Can : ∀ {b : Bin} (c c′ : Can b) → c ≡ c′Many of the alternatives for proving to∘from turn out to be tricky. However, the proof can be straightforward if you use the following lemma, which is a corollary of ≡Can.
proj₁≡→Can≡ : {c c′ : ∃[ b ] Can b} → proj₁ c ≡ proj₁ c′ → c ≡ c′-- 请将代码写在此处
标准库
标准库中可以找到与本章中相似的定义：
import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
Unicode
本章节使用下列 Unicode：
Π U+03A0 大写希腊字母 PI (\Pi)
Σ U+03A3 大写希腊字母 SIGMA (\Sigma)
∃ U+2203 存在 (\ex, \exists)