copy of Braun Tree

我早上（或許是中午 XD）起床再為這些 code 加註，現在快睡著了 XD。

---

首先宣告這個 module 並引入需要的 library modules。

module Braun where

open import Logic.Base
open import Logic.Identity
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool

接著是題目對 Braun tree 的定義。

Parity = Bool

parity : Parity -> Nat
parity false = 0
parity true  = 1

data Braun (A : Set) : Nat -> Set where
  nul : Braun A 0
  bin : {n : Nat} -> A -> (p : Parity) ->
          Braun A (parity p + n) -> Braun A n ->
          Braun A (1 + parity p + (n + n))

要把一個自然數除以 2 很簡單：每找到兩個 suc 就換成一個。

half : Nat -> Nat
half (suc (suc n)) = suc (half n)
half _             = zero

兩個命題 isEven n 和 isOdd n 分別宣稱 n 是偶數或奇數。前者的證明是 by induction，後者則是證明「減 1 後是偶數」。

data isEven : Nat -> Set where
  evenPfBase : isEven zero
  evenPfInd  : {n : Nat} -> isEven n -> isEven (suc (suc n))

data isOdd : Nat -> Set where
  oddPf : {n : Nat} -> isEven n -> isOdd (suc n)

接著有個 function 宣稱一個自然數非奇即偶，並附上證明。因為在 inductive step 要對 even-or-odd (n-2) 做 pattern matching 但 "with" construct 沒辦法運作，所以只好另外寫一個 function 接收額外的參數，然後讓這兩個 functions 彼此呼喚。

mutual

  even-or-odd : (n : Nat) -> (isEven n) \/ (isOdd n)
  even-or-odd zero = \/-IL evenPfBase
  even-or-odd (suc zero) = \/-IR (oddPf evenPfBase)
  even-or-odd (suc (suc m)) = even-or-odd-ind (even-or-odd m)
  -- Why didn't "with" work?
  -- even-or-odd (suc (suc m)) with (even-or-odd m)
  -- ... | \/-IL evenpf = \/-IL (evenPfInd evenpf)
  -- ... | \/-IR (oddPf evenpf) = \/-IR (oddPf (evenPfInd evenpf))

  even-or-odd-ind : {m : Nat} -> (isEven m) \/ (isOdd m) ->
                    (isEven (suc (suc m))) \/ (isOdd (suc (suc m)))
  even-or-odd-ind (\/-IL evenpf) = \/-IL (evenPfInd evenpf)
  even-or-odd-ind (\/-IR (oddPf evenpf)) = \/-IR (oddPf (evenPfInd evenpf))

接著是一些關於 half 的性質。首先有兩個定理：「若能證明 n 是偶數，則 (n + 1)/2 = n/2」以及「若能證明 n 是奇數，則 (n + 1)/2 = 1 + n/2」。舉第一個定理的證明為例：如果 n = 0 顯然成立（by reflexivity）。假設對 m 成立（half (suc m) ≡ half m），欲證明對 m + 2 也成立，即 half (suc (suc (suc m))) ≡ half (suc (suc m))。依 half 的定義，上式可化簡為 suc (half (suc m)) ≡ suc (half m)，即對 induction hypothesis 的等式兩邊都加 1。因此用 congruence（x ≡ y implies f x ≡ f y）把 suc 套到兩邊就可以了。

halfevensuc : {n : Nat} -> isEven n -> half (suc n) ≡ half n
halfevensuc evenPfBase = refl
halfevensuc (evenPfInd indHyp) = cong suc (halfevensuc indHyp)

halfoddsuc : {n : Nat} -> isOdd n -> half (suc n) ≡ suc (half n)
halfoddsuc (oddPf evenpf) = cong suc (sym (halfevensuc evenpf))

接著我們證明 2 + n/2 + n/2 = (n + 2)/2 + (n + 2)/2 for all n。欲證式子的精神是 (suc m) + n ≡ suc (m + n)，這就是 Data.Nat.Properties module 裡面的 +suc，再用 symmetry 和 congruence 湊一湊就可以得到。

suc²2half : (n : Nat) ->
  suc (suc (half n + half n)) ≡ half (suc (suc n)) + half (suc (suc n))
suc²2half n = cong suc (sym (+suc (half n) (half n)))

接著兩個定理告訴我們把兩個 n/2 加起來後和 n 的關係為何。偶數時兩者剛好相等，奇數時兩倍的 n/2 會比 n 少 1。後者的證明用到 substitutivity（是這樣拼嗎？）：n+1 是奇數則 n 是偶數，用第一個定理我們就有 half n + half n ≡ n，現在要證到 suc (half (suc n) + half (suc n)) ≡ suc n。對於偶數我們知道 half (suc n) ≡ half n，所以 half (suc n) + half (suc n) ≡ half n + half n。這裡就用到 Max 談 equational logic 時一個基礎的技巧：把要證的式子寫成 x + x ≡ half n + half n，然後由 reflexivity 知道 x 代 half n 時顯然成立，又知道 half (suc n) ≡ half n，所以 x 代 half (suc n) 時亦成立。

doubleEven : {n : Nat} -> isEven n -> (half n + half n) ≡ n
doubleEven evenPfBase = refl
doubleEven {suc (suc n)} (evenPfInd evenpf) =
  trans (sym (suc²2half n)) (cong suc (cong suc (doubleEven evenpf)))

doubleOdd : {n : Nat} -> isOdd n -> suc (half n + half n) ≡ n
doubleOdd {suc n} (oddPf evenpf) =
  cong suc (trans
    (subst (\x -> x + x ≡ half n + half n) (halfevensuc evenpf) refl)
    (doubleEven evenpf))

最後抵達我們要的 copy function。以「n+1 為偶數」的分支（即最後一個 pattern）為例：n+1 為偶數代表 n 是奇數，我們使用 bin constructor 並遞迴呼叫 copy 造一棵符合條件的 Braun tree，但這棵 Braun tree 的 type 是 Braun A (suc (suc (half n + half n)))，而最後要的 type 是 Braun A (suc n)，所以我們必須證明 suc (suc (half n + half n)) ≡ suc n 之後用 substitutivity 把前者轉換為後者。而這個證明正好可以對 doubleOdd 做些調整而得到。

令人不解的是 Agda interpreter 告訴我 "[Braun.copy] does NOT termination check"，這可能得問問 scm 老師嘍。

-- [Braun.copy] does NOT termination check; why?
copy : {A : Set} -> A -> (n : Nat) -> Braun A n
copy _ zero = nul
copy {A} a (suc n) with even-or-odd n
... | \/-IL evenpf =
  subst (\x -> Braun A x)
        (cong suc (sym (doubleEven evenpf)))
        (bin a false (copy a (half n)) (copy a (half n)))
... | \/-IR oddpf =
  subst (\x -> Braun A x)
        (cong suc (sym (doubleOdd oddpf)))
        (bin a true (copy a (suc (half n))) (copy a (half n)))

--
寫到後來跟寫 Lisp 差不多 XD。