module plfa.part1.Decidable where

我们有两种不同的方式来表示关系：一是表示为由关系成立的证明（Evidence）所构成的数据类型； 二是表示为一个计算（Compute）关系是否成立的函数。在本章中，我们将探讨这两种方式之间的关系。 我们首先研究大家熟悉的布尔值（Boolean）记法，但是之后我们会发现，相较布尔值记法， 使用一种新的可判定性（Decidable）记法将会是更好的选择。

导入

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary.Negation using (¬_)
  renaming (contradiction to ¬¬-intro)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import plfa.part1.Relations using (_<_; z<s; s<s)
open import plfa.part1.Isomorphism using (_⇔_)

证据 vs 计算

回忆我们在 Relations 章节中将比较定义为一个归纳数据类型，其提供了一个数小于或等于另外一个数的证明：

infix 4 _≤_

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

举例来说，我们提供 2 ≤ 4 成立的证明，也可以证明没有 4 ≤ 2 成立的证明。

2≤4 : 2 ≤ 4
2≤4 = s≤s (s≤s z≤n)

¬4≤2 : ¬ (4 ≤ 2)
¬4≤2 (s≤s (s≤s ()))

() 的出现表明了没有 2 ≤ 0 成立的证明：z≤n 不能匹配（因为 2 不是 zero），s≤s 也不能匹配（因为 0 不能匹配 suc n）。

作为替代的定义，我们可以定义一个大家可能比较熟悉的布尔类型：

data Bool : Set where
  true  : Bool
  false : Bool

给定了布尔类型，我们可以定义一个两个数的函数在比较关系成立时来计算出 true， 否则计算出 false：

infix 4 _≤ᵇ_

_≤ᵇ_ : ℕ → ℕ → Bool
zero ≤ᵇ n       =  true
suc m ≤ᵇ zero   =  false
suc m ≤ᵇ suc n  =  m ≤ᵇ n

定义中的第一条与最后一条与归纳数据类型中的两个构造子相对应。因为对于任意的 m，不可能出现 suc m ≤ zero 的证明，我们使用中间一条定义来表示。 举个例子，我们可以计算 2 ≤ᵇ 4 成立，也可以计算 4 ≤ᵇ 2 不成立：

_ : (2 ≤ᵇ 4) ≡ true
_ =
  begin
    2 ≤ᵇ 4
  ≡⟨⟩
    1 ≤ᵇ 3
  ≡⟨⟩
    0 ≤ᵇ 2
  ≡⟨⟩
    true
  ∎

_ : (4 ≤ᵇ 2) ≡ false
_ =
  begin
    4 ≤ᵇ 2
  ≡⟨⟩
    3 ≤ᵇ 1
  ≡⟨⟩
    2 ≤ᵇ 0
  ≡⟨⟩
    false
  ∎

在第一种情况中，我们需要两步来将第一个参数降低到 0，再用一步来计算出真，这对应着我们需要 使用两次 s≤s 和一次 z≤n 来证明 2 ≤ 4。 在第二种情况中，我们需要两步来将第二个参数降低到 0，再用一步来计算出假，这对应着我们需要 使用两次 s≤s 和一次 () 来说明没有 4 ≤ 2 的证明。

将证明与计算相联系

我们希望能够证明这两种方法是有联系的，而我们的确可以。 首先，我们定义一个函数来把计算世界映射到证明世界：

T : Bool → Set
T true   =  ⊤
T false  =  ⊥

回忆到 ⊤ 是只有一个元素 tt 的单元类型，⊥ 是没有值的空类型。（注意 T 是大写字母 t， 与 ⊤ 不同。）如果 b 是 Bool 类型的，那么如果 b 为真，tt 可以提供 T b 成立的证明； 如果 b 为假，则不可能有 T b 成立的证明。

换句话说，T b 当且仅当 b ≡ true 成立时成立。在向前的方向，我们需要针对 b 进行情况分析：

T→≡ : ∀ (b : Bool) → T b → b ≡ true
T→≡ true tt   =  refl
T→≡ false ()

