------------------------------------------------------------------------
-- List-related properties
------------------------------------------------------------------------

-- Note that the lemmas below could be generalised to work with other
-- equalities than _≡_.

module Data.List.Properties where

open import Data.List as List
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool
open import Data.Function
import Data.Product as Prod; open Prod hiding (map)
import Data.Sum as Sum; open Sum using (_⊎_; inj₁; inj₂)
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as Eq
open import Algebra
open import Relation.Binary.FunctionLifting
open import Category.Monad
open RawMonad List.monad

∷-injective : ∀ {A} {x y xs ys} →
              (List A ∶ x ∷ xs) ≡ (y ∷ ys) → (x ≡ y) × (xs ≡ ys)
∷-injective refl = (refl , refl)

right-identity-unique : ∀ {A} (xs : List A) {ys} →
                        xs ≡ xs ++ ys → ys ≡ []
right-identity-unique []       refl = refl
right-identity-unique (x ∷ xs) eq   =
  right-identity-unique xs (proj₂ (∷-injective eq))

-- Map, sum, and append.

map-++-commute : ∀ {a b} (f : a → b) xs ys →
                 map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-commute f []       ys = refl
map-++-commute f (x ∷ xs) ys =
  cong (_∷_ (f x)) (map-++-commute f xs ys)

sum-++-commute : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []       ys = refl
sum-++-commute (x ∷ xs) ys = begin
  x + sum (xs ++ ys)
                         ≡⟨ cong (_+_ x) (sum-++-commute xs ys) ⟩
  x + (sum xs + sum ys)
                         ≡⟨ sym $ +-assoc x _ _ ⟩
  (x + sum xs) + sum ys
                         ∎
  where
  open CommutativeSemiring commutativeSemiring hiding (_+_; sym)
  open ≡-Reasoning

-- Various properties about folds.

foldr-universal : ∀ {a b} (h : List a → b) f e →
                  (h [] ≡ e) →
                  (∀ x xs → h (x ∷ xs) ≡ f x (h xs)) →
                  h ≗ foldr f e
foldr-universal h f e base step []       = base
foldr-universal h f e base step (x ∷ xs) = begin
  h (x ∷ xs)
    ≡⟨ step x xs ⟩
  f x (h xs)
    ≡⟨ cong (f x) (foldr-universal h f e base step xs) ⟩
  f x (foldr f e xs)
    ∎
  where open ≡-Reasoning

foldr-fusion : ∀ {a b c} (h : b → c)
                 {f : a → b → b} {g : a → c → c} (e : b) →
               (∀ x y → h (f x y) ≡ g x (h y)) →
               h ∘ foldr f e ≗ foldr g (h e)
foldr-fusion h {f} {g} e fuse =
  foldr-universal (h ∘ foldr f e) g (h e) refl
                  (λ x xs → fuse x (foldr f e xs))

idIsFold : ∀ {a} → id {a = List a} ≗ foldr _∷_ []
idIsFold = foldr-universal id _∷_ [] refl (λ _ _ → refl)

++IsFold : ∀ {a} (xs ys : List a) →
           xs ++ ys ≡ foldr _∷_ ys xs
++IsFold xs ys =
  begin
    xs ++ ys
  ≡⟨ cong (λ xs → xs ++ ys) (idIsFold xs) ⟩
    foldr _∷_ [] xs ++ ys
  ≡⟨ foldr-fusion (λ xs → xs ++ ys) [] (λ _ _ → refl) xs ⟩
    foldr _∷_ ([] ++ ys) xs
  ≡⟨ refl ⟩
    foldr _∷_ ys xs
  ∎
  where open ≡-Reasoning

mapIsFold : ∀ {a b} {f : a → b} →
            map f ≗ foldr (λ x ys → f x ∷ ys) []
mapIsFold {f = f} =
  begin
    map f
  ≈⟨ cong (map f) ∘ idIsFold ⟩
    map f ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (map f) [] (λ _ _ → refl) ⟩
    foldr (λ x ys → f x ∷ ys) []
  ∎
  where open Eq (_ →-setoid _)

