在Haskell中过滤

Question

我有以下问题.

证明对于某些类型的所有有限列表xs和该类型的谓词p和q:

filter p (filter q xs) = filter q ( filter p xs)

我需要一些示例xs列表来解决这个问题吗？或者如何解决这个问题呢？谢谢.

Answer 1

不,提供一些xs样品不是这个练习所需要的.

这个练习要求你证明所有可能的值p,q,xs,等式成立.请注意,存在无限多的可能值p,q,xs,因此强制所有可能的情况是不可行的:必须提供一般的数学证明,利用一些逻辑原理.

只是为了进行比较,假设你被要求2*x+x = 3*x在练习中证明这一点.预期的解决方案不是"好,它坚持x=4和x=10",而忽略了所有其他(无限多)的值x.一个合理的解决方案可能是:"我有x=1*x,所以通过分配法 2*x+x = 2*x + 1*x = (2+1)*x = 3*x",这对所有人都有效 x.

在这种练习中,通常必须通过对某些东西的归纳来进行.在这里,xs看起来是一个很好的归纳候选人.因此,为了证明所有人的方程都是真的xs,有必要证明

1. 等式适用于 xs=[]
2. 如果等式适用于xs=ys(ys任意),那么它必须保持xs=y:ys(y是任意值)

如果你证明1.和2.那么你就完成了.

只是一个额外的提示:因为y是任意的,你不知道它是否满足谓词p和/或q.但是,你可以在那里查看所有可能的四种情况:既有p,q,只有p,只有q,两者都没有.