Bound View

最近受到 view 的啟發(?),做了幾個簡單但是還滿有趣的東西,例如可以把 N 拆成某個數字以上跟以下,然後對他作 pattern matching,傳統上會用 if … then … else 不過寫起來到是挺有趣的

data Bound (k : ℕ) : ℕ → Set where
below : (n : ℕ) → (l : ℕ) → (l + n ≡ k) → Bound k n
above : (n : ℕ) → (l : ℕ) → (k + (suc l) ≡ n) → Bound k n

定義是寫如果 n 比 K 小,那 l 代表 k – n ,反過來若是比較大,則說比 k 大多少 n 再加 1 (考慮在 k 跟 n 一樣的時候), 並且附帶證明。再來就是把整數轉成  Bound k ,

toBound : (k n : ℕ) → Bound k n
toBound zero zero = below 0 0 refl
toBound zero (suc n) = above (suc n) n refl
toBound (suc n) n’ with toBound n n’
toBound (suc .(l + n)) n | below .n l refl = below n (suc l) refl
toBound (suc n) .(n + 1) | above .(n + 1) zero refl
= below (n + 1) 0 (CommutativeSemiring.+-comm commutativeSemiring n 1)
toBound (suc n) .(n + suc (suc k)) | above .(n + suc (suc k)) (suc k) refl
= above (n + suc (suc k)) k (sym (m+1+n≡1+m+n n (suc k)) )

想法很簡單,先對 k 作 induction,若是 k = 0, 那麼除了 0 以外都比 k 大;接下來考慮 k = 1 + m 的情況,先看 n 跟 m 之間何者較大,因為若是在 n 小於 m 那麼 n 也會小於 m + 1;若n 大於 m,則考慮兩者之差,若是只差 1 那麼在上界加 1 之後,兩者是一樣大的,剩下的情況仍是 n 大於 k,兩者之差因為上界 + 1 之後,故減少 1。

這樣我就可以寫一個整數的除法並傳回餘數,像這樣:

_/_ : (k n : ℕ) → ℕ × ℕ
n / k with toBound k (suc n)
n / k | below .(suc n) l y = 0 , n
n / k | above .(suc n) l y = suc (proj₁ (l / k)) , proj₂ (l / k)

要保證 termination 的話要另外處理 n 跟 l 之間的關係,不過繼先擱著吧。應用同樣的手法應該寫得出一般化的 Z_n

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s