## Stream: Beginner Questions

### Topic: prove function fusion

#### Shaobo He (Apr 16 2022 at 00:21):

Hello, I just started to learn Isabelle and am trying to prove function fusion of the algorithm design with Haskell book. The theorem I have is as follows,

``````lemma master_fusion : "h(f x y) = g x (h y) ⟹ h (foldr f xs e) = foldr g xs (h e)"
apply(induction xs arbitrary: x y)
apply(auto)
``````

I got stuck after the second apply. The goal is as follows,

``````goal (1 subgoal):
1. ⋀a xs x y.
(⋀x y. h (f x y) = g x (h y) ⟹ h (foldr f xs e) = foldr g xs (h e)) ⟹
h (f x y) = g x (h y) ⟹ h (f a (foldr f xs e)) = g a (foldr g xs (h e))
``````

I think I'm close to complete the proof: if I can use the premise of one of the implications to rewrite `h (f a (foldr f xs e)) = g a (foldr g xs (h e))` into `g a (h (foldr f xs e))` and use the induction assumption in the first implication to rewrite the previous result. I was wondering if you could give me any pointers? Thanks!

#### Simon Roßkopf (Apr 16 2022 at 03:04):

I do not think your lemma holds in the current form and quickcheck also finds a counterexample. I think you want your assumption to hold for all `x`,`y`, but currently it only requires there to be such `x`,`y`.

The following goes through:

``````lemma master_fusion:
"(⋀x y . h(f x y) = g x (h y)) ⟹ h (foldr f xs e) = foldr g xs (h e)"
by(induction xs ) (auto)
``````

Last updated: Sep 22 2023 at 08:19 UTC