如果 b 为真，那么 T b 由 tt 证明，b ≡ true 由 refl 证明。 当 b 为假，那么 T b 无法证明。

在向后的方向，不需要针对布尔值 b 的情况分析：

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl  =  tt

如果 b ≡ true 由 refl 证明，我们知道 b 是 true，因此 T b 由 tt 证明。

现在我们可以证明 T (m ≤ᵇ n) 当且仅当 m ≤ n 成立时成立。

在向前的方向，我们考虑 _≤ᵇ_ 定义中的三条语句：

≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n
≤ᵇ→≤ zero    n       tt  =  z≤n
≤ᵇ→≤ (suc m) zero    ()
≤ᵇ→≤ (suc m) (suc n) t   =  s≤s (≤ᵇ→≤ m n t)

第一条语句中，我们立即可以得出 zero ≤ᵇ n 为真，所以 T (m ≤ᵇ n) 由 tt 而得， 相对应地 m ≤ n 由 z≤n 而证明。在中间的语句中，我们立刻得出 suc m ≤ᵇ zero 为假，则 T (m ≤ᵇ n) 为空，因此我们无需证明 m ≤ n，同时也不存在这样的证明。在最后的语句中，我们对于 suc m ≤ᵇ suc n 递归至 m ≤ᵇ n。令 t 为 T (suc m ≤ᵇ suc n) 的证明，如果其存在。 根据 _≤ᵇ_ 的定义，这也是 T (m ≤ᵇ n) 的证明。我们递归地应用函数来获得 m ≤ n 的证明，再使用 s≤s 将其转换成为 suc m ≤ suc n 的证明。

在向后的方向，我们考虑 m ≤ n 成立证明的可能形式：

≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)
≤→≤ᵇ z≤n        =  tt
≤→≤ᵇ (s≤s m≤n)  =  ≤→≤ᵇ m≤n

如果证明是 z≤n，我们立即可以得到 zero ≤ᵇ n 为真，所以 T (m ≤ᵇ n) 由 tt 证明。 如果证明是 s≤s 作用于 m≤n，那么 suc m ≤ᵇ suc n 归约到 m ≤ᵇ n，我们可以递归地使用函数 来获得 T (m ≤ᵇ n) 的证明。

向前方向的证明比向后方向的证明多一条语句，因为在向前方向的证明中我们需要考虑比较结果为真和假 的语句，而向后方向的证明只需要考虑比较成立的语句。这也是为什么我们比起计算的形式，更加偏爱证明的形式， 因为这样让我们做更少的工作：我们只需要考虑关系成立时的情况，而可以忽略不成立的情况。

从另一个角度来说，有时计算的性质可能正是我们所需要的。面对一个大数值上的非显然关系， 使用电脑来计算出答案可能会更加方便。幸运的是，比起在证明或计算之中犹豫， 我们有一种更好的方法来兼取其优。

取二者之精华

一个返回布尔值的函数提供恰好一比特的信息：这个关系成立或是不成立。相反地，证明的形式告诉我们 为什么这个关系成立，但却需要我们自行完成这个证明。不过，我们其实可以简单地定义一个类型来取二者之精华。 我们把它叫做：Dec A，其中 Dec 是可判定的（Decidable）的意思。

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

正如布尔值，这个类型有两个构造子。一个 Dec A 类型的值要么是以 yes x 的形式，其中 x 提供 A 成立的证明，或者是以 no ¬x 的形式，其中 x 提供了 A 无法成立的证明。（也就是说，¬x 是一个给定 A 成立的证据，返回矛盾的函数）

比如说，我们定义一个函数 _≤?_，给定两个数，判定是否一个数小于等于另一个，并提供证明来说明结论。

首先，我们使用两个有用的函数，用于构造不等式不成立的证明：

¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
¬s≤z ()

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n

