You did not specify it, but I assume that :: means linking and use ++ , since this is the operator used in Haskell. To prove this, we carry out induction on xs . First we show that the operator is executed for the base case (ie xs = [] )
foldr fa (xs ++ ys) {- By definition of xs -} = foldr fa ([] ++ ys) {- By definition of ++ -} = foldr fa ys
and
foldr f (foldr fa ys) xs {- By definition of xs -} = foldr f (foldr fa ys) [] {- By definition of foldr -} = foldr fa ys
Now suppose that the induction hypothesis foldr fa (xs ++ ys) = foldr f (foldr fa ys) xs holds for xs and shows that it will hold for the list x:xs .
foldr fa (x:xs ++ ys) {- By definition of ++ -} = foldr fa (x:(xs ++ ys)) {- By definition of foldr -} = x `f` foldr fa (xs ++ ys) ^------------------ call this k1 = x `f` k1
and
foldr f (foldr fa ys) (x:xs) {- By definition of foldr -} = x `f` foldr f (foldr fa ys) xs ^----------------------- call this k2 = x `f` k2
Now, by our inductive assumption, we know that k1 and k2 are equal, therefore
x `f` k1 = x `f` k2
Thus, the proof of our hypothesis.
sabauma
source share