open import Data.Nat open import Data.Bool open import Data.List using (List ; [] ; _∷_) even : ℕ → Bool even zero = true even (suc zero) = false even (suc (suc n)) = even n filter : {A : Set} → (A → Bool) → List A → List A filter p [] = [] filter p (x ∷ xs) with (p x) filter p (x ∷ xs) | false = filter p xs filter p (x ∷ xs) | true = x ∷ filter p xs data _⊆_ {A : Set} : List A → List A → Set where -- ⊆ is \sub= Nil : [] ⊆ [] Sync : {x : A} → {xs ys : List A} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys) Skip : {x : A} → {xs ys : List A} → xs ⊆ ys → xs ⊆ (x ∷ ys) ex : (1 ∷ 3 ∷ 4 ∷ []) ⊆ (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ex = Sync (Skip (Sync (Sync (Skip Nil)))) filter-⊆ : {A : Set} → (p : A → Bool) → (xs : List A) → filter p xs ⊆ xs filter-⊆ p [] = Nil filter-⊆ p (x ∷ xs) with p x filter-⊆ p (x ∷ xs) | false = Skip (filter-⊆ p xs) filter-⊆ p (x ∷ xs) | true = Sync (filter-⊆ p xs)