Verified_まほうしょうじょ_in_Agda.02

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

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

这篇文章主要介绍了 Agda 的基本语法，以及 Agda 中的布尔代数和相关的定理证明。

Agda，启动！

参考资料：

《函数式程序设计》课件

《Verified Programming in Agda》

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

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

类型的声明

在 Agda 中，虽然我们的标准库就会包括 Bool、Natural 等类型，但是我们也可以重新出发，自己定义它们。

我们这次就拿最简单的布尔类型来举例。

布尔类型

我们可以这样定义布尔类型：

module boolean where
-- 如果你想要在后面的代码中使用你所定义的类型，你需要在这里将它所在的文件声明为一个模块（模块名需要与你的文件名相同）

data 𝔹 : Set where
  true : 𝔹
  false : 𝔹

-- data 关键字用于定义一个类型，这里我们定义了一个类型 𝔹，它的值有两个，分别是 true 和 false
-- : Set 用于声明类型，这里我们声明 𝔹 是一个 Set 类型
-- 如何书写特殊符号：在 Agda 中，你可以使用 \+<符号名>+space 来书写特殊符号，例如 \+bB+space 就是 𝔹

这样我们就定义了一个布尔类型，它的值有两个，分别是 true 和 false。

关于set的解释：在 Agda 中，所有的类型都是 Set 类型，Set 类型是一个集合，它包含了所有的类型，包括 Set 类型本身。为了加以区别，以后还会看见 Set 有不同的级别，这么做是为了避免出现类似于罗素悖论的问题。

基本的布尔运算

-- not
~_ : 𝔹 → 𝔹
~ true = false
~ false = true

-- and
_&&_ : 𝔹 → 𝔹 → 𝔹
true && true = true
_ && _ = false

-- or
_||_ : 𝔹 → 𝔹 → 𝔹
false || false = false
_ || _ = true

if_then_else_ : ∀ {l}  {A : Set l} → 𝔹 → A → A → A
if true then x else y = x
if false then x else y = y
-- 此处的 l 用于声明类型 A 的级别，这里我们不需要关心它
-- 输入 ∀ 的方式：\+all+space

-- xor 
_⊕_ : 𝔹 → 𝔹 → 𝔹
x ⊕ y = if x then ~ y else y
-- 输入⊕的方式：\+oplus+space

-- nor
_⊗_ : 𝔹 → 𝔹 → 𝔹
x ⊗ y = ~ (x || y)
-- 输入 ⊗ 的方式：\+otimes+space

这些定义都很简单，它们是布尔代数里面最基本的部分，这里就不再赘述。

Agda 里面会有很多的“花花符号”，这些符号都可以在 Agda 的官方文档中找到。

当然为了速度你也可以记住一些常用的符号，或者向 Github Copilot 请教一下。

Agda 中函数的定义方式与 Haskell 中的定义方式类似，但是会有一些不同，例如：

Agda 中函数定义时使用""来表示参数的“位置”，这使得 Agda 中的函数定义更加灵活，就好像上文中的 if_then_else 函数，这使得 Agda 在某种程度上更加接近于自然语言。
Agda 不仅是一种依靠缩进来表示代码结构的“游标卡尺语言”，它还是一种“空格敏感语言”，所有连一起的都会被视为一个整体，而空格隔开的则是不同的部分。

我们来构造一些证明吧！

在 Agda 中，定理的证明是“函数式的”，它把命题看作是一个类型，而证明则是一个函数，这个函数的输入是命题的前提，输出是命题的结论。

我们可以通过类型检查来验证这个证明是否正确。

这就是 Verified Programming 的基本思想和 Agda 的本质逻辑。

上面这句话是我自己的理解，有可能是暴论，如果有错误的地方欢迎指出。

我们来举一些例子：

把命题看作是一个类型，我们可以这样定义：

1	~ ~ true ≡ true

这里的 ≡ 是 Agda 中的等价关系，它的定义如下：

1 2	data _≡_ {A : Set} (x : A) : A → Set where refl : x ≡ x

为什么我们要这样定义等价关系呢？

首先，等式理论中最基本的公理就是自反性，即任何一个元素都等于自己。

而我们上面讲到，Agda 的证明检查是通过类型检查来实现的，所以我们需要把等式看作是一个类型，而自反性就是这个类型的构造器，只有当恒等号的两边完全相同时，这个类型才能被构造出来，我们才能通过类型检查。

