dual foldr (:) [] == reverse

Duality.hs

定義
(f. g) x = f (g x) -- .
(f. g. h) x = f (g (h x)) -- ..
dual f = dual. f. dual -- dual f
dual xs = reverse (map dual xs) -- dual list
foldr _ z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
map _ [] = []
map f (x:xs) = f x: map f xs

法則
dual. dual == id -- dual則
reverse. reverse == id -- reverse則
reverse. map f == map f. reverse -- reverse. map交換則
map id == id -- map id則
map f. map g == map (f. g) -- map合成
f == \x xs->f x xs (但しf::a->b->c) -- λ
foldr (\x xs->xs++[x]) [] xs == reverse xs -- foldr-reverse(下部で帰納法で証明)

===

左辺
dual foldr (:) [] xs
(dual. foldr. dual) (:) [] xs -- dual f
(dual. foldr (dual (:))) [] xs -- .
(dual. foldr (dual. (:). dual)) [] xs -- dual f
(dual (foldr (dual. (:). dual)) []) xs -- .
(dual. (foldr (dual. (:). dual)) []. dual) xs -- dual f
dual (((foldr (dual. (:). dual)) []) (dual xs)) -- .
dual (foldr (\x xs->xs++[x]) [] (dual xs)) -- ※A
reverse xs -- ※C
右辺

※A
dual. (:). dual
\x xs->(dual. (:). dual) x xs -- λ
\x xs->(dual ((:) (dual x))) xs -- .
\x xs->(dual. ((:) (dual x)). dual) xs -- dual f
\x xs->dual (((:) (dual x)) (dual xs)) -- ..
\x xs->dual (dual x: dual xs) -- 適用
\x xs->reverse (map dual (dual x: dual xs)) -- dual list
\x xs->reverse (dual (dual x): map dual (dual xs)) -- map
\x xs->reverse (x: map dual (dual xs)) -- dual則
\x xs->reverse (x: reverse xs) -- ※B
\x xs->reverse (reverse xs)++[x] -- reverse
\x xs->xs++[x] -- reverse則

※B
map dual (dual xs)
map dual (reverse (map dual xs)) -- dual list
reverse (map dual (map dual xs)) -- reverse. map交換則
reverse (map (dual. dual) xs) -- map合成
reverse (map id xs) -- dual則
reverse xs -- map id則

※C
dual (foldr (\x xs->xs++[x]) [] (dual xs))
dual (reverse (dual xs)) -- foldr-reverse
dual (reverse (reverse (map dual xs))) -- dual list
dual (map dual xs) -- reverse則
dual (map dual xs) -- dual list
reverse (map dual (map dual xs)) -- dual list
reverse (map (dual. dual) xs) -- map合成
reverse (map id xs) -- dual則
reverse xs -- map id則

===

foldr-reverseについて (foldr (\x xs->xs++[x]) [] xs == reverse xsを証明)
(1) xs==[]の時
foldr (\x xs->xs++[x]) [] []
[] -- foldr
reverse [] -- reverse
ok
(2)foldr (\x xs->xs++[x]) [] xs == reverse xs が成立と仮定
foldr (\x xs->xs++[x]) [] (x:xs)
foldr (\x xs->xs++[x]) [] xs++[x] -- foldr
reverse xs++[x] -- 仮定
reverse xs++reverse [x] -- reverse
reverse ([x]++xs) -- reverse分配(略)
reverse (x:xs) -- ++(略)
ok
(1)(2)より証明された