module plfa.part1.Quantifiers where

本章节介绍全称量化（Universal Quantification）和存在量化（Existential Quantification）。

导入

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
open import Function 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}
  → (∀ (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-×) 结果对比。

练习 ⊎∀-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 是同构的。

提示：你需要 ∀-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 中是约束的。

我们定义一个合适的记录类型来形式化存在量化：

record Σ (A : Set) (B : A → Set) : Set where
  constructor ⟨_,_⟩
  field
    proj₁ : A
    proj₂ : B proj₁

此处我们有一个依赖记录，其 proj₂ 的类型依赖于字段 proj₁。 Σ A B 成立的证明由以下形式构成

⟨ M , N ⟩

其中 M 是类型为 A 的项，N 是类型为 B M 的项。 等价地，这样的证明也可以由下面的形式构成

record { proj₁ = M ; proj₂ = N }.

我们为存在量词定义一个方便的语法：

Σ-syntax = Σ
infix 2 Σ-syntax
syntax Σ-syntax A (λ x → Bx) = Σ[ x ∈ A ] Bx

这是我们第一次使用语法声明来定义约束。 它指示了左边的项可以用右边的语法来表示。 注意左边的项包含了一个 lambda 表达式，其中 x 为约束变量。 这个特殊的语法仅在标识符 Σ-syntax 被导入时可用。

这个语法声明使得 Σ[ x ∈ A ] Bx 和 Σ A (λ x → Bx) 等价。 其中，将 Bx 实例化为 B x，我们可得 Σ[ x ∈ A ] B x 和 Σ A (λ x → B x) 等价。 使用 η 规则，我们可得 (λ x → B x) ≡ B，因此它们也等价于 Σ A B。

我们也可以用归纳类型来等价地定义存在量化：

data Σ′ (A : Set) (B : A → Set) : Set where
  ⟨_,_⟩′ : (x : A) → B x → Σ′ A B

proj₁′ : ∀ {A : Set} {B : A → Set} → Σ′ A B → A
proj₁′ ⟨ x , y ⟩′ = x

proj₂′ : ∀ {A : Set} {B : A → Set} → ∀ (w : Σ′ A B) → B (proj₁′ w)
proj₂′ ⟨ x , y ⟩′ = y

依赖的结果之一是 proj₁′ 出现在了 proj₂′ 的类型签名中。

积是存在量词的一种特殊形式，其第二分量不取决于第一分量中的变量。

_×′_ : Set → Set → Set
A ×′ B = Σ[ x ∈ A ] B

（我们此处对 × 加上一撇，防止与标准库中的积产生冲突。我们在上一节的练习中导入使用了积类型。）

当一个积被视为合取的证明时，它的两个分量都是证明，而当一个依赖积被视为存在量词的证明时， 它的第一分量被视为数据类型中的一个元素，而第二分量是一个依赖于第一分量的命题的证明。因为在 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 → 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 → 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′

证明 to∘from 的许多方法实际上比较复杂。然而，如果你使用下面的引理，证明可以非常直接，其为 ≡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)