在 Haskell 中的“定理证明”

在 Haskell 里的“定理证明”

这篇文章讲了什么

总结了 Codewars 上面的几道证明题的思想并加以延拓,如果能在看完这篇文章之前/之后解决练习中的题目可能理解会更深刻。

下面是正文


众所周知,Haskell 并没有真正意义上的 dependent type,但通过一些技巧 (利用GADT)可以“模拟”dependent type,并可以通过其证明一些定理。

利用 GADT 模拟 Dependent Type

首先我们需要作为的类型

1
2
data Z
data S n

注意到,这里的 ZS 都只是单纯的类型,你甚至不能构造出相应类型的值出来。

所以我们需要把它们与实际存在的值联系起来

1
2
3
data Nat a where
Zero :: Nat Z
Succ :: Nat a -> Nat (S a)

于是我们有

1
2
(Succ Zero) :: Nat (S Z)
(Succ (Succ Zero)) :: Nat (S (S Z))

这样我们获得了在类型层次上的自然数,并保持了它与实际的值的同构关系。

光有自然数是没有意义的,我们需要赋予它们运算的能力。

那么 Nat nNat m 相加的结果应该是什么呢?

首先它应该是一个 Nat ,其次它的类型应该对应于两数相加的结果。

借助于 GHC 的 Type Family 与 Type Operator 扩展,我们可以定义出合理的类型层面上的自然数的加法与乘法

1
2
3
4
5
6
7
type family (:+:) (n :: *) (m :: *) :: *
type instance Z :+: m = m
type instance S n :+: m = S (n :+: m)

type family (:*:) (n :: *) (m :: *) :: *
type instance Z :*: m = Z
type instance S n :*: m = m :+: (n :*: m)

于是我们便可以定义自然数的加法与乘法

1
2
3
4
5
6
7
8
9
infixl 4 +
(+) :: Nat n -> Nat m -> Nat (n :+: m)
Zero + a = a
(Succ x) + a = Succ (x + a)

infixl 5 *
(*) :: Nat n -> Nat m -> Nat (n :*: m)
Zero * _ = Zero
(Succ x) * m = m + x * m

1
(Succ (Succ Zero)) * (Succ (Succ Zero)) :: Nat (S (S (S (S Z))))

于是我们便可以定义基于类型层面的自然数的 Vec (在类型中包含了长度信息的 List)了

1
2
3
data Vec a n where
VNil :: Vec a Z
VCons :: a -> Vec a n -> Vec a (S n)

长度为 nVec 与长度为 mVec 连接起来之后的长度为 n + m

1
2
3
(++) :: Vec a n -> Vec a m -> Vec a (n :+: m)
VNil ++ ys = ys
VCons x xs ++ y = VCons x (xs ++ y)

把长度为 mVec 重复 n 次之后得到的 Vec 的长度为 n * m

1
2
3
repeat :: Nat n -> Vec a m -> Vec a (n :*: m)
repeat Zero _ = VNil
repeat (Succ x) xs = xs ++ repeat x xs

有了长度信息,我们就能定义类型安全的 headtail

1
2
3
4
5
headV :: Vec a (S n) -> a
headV (VCons x _) = x

tailV :: Vec a (S n) -> Vec a n
tailV (VCons _ xs) = xs

因为 Vec 作为 GADT 的类型在这里受到了第二个类型参数为 S n 的束缚,所以可以保证这里的 Vec 不会是 VNil ,这两个函数都是 完全 的。

借鉴之前定义类型层面上自然数的加法与乘法的思想,我们可以定义相应的减法、求最大值、最小值等。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
type family (:-:) (n :: *) (m :: *) :: *
type instance n :-: Z = n
type instance Z :-: m = Z
type instance S n :-: S m = n :-: m

type family (:^:) (n :: *) (m :: *) :: *
type instance Z :^: n = n
type instance n :^: Z = n
type instance S n :^: S m = S (n :^: m)

type family (:~:) (n :: *) (m :: *) :: *
type instance Z :~: m = Z
type instance n :~: Z = Z
type instance S n :~: S m = S (n :~: m)

(这里使用了 :~::^: 分别代表求最大值和最小值)

于是有

1
2
3
4
zip :: Vec a n -> Vec b m -> Vec (a, b) (n :~: m)
zip VNil _ = VNil
zip _ VNil = VNil
zip (VCons x xs) (VCons y ys) = VCons (x, y) (zip xs ys)

进行简单的定理证明

Haskell 中没有 Prop ,所以我们得从头开始描述“相等”这个概念。

首先定义代表两个类型层面的自然数相等的类型

1
2
3
data Equal a b where
EqZ :: Equal Z Z
EqS :: Equal a b -> Equal (S a) (S b)

借助于 Type Operator 我们可以写成

1
type a === b = Equal a b

相等关系具有自反性

1
2
3
refl :: Nat n -> n === n
refl Zero = EqZ
refl (Succ x) = EqS $ refl x

相等关系具有对称性

1
2
3
symm ::a === b -> b === a
symm EqZ = EqZ
symm (EqS x) = EqS $ symm x

相等关系具有传递性

1
2
3
(<=>) :: a === b -> b === c -> a === c
EqZ <=> EqZ = EqZ
EqS x <=> EqS y = EqS $ x <=> y

因为 Type Operator 也能定义优先级,所以我们给出:

1
2
3
4
infixl 2 ===
infixl 4 :+:
infixr 4 :-:
infixl 5 :*:

来减少括号的个数

加法结合律

那么我们来试着证明一下加法的结合律

1
plusComb :: Nat n -> Nat m -> Nat p -> n :+: (m :+: p) === n :+: m :+: p

我们对 n 进行归纳:当 n 为 0 的时,在加法中的 0 会直接消除,所以使用 refl (m + p) 就好了;当 nS n1 时,把等式两边的 S 用 EqS 提取出来,再使用归纳假设就可以了:

1
2
3
plusComb :: Nat n -> Nat m -> Nat p -> n :+: (m :+: p) === n :+: m :+: p
plusComb Zero p q = refl (p + q)
plusComb (Succ n) m p = EqS $ plusComb n m p

加法交换律

那么再尝试一下稍微困难一点的加法交换律吧

1
plusCommutes :: Nat n -> Nat m -> n :+: m === m :+: n

m 为 0 的时候的证明很平凡,我们需要的是这么一个类型:

1
Nat n -> n :+: Z === n

只需要对 n 进行归纳就好了。

1
2
3
nPlusZero :: a === a -> a === a :+: Z
nPlusZero EqZ = EqZ
nPlusZero (EqS eq) = EqS $ nPlusZero eq

mS m1 时,我们需要的东西的类型为

1
(n :+: S m1) === S (m1 :+: n)

根据归纳法,我们可以得到

1
EqS (plusCommutes n m1) :: S (m1 :+: n) === S (n :+: m1)

借助于相等的传递性,目标变成了

1
(n :+: S m1) === S (n :+: m1)

而这个命题的证明只需要对 n 进行归纳

1
2
3
nPlusSm :: Nat n -> Nat m -> n :+: S m === S (n :+: m)
nPlusSm Zero m = EqS $ refl m
nPlusSm (Succ n) m = EqS $ nPlusSm n m

于是把这些步骤拼起来,就得到了我们最终的证明

1
2
3
plus2 :: Nat n -> Nat m -> n :+: m === m :+: n
plus2 n Zero = symm $ nPlusZero $ refl n
plus2 n (Succ m) = nPlusSm n m <=> symm (EqS $ plus2 m n)

乘法交换律

看了加法我们再来看乘法

1
multCommute :: Nat n -> Nat m -> n :*: m === m :*: n

证明的方法和加法几乎一样,仍然从归纳法入手,对 n 进行归纳。中间需要用到一些引理,比如

1
2
multCommuteS :: Nat n -> Nat m -> m :*: S n === m :+: m :*: n
plusSwap :: Nat a -> Nat b -> Nat c -> a :+: (b :+: c) === b :+: (a :+: c)

