# 定理证明¶

## 相等性¶

Idris 可以声明命题的相等性，陈述并证明有关程序的定理。 相等性是内建的，不过这里给出其概念上的定义：

```data (=) : a -> b -> Type where
Refl : x = x
```

```fiveIsFive : 5 = 5
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl
```

## 空类型¶

```disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
where
disjointTy : Nat -> Type
disjointTy Z = ()
disjointTy (S k) = Void
```

```void : Void -> a
```

## 简单定理¶

```plusReduces : (n:Nat) -> plus Z n = n
```

```plusReduces n = Refl
```

```plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong (plusReducesZ k)
```

`cong` 是库中定义的一个函数，它指明相等性也适用于函数应用：

```cong : {f : t -> u} -> a = b -> f a = f b
```

```plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong (plusReducesS k m)
```

Idris 提供了交互式编辑的能力，它可以帮助构造证明。关于在编辑器中交互式构造证明的更多详情， 参见 Theorem Proving

## 实践中的证明¶

```parity : (n:Nat) -> Parity n
```

```parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j)))     | Even = Even {n=S j}
parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}
```

```在按照期望的类型
Parity (S (S (j + j)))

Parity (S j + S j) （Even 的类型）

Parity (S (S (plus j j))) （期望的类型）

```

```parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j)))     | Even = let result = Even {n=S j} in
?helpEven
parity (S (S (S (j + j)))) | Odd  = let result = Odd {n=S j} in
?helpOdd
```

```  j : Nat
result : Parity (S (plus j (S j)))
--------------------------------------
helpEven : Parity (S (S (plus j j)))
```

```helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
```

`rewrite ... in` 语法允许你根据相等性证明来改写它，以此改变表达式需要的类型。 在这里，我们使用了 `plusSuccRightSucc`，其类型如下：

```plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
```

```helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = ?helpEven_rhs
```

```  j : Nat
p : Parity (S (plus j (S j)))
--------------------------------------
helpEven_rhs : Parity (S (S (plus j j)))
```

```helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs
```

```  j : Nat
p : Parity (S (plus j (S j)))
_rewrite_rule : S (plus j j) = plus j (S j)
--------------------------------------
helpEven_rhs : Parity (S (plus j (S j)))
```

`Odd` 的情况使用 `rewrite` 和另一个辅助函数，我们可以完成 `parity`

```helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})
```

`rewrite` 的完整细节超出了本入门教程的范围，不过定理证明教程 （见 Theorem Proving）中覆盖了它。

## 完全性检查¶

```-- 利用部分定义的「hd」
empty1 : Void
empty1 = hd [] where
hd : List a -> a
hd (x :: xs) = x

-- 不会终止
empty2 : Void
empty2 = empty2
```

Idris 会在内部检查所有函数的完全性，我们可在提示符中用 `:total` 命令来检查。 我们会看到上面的两个定义都是不完全的：

```*Theorems> :total empty1

不完全，因为有遗漏的情况
*Theorems> :total empty2

```

```total empty2 : Void
empty2 = empty2
```
```对 ./theorems.idr 进行类型检查
theorems.idr:25:empty2 可能不完全，由于递归路径 empty2
```

```*theorems> :total disjoint
Total
```

• 覆盖所有可能的输入
• 良基 的 — 即，当一系列（可能互相）递归的调用再次到达 `f` 时，它必须能够表明其参数之一已经递减。
• 使用的数据类型必须 严格为正（strictly positive）
• 没有调用任何不完全的函数

### 完全性的指令与编译器参数¶

• 使用 `--total` 编译器参数。
• 为源文件添加 `%default total` 指令。在这之后的所有定义都会要求为完全的， 除非显式地标记为 `partial`

`%default total` 声明 之后 的所有函数都会被要求是完全的。与此相应， `%default partial` 声明之后的要求则被放宽。

### 完全性的提示¶

```qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (filter (< x) xs) ++
(x :: qsort (filter (>= x) xs))
```

prelude 中定义的 `assert_smaller` 旨在解决这个问题：

```assert_smaller : a -> a -> a
assert_smaller x y = y
```

```total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
```

```assert_total : a -> a
assert_total x = x
```

 [1] Timothy G. Griffin. 1989. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ‘90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714 http://doi.acm.org/10.1145/96709.96714