------------------------------------------------------------------------
-- The Agda standard library
--
-- List-related properties
------------------------------------------------------------------------

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

module Data.List.Properties where

open import Algebra
open import Data.Bool
open import Data.List as List
open import Data.List.All using (All; []; _∷_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod hiding (map)
open import Function
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.PropositionalEquality as P
using (_≡_; _≢_; _≗_; refl)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Unary using (Decidable)

private
module LM {a} {A : Set a} = Monoid (List.monoid A)

∷-injective :  {a} {A : Set a} {x y xs ys}
(x  xs  List A)  y  ys  x  y × xs  ys
∷-injective refl = (refl , refl)

∷ʳ-injective :  {a} {A : Set a} {x y} xs ys
(xs ∷ʳ x  List A)  ys ∷ʳ y  xs  ys × x  y
∷ʳ-injective []          []          refl = (refl , refl)
∷ʳ-injective (x  xs)    (y   ys)   eq   with ∷-injective eq
∷ʳ-injective (x  xs)    (.x  ys)   eq   | (refl , eq′) =
Prod.map (P.cong (_∷_ x)) id \$ ∷ʳ-injective xs ys eq′

∷ʳ-injective []          (_  [])    ()
∷ʳ-injective []          (_  _  _) ()
∷ʳ-injective (_  [])    []          ()
∷ʳ-injective (_  _  _) []          ()

right-identity-unique :  {a} {A : Set 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))

left-identity-unique :  {a} {A : Set a} {xs} (ys : List A)
xs  ys ++ xs  ys  []
left-identity-unique               []       _  = refl
left-identity-unique {xs = []}     (y  ys) ()
left-identity-unique {xs = x  xs} (y  ys) eq
with left-identity-unique (ys ++ [ x ]) (begin
xs                  ≡⟨ proj₂ (∷-injective eq)
ys ++ x  xs        ≡⟨ P.sym (LM.assoc ys [ x ] xs)
(ys ++ [ x ]) ++ xs )
where open P.≡-Reasoning
left-identity-unique {xs = x  xs} (y  []   ) eq | ()
left-identity-unique {xs = x  xs} (y  _  _) eq | ()

-- Map, sum, and append.

map-++-commute :  {a b} {A : Set a} {B : Set 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 =
P.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)
≡⟨ P.cong (_+_ x) (sum-++-commute xs ys)
x + (sum xs + sum ys)
≡⟨ P.sym \$ +-assoc x _ _
(x + sum xs) + sum ys

where
open CommutativeSemiring commutativeSemiring hiding (_+_)
open P.≡-Reasoning

foldr-universal :  {a b} {A : Set a} {B : Set 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)
≡⟨ P.cong (f x) (foldr-universal h f e base step xs)
f x (foldr f e xs)

where open P.≡-Reasoning

foldr-fusion :  {a b c} {A : Set a} {B : Set b} {C : Set 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} {A : Set a}  id {A = List A}  foldr _∷_ []
idIsFold = foldr-universal id _∷_ [] refl  _ _  refl)

++IsFold :  {a} {A : Set a} (xs ys : List A)
xs ++ ys  foldr _∷_ ys xs
++IsFold xs ys =
begin
xs ++ ys
≡⟨ P.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 P.≡-Reasoning

mapIsFold :  {a b} {A : Set a} {B : Set b} {f : A  B}
map f  foldr  x ys  f x  ys) []
mapIsFold {f = f} =
begin
map f
≈⟨ P.cong (map f)  idIsFold
map f  foldr _∷_ []
≈⟨ foldr-fusion (map f) []  _ _  refl)
foldr  x ys  f x  ys) []

where open EqR (P._→-setoid_ _ _)

concat-map :  {a b} {A : Set a} {B : Set b} {f : A  B}
concat  map (map f)  map f  concat
concat-map {b = b} {f = f} =
begin
concat  map (map f)
≈⟨ P.cong concat  mapIsFold {b = b}
concat  foldr  xs ys  map f xs  ys) []
≈⟨ foldr-fusion {b = b} concat []  _ _  refl)
foldr  ys zs  map f ys ++ zs) []
≈⟨ P.sym
foldr-fusion (map f) []  ys zs  map-++-commute f ys zs)
map f  concat

where open EqR (P._→-setoid_ _ _)

