Is this proof I wrote correct and what's wrong if not?

Question

I already asked a different question realted to this proof, so I'm sorry for duplicate. Just nobody would answer any more, because the other one has an answer.

I am trying to prove the following statement by structural induction:

foldr f st (xs++yx) = f (foldr f st xs) (foldr f st ys)        (foldr.3)

These are the definitions of foldr:

foldr f st [] = st                                             (foldr.1)
foldr f st x:xs = f x (foldr f st xs)                          (foldr.2)

Now I want to start working on the base case passing the empty list to xs. I have this, but I don't know if it is correct.

foldr f st ([]++ys) = f (foldr f st []) (foldr f st ys)
LHS:
    foldr f st ([]++ys) 
  = foldr f st ys                                              by (++) and by (foldr.1)
RHS:
    f (foldr f st []) (foldr f st ys) = 
  = f st (foldr f st ys)                                       by (foldr.1)
  = foldr f st ys                                              by def of st = 0 and f = (+)

LHS = RHS, therefore base case holds

Now this is what I have for my inductive step:

Assume that:
  foldr f st (xs ++ ys) = f (foldr f st xs) (foldr f st ys)        (ind. hyp)

Show that:
  foldr f st (x:xs ++ ys) = f (foldr f st x:xs) (foldr f st ys)

LHS:
    foldr f st (x:xs ++ ys)  
  = f x (foldr f st (xs++yx))                                      (by foldr.2)
  = f x (f (foldr f st xs) (foldr f st ys) )                       (by ind. hyp)
  = f (f x (foldr f st xs)) (foldr f st ys)                        (by assosiativity of f)

RHS:
    f (foldr f st x:xs) (foldr f st ys) 
  = f (f x (foldr f st xs)) (foldr f st ys)                        (by foldr.2)

LHS = RHS, therefore inductive step holds. End of proof.

I am not sure if this proof is valid. I need some help in determining if it correct and if not - what part of it is not.

Answer 1

Upd: The question was edited multiple times. The following makes sense in revision 1 of the question.

This is not possible to prove. You need f to be a monoid: f a (f b c) == f (f a b) c with f a st == a and f st a == a.

A provable statement would be foldr f st (xs++ys) == foldr f (foldr f st ys) xs

---

Assuming f with st define a monoid, we get the following statements:

foldr f st ([]++ys) ==
     -- by definition of neutral element of list monoid, []++ys == ys
                    == foldr f st ys
     -- by definition of neutral element of `f` monoid, f st a == a
                    == f st (foldr f st ys)
     -- by definition of foldr, (foldr f st []) == st
                    == f (foldr f st []) (foldr f st ys)

Then,

foldr f st ((x:xs)++ys) ==
     -- by associativity of list monoid, (x:xs)++ys == x:(xs++ys)
                    == foldr f st (x:(xs++ys))
     -- by definition of foldr, foldr f st (x:t) == f x (foldr f st t)
                    == f x (foldr f st (xs++ys))
     -- by induction, foldr f st (xs++ys) == f (foldr f st xs) (foldr f st ys)
                    == f x (f (foldr f st xs) (foldr f st ys))
     -- by associativity of monoid `f`, f x (f y z) == f (f x y) z
                    == f (f x (foldr f st xs)) (foldr f st ys)
     -- by definition of foldr, f x (foldr f st t) == foldr f st (x:t)
                    == f (foldr f st (x:xs)) (foldr f st ys)

In essence, this is the proof of the monoid homomorphism. Lists being a free monoid, the homomorphism exists, and is exactly of the form you are seeking - it is the catamorphism for f.

Answer 2

before you start to prove something, check a few examples, e.g.,

xs = ys = [] ; st = True ; f _ _ = False