module plfa.part1.Relations where

在定义了加法和乘法等运算以后，下一步我们来定义关系（Relation），比如说小于等于。

导入

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm; +-identityʳ)

定义关系

小于等于这个关系有无穷个实例，如下所示：

0 ≤ 0     0 ≤ 1     0 ≤ 2     0 ≤ 3     ...
          1 ≤ 1     1 ≤ 2     1 ≤ 3     ...
                    2 ≤ 2     2 ≤ 3     ...
                              3 ≤ 3     ...
                                        ...

但是，我们仍然可以用几行有限的定义来表示所有的实例，如下文所示的一对推理规则：

z≤n --------
    zero ≤ n

    m ≤ n
s≤s -------------
    suc m ≤ suc n

以及其 Agda 定义：

data _≤_ : ℕ → ℕ → Set where

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

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

在这里，z≤n 和 s≤s（无空格）是构造子的名称，zero ≤ n、m ≤ n 和 suc m ≤ suc n （带空格）是类型。在这里我们第一次用到了 索引数据类型（Indexed datatype）。我们使用 m 和 n 这两个自然数来索引 m ≤ n 这个类型。在 Agda 里，由两个及以上短横线开始的行是注释行， 我们巧妙利用这一语法特性，用上述形式来表示相应的推理规则。 在后文中，我们还会继续使用这一形式。

这两条定义告诉我们相同的两件事：

  • 起始步骤: 对于所有的自然数 n，命题 zero ≤ n 成立。
  • 归纳步骤：对于所有的自然数 m 和 n，如果命题 m ≤ n 成立， 那么命题 suc m ≤ suc n 成立。

实际上，他们分别给我们更多的信息：

  • 起始步骤: 对于所有的自然数 n，构造子 z≤n 提供了 zero ≤ n 成立的证明。
  • 归纳步骤：对于所有的自然数 m 和 n，构造子 s≤s 将 m ≤ n 成立的证明 转化为 suc m ≤ suc n 成立的证明。

例如，我们在这里以推理规则的形式写出 2 ≤ 4 的证明：

  z≤n -----
      0 ≤ 2
 s≤s -------
      1 ≤ 3
s≤s ---------
      2 ≤ 4

下面是对应的 Agda 证明：

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

隐式参数

这是我们第一次使用隐式参数。定义不等式时，构造子的定义中使用了 ∀， 就像我们在下面的命题中使用 ∀ 一样：

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m

但是我们这里的定义使用了花括号 { }，而不是小括号 ( )。 这意味着参数是隐式的（Implicit），不需要额外声明。实际上，Agda 的类型检查器 会推导（Infer）出它们。因此，我们在 m + n ≡ n + m 的证明中需要写出 +-comm m n， 在 zero ≤ n 的证明中可以省略 n。同理，如果 m≤n 是 m ≤ n的证明， 那么我们写出 s≤s m≤n 作为 suc m ≤ suc n 的证明，无需声明 m 和 n。

如果有希望的话，我们也可以在大括号里显式声明隐式参数。例如，下面是 2 ≤ 4 的 Agda 证明，包括了显式声明了的隐式参数：

_ : 2 ≤ 4
_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

也可以额外加上参数的名字：

_ : 2 ≤ 4
_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} (z≤n {n = 2}))

在后者的形式中，也可以选择只声明一部分隐式参数：

_ : 2 ≤ 4
_ = s≤s {n = 3} (s≤s {n = 2} z≤n)

但是不可以改变隐式参数的顺序，即便加上了名字。

我们可以写出 _ 来让 Agda 用相同的推导方式试着推导一个显式的项。 例如，我们可以为命题 +-identityʳ 定义一个带有隐式参数的变体：

+-identityʳ′ : ∀ {m : ℕ} → m + zero ≡ m
+-identityʳ′ = +-identityʳ _

我们用 _ 来让 Agda 从语境中推导显式参数的值。只有 m 这一个值能够给出正确的证明，因此 Agda 愉快地填入了它。 如果 Agda 推导值失败，那么它会报一个错误。

优先级

我们如下定义比较的优先级：

infix 4 _≤_

我们将 _≤_ 的优先级设置为 4，所以它不如优先级为 6 的 _+_ 结合得紧，因而， 1 + 2 ≤ 3 将被解析为 (1 + 2) ≤ 3。我们用 infix 来表示运算符既不是左结合的， 也不是右结合的。因为 1 ≤ 2 ≤ 3 解析为 (1 ≤ 2) ≤ 3 或者 1 ≤ (2 ≤ 3) 都没有意义。

可判定性

给定两个数，我们可以很直接地决定第一个数是不是小于等于第二个数。我们在此处不给出说明的代码， 但我们会在 Decidable 章节重新讨论这个问题。

反演

在我们的定义中，我们从更小的东西得到更大的东西。例如，我们可以从 m ≤ n 得出 suc m ≤ suc n 的结论，这里的 suc m 比 m 更大 （也就是说，前者包含后者），suc n 也比 n 更大。但有时我们也 需要从更大的东西得到更小的东西。

只有一种方式能够证明对于任意 m 和 n 有 suc m ≤ suc n。 这让我们能够反演（invert）之前的规则。

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

这里的 m≤n（不带空格）是一个变量名，而 m ≤ n（带空格）是一个类型， 且后者是前者的类型。在 Agda 中，将类型中的空格去掉来作为变量名是一种常见的约定。

并不是所有规则都可以反演。实际上，z≤n 的规则没有非隐式的假设， 因此它没有可以被反演的规则。但这种反演通常是成立的。

反演的另一个例子是证明只存在一种情况使得一个数字能够小于或等于零。

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

序关系的性质

数学家对于关系的常见性质给出了约定的名称。

  • 自反（Reflexive）：对于所有的 n，关系 n ≤ n 成立。
  • 传递（Transitive）：对于所有的 m、 n 和 p，如果 m ≤ n 和 n ≤ p 成立，那么 m ≤ p 也成立。
  • 反对称（Anti-symmetric）：对于所有的 m 和 n，如果 m ≤ n 和 n ≤ m 同时成立，那么 m ≡ n 成立。
  • 完全（Total）：对于所有的 m 和 n，m ≤ n 或者 n ≤ m 成立。

_≤_ 关系满足上述四条性质。

对于上述性质的组合也有约定的名称。

  • 预序（Preorder）：满足自反和传递的关系。
  • 偏序（Partial Order）：满足反对称的预序。
  • 全序（Total Order）：满足完全的偏序。

如果你在派对上偶遇一个『关系』，你现在知道怎么样和人讨论了， 可以讨论关于自反、传递、反对称和完全， 或者问一问这是不是预序、偏序或者全序。

更认真的来说，如果你在阅读论文时碰到了一个关系，本文的介绍让你可以对关系有基本的了解和判断， 来判断这个关系是不是预序、偏序或者全序。一个认真的作者一般会在文章指出这个关系具有（或者缺少） 上述性质，比如说指出新定义的关系是一个偏序而不是全序。

练习 orderings（实践）

给出一个不是偏序的预序的例子。

-- 请将代码写在此处。

给出一个不是全序的偏序的例子。

-- 请将代码写在此处。

自反性

我们第一个来证明的性质是自反性：对于任意自然数 n，关系 n ≤ n 成立。我们使用标准库 的惯例来隐式申明参数，在使用自反性的证明时这样可以更加方便。

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

这个证明直接在 n 上进行归纳。在起始步骤中，zero ≤ zero 由 z≤n 证明；在归纳步骤中， 归纳假设 ≤-refl {n} 给我们带来了 n ≤ n 的证明，我们只需要使用 s≤s，就可以获得 suc n ≤ suc n 的证明。

在 Emacs 中来交互式地证明自反性是一个很好的练习，可以使用洞，以及 C-c C-c、 C-c C-, 和 C-c C-r 命令。

传递性