map-id :  {a} {A : Set a}  map id  id {A = List A}
map-id {A = A} = begin
map id        ≈⟨ mapIsFold
foldr _∷_ []  ≈⟨ P.sym  idIsFold {A = A}
id
where open EqR (P._→-setoid_ _ _)

map-compose :  {a b c} {A : Set a} {B : Set b} {C : Set c}
{g : B  C} {f : A  B}
map (g  f)  map g  map f
map-compose {A = A} {B} {g = g} {f} =
begin
map (g  f)
≈⟨ P.cong (map (g  f))  idIsFold
map (g  f)  foldr _∷_ []
≈⟨ foldr-fusion (map (g  f)) []  _ _  refl)
foldr  a y  g (f a)  y) []
≈⟨ P.sym  foldr-fusion (map g) []  _ _  refl)
map g  foldr  a y  f a  y) []
≈⟨ P.cong (map g)  P.sym  mapIsFold {A = A} {B = B}
map g  map f

where open EqR (P._→-setoid_ _ _)

foldr-cong :  {a b} {A : Set a} {B : Set 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
≈⟨ P.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 EqR (P._→-setoid_ _ _)

map-cong :  {a b} {A : Set a} {B : Set b} {f g : A  B}
f  g  map f  map g
map-cong {A = A} {B} {f} {g} f≗g =
begin
map f
≈⟨ mapIsFold
foldr  x ys  f x  ys) []
≈⟨ foldr-cong  x ys  P.cong₂ _∷_ (f≗g x) refl) refl
foldr  x ys  g x  ys) []
≈⟨ P.sym  mapIsFold {A = A} {B = B}
map g

where open EqR (P._→-setoid_ _ _)

-- Take, drop, and splitAt.

take++drop :  {a} {A : Set 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) =
P.cong  xs  x  xs) (take++drop n xs)

splitAt-defn :  {a} {A : Set a} n
splitAt {A = 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 = P.cong (Prod.map (_∷_ x) id) ih

-- TakeWhile, dropWhile, and span.

takeWhile++dropWhile :  {a} {A : Set 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  = P.cong (_∷_ x) (takeWhile++dropWhile p xs)
... | false = refl

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

-- Partition, filter.

partition-defn :  {a} {A : Set 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 = P.cong (Prod.map (_∷_ x) id) eq
...  | false | (ys , zs) | eq = P.cong (Prod.map id (_∷_ x)) eq

filter-filters :  {a p} {A : Set a}
(P : A  Set p) (dec : Decidable P) (xs : List A)
All P (filter (⌊_⌋  dec) xs)
filter-filters P dec []       = []
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

-- Inits, tails, and scanr.

scanr-defn :  {a b} {A : Set a} {B : Set 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 , _ = P.cong₂  z zs  f x₁ z  zs) y≡fx₂⦇f⦈xs eq

scanl-defn :  {a b} {A : Set a} {B : Set 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) = P.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 P.≡-Reasoning

-- Length.

length-map :  {a b} {A : Set a} {B : Set b} (f : A  B) xs
length (map f xs)  length xs
length-map f []       = refl
length-map f (x  xs) = P.cong suc (length-map f xs)

length-++ :  {a} {A : Set a} (xs : List A) {ys}
length (xs ++ ys)  length xs + length ys
length-++ []       = refl
length-++ (x  xs) = P.cong suc (length-++ xs)

length-gfilter :  {a b} {A : Set a} {B : Set 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)

-- Reverse.

unfold-reverse :  {a} {A : Set a} (x : A) (xs : List A)
reverse (x  xs)  reverse xs ∷ʳ x
unfold-reverse x xs = begin
foldl (flip _∷_) [ x ] xs  ≡⟨ helper [ x ] xs
reverse xs ∷ʳ x
where
open P.≡-Reasoning

helper :  {a} {A : Set a} (xs ys : List A)
foldl (flip _∷_) xs ys  reverse ys ++ xs
helper xs []       = P.refl
helper xs (y  ys) = begin
foldl (flip _∷_) (y  xs) ys  ≡⟨ helper (y  xs) ys
reverse ys ++ y  xs          ≡⟨ P.sym \$ LM.assoc (reverse ys) _ _
(reverse ys ∷ʳ y) ++ xs       ≡⟨ P.sym \$ P.cong  zs  zs ++ xs) (unfold-reverse y ys)
reverse (y  ys) ++ xs

reverse-++-commute :
{a} {A : Set a} (xs ys : List A)
reverse (xs ++ ys)  reverse ys ++ reverse xs
reverse-++-commute {a} [] ys = begin
reverse ys                ≡⟨ P.sym \$ proj₂ {a = a} {b = a} LM.identity _
reverse ys ++ []          ≡⟨ P.refl
reverse ys ++ reverse []
where open P.≡-Reasoning
reverse-++-commute (x  xs) ys = begin
reverse (x  xs ++ ys)               ≡⟨ unfold-reverse x (xs ++ ys)
reverse (xs ++ ys) ++ [ x ]          ≡⟨ P.cong  zs  zs ++ [ x ]) (reverse-++-commute xs ys)
(reverse ys ++ reverse xs) ++ [ x ]  ≡⟨ LM.assoc (reverse ys) _ _
reverse ys ++ (reverse xs ++ [ x ])  ≡⟨ P.sym \$ P.cong  zs  reverse ys ++ zs) (unfold-reverse x xs)
reverse ys ++ reverse (x  xs)
where open P.≡-Reasoning

