# Exercise 3.5
List paramorphism operator:
paraL ∷ (α → (List α, β) → β) → β → List α → β
paraL f e Nil = e
paraL f e (Cons x xs) = f x (xs, paraL f e xs)
insert as a paraL instance:
insertPara y = paraL f (wrap y)
where
f x (xs, ys) = if y < x
then Cons y (Cons x xs)
else Cons x ys
We will prove that insert y xs = insertPara y xs for all finite lists
xs by structural induction on xs.
Case Nil:
insertPara y Nil
= { insertPara.1 }
paraL f (wrap y) Nil
= { paraL.1 }
wrap y
= { insert.1 }
insert y Nil
which establishes the case.
Case Cons x xs:
insertPara y (Cons x xs)
= { insertPara.1 }
paraL f (wrap y) (Cons x xs)
= { paraL.2 }
f x (xs, paraL f (wrap y) xs)
= { insertPara, f.1 }
if y < x
then Cons y (Cons x xs)
else Cons x (paraL f (wrap y) xs)
Subcase y < x:
= { subcase def., if }
Cons y (Cons x xs)
= { insert.2, subcase def. }
insert y (Cons x xs)
Subcase y ≥ x:
= { subcase def., if }
Cons x (paraL f (wrap y) xs)
= { hypothesis }
Cons x (insert y xs)
= { insert.2, subcase def. }
insert y (Cons x xs)
which establishes the case. ∎