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

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

这篇文章主要介绍了在 Agda 中定义列表 List 的方法，以及一些和 List 相关的函数和定理证明。

Agda，启动！

参考资料：

《函数式程序设计》课件

《Verified Programming in Agda》

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

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

List 及其定义

1
2
3
4
5
module list where

data List {l} (A : Set l) : Set l where
    []  : List A
    _::_ : (x : A) -> (xs : List A) -> List A

这个 List 的定义和 Haskell 中的 List 定义非常相似，但是 Agda 中的 List 是一个 GADT，因此 Agda 中的 List 可以存储更多的信息。

GADT（Generalized Algebraic Data Type）是一种类型系统，它允许类型构造器的参数类型是任意类型，而不仅仅是类型变量。GADT 也被称为 indexed type，因为类型构造器的参数可以是任意的 index type。

List 的一些函数（基本操作）

这些和 Haskell 中也是相同的，但是要注意的一点是，为了保证我们使用这些函数的时候不会出现错误，我们需要对这些函数进行一些限制，例如 head 函数，我们需要保证 List 不为空，否则就会出现错误。

进行限制的方法就是在使用函数的时候传入一个证明，证明这个 List 不为空。

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
[_] : ∀{l} {A : Set l} -> A -> List A
[ x ] = x :: []

is_empty : ∀{l} {A : Set l} -> List A -> Bool
is_empty [] = true
is_empty _  = false

head : ∀{l} {A : Set l} -> (x : List A) -> (is_empty x ≡ false) -> A
head [] ()
head (x :: xs) _ = x

_++_ : ∀{l} {A : Set l} -> List A -> List A -> List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

map : ∀{l} {A B : Set l} -> (A -> B) -> List A -> List B
map f [] = []
map f (x :: xs) = f x :: map f xs

filter : ∀{l} {A : Set l} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
... | true = x :: filter p xs
... | false = filter p xs

foldr : ∀{l} {A B : Set l} -> (A -> B -> B) -> B -> List A -> B
foldr f z [] = z
foldr f z (x :: xs) = f x (foldr f z xs)

需要注意的是上面的 filter 函数，我们使用了 with 关键字，这个关键字可以让我们在函数中使用 pattern matching，这样我们就可以根据不同的情况进行不同的处理，相当于分类讨论。

而 foldr 也需要注意它是从哪个方向开始折叠的，在这里我更倾向于用从最先添加的元素还是从最后添加的元素开始折叠来描述 foldr，而非从左边开始折叠还是从右边开始折叠；我认为这样可以使描述更加清晰。

List 的一些定理

++ 与序列长度的关系：

1
2
3
length-++ : ∀{l} {A : Set l} -> (xs ys : List A) -> length (xs ++ ys) ≡ (length xs) + (length ys)
length-++ [] ys = refl
length-++ (x :: xs) ys rewrite length-++ xs ys = refl

++ 与 map 的关系：

1
2
3
map-++ : ∀{l} {A B : Set l} -> (f : A -> B) -> (xs ys : List A) -> map f (xs ++ ys) ≡ (map f xs) ++ (map f ys)
map-++ f [] ys = refl
map-++ f (x :: xs) ys rewrite map-++ f xs ys = refl

证明这两个性质都是容易的，按照之前对这些函数的定义展开就行了，他们的思想也都是一样的，都是对 List 进行归纳。

List 的一些定理（续）

length 与 filter 的关系：

1
2
3
4
5
6
7
8
9
postulate 
    ≤ℕ-trans : ∀ {x y z : ℕ} -> x ≤ℕ y ≡ true -> y ≤ℕ z ≡ true -> x ≤ℕ z ≡ true
    ≤ℕ-suc : ∀ (x : ℕ) -> x ≤ℕ suc x ≡ true

length-filter : ∀{l} {A : Set l} -> (p : A -> Bool) -> (xs : List A) -> length (filter p xs) ≤ℕ length xs ≡ true
length-filter p [] = refl
length-filter p (x :: xs) with p x
... | true = length-filter p xs
... | false = ≤ℕ-trans {length (filter p xs)} (length-filter p xs) (≤ℕ-suc (length xs))

这个定理的证明就比较复杂了，我们需要使用到一些之前没有证明的定理，例如 ≤ℕ-trans 和 ≤ℕ-suc，这两个定理的证明是显然的，我们这里就不再赘述了，所以我们这里使用　postulate 来声明这两个定理，我们这样就可以直接把它们像公理一样拿过来使用而不加证明了。

但是并不建议大家使用 postulate 来直接引入过多的公理，它只是一些引入难以在 Agda 中证明的定理的一种方法，或者求方便的一种方法。

如果不是已经被反复证明的定理或者反复验证的公理，我们还是应该尽量避免使用 postulate 来引入它们。

而在 length-filter 的证明中，我们使用了 with 关键字，这里我们也使用了 with 关键字进行分类讨论。

在 ≤ℕ-trans 的使用中，我们得把 length (filter p xs) 放在 {} 中，这是因为　≤ℕ-trans 的第一个参数是一个隐式参数，我们需要在使用的时候显式地传入这个参数，而 {} 就是用来传入隐式参数的，当这些隐式参数不能被 Agda 自动推导出来的时候，我们就需要显式地传入这些参数。

多次 filter 与 filter 的关系：

1
2
3
4
5
filter-idem : ∀{l} {A : Set l} -> (p : A -> Bool) -> (xs : List A) -> filter p (filter p xs) ≡ filter p xs
filter-idem p [] = refl
filter-idem p (x :: xs) with keep (p x)
... | true , p' rewrite p' | p' filter-idem p xs = refl
... | false , p' rewrite p' = filter-idem p xs

