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: Apr 23 2024 at 20:15 UTC