我们第二个证明的性质是传递性：对于任意自然数 m 和 n，如果 m ≤ n 和 n ≤ p 成立，那么 m ≤ p 成立。同样，m、n 和 p 是隐式参数：

≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans z≤n       _          =  z≤n
≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)

这里我们在 m ≤ n 的证据（Evidence）上进行归纳。在起始步骤里，第一个不等式因为 z≤n 而成立， 那么结论亦可由 z≤n 而得出。在这里，n ≤ p 的证明是不需要的，我们用 _ 来表示这个 证明没有被使用。

在归纳步骤中，第一个不等式因为 s≤s m≤n 而成立，第二个不等式因为 s≤s n≤p 而成立， 所以我们已知 suc m ≤ suc n 和 suc n ≤ suc p，求证 suc m ≤ suc p。 通过归纳假设 ≤-trans m≤n n≤p，我们得知 m ≤ p，在此之上使用 s≤s 即可证。

≤-trans (s≤s m≤n) z≤n 不可能发生，因为第一个不等式告诉我们中间的数是一个 suc n， 而第二个不等式告诉我们中间的数是 zero。Agda 可以推断这样的情况不可能发现，所以我们不需要 （也不可以）列出这种情况。

我们也可以将隐式参数显式地声明。

≤-trans′ : ∀ (m n p : ℕ)
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans′ zero    _       _       z≤n       _          =  z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans′ m n p m≤n n≤p)

有人说这样的证明更加的清晰，也有人说这个更长的证明让人难以抓住证明的重点。 我们一般选择使用简短的证明。

对于性质成立证明进行的归纳（如上文中对于 m ≤ n 的证明进行归纳），相比于对于性质成立的值进行的归纳 （如对于 m 进行归纳），有非常大的价值。我们会经常使用这样的方法。

同样，在 Emacs 中来交互式地证明传递性是一个很好的练习，可以使用洞，以及 C-c C-c、 C-c C-, 和 C-c C-r 命令。

反对称性

我们证明的第三个性质是反对称性：对于所有的自然数 m 和 n，如果 m ≤ n 和 n ≤ m 同时成立，那么 m ≡ n 成立：

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym z≤n       z≤n        =  refl
≤-antisym (s≤s m≤n) (s≤s n≤m)  =  cong suc (≤-antisym m≤n n≤m)

同样，我们对于 m ≤ n 和 n ≤ m 的证明进行归纳。

在起始步骤中，两个不等式都因为 z≤n 而成立。因此我们已知 zero ≤ zero 和 zero ≤ zero， 求证 zero ≡ zero，由自反性可证。（注：由等式的自反性可证，而不是不等式的自反性）

在归纳步骤中，第一个不等式因为 s≤s m≤n 而成立，第二个等式因为 s≤s n≤m 而成立。因此我们已知 suc m ≤ suc n 和 suc n ≤ suc m，求证 suc m ≡ suc n。归纳假设 ≤-antisym m≤n n≤m 可以证明 m ≡ n，因此我们可以使用同余性完成证明。

练习 ≤-antisym-cases（实践）

上面的证明中省略了一个参数是 z≤n，另一个参数是 s≤s 的情况。为什么可以省略这种情况？

-- 请将代码写在此处。

完全性

我们证明的第四个性质是完全性：对于任何自然数 m 和 n，m ≤ n 或者 n ≤ m 成立。 在 m 和 n 相等时，两者同时成立。

我们首先来说明怎么样不等式才是完全的：

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

Total m n 成立的证明有两种形式：forward m≤n 或者 flipped n≤m，其中 m≤n 和 n≤m 分别是 m ≤ n 和 n ≤ m 的证明。

（如果你对于逻辑学有所了解，上面的定义可以由析取（Disjunction）表示。 我们会在 Connectives 章节介绍析取。）

这是我们第一次使用带参数的数据类型，这里 m 和 n 是参数。这等同于下面的索引数据类型：

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

类型里的每个参数都转换成构造子的一个隐式参数。索引数据类型中的索引可以变化，正如在 zero ≤ n 和 suc m ≤ suc n 中那样，而参数化数据类型不一样，其参数必须保持相同， 正如在 Total m n 中那样。参数化的声明更短，更易于阅读，而且有时可以帮助到 Agda 的 停机检查器，所以我们尽可能地使用它们，而不是索引数据类型。

在上述准备工作完成后，我们定义并证明完全性。

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero    n                         =  forward z≤n
≤-total (suc m) zero                      =  flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward m≤n  =  forward (s≤s m≤n)
...                        | flipped n≤m  =  flipped (s≤s n≤m)

这里，我们的证明在两个参数上进行归纳，并按照情况分析：

  • 第一起始步骤：如果第一个参数是 zero，第二个参数是 n，那么 forward 条件成立，我们使用 z≤n 作为 zero ≤ n 的证明。

  • 第二起始步骤：如果第一个参数是 suc m，第二个参数是 zero，那么 flipped 条件成立，我们使用 z≤n 作为 zero ≤ suc m 的证明。

  • 归纳步骤：如果第一个参数是 suc m，第二个参数是 suc n，那么归纳假设 ≤-total m n 可以给出如下推断：

    • 归纳假设的 forward 条件成立，以 m≤n 作为 m ≤ n 的证明。以此我们可以使用 s≤s m≤n 作为 suc m ≤ suc n 来证明 forward 条件成立。

    • 归纳假设的 flipped 条件成立，以 n≤m 作为 n ≤ m 的证明。以此我们可以使用 s≤s n≤m 作为 suc n ≤ suc m 来证明 flipped 条件成立。

这是我们第一次在 Agda 中使用 with 语句。with 关键字后面有一个表达式和一或多行。 每行以省略号（...）和一个竖线（|）开头，后面跟着用来匹配表达式的模式，和等式的右手边。

使用 with 语句等同于定义一个辅助函数。比如说，上面的定义和下面的等价：

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero    n        =  forward z≤n
≤-total′ (suc m) zero     =  flipped z≤n
≤-total′ (suc m) (suc n)  =  helper (≤-total′ m n)
  where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n)  =  forward (s≤s m≤n)
  helper (flipped n≤m)  =  flipped (s≤s n≤m)

这也是我们第一次在 Agda 中使用 where 语句。where 关键字后面有一或多条定义，其必须被缩进。 之前等式左手边的约束变量（此例中的 m 和 n）在嵌套的定义中仍然在作用域内。 在嵌套定义中的约束标识符（此例中的 helper ）在等式的右手边的作用域内。

如果两个参数相同，那么两个情况同时成立，我们可以返回任一证明。上面的代码中我们返回 forward 条件， 但是我们也可以返回 flipped 条件，如下：

≤-total″ : ∀ (m n : ℕ) → Total m n
≤-total″ m       zero                      =  flipped z≤n
≤-total″ zero    (suc n)                   =  forward z≤n
≤-total″ (suc m) (suc n) with ≤-total″ m n
...                         | forward m≤n  =  forward (s≤s m≤n)
...                         | flipped n≤m  =  flipped (s≤s n≤m)

两者的区别在于上述代码在对于第一个参数进行模式匹配之前先对于第二个参数先进行模式匹配。

单调性

如果在聚会中碰到了一个运算符和一个序，那么有人可能会问这个运算符对于这个序是不是 单调的（Monotonic）。比如说，加法对于小于等于是单调的，这意味着：

∀ {m n p q : ℕ} → m ≤ n → p ≤ q → m + p ≤ n + q

这个证明可以用我们学会的方法，很直接的来完成。我们最好把它分成三个部分，首先我们证明加法对于 小于等于在右手边是单调的：

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero    p q p≤q  =  p≤q
+-monoʳ-≤ (suc n) p q p≤q  =  s≤s (+-monoʳ-≤ n p q p≤q)

