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

## 2007/11/03

### 我敢發誓

max : List Int -> Int
max = foldr (\x y -> if x > y then x else y) (pos 0)

sum : List Int -> Int
sum = foldr _+_ (pos 0)

concat : {A : Set} -> List (List A) -> List A
concat = foldr _++_ []

inits : {A : Set} -> List A -> List (List A)
inits = foldr (\x xss -> [] :: map (_::_ x) xss) ([] :: [])

til : {A : Set} -> A -> List (List A) -> List (List A)
til x (ys :: yss) = (x :: ys) :: ys :: yss

tails : {A : Set} -> List A -> List (List A)
tails = foldr til ([] :: [])


naive-scanr : {A B : Set} -> (A -> B -> B) -> B -> List A -> List B
naive-scanr f e = map (foldr f e) ○ tails


data Indeed {A : Set} : A -> Set where
indeed : (x : A) -> Indeed x

sc : {A B : Set} -> (A -> B -> B) -> A -> List B -> List B
sc f x (y :: ys) = f x y :: y :: ys

scanr-pf : {A B : Set} -> (f : A -> B -> B) -> (e : B) ->
(xs : List A) -> Indeed ((map (foldr f e) ○ tails) xs)
scanr-pf f e xs = subst Indeed
( 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
) (indeed ((foldr (sc f) (e :: [])) 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


indeedElim : {A : Set}{x : A} -> Indeed x -> A
indeedElim (indeed x) = x


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


naive-mss : List Int -> Int
naive-mss = max ○ map sum ○ concat ○ map inits ○ tails


-- mss-pf : (xs : List Int) ->
--            Indeed ((max ○ map sum ○ concat ○ map inits ○ tails) xs)
-- mss-pf xs = subst Indeed ? ?

-- mss : List Int -> Int
-- mss = indeedElim ○ mss-pf  -- this may not typecheck


--

Labels: ,

yen311/04/2007 2:10 am 說：