和我签订契约，成为函数式魔法少女吧！
——胡振江（伪） in 《函数式魔法少女》

写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。

这篇文章主要介绍了在 Agda 中定义 Peano 自然数、自然数的加法和乘法运算，以及相关的定理证明。

Agda，启动！

参考资料：

《函数式程序设计》课件

《Verified Programming in Agda》

提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode 的基本使用方法

本文章含有 Github Copilot 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。

Peano Natural Numbers

Peano Natural Numbers 的基本思想是，我们可以用一个类型来表示自然数，这个类型有两个值，一个是 0，另一个是后继函数，它接受一个自然数，返回这个自然数的后继。

在 Agda 中，我们可以这样定义 Peano 自然数：

1
2
3
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

自然数的运算

加法

我们利用分类讨论+递归的方法来定义自然数的加法：

1
2
3
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

乘法

定义乘法的方式和加法类似：

1
2
3
_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + (m * n)

前驱

我们可以定义一个前驱函数，它接受一个自然数，返回这个自然数的前驱：

1
2
3
pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n

当然，0 是没有前驱的。

前驱函数可以视作后继函数的逆运算。

加和乘相关定理的证明

0 关于加法的单位元性质：

要证明 0 是加法的单位元，我们需要分别证明 0 + n = n 和 n + 0 = n；也就是证明 0 的左单位元性质和右单位元性质。

1
2
3
4
5
6
0+ : ∀(x : ℕ) → 0 + x ≡ x
0+ x = refl

+0 : ∀(x : ℕ) → x + 0 ≡ x
+0 zero = refl
+0 (suc x) rewrite +0 x = refl

在这里，我们就使用了 rewrite 来进行 数学归纳 证明，这一点在之后的证明中也会经常用到。

这两种证明方法的不同是我们的加法的定义所导致的。

在 0+ 中，等号两边我们可以直接按照定义展开，然后直接使用 refl 即可。

而在 +0 中，直接地展开并不能得到我们想要的结果，因为按照定义，直接展开一步之后我们得到的是 suc (x + 0) ≡ suc (x)，两边不能满足 refl 的构造。

但是如果我们同时在两边拿掉 suc，那么我们的问题就好像被 “剥了一层皮” 一样，退化到了更低一级的情况，并且终究可以退化到最小的边界情形，这时候我们就可以使用归纳假设来完成证明。

加法结合律

我们也可以用归纳法来证明加法的结合律：

1
2
3
+assoc : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
+assoc zero y z = refl
+assoc (suc x) y z rewrite +assoc x y z = refl

我们证明的思路和上面的证明类似，都是先利用我们定义的加法讲式子两边展开，然后利用归纳假设来完成证明。

再写一遍过程：

$l.h.s = suc x + (y + z) = suc (x + (y + z)) r.h.s = suc (x + y) + z = suc ((x + y) + z) $

两边同时去除 suc 之后，我们就可以利用归纳假设来完成证明了。

示例：通过 hole 和辅助引理来证明加法的交换律

1
2
3
+comm : ∀ (x y : N) → x + y ≡ y + x 
+comm zero y = ? 
+comm (suc x) y = ?

在上面的代码中，我们使用一个 ? 来表示我们还没有完成的证明，这时候 Agda 会提示我们需要证明的类型，以及当前的上下文。

按下 Ctrl + C 然后按下 Ctrl + L，我们可以看到 Agda 给出了提示：

1
2
3
4
5
6
+comm : ∀ (x y : N) → x + y ≡ y + x 
+comm zero y = { }0 --{ }0 is a hole
+comm (suc x) y = { }1
---------------------------------------------------------
?0 : zero + y ≡ y + zero
?1 : suc x + y ≡ y + suc x

我们接下来就可以基于这些提示来完成证明了。

观察 hole0。

1
2
3
Goal: y ≡ y+0
--------------------------------------------------
y: N