我们对于第一个参数进行归纳。

  • 起始步骤：第一个参数是 zero，那么 zero + p ≤ zero + q 可以化简为 p ≤ q， 其证明由 p≤q 给出。

  • 归纳步骤：第一个参数是 suc n，那么 suc n + p ≤ suc n + q 可以化简为 suc (n + p) ≤ suc (n + q)。归纳假设 +-monoʳ-≤ n p q p≤q 可以证明 n + p ≤ n + q，我们在此之上使用 s≤s 即可得证。

接下来，我们证明加法对于小于等于在左手边是单调的。我们可以用之前的结论和加法的交换律来证明：

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n  rewrite +-comm m p | +-comm n p  = +-monoʳ-≤ p m n m≤n

用 +-comm m p 和 +-comm n p 来重写，可以让 m + p ≤ n + p 转换成 p + n ≤ p + m， 而我们可以用 +-moroʳ-≤ p m n m≤n 来证明。

最后，我们把前两步的结论结合起来：

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q  =  ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

使用 +-monoˡ-≤ m n p m≤n 可以证明 m + p ≤ n + p， 使用 +-monoʳ-≤ n p q p≤q 可以证明 n + p ≤ n + q，用传递性把两者连接起来， 我们可以获得 m + p ≤ n + q 的证明，如上所示。

练习 *-mono-≤ （延伸）

证明乘法对于小于等于是单调的。

-- 请将代码写在此处。

严格不等关系

我们可以用类似于定义不等关系的方法来定义严格不等关系。

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

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

严格不等关系与不等关系最重要的区别在于，0 小于任何数的后继，而不小于 0。

显然，严格不等关系不是自反的，而是非自反的（Irreflexive），表示 n < n 对于 任何值 n 都不成立。和不等关系一样，严格不等关系是传递的。严格不等关系不是完全的，但是满足 一个相似的性质：三分律（Trichotomy）：对于任意的 m 和 n，m < n、m ≡ n 或者 m > n 三者有且仅有一者成立。（我们定义 m > n 当且仅当 n < m 成立时成立） 严格不等关系对于加法和乘法也是单调的。

我们把一部分上述性质作为习题。非自反性需要逻辑非，三分律需要证明三者是互斥的，因此这两个性质 暂不做为习题。我们会在 Negation 章节来重新讨论。

我们可以直接地来证明 suc m ≤ n 蕴涵了 m < n，及其逆命题。 因此我们亦可从不等关系的性质中，使用此性质来证明严格不等关系的性质。

练习 <-trans （推荐）

证明严格不等是传递的。请直接证明。（后续的练习中我们将使用 < 和 ≤ 的关系。）

-- 请将代码写在此处。

练习 trichotomy（实践）

证明严格不等关系满足弱化的三元律，证明对于任意 m 和 n，下列命题有一条成立：

  • m < n，
  • m ≡ n，或者
  • m > n。

定义 m > n 为 n < m。你需要一个合适的数据类型声明，如同我们在证明完全性中使用的那样。 （我们会在介绍完否定之后证明三者是互斥的。）

-- 请将代码写在此处。

练习 +-mono-<（实践）

证明加法对于严格不等关系是单调的。正如不等关系中那样，你可以需要额外的定义。

-- 请将代码写在此处。

练习 ≤-iff-< (推荐)

证明 suc m ≤ n 蕴涵了 m < n，及其逆命题。

-- 请将代码写在此处。

练习 <-trans-revisited（实践）

用另外一种方法证明严格不等是传递的，使用之前证明的不等关系和严格不等关系的联系， 以及不等关系的传递性。

-- 请将代码写在此处。

奇和偶

作为一个额外的例子，我们来定义奇数和偶数。不等关系和严格不等关系是二元关系，而奇偶性 是一元关系，有时也被叫做谓词（Predicate）：

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where

  suc  : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

一个数是偶数，如果它是 0，或者是奇数的后继。一个数是奇数，如果它是偶数的后继。

