Фильтр в Haskell

Question

У меня есть следующая проблема.

Доказать, что для всех конечных списков хз некоторого типа и предикаты р и д на этом типе:

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, ни.