{-
Types Summer School 2007
Bertinoro
Aug 19 - 31, 2007
Agda
Ulf Norell
-}
module Filter where
open import Nat
data Bool : Set where
false : Bool
true : Bool
infixr 40 _::_
data List (A : Set) : Set where
[] : List A
_::_ : A -> List A -> List A
filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
filter p (x :: xs) | true = x :: filter p xs
filter p (x :: xs) | false = filter p xs
infix 20 _⊆_
data _⊆_ {A : Set} : List A -> List A -> Set where
stop : [] ⊆ []
drop : forall {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys
subset : {A : Set}(p : A -> Bool)(xs : List A) -> filter p xs ⊆ xs
subset p [] = stop
subset p (x :: xs) with p x
... | true = keep (subset p xs)
... | false = drop (subset p xs)
{-
subset p (x :: xs) with p x
subset p (x :: xs) | true = keep (subset p xs)
subset p (x :: xs) | false = drop (subset p xs)
-}