这是我们第一次定义一个相互递归的数据类型。因为每个标识符必须在使用前声明，所以 我们首先声明索引数据类型 even 和 odd （省略 where 关键字和其构造子的定义）， 然后声明其构造子（省略其签名 ℕ → Set，因为在之前已经给出）。

这也是我们第一次使用重载（Overloaded）的构造子。这意味着不同类型的构造子 拥有相同的名字。在这里 suc 表示下面三种构造子其中之一：

suc : ℕ → ℕ

suc : ∀ {n : ℕ}
  → odd n
    ------------
  → even (suc n)

suc : ∀ {n : ℕ}
  → even n
    -----------
  → odd (suc n)

同理，zero 表示两种构造子的一种。因为类型推导的限制，Agda 不允许重载已定义的名字， 但是允许重载构造子。我们推荐将重载限制在有关联的定义中，如我们所做的这样，但这不是必须的。

我们证明两个偶数之和是偶数：

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

e+e≡e zero     en  =  en
e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

与相互递归的定义对应，我们用两个相互递归的函数，一个证明两个偶数之和是偶数，另一个证明 一个奇数与一个偶数之和是奇数。

这是我们第一次使用相互递归的函数。因为每个标识符必须在使用前声明，我们先给出两个函数的签名， 然后再给出其定义。

要证明两个偶数之和为偶，我们考虑第一个数为偶数的证明。如果是因为第一个数为 0， 那么第二个数为偶数的证明即为和为偶数的证明。如果是因为第一个数为奇数的后继， 那么和为偶数是因为他是一个奇数和一个偶数的和的后续，而这个和是一个奇数。

要证明一个奇数和一个偶数的和是奇数，我们考虑第一个数是奇数的证明。 如果是因为它是一个偶数的后继，那么和为奇数，因为它是两个偶数之和的后继， 而这个和是一个偶数。

练习 o+o≡e (延伸)

证明两个奇数之和为偶数。

-- 请将代码写在此处。

练习 Bin-predicates (延伸)

回忆我们在练习 Bin 中定义了一个数据类型 Bin 来用二进制字符串表示自然数。 这个表达方法不是唯一的，因为我们在开头加任意个 0。因此，11 可以由以下方法表示：

⟨⟩ I O I I
⟨⟩ O O I O I I

定义一个谓词

Can : Bin → Set

其在一个二进制字符串的表示是标准的（Canonical）时成立，表示它没有开头的 0。在两个 11 的表达方式中， 第一个是标准的，而第二个不是。在定义这个谓词时，你需要一个辅助谓词：

One : Bin → Set

其仅在一个二进制字符串开头为 1 时成立。一个二进制字符串是标准的，如果它开头是 1 （表示一个正数）， 或者它仅是一个 0 （表示 0）。

证明递增可以保持标准性。

Can b
------------
Can (inc b)

证明从自然数转换成的二进制字符串是标准的。

----------
Can (to n)

证明将一个标准的二进制字符串转换成自然数之后，再转换回二进制字符串与原二进制字符串相同。

Can b
---------------
to (from b) ≡ b

提示：对于每一条习题，先从 One 的性质开始。 证明以下命题也会很有帮助。

One b
----------
1 ≤ from b

1 ≤ n
---------------------
to (2 * n) ≡ (to n) O
-- 请将代码写在此处。

标准库

标准库中有类似于本章介绍的定义：

import Data.Nat using (_≤_; z≤n; s≤s)
import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                  +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)

在标准库中，≤-total 是使用析取定义的（我们将在 Connectives 章节定义）。 +-monoʳ-≤、+-monoˡ-≤ 和 +-mono-≤ 的证明方法和本书不同。 更多的参数是隐式申明的。

Unicode

本章使用了如下 Unicode 符号：

≤  U+2264  小于等于 (\<=, \le)
≥  U+2265  大于等于 (\>=, \ge)
ˡ  U+02E1  小写字母 L 标识符 (\^l)
ʳ  U+02B3  小写字母 R 标识符 (\^r)

\^l 和 \^r 命令给出了左右箭头，以及上标字母 l 和 r。