怎樣寫出沒有 bug 的程序：程序證明的簡單例子

data Tree : Type -> Type where Leaf : a -> Tree a Branch : a -> Tree a -> Tree a -> Tree aflipTree : Tree a -> Tree aflipTree (Leaf x) = Leaf xflipTree (Branch x l r) = Branch x (flipTree r) (flipTree l)

那麼我要怎麼證明我的 flipTree 是對的呢？之前 @Canto Ostinato 在 紅塵里的Haskell（之三）-- 基於屬性的單元測試 介紹了怎麼根據命題去單元測試，然而，咱們現在用的是 idris，可以在直接去把這個屬性給證明出來！

下面的過程是在 VSCode 加上其 idris 插件的基礎上介紹的，其他編輯器也有類似的插件。

1. 寫出命題

flipTreeSym : (t : Tree a) -> t = flipTree (flipTree t)

2. 我們看下命題的形式，它是關於 Tree 的，那麼可以採用歸納法進行：

flipTreeSym : (t : Tree a) -> t = flipTree (flipTree t)flipTreeSym (Leaf x) = ?g1flipTreeSym (Branch x l r) = ?g2

這兒的 ?g1 和 ?g2 表示還沒寫好的部分，兩個坑。你可以把游標移動上去然後按 Ctrl-Shift-O（Type of），此時在輸出面板上面會顯示：

Idris: Type of g1 a : Type x : a--------------------------------------g1 : Leaf x = Leaf x

這個地方橫線上方的內容表示我們已知的條件，下方是待填的坑應有的類型。

3. 對於 g1 的部分，它的值要求有類型 Leaf x = Leaf x —— 很容易就能看出填入 Refl 就可以了，於是我們按 Ctrl-Shift-S（Proof Search），此時編輯器中內容變為

flipTreeSym : (t : Tree a) -> t = flipTree (flipTree t)flipTreeSym (Leaf x) = ReflflipTreeSym (Branch x l r) = ?g2

很好坑少了一個……

4. 同樣的方法，把游標移動到 ?g2 上面，此時它的類型是：

Idris: Type of g2 a : Type x : a l : Tree a r : Tree a--------------------------------------g2 : Branch x l r = Branch x (flipTree (flipTree l)) (flipTree (flipTree r))

由於我們是用歸納法，那麼此時可以得知有以下兩個命題成立：

flipTreeSym lflipTreeSym r

那麼使用 let 把它們填進去：

flipTreeSym (Branch x l r) = do let recL = flipTreeSym l let recR = flipTreeSym r ?g2

在 ?g2 上面按 Ctrl-Shift-O 顯示的結果是：

Idris: Type of g2 a : Type x : a l : Tree a r : Tree a recL : l = flipTree (flipTree l) recR : r = flipTree (flipTree r)--------------------------------------g2 : Branch x l r = Branch x (flipTree (flipTree l)) (flipTree (flipTree r))

5. 我們已經勝利在望了，現在只要把 recL 和 recR 利用起來就可以填 g2 的坑了——而這個步驟可以使用 rewrite 完成，我們可以進行等量替換：

flipTreeSym (Branch x l r) = do let recL = flipTreeSym l let recR = flipTreeSym r rewrite recL in ?g2

此時 g2「坑」的類型變為了：

Idris: Type of g2 a : Type x : a l : Tree a r : Tree a recL : l = flipTree (flipTree l) recR : r = flipTree (flipTree r) _rewrite_rule : l = flipTree (flipTree l)--------------------------------------g2 : Branch x (flipTree (flipTree l)) r = Branch x (flipTree (flipTree l)) (flipTree (flipTree r))

其中一處已經被替換了。繼續：

flipTreeSym (Branch x l r) = do let recL = flipTreeSym l let recR = flipTreeSym r rewrite recL in rewrite recR in ?g2

此時：

Idris: Type of g2 a : Type x : a l : Tree a r : Tree a recL : l = flipTree (flipTree l) recR : r = flipTree (flipTree r) _rewrite_rule : l = flipTree (flipTree l) _rewrite_rule1 : r = flipTree (flipTree r)--------------------------------------g2 : Branch x (flipTree (flipTree l)) (flipTree (flipTree r)) = Branch x (flipTree (flipTree l)) (flipTree (flipTree r))

太好了，g2 終於變成了 A = A 的形式，可以填上 Refl 了：

flipTreeSym (Branch x l r) = do let recL = flipTreeSym l let recR = flipTreeSym r rewrite recL in rewrite recR in Refl

freeTypeSym 已經填好，它就是一個定理了，保證了我們反轉二叉樹的正確性。

ps. 下面這個就是關於 List 真的是個 Functor 的證明：

map_id : Functor f => f a -> f amap_id = map idinterface Functor f => VerifiedFunctor (f : Type -> Type) where identity : (fa : f a) -> map_id fa = fa dist : (fa : f a) -> (g : b -> c) -> (h : a -> b) -> map (g . h) fa = (map g) . (map h) $ faVerifiedFunctor List where identity [] = Refl identity (x::xs) = let ih = (identity xs) in rewrite ih in Refl dist [] _ _ = Refl dist (x::xs) g h = let ih = (dist xs g h) in rewrite ih in Refl

推薦閱讀：