第一个函数断言了 ¬ (suc m ≤ zero)，由荒谬可得。因为每个不等式的成立证明必须是 zero ≤ n 或者 suc m ≤ suc n 的形式，两者都无法匹配 suc m ≤ zero。 第二个函数取 ¬ (m ≤ n) 的证明 ¬m≤n，返回 ¬ (suc m ≤ suc n) 的证明。 所有形如 suc m ≤ suc n 的证明必须是以 s≤s m≤n 的形式给出。因此我们可以构造一个 矛盾，以 ¬m≤n m≤n 来证明。

使用这些，我们可以直接的判定不等关系：

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero  ≤? n                   =  yes z≤n
suc m ≤? zero                =  no ¬s≤z
suc m ≤? suc n with m ≤? n
...               | yes m≤n  =  yes (s≤s m≤n)
...               | no ¬m≤n  =  no (¬s≤s ¬m≤n)

与 _≤ᵇ_ 一样，定义有三条语句。第一条语句中，zero ≤ n 立即成立，由 z≤n 证明。 第二条语句中，suc m ≤ zero 立即不成立，由 ¬s≤z 证明。 第三条语句中，我们需要递归地应用 m ≤? n。有两种可能性，在 yes 的情况中，它会返回 m ≤ n 的证明 m≤n，所以 s≤s m≤n 即可作为 suc m ≤ suc n 的证明；在 no 的情况中， 它会返回 ¬ (m ≤ n) 的证明 ¬m≤n，所以 ¬s≤s ¬m≤n 即可作为 ¬ (suc m ≤ suc n) 的证明。

当我们写 _≤ᵇ_ 时，我们必须写两个其他的函数 ≤ᵇ→≤ 和 ≤→≤ᵇ 来证明其正确性。 作为对比，_≤?_ 的定义自身就证明了其正确性，由类型即可得知。_≤?_ 的代码也比 _≤ᵇ_、≤ᵇ→≤ 和 ≤→≤ᵇ 加起来要简洁的多。我们稍后将会证明，如果我们需要后三者， 我们亦可简单地从 _≤?_ 中派生出来。

我们可以使用我们新的函数来计算出我们之前需要自己想出来的证明。

_ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
_ = refl

_ : 4 ≤? 2 ≡ no (¬s≤s (¬s≤s ¬s≤z))
_ = refl

你可以验证 Agda 的确计算出了这些值。输入 C-c C-n 并给出 2 ≤? 4 或者 4 ≤? 2 作为 需要的表达式，Agda 会输出如上的值。

（小细节：如果我们不把 ¬s≤z 和 ¬s≤s 作为顶层函数来定义，而是使用内嵌的匿名函数， Agda 可能会在规范化否定的证明中出现问题。）

练习 _<?_ （推荐）

与上面的函数相似，定义一个判定严格不等性的函数：

postulate
  _<?_ : ∀ (m n : ℕ) → Dec (m < n)

-- 请将代码写在此处

练习 _≡ℕ?_（实践）

定义一个函数来判定两个自然数是否相等。

postulate
  _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)

-- 请将代码写在此处

从可判定的值到布尔值，从布尔值到可判定的值

好奇的读者可能会思考能不能重用 m ≤ᵇ n 的定义，加上它与 m ≤ n 等价的证明， 来证明可判定性。的确，我们是可以做到的：

_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)
m ≤?′ n with m ≤ᵇ n | ≤ᵇ→≤ m n | ≤→≤ᵇ {m} {n}
...        | true   | p        | _            = yes (p tt)
...        | false  | _        | ¬p           = no ¬p

如果 m ≤ᵇ n 为真，那么 ≤ᵇ→≤ 会返回一个 m ≤ n 成立的证明。 如果 m ≤ᵇ n 为假，那么 ≤→≤ᵇ 会取一个 m ≤ n 成立的证明，将其转换为一个矛盾。

在这个证明中，with 语句的三重约束是必须的。如果我们取而代之的写：

_≤?″_ : ∀ (m n : ℕ) → Dec (m ≤ n)
m ≤?″ n with m ≤ᵇ n
... | true   =  yes (≤ᵇ→≤ m n tt)
... | false  =  no (≤→≤ᵇ {m} {n})

那么 Agda 对于每条语句会有一个抱怨：