左边按照加法定义展开之后，我们得到的是 y ≡ y + zero，这时候我们就可以使用 +0 来完成证明了。

1
2
3
+comm : ∀ (x y : N) → x + y ≡ y + x 
+comm zero y rewrite +0 y = refl
+comm (suc x) y = { }0

观察 hole1。

1
2
3
4
Goal: suc (x + y) ≡ y + suc x 
---------------------------------------------------------
y : N 
x : N

尝试用归纳假设重写一下，这样可以使 x 和 y 的位置在左右两边对称。

1
2
3
+comm : ∀ (x y : N) → x + y ≡ y + x
+comm zero y rewrite +0 y = refl
+comm (suc x) y rewrite +comm x y = { }0

再次观察 hole1。

1
2
3
4
Goal: suc (y + x) ≡ y + suc x 
---------------------------------------------------------
y : N 
x : N

在此处，按照加法的定义，我们不能再对左右两边进行任何的展开，我们此时必须把上式作为一个辅助引理来证明。

1
2
3
+suc : ∀ (x y : N) → x + (suc y) ≡ suc (x + y) 
+suc zero y = refl 
+suc (suc x) y rewrite +suc x y = refl

辅助引理的证明此处就不再赘述了。

接下来使用辅助引理来证明即可。

1
2
3
+comm : ∀ (x y : N) → x + y ≡ y + x
+comm zero y rewrite +0 y = refl
+comm (suc x) y rewrite +comm x y | +suc y x = refl

在 rewrite 中使用 | 可以使用多个 rewrite 规则，按照从左到右的顺序依次进行 rewrite

此外，Agda 不像 Haskell 那样无需顾及函数在代码中定义的顺序，所以我们在写代码时必须把辅助引理写在主要的证明之前，否则 Agda 会提示我们找不到辅助引理（not in scope）。

证明乘法的分配律

1
2
3
*distrib : ∀ (x y z : ℕ) → (x + y) * z ≡ (x * z) + (y * z)
*distrib zero y z = refl
*distrib (suc x) y z rewrite *distrib x y z | +assoc z (x * z) (y * z) = refl

这个证明的操作流程和上文中利用 hole 来证明加法交换律的过程类似，这里就不再赘述了。

自然数的比较

当然，自然数也是具有三岐性的，任意两个自然数都可以比较大小。

我们可以这样定义自然数的比较：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

infixl 5 _<ℕ_
_<ℕ_ : ℕ → ℕ → Bool
zero <ℕ zero = false
zero <ℕ suc y = true
suc x <ℕ zero = false
suc x <ℕ suc y = x <ℕ y

infix 4 _=ℕ_
_=ℕ_ : ℕ → ℕ → Bool
zero =ℕ zero = true
zero =ℕ suc y = false
suc x =ℕ zero = false
suc x =ℕ suc y = x =ℕ y

infixl 5 _≤ℕ_
_≤ℕ_ : ℕ → ℕ → Bool
zero ≤ℕ zero = true
zero ≤ℕ suc y = true
suc x ≤ℕ zero = false
suc x ≤ℕ suc y = x ≤ℕ y

infixl 5 _≥ℕ_
_≥ℕ_ : ℕ → ℕ → Bool
x ≥ℕ y = y ≤ℕ x

infixl 5 _>ℕ_
_>ℕ_ : ℕ → ℕ → Bool
x >ℕ y = y <ℕ x

在这里我们使用了标准库中的 Bool 类型，我们可以通过 open import Data.Bool 来导入标准库中的 Bool 类型。

自然数比较的定理证明

自然数不能小于 0

1
2
3
<0 : ∀ (x : ℕ) → x <ℕ zero ≡ false
<0 zero = refl
<0 (suc x) = refl

上述证明是显然的，但是要注意一点：

1
2
<0 : ∀ (x : ℕ) → x <ℕ zero ≡ false
<0 x = refl