concat-map : ∀ {a b} {f : a → b} →
             concat ∘ map (map f) ≗ map f ∘ concat
concat-map {f = f} =
  begin
    concat ∘ map (map f)
  ≈⟨ cong concat ∘ mapIsFold ⟩
    concat ∘ foldr (λ xs ys → map f xs ∷ ys) []
  ≈⟨ foldr-fusion concat [] (λ _ _ → refl) ⟩
    foldr (λ ys zs → map f ys ++ zs) []
  ≈⟨ sym ∘
     foldr-fusion (map f) [] (λ ys zs → map-++-commute f ys zs) ⟩
    map f ∘ concat
  ∎
  where open Eq (_ →-setoid _)

map-compose : ∀ {a b c} {g : b → c} {f : a → b} →
              map (g ∘ f) ≗ map g ∘ map f
map-compose {g = g} {f} =
  begin
    map (g ∘ f)
  ≈⟨ cong (map (g ∘ f)) ∘ idIsFold ⟩
    map (g ∘ f) ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (map (g ∘ f)) [] (λ _ _ → refl) ⟩
    foldr (λ a y → g (f a) ∷ y) []
  ≈⟨ sym ∘ foldr-fusion (map g) [] (λ _ _ → refl) ⟩
    map g ∘ foldr (λ a y → f a ∷ y) []
  ≈⟨ cong (map g) ∘ sym ∘ mapIsFold ⟩
    map g ∘ map f
  ∎
  where open Eq (_ →-setoid _)

foldr-cong : ∀ {a b} {f₁ f₂ : a → b → b} {e₁ e₂ : b} →
             (∀ x y → f₁ x y ≡ f₂ x y) → e₁ ≡ e₂ →
             foldr f₁ e₁ ≗ foldr f₂ e₂
foldr-cong {f₁ = f₁} {f₂} {e} f₁≗₂f₂ refl =
  begin
    foldr f₁ e
  ≈⟨ cong (foldr f₁ e) ∘ idIsFold ⟩
    foldr f₁ e ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (foldr f₁ e) [] (λ x xs → f₁≗₂f₂ x (foldr f₁ e xs)) ⟩
    foldr f₂ e
  ∎
  where open Eq (_ →-setoid _)

map-cong : ∀ {a b} {f g : a → b} → f ≗ g → map f ≗ map g
map-cong {f = f} {g} f≗g =
  begin
    map f
  ≈⟨ mapIsFold ⟩
    foldr (λ x ys → f x ∷ ys) []
  ≈⟨ foldr-cong (λ x ys → cong₂ _∷_ (f≗g x) refl) refl ⟩
    foldr (λ x ys → g x ∷ ys) []
  ≈⟨ sym ∘ mapIsFold ⟩
    map g
  ∎
  where open Eq (_ →-setoid _)

-- Take, drop, and splitAt.

take++drop : ∀ {a} n (xs : List a) → take n xs ++ drop n xs ≡ xs
take++drop zero    xs       = refl
take++drop (suc n) []       = refl
take++drop (suc n) (x ∷ xs) =
  cong (λ xs → x ∷ xs) (take++drop n xs)

splitAt-defn : ∀ {a} n → splitAt {a} n ≗ < take n , drop n >
splitAt-defn zero    xs       = refl
splitAt-defn (suc n) []       = refl
splitAt-defn (suc n) (x ∷ xs) with splitAt n xs | splitAt-defn n xs
... | (ys , zs) | ih = cong (Prod.map (_∷_ x) id) ih

-- TakeWhile, dropWhile, and span.

takeWhile++dropWhile : ∀ {a} (p : a → Bool) (xs : List a) →
                       takeWhile p xs ++ dropWhile p xs ≡ xs
takeWhile++dropWhile p []       = refl
takeWhile++dropWhile p (x ∷ xs) with p x
... | true  = cong (_∷_ x) (takeWhile++dropWhile p xs)
... | false = refl

span-defn : ∀ {a} (p : a → Bool) →
            span p ≗ < takeWhile p , dropWhile p >
