間違ってるのが一応出来たけれども

filter : {X : Set0} -> (X -> Bool) -> List X -> List X
filter p [] = []
filter p (x :: xs) with p x
... | true = filter p xs -- x :: (filter p xs)
... | false = filter p xs

filterをこう書き直して、つまり、[]しか返さないんですけれども、これでfilterproofを書き上げてみようとしてみました。

が、エラーが分け分からなくて、もう分け分からないからそろそろ豆タンクちゃん見て癒されないと酷いと思ったあたりで

filter : {X : Set0} -> (X -> Bool) -> List X -> List X
filter p [] = []
filter p (x :: xs) = filter p xs

こう書き直してみたら出来た。

多分"with p x"に相当する部分をfilterproof内に書いて上げないといけないんだと思う。

そういう事に気付けたのも含めてこれはまぁ良かったかなーと思うものの

filterproof : {X : Set0} {p : (X -> Bool)} {xs : List X}  -> (length (filter p xs)) NatPair (length xs)
filterproof {X} {p} {xs} with xs
...

こんな感じで証明しちゃってて、ういーーー。filterproofの返値が利用出来ない感じで、

filterproof : {X : Set0} {p : (X -> Bool)} {xs : List X}  -> (filter p xs) ListPair xs
filterproof {X} {p} {xs} with xs
...

で書き直す。起きてから。寝ます。寝て無いです。