From 131e69da1b718d7f9c44c4016f104bc45f89e15f Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Fri, 23 Jan 2015 14:44:04 +0100
Subject: [PATCH] Some properties of Data.List.gfilter.

---
 src/Data/List/Properties.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 1d291f8488..c47eda70fe 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -264,6 +264,24 @@ filter-filters P dec (x ∷ xs) with dec x
 filter-filters P dec (x ∷ xs) | yes px = px ∷ filter-filters P dec xs
 filter-filters P dec (x ∷ xs) | no ¬px = filter-filters P dec xs
 
+-- Gfilter.
+
+gfilter-just : ∀ {a} {A : Set a} (xs : List A) → gfilter just xs ≡ xs
+gfilter-just []       = refl
+gfilter-just (x ∷ xs) = P.cong (_∷_ x) (gfilter-just xs)
+
+gfilter-nothing : ∀ {a} {A : Set a} (xs : List A) →
+  gfilter {B = A} (λ _ → nothing) xs ≡ []
+gfilter-nothing []       = refl
+gfilter-nothing (x ∷ xs) = gfilter-nothing xs
+
+gfilter-concatMap : ∀ {a b} {A : Set a} {B : Set b} (f : A → Maybe B) →
+  gfilter f ≗ concatMap (fromMaybe ∘ f)
+gfilter-concatMap f [] = refl
+gfilter-concatMap f (x ∷ xs) with f x
+gfilter-concatMap f (x ∷ xs) | just y  = P.cong (_∷_ y) (gfilter-concatMap f xs)
+gfilter-concatMap f (x ∷ xs) | nothing = gfilter-concatMap f xs
+
 -- Inits, tails, and scanr.
 
 scanr-defn : ∀ {a b} {A : Set a} {B : Set b}