我寫的這個證明是否正確，如果不是，有什麼不對？

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