Filter の Lemma - zyxwvの日記

$xs'\;=\;\mbox{filter}\;\mbox{p}\;\mbox{xs}$ なときに、 $\forall x\;\in\;xs.\;p\;x$ である証明。よくわかってない。まず filter の定義。

filter : forall {a} -> (a -> Bool) -> [ a ] -> [ a ]
filter p []       = []
filter p (x &#8759; xs) with p x
... | true  = x &#8759; filter p xs
... | false =     filter p xs

で、証明。

module Filter where
  open import Data.Function
  open import Data.List
  open import Data.Bool

  infixr 30 _:all:_
  data All {A : Set}(P : A -> Set) : [ A ] -> Set where
    all[]   : All P []
    _:all:_ : forall {x xs} -> P x -> All P xs -> All P (x &#8759; xs)

  isTrue : {A : Set} -> (A -> Bool) -> A -> Set
  isTrue p x = T (p x)
    
  lem-filter : {A : Set}(p : A -> Bool) -> (xs : [ A ]) -> All (isTrue p) (filter p xs)
  lem-filter p [] = all[]
  lem-filter p (x &#8759; xs) with p x
  ... | true  = _ :all: lem-filter p xs
  ... | false = lem-filter p xs

Emacs の agda-mode が使えないのでしんどい。
これが agda の応答。

_65 : T (p x)  [ at /Users/sho/src/agda/Filter.agda:17,17-18 ]

要素 x が条件 p を満たすという証明をアンダースコアのところに書けばいいと思うんだけど、やっぱりわからない。わからないことだらけですね。