Valid filter.

Filter.idr

import Data.List
import Data.List.Quantifiers

data SubsetEq : (xs, ys : List a) -> Type where
  Empty : SubsetEq Nil xs

  Cons : (Elem x ys)
      -> SubsetEq xs ys
      -> SubsetEq (x::xs) ys

abs : (y : a) -> SubsetEq xs ys -> SubsetEq xs (y::ys)
abs y Empty = Empty
abs y (Cons z w) = Cons (There z) (abs y w)


filter : (test   : (value : type) -> Dec (holds value))
      -> (input  : List type)
      -> (output     : List type **
          isSubsetEq : SubsetEq output input **
          All holds output)
filter pred [] = ([] ** Empty ** [])
filter pred (x :: xs) with (pred x)
  filter pred (x :: xs) | (Yes prf) =
     let (rest ** prfA ** prfB) = filter pred xs
       in (x::rest ** (Cons Here (abs x prfA)) ** prf :: prfB)
  filter pred (x :: xs) | (No contra) =
     let (rest ** prfA ** prfB) = filter pred xs
       in (rest ** abs x prfA ** prfB)

FilterImproved.idr

import Data.List
import Data.List.Quantifiers

data Interleaving : (xs, ys, zs : List a) -> Type where
  Empty   : Interleaving Nil Nil Nil
  LeftAdd : (x : type)
         -> Interleaving xs ys zs
         -> Interleaving (x::xs) ys (x::zs)
  RightAdd : (y : type)
          -> Interleaving xs ys zs
          -> Interleaving xs (y::ys) (y::zs)

-- temp : Interleaving [1,3,5,7,9] [2,4,6,8] [1,2,3,4,5,6,7,8,9]

data Filter : (holdsFor : type -> Type)
           -> (input : List type)
           -> Type where
  MkFilter : (kept : List type)
          -> (prfOrdering : Interleaving kept thrown input)
          -> (prfKept     : All holdsFor kept)
          -> (prfThrown   : All (\x => Not (holdsFor x)) thrown)
          -> Filter holdsFor input

filter : (test   : (value : type) -> Dec (holds value))
      -> (input  : List type)
      -> Filter holds input
filter test [] = MkFilter [] Empty [] []
filter test (x :: xs) with (filter test xs)
  filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) with (test x)
    filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) | (Yes prf) =
      MkFilter (x::kept) (LeftAdd x prfOrdering) (prf :: prfKept) prfThrown
    filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) | (No contra) =
      MkFilter kept (RightAdd x prfOrdering) prfKept (contra :: prfThrown)