临时定义¶

```data Parity : Nat -> Type where
Even : Parity (n + n)
Odd  : Parity (S (n + 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}
```

```viewsbroken.idr:12:10: 在解析 ViewsBroken.parity 的右侧时：
Parity (plus (S j) (S j))

Parity (S (S (plus j j)))

plus (S j) (S j)
与
S (S (plus j j))
的类型不匹配
```

临时定义¶

• 成型（Prototyping） 时，它可在所有的证明细节结束前测试程序。
• 阅读 程序时，推迟证明的细节通常会让过程更清晰，避免读者从底层算法中分心。

```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}
```

```*views> :m
Global holes:
[views.parity_lemma_2,views.parity_lemma_1]
```

```*views> :p views.parity_lemma_1

---------------------------------- (views.parity_lemma_1) --------
{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))

-views.parity_lemma_1>
```

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

```-views.parity_lemma_1> compute

---------------------------------- (views.parity_lemma_1) --------
{hole0} : (j : Nat) -> (Parity (S (plus j (S j)))) -> Parity (S (S (plus j j)))
```

```-views.parity_lemma_1> intros

j : Nat
value : Parity (S (plus j (S j)))
---------------------------------- (views.parity_lemma_1) --------
{hole2} : Parity (S (S (plus j j)))
```

```-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)

j : Nat
value : Parity (S (plus j (S j)))
---------------------------------- (views.parity_lemma_1) --------
{hole3} : Parity (S (plus j (S j)))
```

`sym` 是一个在库中定义的函数，它可以反转重写的顺序：

```sym : l = r -> r = l
sym Refl = Refl
```

```*views> show (natToBin 42)
"[False, True, False, True, False, True]" : String
```

暂且相信¶

Idris 在编译程序前需要完成证明（尽管在提示符中求值可以无需详细证明）。然而有时候， 特别在成型时，不去完成证明反而更容易。在尝试证明它们之前就测试程序甚至可能会更好， 如果测试找到了一个错误，你就会知道最好不要花时间去证明某些东西了！

```believe_me : a -> b
```

```views.parity_lemma_2 = proof {
intro;
intro;
exact believe_me value;
}
```

`exact` 策略允许我们为该证明提供一个确切的值。在本例中，我们断言给出的值是正确的。

示例：二进制数¶

```data Binary : Nat -> Type where
BEnd : Binary Z
BO : Binary n -> Binary (n + n)
BI : Binary n -> Binary (S (n + n))
```

`BO``BI` 接受一个二进制数作为其参数并立即将它左移一位， 然后再加零或一作为新的最低位。索引 `n + n``S (n + n)` 描述了左移后再相加的结果与该数值的意义相同。它会产生低位在前的表示。

```natToBin : (n:Nat) -> Binary n
```

`Parity` 视角让定义变得相当简单：把数折半其实就是进行一次右移，尽管我们需要在 Odd 的情况下使用临时定义：

```natToBin : (n:Nat) -> Binary n
natToBin Z = BEnd
natToBin (S k) with (parity k)
natToBin (S (j + j))     | Even  = BI (natToBin j)
natToBin (S (S (j + j))) | Odd  ?= BO (natToBin (S j))
```

Odd 情况的问题与 `parity` 定义中的相同，其证明过程也一样：

```natToBin_lemma_1 = proof {
intro;
intro;
rewrite sym (plusSuccRightSucc j j);
trivial;
}
```

```main : IO ()
main = do putStr "Enter a number: "
x <- getLine
print (natToBin (fromInteger (cast x)))
```

```Show (Binary n) where
show (BO x) = show x ++ "0"
show (BI x) = show x ++ "1"
show BEnd = ""
```