等等,这里不再详细说明具体的推导,直接给出实现,有兴趣的同学可以试着自己写一遍

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
equalPlus :: Nat a -> Nat b -> a === b -> Nat c -> a :+: c === b :+: c
equalPlus a b eq Zero = symm (nPlusZero a) <=> eq <=> nPlusZero b
equalPlus a b eq (Succ c) = nPlusSm a c <=> Fuck (equalPlus a b eq c) <=> symm (nPlusSm b c)

equalPlus' :: Nat a -> Nat b -> a === b -> Nat c -> c :+: a === c :+: b
equalPlus' a b eq c = plusCommutes c a <=> equalPlus a b eq c <=> plusCommutes b c

plusSwap' :: Nat a -> Nat b -> Nat c -> a :+: b :+: c === b :+: a :+: c
plusSwap' a b = equalPlus (a + b) (b + a) (plusCommutes a b)

plusSwap :: Nat a -> Nat b -> Nat c -> a :+: (b :+: c) === b :+: (a :+: c)
plusSwap a b c = plusCommute a b c <=> plusSwap' a b c <=> symm (plusCommute b a c)

multCommuteS_1 :: Nat n -> Nat m -> n :+: (m :*: S n) === m :+: (n :+: (m :*: n))
multCommuteS_1 n m = equalPlus' (m * Succ n) (m + m * n) (multCommuteS n m) n <=> plusSwap n m (m * n)

multCommuteS :: Nat n -> Nat m -> m :*: S n === m :+: m :*: n
multCommuteS _ Zero = Refl
multCommuteS n (Succ m) = Fuck $ multCommuteS_1 n m