⊤ !=< (T (m ≤ᵇ n)) of type Set
when checking that the expression tt has type T (m ≤ᵇ n)

T (m ≤ᵇ n) !=< ⊥ of type Set
when checking that the expression ≤→≤ᵇ {m} {n} has type ¬ m ≤ n

将表达式放在 with 语句中能让 Agda 利用下列事实：当 m ≤ᵇ n 为真时，T (m ≤ᵇ n) 是 ⊤；当 m ≤ᵇ n 为假时，T (m ≤ᵇ n) 是 ⊥。

然而，总体来说还是直接定义 _≤?_ 比较方便，正如之前部分中那样。如果有人真的很需要 _≤ᵇ_， 那么它和它的性质可以简单地从 _≤?_ 中派生出来，正如我们接下来要展示的一样。

擦除（Erasure）将一个可判定的值转换为一个布尔值：

⌊_⌋ : ∀ {A : Set} → Dec A → Bool
⌊ yes x ⌋  =  true
⌊ no ¬x ⌋  =  false

使用擦除，我们可以简单地从 _≤?_ 中派生出 _≤ᵇ_：

_≤ᵇ′_ : ℕ → ℕ → Bool
m ≤ᵇ′ n  =  ⌊ m ≤? n ⌋
更进一步来说，如果 D 是一个类型为 Dec A 的值，那么 T ⌊ D ⌋ 当且仅当 A 成立时成立：
toWitness : ∀ {A : Set} {D : Dec A} → T ⌊ D ⌋ → A
toWitness {A} {yes x} tt  =  x
toWitness {A} {no ¬x} ()

fromWitness : ∀ {A : Set} {D : Dec A} → A → T ⌊ D ⌋
fromWitness {A} {yes x} _  =  tt
fromWitness {A} {no ¬x} x  =  ¬x x

使用这些，我们可以简单地派生出 T (m ≤ᵇ′ n) 当且仅当 m ≤ n 成立时成立。

≤ᵇ′→≤ : ∀ {m n : ℕ} → T (m ≤ᵇ′ n) → m ≤ n
≤ᵇ′→≤  =  toWitness

≤→≤ᵇ′ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ′ n)
≤→≤ᵇ′  =  fromWitness

总结来说，最好避免直接使用布尔值，而使用可判定的值。如果有需要布尔值的时候，它们和它们的性质 可以简单地从对应的可判定的值中派生而来。

逻辑连接符

大多数读者对于布尔值的逻辑运算符很熟悉了。每个逻辑运算符都可以被延伸至可判定的值。

两个布尔值的合取当两者都为真时为真，当任一为假时为假：

infixr 6 _∧_

_∧_ : Bool → Bool → Bool
true  ∧ true  = true
false ∧ _     = false
_     ∧ false = false

在 Emacs 中，第三个等式的左手边显示为灰色，表示这些等式出现的顺序决定了是第二条还是第三条 会被匹配到。然而，不管是哪一条被匹配到，结果都是一样的。

相应地，给定两个可判定的命题，我们可以判定它们的合取：

infixr 6 _×-dec_

_×-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A × B)
yes x ×-dec yes y = yes ⟨ x , y ⟩
no ¬x ×-dec _     = no λ{ ⟨ x , y ⟩ → ¬x x }
_     ×-dec no ¬y = no λ{ ⟨ x , y ⟩ → ¬y y }

两个命题的合取当两者都成立时成立，其否定则当任意一者否定成立时成立。如果两个都成立， 我们将每一证明放入数据对中，作为合取的证明。如果任意一者的否定成立，假设整个合取将会引入一个矛盾。

同样地，在 Emacs 中，第三条等式在左手边以灰色显示，说明等式的顺序决定了第二条还是第三条会被匹配。 这一次，我们给出的结果会因为是第二条还是第三条而不一样。如果两个命题都不成立，我们选择第一个来构造矛盾， 但选择第二个也是同样正确的。

两个布尔值的析取当任意为真时为真，当两者为假时为假：

infixr 5 _∨_