这个定理的证明是需要分类讨论的，我们使用了 with 关键字进行分类讨论，而在分类讨论的时候，我们使用了 keep 函数，来在之后使用 p(x) 的值。

我们使用 hole 就可以很容易地证明这个命题了，希望读者自己推导一下。

但是这里的 keep 函数不是一个标准的 Agda 写法，我们只是这样写便于理解，在实践中我们会用到别的方法，请让我请教一下老师之后再来补充这里的内容。

补充修正

使用 Agda 的标准方法，我么需要用到 inspect 关键字，它可以让我们在模式匹配的同时，对模式进行检查，这样我们就可以在之后使用这个模式的值了。

写法可以参考如下的代码：

1
2
3
4
5
6
7
open import Relation.Binary.PropositionalEquality -- to use inspect

filter-idem : ∀{l} {A : Set l} -> (p : A -> Bool) -> (xs : List A) -> filter p (filter p xs) ≡ filter p xs
filter-idem p [] = refl
filter-idem p (x :: xs) with (p x) | inspect (p x)
... | true | [ p' ] rewrite p' | p' filter-idem p xs = refl
... | false | [ p' ] rewrite p' = filter-idem p xs

但是 inspect 的构造器 [_] 会和 List 的构造器 [_] 冲突，所以我们可能需要改一些名字。

小练习

  1. 定义一个　List 的函数　takewhile ，它接受一个　List 和一个　Bool 函数，然后返回这个　List 中满足这个　Bool 函数的最长前缀。

  2. 定义一个　List 的函数　repeat ，它接受一个任意类型的元素和一个　Nat，然后返回一个　List，这个　List 中的元素都是这个任意类型的元素，而这个　List 的长度就是这个　Nat。

  3. 证明一个性质：takewhile p (repeat n a) ≡ repeat n a，其中 p 是一个 Bool 函数，n 是一个 Nat，a 是一个任意类型的元素，当然使用的是你自己定义的 repeat 和 takewhile 函数。

答案可参考文末代码。

最终参考代码

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
module list where

open import natural
open import Data.Bool 
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; step-≡; step-≡˘; _≡⟨⟩_; _∎)

data List {l} (A : Set l) : Set l where
    []  : List A
    _::_ : (x : A) -> (xs : List A) -> List A

[_] : ∀{l} {A : Set l} -> A -> List A
[ x ] = x :: []

is_empty : ∀{l} {A : Set l} -> List A -> Bool
is_empty [] = true
is_empty _  = false

head : ∀{l} {A : Set l} -> (x : List A) -> (is_empty x ≡ false) -> A
head [] ()
head (x :: xs) _ = x

length : ∀{l} {A : Set l} -> List A -> ℕ
length [] = zero
length (x :: xs) = suc (length xs)

_++_ : ∀{l} {A : Set l} -> List A -> List A -> List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

map : ∀{l} {A B : Set l} -> (A -> B) -> List A -> List B
map f [] = []
map f (x :: xs) = f x :: map f xs

filter : ∀{l} {A : Set l} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
... | true = x :: filter p xs
... | false = filter p xs

foldr : ∀{l} {A B : Set l} -> (A -> B -> B) -> B -> List A -> B
foldr f z [] = z
foldr f z (x :: xs) = f x (foldr f z xs)

length-++ : ∀{l} {A : Set l} -> (xs ys : List A) -> length (xs ++ ys) ≡ (length xs) + (length ys)
length-++ [] ys = refl
length-++ (x :: xs) ys rewrite length-++ xs ys = refl

map-++ : ∀{l} {A B : Set l} -> (f : A -> B) -> (xs ys : List A) -> map f (xs ++ ys) ≡ (map f xs) ++ (map f ys)
map-++ f [] ys = refl
map-++ f (x :: xs) ys rewrite map-++ f xs ys = refl

postulate 
    ≤ℕ-trans : ∀ {x y z : ℕ} -> x ≤ℕ y ≡ true -> y ≤ℕ z ≡ true -> x ≤ℕ z ≡ true
    ≤ℕ-suc : ∀ (x : ℕ) -> x ≤ℕ suc x ≡ true

length-filter : ∀{l} {A : Set l} -> (p : A -> Bool) -> (xs : List A) -> length (filter p xs) ≤ℕ length xs ≡ true
length-filter p [] = refl
length-filter p (x :: xs) with p x
... | true = length-filter p xs
... | false = ≤ℕ-trans {length (filter p xs)} (length-filter p xs) (≤ℕ-suc (length xs))

-- filter-idem : ∀{l} {A : Set l} -> (p : A -> Bool) -> (xs : List A) -> filter p (filter p xs) ≡ filter p xs
-- filter-idem p [] = refl
-- filter-idem p (x :: xs) with keep (p x)
-- ... | true , p' rewrite p' | p' filter-idem p xs = refl
-- ... | false , p' rewrite p' = filter-idem p xs

variable
  A : Set

takeWhile : (p : A → Bool) → List A → List A
takeWhile p [] = []
takeWhile p (x :: xs) with p x
... | true = x :: takeWhile p xs
... | false = []

replicate : ℕ → A → List A
replicate zero _ = []
replicate (suc n) a = a :: replicate n a

takeWhile-tt : ∀ (x : A) (xs : List A) (p : A → Bool) → p x ≡ true → takeWhile p (x :: xs) ≡ x :: takeWhile p xs
takeWhile-tt x xs p px rewrite px = refl

prop : (a : A) (n : ℕ)
  → (p : A → Bool)
  → p a ≡ true
    -------------------------------------
  → takeWhile p (replicate n a) ≡ replicate n a
prop a zero p _ = refl
prop a (suc n) p pa rewrite prop a n p pa | takeWhile-tt a (replicate n a) p pa | prop a n p pa = refl