Skip to content

Instantly share code, notes, and snippets.

@gallais
Created Mar 3, 2019
Embed
What would you like to do?
Fully certified filter
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment