我写的这个证明是否正确，如果不是，有什么不对？

Question

我已经提出了一个与此证明相关的不同问题，所以我很抱歉重复。只有没有人会回答，因为另一个人有答案。

我试图证明通过结构归纳如下声明：

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

这些foldr相似的定义：

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

现在我要开始的基本情况通过空工作列表到xs。我有这个，但我不知道这是否正确。

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 

现在，这是我对我的归纳步：

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. 

我不知道，如果这个证明是有效的。我需要一些帮助来确定它是否正确，如果不正确 - 哪部分不是。

Answer 1

UPD：此问题已修改多次。以下在问题的revision 1中有意义。

这是不可能证明的。你需要f是一个monoid：f a (f b c) == f (f a b) c与f a st == a和f st a == a。

可证明的声明将是foldr f st (xs++ys) == foldr f (foldr f st ys) xs

---

假设f与st定义一个独异，我们可以得到下面的语句：

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) 

然后，

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) 

在本质上，这是monoid homomorp的证明hism。列表是一个自由幺半群，同态存在，并且正是你正在寻找的形式 - 它是f的变形。

Answer 2

你开始证明什么，查了几个例子，如前，

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