这样就保证了我们有一套正确的方法去检查证明的正确性。

现在我们可以写一些简单的证明了：

~~true : ~ ~ true ≡ true
~~true = refl

~~false : ~ ~ false ≡ false
~~false = refl

这里的 refl 就是自反性，我们利用等式理论构造的证明一般都要回归到自反性公理。

Agda 会自动将等号的两边进行化简，所以我们可以直接写出这样的证明。

你可能会发现，这样的证明并没有什么意义，因为它们都是显然成立的，但是这只是一个例子，我们后面会看到更有意义的证明。

模式匹配

在 Agda 中，我们可以使用模式匹配来构造证明，例如：

1
2
3

~~-elim : ∀ (b : 𝔹) → ~ ~ b ≡ b
~~-elim true = refl
~~-elim false = refl

这和在 Haskell 中的情况是类似的。

$\color{red}注意，这种证明类似于分类讨论，你列出的参数的情况需要涵盖整个定义域！$

隐含的参数，自动类型推导

在 Agda 中，我们可以使用隐含的参数来简化我们的代码，例如：

1
2
3

~~-elim : ∀ b → ~ ~ b ≡ b
~~-elim true = refl
~~-elim false = refl

这里我们省略了参数的类型，Agda 会自动推导出参数的类型。

我们还可以进一步让它隐含整个参数，例如：

1
2
3

~~-elim : ∀ {b} → ~ ~ b ≡ b
~~-elim {true} = refl
~~-elim {false} = refl

这里我们省略了参数的名字，Agda 会自动推导出参数的名字。

带有假设的定理证明

举个例子：

||≡ff₂ : ∀ {b1 b2} → b1 || b2 ≡ false → b2 ≡ false
||≡ff₂ {true} ()
||≡ff₂ {false}{true} ()
||≡ff₂ {false}{false} p = refl

这个命题是在说，如果 b1 || b2 ≡ false，那么 b2 也必须等于 false。

其中的 p 是一个对 b1 || b2 ≡ false 的证明；当然，由于我们的 b1 和 b2 是给定的前提，所以你在这里写 refl 也是可以的。

这里就有点像大前提、小前提、结论的三段论式证明了。

在这里，我们使用一个空的元组 () 来表达假设的矛盾（Absurd Pattern），这样我们就可以处理前提不正确的情况了。

小练习：证明以下命题：
1
||≡ff₁ : ∀ {b1 b2} → b1 || b2 ≡ false → b1 ≡ false

$\color{red}出问题了？$

当你将上述内容抄写到你的 agda 文件中时，你可能会发现 Agda 会报错，它会遇见一些 Parse Error。

这是因为你没有指定这些运算符的优先级，你需要在文件开头为他们指定优先级，例如：

-- 优先级 30
infixl 30 ~_ -- not

-- 优先级 20
infixr 20 _⊗_ -- nor

-- 优先级 15
infixl 15 _⊕_ -- xor

-- 优先级 10
infixr 10 _||_ -- or

-- 优先级 5
infixr 5 _&&_ -- and

-- 优先级 0
infix 4 _≡_ -- ≡

这样就可以解决这个问题了。

infix 用来指定运算符的优先级，infixl 和 infixr 用来指定运算符的结合性（左/右），数字越大优先级越高，数字越小优先级越低。

等式证明中的模式匹配

在Agda中，"dot pattern"是一种用于模式匹配的特殊语法。它用于匹配任意类型的参数，并将其绑定到一个无关紧要的标识符上。这在某些情况下非常有用，特别是当您只关心参数的存在而不关心其具体值时。例如：

