快瘋了

想證明 pop 跟 push 對於 queue 的操作而言, 會保持等式, 也就是 qs_{1} =_{Q} qs_{2} (即 fs_{1} + rs_{1}^{r} = fs_{2} + rs_{2}^{r}), 而對於同樣的 queue, pop 跟 push 必須產生同樣的結果, 而不管用什麼樣的表示。

但光是把 case split 出來, 就一堆東西了, 到底要怎麼寫啊, 不是這樣的吧 囧

pop-eq : ∀ {n m a} → {xs : Queue a (suc n)}{ys : Queue a (suc m)} → xs ∼ ys → (pop' xs) ∼ (pop' ys)
pop-eq {n} {m} {a} {xs} {ys} qeq with front xs | rear xs | front ys | rear ys | length-sum xs | length-sum ys | length-eq qeq | pop' xs | pop' ys
pop-eq qeq | .0 , [] | .0 , [] | n' , fs' | m0 , rs' | () | pf | refl | xs' | ys'
pop-eq qeq | .0 , [] | suc n , (f ∷ fs) | .0 , [] | .0 , [] | refl | () | refl | xs' | ys'
pop-eq qeq | .0 , [] | suc n , (r ∷ rs) | .0 , [] | .(suc n) , (r' ∷ rs') | refl | refl | refl | xs' | ys' = {!  !}
pop-eq qeq | .0 , [] | suc .(n' + m') , (r ∷ rs) | (suc n') , (f' ∷ fs') | m' , rs' | refl | refl | refl | xs' | ys' = {! !}
pop-eq qeq | suc n , (f ∷ fs) | m , rs | .0 , [] | .(suc (n + m)) , rs' | refl | refl | refl | xs' | ys' = {!  !}
pop-eq qeq | suc n , (f ∷ fs) | m , rs | (suc n') ,(f' ∷ fs') | m' , rs' | refl | pf2 | refl | xs' | ys' = {! !}

push-eq : ∀ {n m a} → {xs : Queue a n}{ys : Queue a m}{x : a} → xs ∼ ys → (push xs x) ∼ (push ys x)
push-eq {n} {m} {a} {xs} {ys} {x} qeq with length-sum xs | length-sum ys | length-eq qeq
push-eq {.(n + m)} {.(n' + m')} {a} {que {n} {m} fs rs} {que {n'} {m'} fs' rs'} {x} qeq | refl | refl | pf with push (que fs rs) x | push (que fs' rs') x
... | xs' | ys' with front xs' | rear xs' | front ys' | rear ys'
... | n1 , fs1 | m1 , rs1 | n2 , fs2 | m2 , rs2 = {! !}

所以我到底要不要改 equality 更為 constructive 一點?但現在想做的是用 constructive 的定義去證明具有 (non-constructive) 抽象的性質 … ~”~

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