Fully certified filter

filter.agda

open import Level
open import Data.List.Base hiding (filter)
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Ternary.Interleaving.Propositional
open import Function
open import Relation.Nullary
open import Relation.Unary

module _ {a} {A : Set a} where

  infix 3 _≡_⊎_
  record Filter {p} (P : Pred A p) (xs : List A) : Set (a ⊔ p) where
    constructor _≡_⊎_
    field {kept}   : List A
          {thrown} : List A
          cover    : Interleaving kept thrown xs
          allP     : All P kept
          all¬P    : All (∁ P) thrown

  module _ {p} {P : Pred A p} (P? : Decidable P) where

    filter : ∀ xs → Filter P xs
    filter []       = [] ≡ [] ⊎ []
    filter (x ∷ xs) with P? x | filter xs
    ... | yes p | xs' ≡ ps ⊎ ¬ps = consˡ xs' ≡ p ∷ ps ⊎      ¬ps
    ... | no ¬p | xs' ≡ ps ⊎ ¬ps = consʳ xs' ≡     ps ⊎ ¬p ∷ ¬ps