span-defn p []       = refl
span-defn p (x ∷ xs) with p x
... | true  = cong (Prod.map (_∷_ x) id) (span-defn p xs)
... | false = refl

-- Partition.

partition-defn : ∀ {a} (p : a → Bool) →
                 partition p ≗ < filter p , filter (not ∘ p) >
partition-defn p []       = refl
partition-defn p (x ∷ xs)
 with p x | partition p xs | partition-defn p xs
...  | true  | (ys , zs) | eq = cong (Prod.map (_∷_ x) id) eq
...  | false | (ys , zs) | eq = cong (Prod.map id (_∷_ x)) eq

-- Inits, tails, and scanr.

scanr-defn : ∀ {a b} (f : a → b → b) (e : b) →
             scanr f e ≗ map (foldr f e) ∘ tails
scanr-defn f e []             = refl
scanr-defn f e (x ∷ [])       = refl
scanr-defn f e (x₁ ∷ x₂ ∷ xs)
  with scanr f e (x₂ ∷ xs) | scanr-defn f e (x₂ ∷ xs)
...  | [] | ()
...  | y ∷ ys | eq with ∷-injective eq
...        | y≡fx₂⦇f⦈xs , _ = cong₂ (λ z zs → f x₁ z ∷ zs) y≡fx₂⦇f⦈xs eq

scanl-defn : ∀ {a b} (f : a → b → a) (e : a) →
             scanl f e ≗ map (foldl f e) ∘ inits
scanl-defn f e []       = refl
scanl-defn f e (x ∷ xs) = cong (_∷_ e) (begin
     scanl f (f e x) xs
  ≡⟨ scanl-defn f (f e x) xs ⟩
     map (foldl f (f e x)) (inits xs)
  ≡⟨ refl ⟩
     map (foldl f e ∘ (_∷_ x)) (inits xs)
  ≡⟨ map-compose (inits xs) ⟩
     map (foldl f e) (map (_∷_ x) (inits xs))
  ∎)
  where open ≡-Reasoning

-- Length.

length-map : ∀ {A B} (f : A → B) xs →
             length (map f xs) ≡ length xs
length-map f []       = refl
length-map f (x ∷ xs) = cong suc (length-map f xs)

length-gfilter : ∀ {A B} (p : A → Maybe B) xs →
                 length (gfilter p xs) ≤ length xs
length-gfilter p []       = z≤n
length-gfilter p (x ∷ xs) with p x
length-gfilter p (x ∷ xs) | just y  = s≤s (length-gfilter p xs)
length-gfilter p (x ∷ xs) | nothing = ≤-step (length-gfilter p xs)

-- _∈_.

∈-++ˡ : ∀ {A} {x : A} {xs ys} → x ∈ xs → x ∈ xs ++ ys
∈-++ˡ here         = here
∈-++ˡ (there x∈xs) = there (∈-++ˡ x∈xs)

∈-++ʳ : ∀ {A} {x : A} xs {ys} → x ∈ ys → x ∈ xs ++ ys
∈-++ʳ []       x∈ys = x∈ys
∈-++ʳ (x ∷ xs) x∈ys = there (∈-++ʳ xs x∈ys)

++-∈ : ∀ {A} {x : A} xs {ys} → x ∈ xs ++ ys → x ∈ xs ⊎ x ∈ ys
++-∈ []       x∈ys             = inj₂ x∈ys
++-∈ (x ∷ xs) here             = inj₁ here
++-∈ (x ∷ xs) (there x∈xs++ys) = Sum.map there id (++-∈ xs x∈xs++ys)

∈-map : ∀ {A B} {f : A → B} {x xs} →
        x ∈ xs → f x ∈ map f xs
∈-map here         = here
∈-map (there x∈xs) = there (∈-map x∈xs)

map-∈ : ∀ {A B} {f : A → B} {fx} xs →
        fx ∈ map f xs → ∃ λ x → x ∈ xs × f x ≡ fx
map-∈ []       ()
map-∈ (x ∷ xs) here           = (x , here , refl)
map-∈ (x ∷ xs) (there fx∈fxs) =
  Prod.map id (Prod.map there id) (map-∈ xs fx∈fxs)

