Even or Odd

寫了一段 Agda code，證明一個自然數非奇即偶，並附證明：

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)

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)

  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))

令人不解的是粗體標示部份，我其實想寫成

even-or-odd (suc (suc m)) with (even-or-odd m)
... | \/-IL evenpf = \/-IL (evenPfInd evenpf)
... | \/-IR (oddPf evenpf) = \/-IR (oddPf (evenPfInd evenpf))

這樣就不需要另外寫一個 function even-or-odd-ind。難道是 with 有先天上的限制嗎？

--
用 Aquamacs + Agda2 mode 後有點寫上癮了 XD。

---

原來 2 + n/2 + n/2 = (2+n)/2 + (2+n)/2 是這麼難證明的事情 XD。

其實如果只要達成 copy 的功能的話可以不要做除法，慢慢地一個一個插進去就行了 XD。不過看起來解決除法相關的問題更有意思？XD

--
'/' 是整數除法 XD。