left-zero :  {} {A B : Set } (f : A  List B)  ( >>= f)
left-zero f = refl

right-zero :  {} {A B : Set } (xs : List A)
(xs >>= const )  (  List B)
right-zero []       = refl
right-zero (x  xs) = right-zero xs

private

not-left-distributive :
let xs = true  false  []; f = return; g = return in
(xs >>= λ x  f x  g x)  ((xs >>= f)  (xs >>= g))
not-left-distributive ()

right-distributive :  {} {A B : Set }
(xs ys : List A) (f : A  List B)
(xs  ys >>= f)  ((xs >>= f)  (ys >>= f))
right-distributive []       ys f = refl
right-distributive (x  xs) ys f = begin
f x  (xs  ys >>= f)            ≡⟨ P.cong (_∣_ (f x)) \$ right-distributive xs ys f
f x  ((xs >>= f)  (ys >>= f))  ≡⟨ P.sym \$ LM.assoc (f x) _ _
(f x  (xs >>= f))  (ys >>= f)
where open P.≡-Reasoning

left-identity :  {} {A B : Set } (x : A) (f : A  List B)
(return x >>= f)  f x
left-identity {} x f = proj₂ (LM.identity {a = }) (f x)

right-identity :  {a} {A : Set a} (xs : List A)
(xs >>= return)  xs
right-identity []       = refl
right-identity (x  xs) = P.cong (_∷_ x) (right-identity xs)

associative :  {} {A B C : Set }
(xs : List A) (f : A  List B) (g : B  List C)
(xs >>= λ x  f x >>= g)  (xs >>= f >>= g)
associative []       f g = refl
associative (x  xs) f g = begin
(f x >>= g)  (xs >>= λ x  f x >>= g)  ≡⟨ P.cong (_∣_ (f x >>= g)) \$ associative xs f g
(f x >>= g)  (xs >>= f >>= g)          ≡⟨ P.sym \$ right-distributive (f x) (xs >>= f) g
(f x  (xs >>= f) >>= g)
where open P.≡-Reasoning

cong :  {} {A B : Set } {xs₁ xs₂} {f₁ f₂ : A  List B}
xs₁  xs₂  f₁  f₂  (xs₁ >>= f₁)  (xs₂ >>= f₂)
cong {xs₁ = xs} refl f₁≗f₂ = P.cong concat (map-cong f₁≗f₂ xs)

-- The applicative functor derived from the list monad.

-- Note that these proofs (almost) show that RawIMonad.rawIApplicative
-- is correctly defined. The proofs can be reused if proof components

module Applicative where

open P.≡-Reasoning

private

-- A variant of flip map.

pam :  {} {A B : Set }  List A  (A  B)  List B
pam xs f = xs >>= return  f

-- ∅ is a left zero for _⊛_.

left-zero :  {} {A B : Set } xs  (  List (A  B))  xs
left-zero xs = begin
xs          ≡⟨ refl
( >>= pam xs)  ≡⟨ Monad.left-zero (pam xs)

-- ∅ is a right zero for _⊛_.