如果你这样写，那么 Agda 就会报错，因为 Agda 无法通过模式匹配来判断 x 是 0 还是 suc x，所以会导致 x <ℕ zero 无法直接求出结果，必须对 x 进行分类讨论，才能进行模式匹配进而得到结果。

而如果你的 <ℕ 定义为：

1
2
3
4
_<ℕ_ : ℕ → ℕ → Bool
_ <ℕ zero = false
zero <ℕ suc y = true
suc x <ℕ suc y = x <ℕ y

则上述第二种证明就成为了正确的书写方式。

这个例子告诉我们，对于函数性质证明的书写，我们必须要认真地考虑函数原本的定义方式，以及 Agda 的模式匹配机制，才能写出正确的证明。

不等号的传递性

我们在这里需要用到类似之前 Absurd 的东西，但是我们不能像之前一样直接将一个零元组 () 作为 Absurd Pattern，因为我们这里要推出的是一个 Bool 类型的假设不成立情况下的 Absurd，所以我们需要把上回 Bool 最后写的那个 𝔹-contra 拿过来用用。

1
2
3
4
5
6
7
8
9
𝔹-contra : false ≡ true → ∀{l} {P : Set l} → P 
𝔹-contra ()

<-trans : ∀ {x y z : ℕ} → (x <ℕ y) ≡ true → (y <ℕ z) ≡ true → (x <ℕ z) ≡ true
<-trans {x} {zero} p1 p2 rewrite <0 x = 𝔹-contra p1
<-trans {zero} {suc y} {zero} p1 () 
<-trans {zero} {suc y} {suc z} p1 p2 = refl
<-trans {suc x} {suc y} {zero} p1 () 
<-trans {suc x} {suc y} {suc z} p1 p2 = <-trans {x} {y} {z} p1 p2

证明相等测试的正确性

如何证明我们上文所定义的 =ℕ 的确实反映了自然数的相等关系呢？

1
2
3
4
5
_=ℕ_ : ℕ → ℕ → Bool
zero =ℕ zero = true
zero =ℕ suc y = false
suc x =ℕ zero = false
suc x =ℕ suc y = x =ℕ y

我们需要证明 x =ℕ y ≡ true 是 x ≡ y 的充分必要条件。

1
2
3
4
5
6
7
8
9
10
11
12
13
=ℕ-to-≡ : ∀ {x y : ℕ} → x =ℕ y ≡ true → x ≡ y
=ℕ-to-≡ {zero} {zero} u = refl
=ℕ-to-≡ {suc x} {zero} ()
=ℕ-to-≡ {zero} {suc y} ()
=ℕ-to-≡ {suc x} {suc y} u rewrite =ℕ-to-≡ {x} {y} u = refl

=ℕ-refl : ∀ (x : ℕ) → (x =ℕ x) ≡ true
=ℕ-refl zero = refl
=ℕ-refl (suc x) = =ℕ-refl x


=ℕ-from-≡ : ∀ {x y : ℕ} → x ≡ y → x =ℕ y ≡ true
=ℕ-from-≡ {x} refl = =ℕ-refl x

这本来就是一件非常简单的事情。

相互递归的函数定义

因为我们是 FP，所以我们当然可以定义相互递归的函数，只要它们能够最终到达边界条件。

例如一个奇偶性判断函数：

1
2
3
4
5
6
isEven : ℕ → Bool
isOdd : ℕ → Bool
isEven zero = true
isEven (suc x) = isOdd x
isOdd zero = false
isOdd (suc x) = isEven x

当然由于 Agda 向前以来的尿性，我们必须像在 C++ 里面一样，先写下类型签名来声明函数，然后再写函数体（定义）。

这一点就使得它不如 Haskell 那样优雅了。

相互递归的证明

就拿证明 isEven 与 isOdd 的互反性来说：

1
2
3
4
5
6
7
8
9
10
~_ : Bool → Bool
~ true = false
~ false = true

