{-# OPTIONS --without-K --safe #-}

module Data.List.Properties.Ext where

open import Data.Bool using (Bool)
open import Data.Empty using (⊥-elim)
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (Any)
open import Data.Product using (Σ)
open import Function using (Equivalence; _⇔_; _∘_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; cong; cong₂)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Unary using (Pred; Decidable; _≐_)

private
  variable
    a p : Level
    A B : Set a

open Any
open Bool
open Dec
open Equivalence
open _≡_
open Σ

-- Properties of filter -------------------------------------------------------

module _ {P : Pred A p} (P? : Decidable P) where
  filter-cong :
    ∀ {Q : Pred A a} (Q? : Decidable Q) → P ≐ Q → filter P? ≗ filter Q?
  filter-cong Q? P≐Q [] = refl
  filter-cong Q? P≐Q (x ∷ xs) with P? x | Q? x
  ... | yes Px | yes Qx = cong (x ∷_) (filter-cong Q? P≐Q xs)
  ... | yes Px | no ¬Qx = ⊥-elim (¬Qx (P≐Q .proj₁ Px))
  ... | no ¬Px | yes Qx = ⊥-elim (¬Px (P≐Q .proj₂ Qx))
  ... | no ¬Px | no ¬Qx = filter-cong Q? P≐Q xs

  filter-map :
    ∀ (f : B → A) xs →
    filter P? (map f xs) ≡ map f (filter (P? ∘ f) xs)
  filter-map f []       = refl
  filter-map f (x ∷ xs) with does (P? (f x))
  ... | true  = cong (f x ∷_) (filter-map f xs)
  ... | false = filter-map f xs

  map-filter-cong :
    ∀ {f g : A → B} → (f≗g : ∀ {x} → P x → f x ≡ g x) →
    map f ∘ filter P? ≗ map g ∘ filter P?
  map-filter-cong f≗g []       = refl
  map-filter-cong f≗g (x ∷ xs) with P? x
  ... | yes Px = cong₂ _∷_ (f≗g Px) (map-filter-cong f≗g xs)
  ... | no ¬Px = map-filter-cong f≗g xs

  filter-map-comm :
    ∀ {Q : Pred B a} (Q? : Decidable Q) {f g : B → A} xs →
    (∀ {x} → x ∈ xs → P (f x) ⇔ Q x) →
    (∀ {x} → Q x → f x ≡ g x) →
    filter P? (map f xs) ≡ map g (filter Q? xs)
  filter-map-comm Q?     []       P⇔Q f≗g = refl
  filter-map-comm Q? {f} (x ∷ xs) P⇔Q f≗g with P? (f x) | Q? x
  ... | yes Pfx | yes Qx =
    cong₂ _∷_ (f≗g Qx) (filter-map-comm Q? xs (P⇔Q ∘ there) f≗g)
  ... | yes Pfx | no ¬Qx = ⊥-elim (¬Qx (P⇔Q (here refl) .to Pfx))
  ... | no ¬Pfx | yes Qx = ⊥-elim (¬Pfx (P⇔Q (here refl) .from Qx))
  ... | no ¬Pfx | no ¬Qx = filter-map-comm Q? xs (P⇔Q ∘ there) f≗g