map then filter on vectors and lists

filter.agda

module filter where

open import Data.Bool           using (Bool; true; false)
open import Data.List           using (List; []; _∷_)
open import Data.Nat            using (ℕ; suc; _≤_; z≤n; s≤s; _≟_)
open import Data.Nat.Properties using (≤-trans)
open import Data.Nat.Show       using (show)
open import Data.Product        using (Σ-syntax; _×_; _,_)
open import Data.String         using (String)
open import Data.Vec            using (Vec;  []; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst)
open import Relation.Nullary    using (yes; no)

import Data.List   as L
import Data.String as S

-- If 2 ≤ 4, then 2 ≤ 5.
step≤ : {n m : ℕ} → n ≤ m → n ≤ suc m
step≤ z≤n     = z≤n
step≤ (s≤s p) = s≤s (step≤ p)

-- If two numbers are equal you can get a proof that one is no greater than the
-- other.
lemma-≡→≤ : {n m : ℕ} → n ≡ m → n ≤ m
lemma-≡→≤ {    0} {      .0} refl = z≤n
lemma-≡→≤ {suc n} {.(suc n)} refl = s≤s (lemma-≡→≤ refl)

foo : ℕ → String
foo = show

bar : String -> Bool
bar x with S.length x ≟ 2
bar x | yes p = true
bar x | no ¬p = false


module Vectors where

  -- Vecs very naturally express that the result length is equal to the input
  -- length.
  map : {A B : Set} {n : ℕ} → (A → B) → Vec A n → Vec B n
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs

  -- Return a triple-product: a length, a proof that it's no longer than the
  -- input, and the result Vec.
  filter : {A : Set} {m : ℕ} → (A → Bool) → Vec A m → Σ[ n ∈ ℕ ] (n ≤ m × Vec A n)
  filter f [] = 0 , z≤n , []
  filter f (x ∷ xs) with filter f xs | f x
  filter f (x ∷ xs) | n , prf , ys   | true  = suc n ,   s≤s prf , x ∷ ys
  filter f (x ∷ xs) | n , prf , ys   | false =     n , step≤ prf ,     ys

  -- Compose the two.
  foobar : {m : ℕ} → Vec ℕ m → Σ[ n ∈ ℕ ] (n ≤ m × Vec String n)
  foobar xs = filter bar (map foo xs)

  -- Type-checking time unit tests.
  test₀ : foobar (5 ∷ 10 ∷ 120 ∷ 52 ∷ []) ≡ (2 , _ , "10" ∷ "52" ∷ [])
  test₀ = refl

  test₁ : foobar (50 ∷ 11 ∷ 122 ∷ 99 ∷ []) ≡ (3 , _ , "50" ∷ "11" ∷ "99" ∷ [])
  test₁ = refl


module Lists where

  -- Just a normal map function.
  map : {A B : Set} → (A → B) → List A → List B
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs

  -- Just a normal filter function.
  filter : {A : Set} → (A → Bool) → List A → List A
  filter f [] = []
  filter f (x ∷ xs) with filter f xs | f x
  filter f (x ∷ xs) | ys | true  = x ∷ ys
  filter f (x ∷ xs) | ys | false =     ys

  -- Proof that input and output lengths are equal.
  map≡ : {A B : Set} (f : A → B) (xs : List A) → L.length (map f xs) ≡ L.length xs
  map≡ f [] = refl
  map≡ f (x ∷ xs) = cong suc (map≡ f xs)

  -- Proof that output is shorter than input or of equal length.
  filter≤ : {A : Set} (f : A → Bool) (xs : List A) → L.length (filter f xs) ≤ L.length xs
  filter≤ f [] = z≤n
  filter≤ f (x ∷ xs) with filter≤ f xs | f x
  filter≤ f (x ∷ xs) | prf | true  =   s≤s prf
  filter≤ f (x ∷ xs) | prf | false = step≤ prf

  -- Compose the two.
  foobar : List ℕ → List String
  foobar xs = filter bar (map foo xs)

  -- Compose the proofs with ≤-trans.
  foobar≤ : (xs : List ℕ) → L.length (foobar xs) ≤ L.length xs
  foobar≤ xs = ≤-trans (filter≤ bar (map foo xs)) (lemma-≡→≤ (map≡ foo xs))


module AtMostVecs where

  -- A shitty representation of vectors of at-most n elements which makes
  -- explicit where the gaps are.
  data Vec′ (A : Set) : ℕ → Set where
    [] : Vec′ A 0
    skip : {n : ℕ} →     Vec′ A n → Vec′ A (suc n)
    _∷_  : {n : ℕ} → A → Vec′ A n → Vec′ A (suc n)

  -- Build from the values in a Vec.
  from-vec : {A : Set} {n : ℕ} → Vec A n → Vec′ A n
  from-vec [] = []
  from-vec (x ∷ xs) = x ∷ from-vec xs

  -- Extract the values as a List.
  to-list : {A : Set} {n : ℕ} → Vec′ A n → List A
  to-list [] = []
  to-list (skip xs) =     to-list xs
  to-list ( x ∷ xs) = x ∷ to-list xs

  -- The list of values is no longer than the index.
  lemma-to-list : {A : Set} {n : ℕ} → (xs : Vec′ A n) → L.length (to-list xs) ≤ n
  lemma-to-list [] = z≤n
  lemma-to-list (skip xs) = step≤ (lemma-to-list xs)
  lemma-to-list ( x ∷ xs) =   s≤s (lemma-to-list xs)

  map : {A B : Set} {n : ℕ} → (A → B) → Vec′ A n → Vec′ B n
  map f [] = []
  map f (skip xs) = skip (map f xs)
  map f ( x ∷ xs) = f x ∷ map f xs

  filter : {A : Set} {n : ℕ} → (A → Bool) → Vec′ A n → Vec′ A n
  filter f [] = []
  filter f (skip xs) = skip (filter f xs)
  filter f ( x ∷ xs) with f x
  filter f ( x ∷ xs) | true  =  x ∷ (filter f xs)
  filter f ( x ∷ xs) | false = skip (filter f xs)

  -- No weird index messing about, the index is just the upper bound and stays
  -- unchanged.
  foobar : {n : ℕ} → Vec′ ℕ n → Vec′ String n
  foobar xs = filter bar (map foo xs)

  -- The list we get out of calling foobar is no longer than the input Vec.
  foobar≤ : {n : ℕ} → (xs : Vec ℕ n) → L.length (to-list (foobar (from-vec xs))) ≤ n
  foobar≤ xs = lemma-to-list (foobar (from-vec xs))