even~odd : ∀ (x : ℕ) → isEven x ≡ ~ isOdd x
odd~even : ∀ (x : ℕ) → isOdd x ≡ ~ isEven x
even~odd zero = refl
even~odd (suc x) = odd~even x
odd~even zero = refl
odd~even (suc x) = even~odd x

小练习：

  1. 证明自然数的加法满足交换律和结合律
  1. 证明如下的性质：
    ∀ (n : ℕ) → n <ℕ n ≡ ff
    ∀ {x y : ℕ} → x <ℕ y ≡ tt → y <ℕ x ≡ ff
    ∀ (n m : ℕ) → n <ℕ m || n =ℕ m || m <ℕ n ≡ tt

最终参考代码

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
module natural where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym)
open import Data.Bool

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)
infixl 7 _*_
_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + (m * n)

pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n

0+ : ∀(x : ℕ) → zero + x ≡ x
0+ x = refl

+0 : ∀(x : ℕ) → x + zero ≡ x
+0 zero = refl
+0 (suc x) rewrite +0 x = refl

+assoc : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
+assoc zero y z = refl
+assoc (suc x) y z rewrite +assoc x y z = refl

+suc : ∀ (x y : ℕ) → x + suc y ≡ suc (x + y)
+suc zero y = refl
+suc (suc x) y rewrite +suc x y = refl

+comm : ∀ (x y : ℕ) → x + y ≡ y + x
+comm zero y rewrite +0 y = refl
+comm (suc x) y rewrite +comm x y | +suc y x = refl

*distrib : ∀ (x y z : ℕ) → (x + y) * z ≡ (x * z) + (y * z)
*distrib zero y z = refl
*distrib (suc x) y z rewrite *distrib x y z | +assoc z (x * z) (y * z) = refl


_<ℕ_ : ℕ → ℕ → Bool
zero <ℕ zero = false
zero <ℕ suc y = true
suc x <ℕ zero = false
suc x <ℕ suc y = x <ℕ y


_=ℕ_ : ℕ → ℕ → Bool
zero =ℕ zero = true
zero =ℕ suc y = false
suc x =ℕ zero = false
suc x =ℕ suc y = x =ℕ y


_≤ℕ_ : ℕ → ℕ → Bool
zero ≤ℕ zero = true
zero ≤ℕ suc y = true
suc x ≤ℕ zero = false
suc x ≤ℕ suc y = x ≤ℕ y


_≥ℕ_ : ℕ → ℕ → Bool
x ≥ℕ y = y ≤ℕ x

_>ℕ_ : ℕ → ℕ → Bool
x >ℕ y = y <ℕ x

<0 : ∀ (x : ℕ) → (x <ℕ zero) ≡ false
<0 zero = refl
<0 (suc x) = refl

𝔹-contra : false ≡ true → ∀{l} {P : Set l} → P 
𝔹-contra ()

<-trans : ∀ {x y z : ℕ} → (x <ℕ y) ≡ true → (y <ℕ z) ≡ true → (x <ℕ z) ≡ true
<-trans {x} {zero} p1 p2 rewrite <0 x = 𝔹-contra p1
<-trans {zero} {suc y} {zero} p1 () 
<-trans {zero} {suc y} {suc z} p1 p2 = refl
<-trans {suc x} {suc y} {zero} p1 () 
<-trans {suc x} {suc y} {suc z} p1 p2 = <-trans {x} {y} {z} p1 p2

=ℕ-to-≡ : ∀ {x y : ℕ} → x =ℕ y ≡ true → x ≡ y
=ℕ-to-≡ {zero} {zero} u = refl
=ℕ-to-≡ {suc x} {zero} ()
=ℕ-to-≡ {zero} {suc y} ()
=ℕ-to-≡ {suc x} {suc y} u rewrite =ℕ-to-≡ {x} {y} u = refl

