{-# OPTIONS --safe #-}

module Data.List.Properties where

open import Prelude

mapl-id : (xs : List A) → mapl id xs ≡ xs
mapl-id [] = refl
mapl-id (x ∷ xs) = cong (x ∷_) (mapl-id xs)

foldr-universal : ∀ (h : List B → A) f e
                → (h [] ≡ e)
                → (∀ x xs → h (x ∷ xs) ≡ f x (h xs))
                → ∀ xs → h xs ≡ foldr f e xs
foldr-universal h f e base step [] = base
foldr-universal h f e base step (x ∷ xs) =
  step x xs ⨾ cong (f x) (foldr-universal h f e base step xs)

foldr-fusion : ∀ (f : C → A) {_⊕_ : B → C → C} {_⊗_ : B → A → A} e
              → (∀ x y → f (x ⊕ y) ≡ x ⊗ f y)
              → ∀ xs → f (foldr _⊕_ e xs) ≡ foldr _⊗_ (f e) xs
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))

foldr-++ : (f : A → B → B) (b : B) (xs ys : List A)
         → foldr f b (xs ++ ys) ≡ foldr f (foldr f b ys) xs
foldr-++ f b xs ys = foldr-fusion (foldr f b) ys (λ _ _ → refl) xs

foldl-by-r : (B → A → B) → B → List A → B
foldl-by-r f b xs = foldr (λ x k xs → k (f xs x)) id xs b

foldl-is-foldr : (f : B → A → B) (z : B) (xs : List A) →
                 foldl f z xs ≡ foldl-by-r f z xs
foldl-is-foldr f z xs =
  cong (_$ z) (foldr-universal (flip (foldl f)) (λ x k xs → k (f xs x)) id refl (λ x xs → refl) xs) 

foldl-fusion : ∀ (f : C → A) {_⊕_ : C → B → C}  {_⊗_ : A → B → A} e →
                 (∀ x y → f (x ⊕ y) ≡ f x ⊗ y) →
                 ∀ xs → f (foldl _⊕_ e xs) ≡ foldl _⊗_ (f e) xs
foldl-fusion h {f} {g} e fuse [] = refl
foldl-fusion h {f} {g} e fuse (x ∷ xs) =
  foldl-fusion h (f e x) fuse xs ⨾ cong (flip (foldl g) xs) (fuse e x)

module _ {A : Type a} {B : Type b} where
  foldl-++ : (f : B → A → B) (b : B) (xs ys : List A)
          → foldl f b (xs ++ ys) ≡ foldl f (foldl f b xs) ys
  foldl-++ f b xs ys =
    foldl f b (xs ++ ys) ≡⟨ foldl-is-foldr f b (xs ++ ys) ⟩
    foldl-by-r f b (xs ++ ys) ≡⟨ cong (_$ b) (foldr-++ (λ x k b → k (f b x)) id xs ys) ⟩
    foldr (λ x k b → k (f b x)) (foldr (λ x k b → k (f b x)) id ys) xs b ≡˘⟨ cong (λ e → foldr (λ x k b → k (f b x)) e xs b) (funExt λ b → foldl-is-foldr f b ys) ⟩
    foldr (λ x k b → k (f b x)) (flip (foldl f) ys) xs b ≡˘⟨ cong′ {A = B → B} (_$ b) (foldr-universal (λ xs b → foldl f (foldl f b xs) ys) (λ x k b → k (f b x)) (flip (foldl f) ys) refl (λ _ _ → refl) xs ) ⟩
    foldl f (foldl f b xs) ys ∎

open import Data.Fin

_!_ : (xs : List A) → Fin (length xs) → A
(x ∷ xs) ! fz = x
(x ∷ xs) ! fs i = xs ! i

Any All : (A → Type p) → List A → Type p
Any P xs = Σ[ i ⦂ Fin (length xs) ] × P (xs ! i)
All P xs = ∀ (i : Fin (length xs)) → P (xs ! i)


here : ∀ (x : A) xs {P : A → Type p} → P x → Any P (x ∷ xs)
here _ _ Px = (fz , Px)

there : ∀ {P : A → Type p} (x : A) {xs} → Any P xs → Any P (x ∷ xs)
there _ (i , Pxs) = fs i , Pxs

module _ {A : Type a} {P : A → Type p} (P? : ∀ x → Dec (P x)) where
  Any? : ∀ xs → Dec (Any P xs)
  Any? [] = no (λ ())
  Any? (x ∷ xs) with P? x | Any? xs
  ... | yes Px | Pxs = yes (fz , Px)
  ... | no ¬Px | yes (i , Pxs) = yes (fs i , Pxs)
  ... | no ¬Px | no ¬Pxs = no λ { (fz , Pxs) → ¬Px Pxs ; (fs x , Pxs) → ¬Pxs (x , Pxs)}

  All? : ∀ xs → Dec (All P xs)
  All? [] = yes λ ()
  All? (x ∷ xs) with P? x | All? xs
  ... | no ¬Px | _ = no λ z → ¬Px (z fz)
  ... | yes Px | no ¬Pxs = no λ z → ¬Pxs (λ i → z (fs i))
  ... | yes Px | yes Pxs = yes λ { fz → Px ; (fs i) → Pxs i }