$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/11/04

### A Final Remark on scanr

scanr-pf 的 return type 其實可以復用 Logic.Identity module 裡面的 "_≡_" 和 scm 老師定義的 "_⋮_"：

scanr-pf' : {A B : Set} -> (f : A -> B -> B) -> (e : B) -> (xs : List A) ->
List B ⋮ _≡_ ((map (foldr f e) ○ tails) xs)
scanr-pf' f e xs = sub ((foldr (sc f) (e :: [])) xs)
( chain> (map (foldr f e) ○ tails) xs
=== foldr (sc f) (e :: []) xs
by foldr-fusion {_}{_}{_}
{til}{[] :: []}{map (foldr f e)}{sc f} fuse-cond xs
) where
fuse-cond : {A B : Set}{f : A -> B -> B}{e : B} ->
(x : A)(yss : List (List A)) ->
map (foldr f e) (til x yss) ≡ (sc f) x (map (foldr f e) yss)
fuse-cond x (ys :: yss) = refl


subElim : {A : Set}{P : A -> Set} -> A ⋮ P -> A
subElim (sub x _) = x

scanr' : {A B : Set} -> (A -> B -> B) -> B -> List A -> List B
scanr' f e xs = subElim (scanr-pf' f e xs)


--

Labels: ,

scm11/04/2007 7:04 am 說：

(scanr' f e) ≡ ((map (foldr f e) ○ tails) xs)

Josh Ko11/04/2007 10:15 am 說：

> 週五你跟我們談談這個吧？

OK. XD

> 那麼我們用 _⋮_ 把 scanr' 和他的證明綁一起，和傳統方法比較之下有什麼好處呢？