filter_challenge_2

夏休みに「software foundation」を読み返している。もう読み始めて何年たってるのか。前読んでた時から半年とか空くと全部忘れてるのでまた読み直しが発生して、とかの悪循環。どんどん後退している。年も食ってるし。

以前の自分の解答で諦めてたらしい(諦めたことも忘れている。)filter_challenge_2が出来たっぽいので久し振りにBLOGを書く。

問題はこうだ。

[filter] の振る舞いに関する特性を別の切り口で表すとこうなります。
「[test] の結果が [true] なる要素だけでできた、リスト [l] のすべての部分リストの中で、[filter test l] が最も長いリストである。」これを形式的に記述し、それを証明しなさい。

filterは各要素が満たすべき関数とリストを渡して、リストから関数のチェックをパスする要素だけ集めたリストを返すよくあるやつ。

今回も最初案の定全く分からなかったが、問題を分割して考えたら上手く行けそうな感じがした。

まず、

「[test] の結果が [true] なる要素だけでできた、リスト [l] のすべての部分リスト

これを形式化、つまり上記のリスト全てを構成する方法を考える。
二つの空リストから出発して、各リストに要素を上記の条件を満たすように加えていくのである。そうすれば、上記のリストを全て構成することが出来る。
このやりかたは、偶数を構成する命題や、二つの数字を比較する関係や正規表現などなどで、IndProp.vの章まででいろいろやっているのでなんとなく分かる。

Inductive part_test_list {X}  (test : (X -> bool)) : list X -> list X -> Prop :=
| ptl_nil : part_test_list test [] []
| ptl_true : forall l1 l2 x, part_test_list test l1 l2 -> test x = true -> part_test_list test (x :: l1) (x :: l2)
| ptl_any : forall l1 l2 x, part_test_list test l1 l2 -> part_test_list test (x::l1) l2.

最初testを各枝のforallに入れていて訳分かんなくなった。

つぎに、「〜が最も長い」ということを形式化する。

なんかのリストの集合の要素lの長さは、HOGEの長さを越えない。

forall l, なんかlが満たすべき属性 ->  length l <= length HOGE.

という感じで行けそう？

という感じで以下になる。

Lemma filter_challenge_2 : forall X test (l1 l2 : list X),
  part_test_list test l1 l2 -> (length l2) <= (length (filter test l1)).
Proof.
Admitted.

解答をネットに上げてくれるな。と書いてあるので最後までは書かない。
証明はそんなに難しいものではない。普通の帰納法で行ける。