FilterExamples.agda

module FilterExamples where
  data Bool : Set where
    true false : Bool -- two constructors, true and false

  data List (A : Set) : Set where
    []  : List A
    _∷_ : A → List A → List A

  [_] : {A : Set} → A → List A
  [ a ] = a ∷ []

  infix 4 _≡_
  data _≡_ {A : Set} (x : A) : A → Set where
    refl : x ≡ x

  sym : {A : Set} {a b : A} → a ≡ b → b ≡ a
  sym refl = refl

  trans : {A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
  trans refl refl = refl

  cong : {A B : Set} {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
  cong f refl = refl

  -- a fun way to write transitivity
  infixr 5 _~_
  _~_ = trans

  filter : {A : Set} → (A → Bool) → List A → List A
  filter p [] = []
  filter p (a ∷ as) with p a
  ... | true  = a ∷ filter p as
  ... | false = filter p as

  filterN : {A : Set} → (A → Bool) → List A → List A
  filterN p [] = []
  filterN p (a ∷ as) with p a
  filterN p (a ∷ as) | true with as
  filterN p (a ∷ as) | true | [] = a ∷ []
  filterN p (a ∷ as) | true | b ∷ bs with p b
  filterN p (a ∷ as) | true | b ∷ bs | true  = a ∷ (b ∷ filterN p bs)
  filterN p (a ∷ as) | true | b ∷ bs | false = a ∷ filterN p bs
  filterN p (a ∷ as) | false = filterN p as

  filterP : {A : Set} → (A → Bool) → List A → List A
  filterP p [] = []
  filterP p (a ∷ []) with p a
  filterP p (a ∷ []) | true  = a ∷ []
  filterP p (a ∷ []) | false = []
  filterP p (a ∷ (b ∷ bs)) with p a | p b
  filterP p (a ∷ (b ∷ bs)) | true  | true  = a ∷ (b ∷ filterP p bs)
  filterP p (a ∷ (b ∷ bs)) | true  | false = a ∷ filterP p bs
  filterP p (a ∷ (b ∷ bs)) | false | true  = b ∷ filterP p bs
  filterP p (a ∷ (b ∷ bs)) | false | false = filterP p bs

  filter≡filterN₀ : {A : Set} → (p : A → Bool) → (as : List A) → filter p as ≡ filterN p as
  filter≡filterN₀ p []       = refl
  filter≡filterN₀ p (a ∷ as) with p a
  filter≡filterN₀ p (a ∷ as) | true with as
  filter≡filterN₀ p (a ∷ as) | true | [] = refl
  filter≡filterN₀ p (a ∷ as) | true | b ∷ bs with p b
  filter≡filterN₀ p (a ∷ as) | true | b ∷ bs | true  = cong (λ x → a ∷ (b ∷ x)) (filter≡filterN₀ p bs)
  filter≡filterN₀ p (a ∷ as) | true | b ∷ bs | false = cong (λ x → a ∷ x) (filter≡filterN₀ p bs)
  filter≡filterN₀ p (a ∷ as) | false = filter≡filterN₀ p as

  {- This fails to be provable, because Agda can't seem to apply the definition of filter
     to normalize things.
  -}
  filter≡filterP₀ : {A : Set} → (p : A → Bool) → (as : List A) → filter  p as ≡ filterP p as
  filter≡filterP₀ p [] = refl
  filter≡filterP₀ p (a ∷ []) with p a
  filter≡filterP₀ p (a ∷ []) | true  = refl
  filter≡filterP₀ p (a ∷ []) | false = refl
  filter≡filterP₀ p (a ∷ (b ∷ bs)) with p a | p b
  {- Agda says:
     Goal: a ∷ (filter p (b ∷ bs) | p b) ≡ a ∷ (b ∷ filterP p bs)
  -}
  filter≡filterP₀ p (a ∷ (b ∷ bs)) | true  | true  = {!!}
  filter≡filterP₀ p (a ∷ (b ∷ bs)) | true  | false = {!!}
  filter≡filterP₀ p (a ∷ (b ∷ bs)) | false | true  = {!!}
  filter≡filterP₀ p (a ∷ (b ∷ bs)) | false | false = {!!}

  {- Unlike the attempt above, if we uses nested with-clauses instead of a parallel with-clause
     then agda is able to normalize things and the proof works. -}
  filter≡filterP₁ : {A : Set} → (p : A → Bool) → (as : List A) → filter  p as ≡ filterP p as
  filter≡filterP₁ p [] = refl
  filter≡filterP₁ p (a ∷ []) with p a
  filter≡filterP₁ p (a ∷ []) | true  = refl
  filter≡filterP₁ p (a ∷ []) | false = refl
  filter≡filterP₁ p (a ∷ (b ∷ bs)) with p a
  filter≡filterP₁ p (a ∷ (b ∷ bs)) | true  with p b
  filter≡filterP₁ p (a ∷ (b ∷ bs)) | true  | true  = cong (λ x → a ∷ (b ∷ x)) (filter≡filterP₁ p bs)
  filter≡filterP₁ p (a ∷ (b ∷ bs)) | true  | false = cong (λ x → a ∷ x) (filter≡filterP₁ p bs)
  filter≡filterP₁ p (a ∷ (b ∷ bs)) | false with p b
  filter≡filterP₁ p (a ∷ (b ∷ bs)) | false | true  = cong (λ x → b ∷ x) (filter≡filterP₁ p bs)
  filter≡filterP₁ p (a ∷ (b ∷ bs)) | false | false = filter≡filterP₁ p bs