right-zero :  {} {A B : Set } (fs : List (A  B))  fs
right-zero {} fs = begin
fs              ≡⟨ refl
(fs >>= pam )    ≡⟨ (Monad.cong (refl {x = fs}) λ f
(fs >>= λ _  )  ≡⟨ Monad.right-zero fs

-- _⊛_ distributes over _∣_ from the right.

right-distributive :
{} {A B : Set } (fs₁ fs₂ : List (A  B)) xs
(fs₁  fs₂)  xs  (fs₁  xs  fs₂  xs)
right-distributive fs₁ fs₂ xs = begin
(fs₁  fs₂)  xs                     ≡⟨ refl
(fs₁  fs₂ >>= pam xs)               ≡⟨ Monad.right-distributive fs₁ fs₂ (pam xs)
(fs₁ >>= pam xs)  (fs₂ >>= pam xs)  ≡⟨ refl
fs₁  xs  fs₂  xs

-- _⊛_ does not distribute over _∣_ from the left.

private

not-left-distributive :
let fs = id  id  []; xs₁ = true  []; xs₂ = true  false  [] in
fs  (xs₁  xs₂)  (fs  xs₁  fs  xs₂)
not-left-distributive ()

-- Applicative functor laws.

identity :  {a} {A : Set a} (xs : List A)  return id  xs  xs
identity xs = begin
return id  xs          ≡⟨ refl
(return id >>= pam xs)  ≡⟨ Monad.left-identity id (pam xs)
(xs >>= return)         ≡⟨ Monad.right-identity xs
xs

private

pam-lemma :  {} {A B C : Set }
(xs : List A) (f : A  B) (fs : B  List C)
(pam xs f >>= fs)  (xs >>= λ x  fs (f x))
pam-lemma xs f fs = begin
(pam xs f >>= fs)                   ≡⟨ P.sym \$ Monad.associative xs (return  f) fs
(xs >>= λ x  return (f x) >>= fs)  ≡⟨ Monad.cong (refl {x = xs})  x  Monad.left-identity (f x) fs)
(xs >>= λ x  fs (f x))

composition :
{} {A B C : Set }
(fs : List (B  C)) (gs : List (A  B)) xs
return _∘′_  fs  gs  xs  fs  (gs  xs)
composition {} fs gs xs = begin
return _∘′_  fs  gs  xs                      ≡⟨ refl
(return _∘′_ >>= pam fs >>= pam gs >>= pam xs)  ≡⟨ Monad.cong (Monad.cong (Monad.left-identity _∘′_ (pam fs))
f  refl {x = pam gs f}))
fg  refl {x = pam xs fg})
(pam fs _∘′_ >>= pam gs >>= pam xs)             ≡⟨ Monad.cong (pam-lemma fs _∘′_ (pam gs))  _  refl)
((fs >>= λ f  pam gs (_∘′_ f)) >>= pam xs)     ≡⟨ P.sym \$ Monad.associative fs  f  pam gs (_∘′_ f)) (pam xs)
(fs >>= λ f  pam gs (_∘′_ f) >>= pam xs)       ≡⟨ (Monad.cong (refl {x = fs}) λ f
pam-lemma gs (_∘′_ f) (pam xs))
(fs >>= λ f  gs >>= λ g  pam xs (f ∘′ g))     ≡⟨ (Monad.cong (refl {x = fs}) λ f
Monad.cong (refl {x = gs}) λ g
P.sym \$ pam-lemma xs g (return  f))
(fs >>= λ f  gs >>= λ g  pam (pam xs g) f)    ≡⟨ (Monad.cong (refl {x = fs}) λ f
Monad.associative gs (pam xs) (return  f))
(fs >>= pam (gs >>= pam xs))                    ≡⟨ refl
fs  (gs  xs)

homomorphism :  {} {A B : Set } (f : A  B) x
return f  return x  return (f x)
homomorphism f x = begin
return f  return x            ≡⟨ refl
(return f >>= pam (return x))  ≡⟨ Monad.left-identity f (pam (return x))
pam (return x) f               ≡⟨ Monad.left-identity x (return  f)
return (f x)

interchange :  {} {A B : Set } (fs : List (A  B)) {x}
fs  return x  return  f  f x)  fs
interchange fs {x} = begin
fs  return x                    ≡⟨ refl
(fs >>= pam (return x))          ≡⟨ (Monad.cong (refl {x = fs}) λ f