∈-concat : ∀ {A} {x : A} {xs xss} →
           x ∈ xs → xs ∈ xss → x ∈ concat xss
∈-concat x∈xs here                    = ∈-++ˡ x∈xs
∈-concat x∈xs (there {y = ys} xs∈xss) = ∈-++ʳ ys (∈-concat x∈xs xs∈xss)

concat-∈ : ∀ {A} {x : A} xss →
           x ∈ concat xss → ∃ λ xs → x ∈ xs × xs ∈ xss
concat-∈ []               ()
concat-∈ ([]       ∷ xss) x∈cxss         = Prod.map id (Prod.map id there)
                                             (concat-∈ xss x∈cxss)
concat-∈ ((x ∷ xs) ∷ xss) here           = (x ∷ xs , here , here)
concat-∈ ((y ∷ xs) ∷ xss) (there x∈cxss) with concat-∈ (xs ∷ xss) x∈cxss
... | (.xs , x∈xs , here)         = (y ∷ xs , there x∈xs , here)
... | (ys  , x∈ys , there ys∈xss) = (ys     , x∈ys       , there ys∈xss)

∈->>= : ∀ {A B} (f : A → List B) {x y xs} →
        x ∈ xs → y ∈ f x → y ∈ (xs >>= f)
∈->>= f x∈xs y∈fx = ∈-concat y∈fx (∈-map x∈xs)

>>=-∈ : ∀ {A B} (f : A → List B) {y} xs →
        y ∈ (xs >>= f) → ∃ λ x → x ∈ xs × y ∈ f x
>>=-∈ f xs y∈xs>>=f with Prod.map id (Prod.map id (map-∈ xs)) $
                           concat-∈ (map f xs) y∈xs>>=f
>>=-∈ f xs y∈xs>>=f | (.(f x) , y∈fx , (x , x∈xs , refl)) =
  (x , x∈xs , y∈fx)

∈-⊛ : ∀ {A B} {fs : List (A → B)} {xs f x} →
      f ∈ fs → x ∈ xs → f x ∈ fs ⊛ xs
∈-⊛ f∈xs x∈xs = ∈->>= _ f∈xs (∈->>= _ x∈xs here)

⊛-∈ : ∀ {A B} (fs : List (A → B)) xs {fx} →
      fx ∈ fs ⊛ xs → ∃₂ λ f x → f ∈ fs × x ∈ xs × f x ≡ fx
⊛-∈ fs xs fx∈fs⊛xs with >>=-∈ _ fs fx∈fs⊛xs
⊛-∈ fs xs fx∈fs⊛xs | (f , f∈fs , fx∈) with >>=-∈ _ xs fx∈
⊛-∈ fs xs fx∈fs⊛xs | (f , f∈fs , fx∈) | (x , x∈xs , here) =
  (f , x , f∈fs , x∈xs , refl)
⊛-∈ fs xs fx∈fs⊛xs | (f , f∈fs , fx∈) | (x , x∈xs , there ())

any-∈ : ∀ {A} (p : A → Bool) xs →
        any p xs ≡ true → ∃ λ x → x ∈ xs × p x ≡ true
any-∈ p []       ()
any-∈ p (x ∷ xs) eq with inspect (p x)
any-∈ p (x ∷ xs) eq | true  with-≡ eq′  = (x , here , sym eq′)
any-∈ p (x ∷ xs) eq | false with-≡ eq′  with p x
any-∈ p (x ∷ xs) eq | false with-≡ refl | .false =
  Prod.map id (Prod.map there id) (any-∈ p xs eq)

∈-any : ∀ {A x} (p : A → Bool) {xs} →
        x ∈ xs → p x ≡ true → any p xs ≡ true
∈-any p (here {x = x})       eq   with p x
∈-any p here                 refl | .true = refl
∈-any p (there {y = y} x∈xs) eq   with p y
∈-any p (there {y = y} x∈xs) eq   | true  = refl
∈-any p (there {y = y} x∈xs) eq   | false = ∈-any p x∈xs eq