=ℕ-refl : ∀ (x : ℕ) → (x =ℕ x) ≡ true
=ℕ-refl zero = refl
=ℕ-refl (suc x) = =ℕ-refl x


=ℕ-from-≡ : ∀ {x y : ℕ} → x ≡ y → x =ℕ y ≡ true
=ℕ-from-≡ {x} refl = =ℕ-refl x

isEven : ℕ → Bool
isOdd : ℕ → Bool
isEven zero = true
isEven (suc x) = isOdd x
isOdd zero = false
isOdd (suc x) = isEven x

~_ : Bool → Bool
~ true = false
~ false = true

even~odd : ∀ (x : ℕ) → isEven x ≡ ~ isOdd x
odd~even : ∀ (x : ℕ) → isOdd x ≡ ~ isEven x
even~odd zero = refl
even~odd (suc x) = odd~even x
odd~even zero = refl
odd~even (suc x) = even~odd x

+assoc2 : ∀ (x y z : ℕ) → (x + y) + z ≡ x + (y + z)
+assoc2 zero y z = refl
+assoc2 (suc x) y z rewrite +assoc2 x y z = refl

+-swap : ∀ (x y z : ℕ) → x + (y + z) ≡ y + (x + z)
+-swap x y z rewrite sym(+assoc2 y x z) | sym(+assoc2 x y z) | +comm x y = refl

*0 : ∀ (x : ℕ) → x * zero ≡ zero
*0 zero = refl
*0 (suc x) rewrite *0 x = refl

*-suc : ∀ (x y : ℕ) → x * suc y ≡ x + x * y
*-suc zero y = refl
*-suc (suc x) y rewrite *-suc x y | +-swap y x (x * y) = refl

*-comm : (x y : ℕ) → x * y ≡ y * x
*-comm zero y rewrite *0 y = refl
*-comm (suc x) y rewrite *-suc y x | *-comm x y = refl

+-samex : ∀ (x y z : ℕ) → y ≡ z → x + y ≡ x + z
+-samex zero y z p = p 
+-samex (suc x) y z p rewrite +-samex x y z p = refl

*-distri2 : (x y z : ℕ) → x * (y + z) ≡ x * y + x * z
*-distri2 zero y z = refl
*-distri2 (suc x) y z rewrite *-distri2 x y z | +assoc2 y z (x * y + x * z) | +assoc2 y (x * y) (z + x * z) = +-samex y (z + (x * y + x * z)) (x * y + (z + x * z)) (+-swap z (x * y) (x * z))

-- problem 1.2: associativity of _*_
*-assoc : (x y z : ℕ) → (x * y) * z ≡ x * (y * z)
*-assoc zero y z = refl
*-assoc (suc x) y z rewrite *-assoc x y z | sym(+assoc2 y z (x * y + x * z)) | *-comm (y + x * y) z | *-distri2 z y (x * y) | *-comm z y | *-comm z (x * y) | sym(*-assoc x y z) = refl

n≮n : (n : ℕ) → (n <ℕ n) ≡ false
n≮n zero = refl 
n≮n (suc n) rewrite n≮n n = refl

-- 反对称性
<-antisym : (x y : ℕ) → (x <ℕ y) ≡ true → (y <ℕ x) ≡ false
<-antisym zero zero ()
<-antisym (suc x) zero ()
<-antisym zero (suc y) p = refl
<-antisym (suc x) (suc y) p rewrite <-antisym x y p = refl

-- 三岐性
infix 20 _or_
_or_ : Bool → Bool → Bool
true or _ = true
false or b = b

<-trichotomy : (x y : ℕ) → (((x <ℕ y) or (x =ℕ y)) or (y <ℕ x)) ≡ true
<-trichotomy zero zero = refl
<-trichotomy (suc x) zero = refl
<-trichotomy zero (suc y) = refl
<-trichotomy (suc x) (suc y) rewrite <-trichotomy x y = refl