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

## 2008/02/16

foldr-univr : {A B : Set} -> (h : [ A ] -> B) -> forall f e ->
(h [] ≡ e) -> (forall x xs -> h (x ∷ xs) ≡ f x (h xs)) ->
(forall x -> h x ≡ foldr f e x)
foldr-univr h f e base-cond step-cond []       = base-cond
foldr-univr h f e base-cond step-cond (x ∷ xs) =
≡-trans (step-cond x xs)
(≡-cong (f x) (foldr-univr h f e base-cond step-cond xs))

foldr-fusion : {A B C : Set} -> (h : B -> C) -> {f : A -> B -> B} ->
{g : A -> C -> C} -> {e : B} -> (forall x y -> h (f x y) ≡ g x (h y)) ->
forall x -> (h ∘ foldr f e) x ≡ foldr g (h e) x
foldr-fusion {_} {_} {_} h {f} {g} {e} fuse-cond =
foldr-univr (h ∘ foldr f e) g (h e) ≡-refl
(\x xs -> fuse-cond x (foldr f e xs))


--

Labels: ,

yen32/16/2008 11:16 pm 說：