View for (mod n)

延續上一個 Bound View, 稍微修改之後, 再配合 \mathbb{Z}_n 結構, 可以得到一個對 \mathbb{N} 的模數 n 的 view。首先修改 Bound 為

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

亦即將 below 的條件改為 n < k,而 above 則是 n \geq k。toBound 根據此稍作修改。接下來是 \mathbb{Z}_n 的結構定義,因為要作成 \mathbb{N} 的 view,index 上放入自然數。

data Z (k : ℕ) : ℕ → Set where
 cl : (m : ℕ){m<k : (suc m) ≤ k} (n : ℕ) → Z k (m + (n * k))

接下來就是將自然數轉成 \mathbb{Z}_n

toK : (k n : ℕ){k≠0 : False (k ≟ 0)} → Z k n
toK k n with toBound k n
toK ._ n | below .n l refl  =
 subst (Z (l + suc n))
  (CommutativeSemiring.+-comm commutativeSemiring n 0)
  (cl n {(n≤m+n l (suc n))} 0)
toK zero zero {()} | _
toK (suc n) zero | above .0 l eq with trans
 (CommutativeSemiring.+-comm commutativeSemiring (suc n) l)
 eq
... | ()
toK k  (suc n) {k≠0} | above ._ _ _ with toK k n {k≠0}
toK k  (suc ._) | above ._ _ _ | cl m _ with (suc m) ≟ k
toK k  (suc ._) | above ._ _ _ | cl m {m<k} n | no ¬p =
 cl (suc m) {lemma ¬p m<k} n
toK ._ (suc ._) | above ._ _ _ | cl _ n   | yes refl =
 cl 0 {s≤s z≤n} (suc n)

原本在 Ulf 的導覽文件中,展示的 toParity 就變成 toK 2 了,需要 proof term 的部份有 False (k ≟ 0) 直接算出來,用起來除了 pattern matching 的時候要多比對幾次把所有的項次展開以外,都一樣。
記得剛學 Agda 的時候也想過這個問題,不過那時候連該怎麼定義 \mathbb{Z}_n 都想不出來,算是有進步吧 XD

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