これは私が正しいと書いた証拠で、そうでなければ何が間違っていますか？ - haskell

私はすでにこの証明に当てはまる別の質問をしたので、重複して申し訳ありません。他の人が答えを持っているので、誰もこれ以上答えないでしょう。

私は構造的帰納法によって次のステートメントを証明しようとしています：

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.

この証明が有効かどうかはわかりません。それが正しいかどうか、正しくない場合は、どの部分が正しくないかを判断するのに助けが必要です。

回答：

回答№1は2

Upd：質問は複数回編集されました。以下は意味があります リビジョン1 質問の。

これを証明することはできません。あなたが必要 f モノイドになる： 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)

本質的に、これはモノイド準同型の証拠です。リストは自由モノイドであり、準同型が存在し、まさにあなたが探している形です-それはのためのカタモルフィズムです f.

---

回答№2については4

何かを証明し始める前に、いくつかの例を確認してください。

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

---