1 2	\|\|-cong₁ : ∀ {b1 b1' b2} → b1 ≡ b1' → b1 \|\| b2 ≡ b1' \|\| b2 \|\|-cong₁ refl = refl

可以写成：

1 2	\|\|-cong₁ : ∀ {b1 b1' b2} → b1 ≡ b1' → b1 \|\| b2 ≡ b1' \|\| b2 \|\|-cong₁{b1}{.b1’}{b2} refl = refl

这里的 .b1’ 就是一个 dot pattern，它表示我们不关心 b1’ 的值，只关心它的存在。

Rewrite

在 Agda 中，我们可以使用 rewrite 来进行等式的重写，例如：

1
2
3

||-cong₂ : ∀ {b1 b2 b2'} →
b2 ≡ b2' → b1 || b2 ≡ b1 || b2'
||-cong₂ p rewrite p = refl

rewrite 关键字的作用如下：

有一个等式 p : x ≡ y，我们可以使用 rewrite p 来将待证明等式中的所有 x 替换为 y，这种替换是使用模式识别来实现的，但是有时候它可能不够聪明，所以需要具体情况具体分析。

在这个例子中，原来待证的等式是 b1 || b2 ≡ b1 || b2’，我们使用 rewrite p 将 b2 替换为 b2’，这样就得到了 b1 || b2’ ≡ b1 || b2’，此时我们只需要使用 refl 就可以完成证明了。

$\color{red}出问题了？$

当你将上述内容抄写到你的 agda 文件中时，你可能会发现 Agda 会报错，它会遇见 rewrite 的错误。

这是因为 rewrite 关键字需要作用于 Agda 系统内置的等式，所以你需要在你的等号构造器声明后面加上一行声明以告诉 Agda 这个等号构造器绑定了 Agda 系统内置的等号构造器，例如：

1	{-# BUILTIN EQUALITY _≡_ #-}

这样就可以解决这个问题了。

多态

在 Agda 中，我们可以使用类似 Haskell 里面的类型变量，例如：

1
2
3

ite-same : ∀ {b} {A : Set} (x : A) → if b then x else x ≡ x
ite-same {true} x = refl
ite-same {false} x = refl

这里的 A 就是一个类型变量，它可以是任何类型，我们可以使用它来构造多态的证明。

布尔矛盾

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

这个命题是在说，如果 true ≡ false，那么任何类型都可以被证明，这是为了避免 Agda 的类型系统在前提出错时出现问题。

我们之后会使用这个命题来处理一些不可能发生的情况。

小练习：证明以下命题：

1	ite-arg : {A : Set} {B : Set} → (f : A → B) (b : 𝔹) (x y : A) → (f (if b then x else y)) ≡ (if b then f x else f y)

完结撒花！

这篇文章中的源代码参见以下（包括所有的小练习）：

module boolean where

data 𝔹 : Set where
  true : 𝔹
  false : 𝔹

-- 优先级 30
infixl 30 ~_ -- not

-- 优先级 20
infixr 20 _⊗_ -- nor

-- 优先级 15
infixl 15 _⊕_ -- xor

-- 优先级 10
infixr 10 _||_ -- or

-- 优先级 5
infixr 5 _&&_ -- and

-- 优先级 0
infix 4 _≡_ -- ≡

-- not
~_ : 𝔹 → 𝔹
~ true = false
~ false = true

-- and
_&&_ : 𝔹 → 𝔹 → 𝔹
true && true = true
_ && _ = false

-- or
_||_ : 𝔹 → 𝔹 → 𝔹
false || false = false
_ || _ = true

if_then_else_ : ∀ {l}  {A : Set l} → 𝔹 → A → A → A
if true then x else y = x
if false then x else y = y

-- xor 
_⊕_ : 𝔹 → 𝔹 → 𝔹
x ⊕ y = if x then ~ y else y

-- nor
_⊗_ : 𝔹 → 𝔹 → 𝔹
x ⊗ y = ~ (x || y)


data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

||≡ff₂ : ∀ {b1 b2} → b1 || b2 ≡ false → b2 ≡ false
||≡ff₂ {true} ()
||≡ff₂ {false}{true} ()
||≡ff₂ {false}{false} p = refl

||≡ff₁ : ∀ {b1 b2} → b1 || b2 ≡ false → b1 ≡ false
||≡ff₁ {true} ()
||≡ff₁ {false}{true} ()
||≡ff₁ {false}{false} p = refl

||-cong₁ : ∀ {b1 b1' b2} → b1 ≡ b1' → b1 || b2 ≡ b1' || b2
||-cong₁ refl = refl

||-cong₂ : ∀ {b1 b2 b2'} → b2 ≡ b2' → b1 || b2 ≡ b1 || b2'
||-cong₂ p rewrite p = refl

ite-same : ∀ {b} {A : Set} (x : A) → if b then x else x ≡ x
ite-same {true} x = refl
ite-same {false} x = refl

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

ite-arg : {A : Set} {B : Set} → (f : A → B) (b : 𝔹) (x y : A) → (f (if b then x else y)) ≡ (if b then f x else f y)
ite-arg f true x y = refl
ite-arg f false x y = refl