Доказывая foldr е го (хз ++ Я.С.) = F (foldr е го хз) (foldr е й ув)

Question

Я пытаюсь доказать следующее утверждение структурной индукции:

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

Однако я не даже уверен, как определить foldr, поэтому я застрял, поскольку мне не было предоставлено никаких определений. Сейчас я считаю, что foldr может быть определена как

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

Теперь я хочу, чтобы начать работать на базовом случае прохождения пустой список foldr. У меня это есть, но я не думаю, что это правильно.

foldr f st ([]++[]) = f (foldr f st []) (foldr f st []) 
LHS: 
    foldr f st ([]++[]) = foldr f st []      by (++) 
    foldr f st [] = st           by (foldr.1) 
RHS: 
    f (foldr f st []) (foldr f st []) = f st st    by (foldr.1) 
    = st              by definition of identity, st = 0 

LHS = RHS, therefore base case holds 

Теперь это то, что у меня есть для моего шага индукции:

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) (inductive step) 

LHS: 
    foldr f st (x:xs ++ ys) = f x (foldr f st xs) (foldr f st ys) (by foldr.2) 
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) 
    = f x (foldr f st xs) (foldr f st ys) 

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

Я не уверен, если это доказательство является действительным. Мне нужна помощь в определении, правильно ли это, а если нет - в какой части нет.

Answer 1

Во-первых: вы можете найти определение для многих основных функций Haskell через документацию API, доступную в Hackage. Документация для base: here. foldr экспортируется в Prelude, которая имеет связь с its source code:

foldr :: (a -> b -> b) -> b -> [a] -> b 
foldr k z = go 
      where 
      go []  = z 
      go (y:ys) = y `k` go ys 

Это определено, как это по соображениям эффективности; найдите «рабочую обертку». Это эквивалентно

foldr f st [] = st 
foldr f st (y:ys) = f y (foldr f st ys) 

Во-вторых: В вашем желаемом доказательства, тип f должен быть a -> a -> a, который является менее общим, чем a -> b -> b.

Давайте работать через базовый чехол (xs = ys = []).

foldr f st ([]++[]) = f (foldr f st []) (foldr f st []) 
-- Definition of ++ 
foldr f st []  = f (foldr f st []) (foldr f st []) 
-- Equation 1 of foldr 
st     = f st    st 

Это уравнение не выполняется вообще. Чтобы продолжить доказательство, вам придется предположить, что st является идентификатором для f.

В случае с базой данных вы также должны принять, что f является ассоциативным, я считаю. Эти два предположения, объединенные, показывают, что f и st образуют моноид. Вы пытаетесь что-то доказать о foldMap?