_∨_ : Bool → Bool → Bool
true  ∨ _      = true
_     ∨ true   = true
false ∨ false  = false

在 Emacs 中，第二个等式的左手边显示为灰色，表示这些等式出现的顺序决定了是第一条还是第二条 会被匹配到。然而，不管是哪一条被匹配到，结果都是一样的。

相应地，给定两个可判定的命题，我们可以判定它们的析取：

infixr 5 _⊎-dec_

_⊎-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)
yes x ⊎-dec _     = yes (inj₁ x)
_     ⊎-dec yes y = yes (inj₂ y)
no ¬x ⊎-dec no ¬y = no λ{ (inj₁ x) → ¬x x ; (inj₂ y) → ¬y y }

两个命题的析取当任意一者成立时成立，其否定则当两者的否定成立时成立。如果任意一者成立， 我们使用其证明来作为析取的证明。如果两个的否定都成立，假设任意一者都会引入一个矛盾。

同样地，在 Emacs 中，第二条等式在左手边以灰色显示，说明等式的顺序决定了第一条还是第二条会被匹配。 这一次，我们给出的结果会因为是第二条还是第三条而不一样。如果两个命题都成立，我们选择第一个来构造析取， 但选择第二个也是同样正确的。

一个布尔值的否定当值为真时为假，反之亦然：

not : Bool → Bool
not true  = false
not false = true

相应地，给定一个可判定的命题，我们可以判定它的否定：

¬? : ∀ {A : Set} → Dec A → Dec (¬ A)
¬? (yes x)  =  no (¬¬-intro x)
¬? (no ¬x)  =  yes ¬x

我们直接把 yes 和 no 交换。在第一个等式中，右手边断言了 ¬ A 的否定成立，也就是说 ¬ ¬ A 成立——这是一个 A 成立时可以简单得到的推论。

还有一个与蕴涵相对应，但是稍微不那么知名的运算符：

_⊃_ : Bool → Bool → Bool
_     ⊃ true   =  true
false ⊃ _      =  true
true  ⊃ false  =  false

当任何一个布尔值为真的时候，另一个布尔值恒为真，我们成为第一个布尔值蕴涵第二个布尔值。 因此，两者的蕴涵在第二个为真或者第一个为假时为真，在第一个为真而第二个为假时为假。 在 Emacs 中，第二个等式的左手边显示为灰色，表示这些等式出现的顺序决定了是第一条还是第二条 会被匹配到。然而，不管是哪一条被匹配到，结果都是一样的。

相应地，给定两个可判定的命题，我们可以判定它们的析取：

_→-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A → B)
_     →-dec yes y  =  yes (λ _ → y)
no ¬x →-dec _      =  yes (λ x → ⊥-elim (¬x x))
yes x →-dec no ¬y  =  no (λ f → ¬y (f x))

两者的蕴涵在第二者成立或者第一者的否定成立时成立，其否定在第一者成立而第二者否定成立时成立。 蕴涵成立的证明是一个从第一者成立的证明到第二者成立的证明的函数。如果第二者成立，那么这个函数 直接返回第二者的证明。如果第一者的否定成立，那么使用第一者成立的证明，构造一个矛盾。 如果第一者成立，第二者不成立，给定蕴涵成立的证明，我们必须构造一个矛盾：我们将成立的证明 f 应用于第一者成立的证明 x，再加以第二者否定成立的证明 ¬y 来构造矛盾。

同样地，在 Emacs 中，第二条等式在左手边以灰色显示，说明等式的顺序决定了第一条还是第二条会被匹配。 这一次，我们给出的结果会因为是哪一条被匹配而不一样，但两者都是同样正确的。

练习 erasure（实践）

证明擦除将对应的布尔值和可判定的值的操作联系了起来：

postulate
  ∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
  ∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
  not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋

练习 iff-erasure （推荐）

给出与同构与嵌入章节中 _↔︎_ 相对应的布尔值与可判定的值的操作， 并证明其对应的擦除：

postulate
  _iff_ : Bool → Bool → Bool
  _⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
  iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋

-- 请将代码写在此处

互映证明

让我们回顾一下章节自然数中 monus 的定义。 如果从一个较小的数中减去一个较大的数，结果为零。毕竟我们总是要得到一个结果。 我们可以用其他方式定义吗？可以定义一版带有守卫（guarded）的减法──只有当 n ≤ m 时才能从 m 中减去 n ：

minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
minus m       zero    _         = m
minus (suc m) (suc n) (s≤s n≤m) = minus m n n≤m

然而这种定义难以使用，因为我们必须显式地为 n ≤ m 提供证明：

_ : minus 5 3 (s≤s (s≤s (s≤s z≤n))) ≡ 2
_ = refl

这个问题没有通用的解决方案，但是在上述的情景下，我们恰好静态地知道这两个数字。这种情况下，我们可以使用一种被称为互映证明（proof by reflection）的技术。 实质上，在类型检查的时候我们可以让 Agda 运行可判定的等式 n ≤? m 并且保证 n ≤ m！

我们使用「隐式参数」的一个特性来实现这个功能。如果 Agda 可以填充一个记录类型的所有字段，那么 Agda 就可以填充此记录类型的隐式参数。 由于空记录类型没有任何字段，Agda 总是会设法填充空记录类型的隐式参数。这就是 ⊤ 类型被定义成空记录的原因。

这里的技巧是设置一个类型为 T ⌊ n ≤? m ⌋ 的隐式参数。让我们一步一步阐述这句话的含义。 首先，我们运行判定过程 n ≤? m。它向我们提供了 n ≤ m 是否成立的证据。我们擦除证据得到布尔值。 最后，我们应用 T。回想一下，T 将布尔值映射到证据的世界：true 变成了单位类型 ⊤， false 变成了空类型 ⊥ 。在操作上，这个类型的隐式参数起到了守卫的作用。

  • 如果 n ≤ m 成立，隐式参数的类型归约为 ⊤。 然后 Agda 会欣然地提供隐式参数。
  • 否则，类型归约为 ⊥ ，Agda 无法为此类型提供对应的值，因此会报错。例如，如果我们调用 3 - 5 会得到 _n≤m_254 : ⊥。

我们使用之前定义的 toWitness 获得了 n ≤ m 的证据：

_-_ : (m n : ℕ) {n≤m : T ⌊ n ≤? m ⌋} → ℕ
_-_ m n {n≤m} = minus m n (toWitness n≤m)

我们现在只要能静态地知道这两个数就可以安全地使用 _-_ 了：

_ : 5 - 3 ≡ 2
_ = refl

事实上，这种惯用语法非常普遍。标准库为 T ⌊ ? ⌋ 定义了叫做 True 的同义词：

True : ∀ {Q} → Dec Q → Set
True Q = T ⌊ Q ⌋

练习 False （实践）

给出 True，toWitness 和 fromWitness 的相反定义。分别称为 False，toWitnessFalse 和 fromWitnessFalse。

练习 Bin-decidable（延伸）

回想练习 Bin、 Bin-laws 和 Bin-predicates，定义一个用比特串表示自然数的数据类型 Bin，并定义以下谓词：

One  : Bin → Set
Can  : Bin → Set

证明以上二者是可判定的。

One? : ∀ (b : Bin) → Dec (One b)
Can? : ∀ (b : Bin) → Dec (Can b)

标准库

import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
import Data.Nat using (_≤?_)
import Relation.Nullary using (Dec; yes; no)
import Relation.Nullary.Decidable using
  (⌊_⌋; True; toWitness; fromWitness; _×-dec_; _⊎-dec_; ¬?)
import Relation.Binary.Definitions using (Decidable)

Unicode

∧  U+2227  逻辑和 (\and, \wedge)
∨  U+2228  逻辑或 (\or, \vee)
⊃  U+2283  超集 (\sup)
ᵇ  U+1D47  修饰符小写 B  (\^b)
⌊  U+230A  左向下取整 (\clL)
⌋  U+230B  右向下取整 (\clR)