multCommutes :: Nat n -> Nat m -> n :*: m === m :*: n
multCommutes Zero m = symm $ multNZero m
multCommutes (Succ n) m =
symm
(multCommuteS n m <=> equalPlus' (m * n) (n * m) (multCommutes m n) m)

从自然数说开去

我们在上面定义的“相等”中,只对自然数进行了规定,那么我们怎么表示任何一种东西相等的概念呢?我们需要对 Equal 进行修改。

1
2
3
data Equal a b where
Refl :: Equal a a
Derive :: Equal a b -> Equal (p a) (p b)

Refl 对应之前的 EqZ , Derive 对应 EqS 。从定义上我们就能知道相等关系的自反性。

这样重新定义之后,我们就再也不需要 refl 这个函数了,因为直接使用 Refl 就可以了。

symm 的定义和原来类似,trans 则需要一点小小的修改:

1
2
3
4
5
(<=>) :: a === b -> b === c -> a === c
Refl <=> Refl = Refl
Derive x <=> Refl = Derive $ x <=> Refl
Refl <=> Derive y = Derive $ Refl <=> y
Derive x <=> Derive y = Derive $ x <=> y

为了证明我们定义的 Equal 不仅仅对自然数有用,我们引入了类型层面的 Bool 来增加多样性。

首先是类型定义

1
2
data T
data F

然后是对应的数据类型

1
2
3
data Boolean :: * -> * where
Tr :: Boolean T
Fa :: Boolean F

对于每一个需要参与证明的函数,我们需要在类型上实现一遍。

对于 Boolean 而言,先实现与或非

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
type family Inv (n :: *) :: *
type instance Inv T = F
type instance Inv F = T

type family (||) (n :: *) (m :: *) :: *
type instance T || T = T
type instance F || T = T
type instance T || F = T
type instance F || F = F

type family (&&) (n :: *) (m :: *) :: *
type instance T && T = T
type instance T && F = F
type instance F && T = F
type instance F && F = F

首先证明双重否定律

1
2
3
doubleNeg :: Boolean b -> Inv (Inv b) === b
doubleNeg Tr = Refl
doubleNeg Fa = Refl

要注意的是,这里并不能把两个分支合在一起写,因为它并不能直接把 Inv (Inv b) 推导到 b

然后是德摩根律

1
2
3
4
5
demorgan :: Boolean a -> Boolean b -> Inv (a && b) === Inv a || Inv b
demorgan Tr Tr = Refl
demorgan Tr Fa = Refl
demorgan Fa Tr = Refl
demorgan Fa Fa = Refl

仍然要进行详细的分类讨论,理由同上

同样的,我们还能利用 Type Family 描述一些性质 ,比如自然数的奇偶性

1
2
3
4
5
6
7
8
9
type family IsOdd (n :: *) :: *
type instance IsOdd Z = F
type instance IsOdd (S Z) = T
type instance IsOdd (S (S n)) = IsOdd n

type family IsEven (n :: *) :: *
type instance IsEven Z = T
type instance IsEven (S Z) = F
type instance IsEven (S (S n)) = IsEven n

试着证明一下:

1
oddPlus :: Nat n -> Nat m -> IsOdd (n :+: m) === IsOdd n ^ IsOdd m

因为 IsEvenIsOdd 的递归定义中都有两层的预设,所以我们在用归纳法证明时也需要考虑相应的 3 种情况

  1. nZ
1
oddPlus Zero m :: IsOdd m === (F ^ IsOdd m)

只需要实现这两个函数(它们的实现都是平凡的)

1
2
falseXor :: Boolean b -> b === F ^ b
isodd :: Nat a -> Boolean (IsOdd a)

就有

1
oddPlus Zero x = falseXor $ isodd x
  1. nS Z

m 进行归纳,当 mZS Z 时,结果就是 Refl ,而当 mS (S m') 时,我们需要的类型为

1
oddPlus (Succ Zero) (Succ (Succ x)) :: IsOdd (S n3) === (T ^ IsOdd n3)

同样的,只需要把它拎出去,用归纳法再证一遍就好了

  1. nS (S n')

我们需要的类型为:

1
oddPlus (Succ (Succ x)) y :: IsOdd (n2 :+: m) === (IsOdd n2 ^ IsOdd m)

利用归纳假设就能直接证明了

1
oddPlus (Succ (Succ x)) y = oddPlus x y

还有什么?

注意到我们的很多证明,实际上都只是在类型层面的变化。比如下面这个

1
2
3
4
oddEvenS :: Nat n -> IsOdd n === IsEven (S n)
oddEvenS Zero = Refl
oddEvenS (Succ Zero) = Refl
oddEvenS (Succ (Succ x)) = oddEvenS x

把递归展开的话就能发现它所有情况下的 “值” 都是 Refl ,但我们确不能直接对所有的情况赋 Refl ,因为这个递归是对 Refl 上的类型进行修改的过程。类型的自动推导不会对 type family 中的递归定义进行展开,所以我们还是得自己动手证明一遍。

“性质” 的表示方法

我们使用了 Equal 表示两个类型相等的概念,那么同样的,我们还可以用这种方法描述其它的一元/二元/多元关系,比如我们可以换一种方式表示奇偶性:

1
2
3
4
5
6
7
data Even :: * -> * where
ZeroEven :: Even Z
Add2Even :: Even n -> Even (S (S n))

data Odd :: * -> * where
OneOdd :: Odd (S Z)
Add2Odd :: Odd n -> Odd (S (S n))

或者描述两个自然数的大小关系:

1
2
3
4
data Greater :: * -> * where
GreZ :: Greater (S Z) Z
GreS1 :: Greater x y -> Greater (S x) y
GreS2 :: Greater x y -> Greater (S x) (S y)

Derive 的局限

事实上,我们在 Equal 中定义的 Derive 并不是万能的,比如我们不能这样

1
2
deriveOdd :: Nat n -> n === m -> IsOdd n === IsOdd m
deriveOdd _ eq = Derive eq -- wrong !

报错信息为

1
2
3
Couldn't match typeIsOdd n’ with ‘p0 n’
Expected type: IsOdd n === IsOdd m
Actual type: p0 n === p0 m

它只能对字面量进行推导,比如

1
deriveS :: n === m -> S n === S m

练习

你现在应该可以解决下面几道题目

https://www.codewars.com/kata/singletons

https://www.codewars.com/kata/odd-plus-even-equals-odd-prove-it

https://www.codewars.com/kata/a-plus-b-equals-b-plus-a-prove-it

更多练习

证明乘法交换律

1
multCommute :: Nat n -> Nat m -> Nat p -> n :*: m :*: p === n :*: (m :*: p)

以及更多你能想到的东西