Programming Language Foundations in Agda: Lists

Lists.agda

module Lists where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ; *-distribʳ-+; *-distribˡ-∸; *-comm; +-suc)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
open import Level using (Level)

-- https://gist.github.com/pedrominicz/bce9bcfc44f55c04ee5e0b6d903f5809
open import Isomorphism using (_≃_; _⇔_; extensionality; ∀-extensionality)

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

infixr 5 _∷_

-- Hmmm... I haven't ever used a language with proper macros (i.e. Lisp), but
-- sometimes I do think we could learn something from them.
pattern [_] z = z ∷ []
pattern [_,_] y z = y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_,_] t u v w x y z = t ∷ u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []

_++_ : ∀ {a : Set} → List a → List a → List a
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

++-assoc : ∀ {a : Set} (xs ys zs : List a)
    → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc []       ys zs                           = refl
++-assoc (x ∷ xs) ys zs rewrite ++-assoc xs ys zs = refl

++-identityˡ : ∀ {a : Set} (xs : List a) → [] ++ xs ≡ xs
++-identityˡ xs = refl

++-identityʳ : ∀ {a : Set} (xs : List a) → xs ++ [] ≡ xs
++-identityʳ []                               = refl
++-identityʳ (x ∷ xs) rewrite ++-identityʳ xs = refl

length : ∀ {a : Set} → List a → ℕ
length []       = zero
length (x ∷ xs) = suc (length xs)

length-++ : ∀ {a : Set} (xs ys : List a)
    → length (xs ++ ys) ≡ length xs + length ys
length-++ []       ys                         = refl
length-++ (x ∷ xs) ys rewrite length-++ xs ys = refl

reverse : ∀ {a : Set} → List a → List a
reverse []       = []
reverse (x ∷ xs) = reverse xs ++ [ x ]

reverse-++-distrib : ∀ {a : Set} (xs ys : List a)
    → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-distrib [] ys
    rewrite ++-identityʳ (reverse ys) = refl
reverse-++-distrib (x ∷ xs) ys
    rewrite reverse-++-distrib xs ys
          | ++-assoc (reverse ys) (reverse xs) [ x ] = refl

reverse-involutive : ∀ {a : Set} (xs : List a) → reverse (reverse xs) ≡ xs
reverse-involutive [] = refl
reverse-involutive (x ∷ xs)
    rewrite reverse-++-distrib (reverse xs) [ x ]
          | reverse-involutive xs = refl

shunt : ∀ {a : Set} → List a → List a → List a
shunt []       ys = ys
shunt (x ∷ xs) ys = shunt xs (x ∷ ys)

shunt-reverse : ∀ {a : Set} (xs ys : List a)
    → shunt xs ys ≡ reverse xs ++ ys
shunt-reverse [] ys = refl
shunt-reverse (x ∷ xs) ys
    rewrite ++-assoc (reverse xs) [ x ] ys
          | shunt-reverse xs (x ∷ ys) = refl

reverse' : ∀ {a : Set} → List a → List a
reverse' xs = shunt xs []

reverses : ∀ {a : Set} (xs : List a) → reverse' xs ≡ reverse xs
reverses xs
    rewrite shunt-reverse xs []
          | ++-identityʳ (reverse xs) = refl

map : ∀ {a b : Set} → (a → b) → List a → List b
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

map-compose : ∀ {a b c : Set} (f : a → b) (g : b → c)
    → map (g ∘ f) ≡ map g ∘ map f
map-compose {a} {b} {c} f g = extensionality λ xs → map-compose' f g xs
    where
    map-compose' : ∀ (f : a → b) (g : b → c) (xs : List a)
        → map (g ∘ f) xs ≡ (map g ∘ map f) xs
    map-compose' f g []                                   = refl
    map-compose' f g (x ∷ xs) rewrite map-compose' f g xs = refl

map-++-distrib : ∀ {a b : Set} (f : a → b) (xs ys : List a)
    → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-distrib f []       ys                                = refl
map-++-distrib f (x ∷ xs) ys rewrite map-++-distrib f xs ys = refl

data Tree (a b : Set) : Set where
    leaf : a → Tree a b
    node : Tree a b → b → Tree a b → Tree a b

map-Tree : ∀ {a b c d : Set} → (a → c) → (b → d) → Tree a b → Tree c d
map-Tree f g (leaf a)     = leaf (f a)
map-Tree f g (node l b r) = node (map-Tree f g l) (g b) (map-Tree f g r)

foldr : ∀ {a b : Set} → (a → b → b) → b → List a → b
foldr _⊗_ e []       = e
foldr _⊗_ e (x ∷ xs) = x ⊗ foldr _⊗_ e xs

sum : List ℕ → ℕ
sum = foldr _+_ 0

product : List ℕ → ℕ
product = foldr _*_ 1

foldr-++ : ∀ {a b : Set} (_⊗_ : a → b → b) (e : b) (xs ys : List a)
    → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
foldr-++ _⊗_ e []       ys                              = refl
foldr-++ _⊗_ e (x ∷ xs) ys rewrite foldr-++ _⊗_ e xs ys = refl

foldr-∷ : ∀ {a : Set} (xs : List a) → foldr _∷_ [] xs ≡ xs
foldr-∷ []                          = refl
foldr-∷ (x ∷ xs) rewrite foldr-∷ xs = refl

foldr-++-∷ : ∀ {a : Set} (xs ys : List a) → xs ++ ys ≡ foldr _∷_ ys xs
foldr-++-∷ []       ys                          = refl
foldr-++-∷ (x ∷ xs) ys rewrite foldr-++-∷ xs ys = refl

map-is-foldr : ∀ {a b : Set} (f : a → b)
    → map f ≡ foldr (λ x xs → f x ∷ xs) []
map-is-foldr {a} {b} f = extensionality λ x → map-is-foldr' f x
    where
    map-is-foldr' : ∀ (f : a → b) (xs : List a)
        → map f xs ≡ foldr (λ x xs → f x ∷ xs) [] xs
    map-is-foldr' f []                                  = refl
    map-is-foldr' f (x ∷ xs) rewrite map-is-foldr' f xs = refl

fold-Tree : ∀ {a b c : Set} → (a → c) → (c → b → c → c) → Tree a b → c
fold-Tree f g (leaf a)     = f a
fold-Tree f g (node l b r) = g (fold-Tree f g l) b (fold-Tree f g r)

map-is-fold-Tree : ∀ {a b c d : Set} (f : a → c) (g : b → d)
    → map-Tree f g ≡ fold-Tree (λ a → leaf (f a)) (λ l b r → node l (g b) r)
map-is-fold-Tree {a} {b} {c} {d} f g = extensionality λ x → map-is-fold-Tree' f g x
    where
    map-is-fold-Tree' : ∀ (f : a → c) (g : b → d) (x : Tree a b)
        → map-Tree f g x ≡ fold-Tree (λ a → leaf (f a)) (λ l b r → node l (g b) r) x
    map-is-fold-Tree' f g (leaf a) = refl
    map-is-fold-Tree' f g (node l b r)
        rewrite map-is-fold-Tree' f g l
              | map-is-fold-Tree' f g r = refl

downFrom : ℕ → List ℕ
downFrom zero    = []
downFrom (suc n) = n ∷ downFrom n

-- This shows a problem with `rewrite`: it's really hard to read and get what
-- is going on.
sum-downFrom-helper : ∀ (n : ℕ) → n + n * n ≡ n * 2 + n * (n ∸ 1)
sum-downFrom-helper zero = refl
sum-downFrom-helper (suc n)
    rewrite *-comm n (suc n)
          | sum-downFrom-helper n
          | *-comm n 2
          | +-identityʳ n
          | +-suc n (n + (n + n + n * (n ∸ 1)))
          | +-assoc n n (n + n + n * (n ∸ 1)) = refl

sum-downFrom : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-downFrom zero = refl
sum-downFrom (suc n)
    rewrite *-distribʳ-+ 2 n (sum (downFrom n))
          | sum-downFrom-helper n
          | sum-downFrom n = refl

record IsMonoid {a : Set} (_⊗_ : a → a → a) (e : a) : Set where
    field
        assoc : ∀ (x y z : a) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
        identityˡ : ∀ (x : a) → e ⊗ x ≡ x
        identityʳ : ∀ (x : a) → x ⊗ e ≡ x

open IsMonoid

+-monoid : IsMonoid _+_ 0
+-monoid = record
    { assoc     = +-assoc
    ; identityˡ = +-identityˡ
    ; identityʳ = +-identityʳ
    }

*-monoid : IsMonoid _*_ 1
*-monoid = record
    { assoc     = *-assoc
    ; identityˡ = *-identityˡ
    ; identityʳ = *-identityʳ
    }

++-monoid : ∀ {a : Set} → IsMonoid {List a} _++_ []
++-monoid = record
    { assoc     = ++-assoc
    ; identityˡ = ++-identityˡ
    ; identityʳ = ++-identityʳ
    }

foldr-monoid : ∀ {a : Set} (_⊗_ : a → a → a) (e : a) → IsMonoid _⊗_ e
    → ∀ (xs : List a) (y : a) → foldr _⊗_ y xs ≡ foldr _⊗_ e xs ⊗ y
foldr-monoid _⊗_ e monoid [] y rewrite identityˡ monoid y = refl
foldr-monoid _⊗_ e monoid (x ∷ xs) y
    rewrite assoc monoid x (foldr _⊗_ e xs) y
          | foldr-monoid _⊗_ e monoid xs y = refl

foldr-monoid-++ : ∀ {a : Set} (_⊗_ : a → a → a) (e : a) → IsMonoid _⊗_ e
    → ∀ (xs ys : List a)
    → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
foldr-monoid-++ _⊗_ e monoid [] ys
    rewrite identityˡ monoid (foldr _⊗_ e ys) = refl
foldr-monoid-++ _⊗_ e monoid (x ∷ xs) ys
    rewrite assoc monoid x (foldr _⊗_ e xs) (foldr _⊗_ e ys)
          | foldr-monoid-++ _⊗_ e monoid xs ys = refl

foldl : ∀ {a b : Set} → (b → a → b) → b → List a → b
foldl _⊗_ e []       = e
foldl _⊗_ e (x ∷ xs) = foldl _⊗_ (e ⊗ x) xs

-- The difficulty for this one was listed as "practice". I probably found an
-- overcomplicated solution.
foldr-monoid-foldl-helper : ∀ {a : Set} (_⊗_ : a → a → a) (e : a) → IsMonoid _⊗_ e
    → ∀ (y : a) (xs : List a) → foldl _⊗_ y xs ≡ y ⊗ foldl _⊗_ e xs
foldr-monoid-foldl-helper _⊗_ e monoid y []
    rewrite identityʳ monoid y = refl
foldr-monoid-foldl-helper _⊗_ e monoid y (x ∷ xs)
    rewrite identityˡ monoid x
          | foldr-monoid-foldl-helper _⊗_ e monoid x xs
          | sym (assoc monoid y x (foldl _⊗_ e xs))
          | foldr-monoid-foldl-helper _⊗_ e monoid (y ⊗ x) xs = refl

foldr-monoid-foldl : ∀ {a : Set} (_⊗_ : a → a → a) (e : a) → IsMonoid _⊗_ e
    → ∀ (xs : List a) → foldr _⊗_ e xs ≡ foldl _⊗_ e xs
foldr-monoid-foldl _⊗_ e monoid [] = refl
foldr-monoid-foldl _⊗_ e monoid (x ∷ xs)
    rewrite identityˡ monoid x
          | foldr-monoid-foldl-helper _⊗_ e monoid x xs
          | foldr-monoid-foldl _⊗_ e monoid xs = refl

data All {a : Set} (P : a → Set) : List a → Set where
    []  : All P []
    _∷_ : ∀ {x : a} {xs : List a} → P x → All P xs → All P (x ∷ xs)

data Any {a : Set} (P : a → Set) : List a → Set where
    here  : ∀ {x : a} {xs : List a} → P x → Any P (x ∷ xs)
    there : ∀ {x : a} {xs : List a} → Any P xs → Any P (x ∷ xs)

infix 4 _∈_ _∉_

_∈_ : ∀ {a : Set} (x : a) (xs : List a) → Set
x ∈ xs = Any (x ≡_) xs

_∉_ : ∀ {a : Set} (x : a) (xs : List a) → Set
x ∉ xs = ¬ (x ∈ xs)

All-++-≃ : ∀ {a : Set} {P : a → Set} (xs ys : List a)
    → All P (xs ++ ys) ≃ (All P xs × All P ys)
All-++-≃ {a} {P} xs ys = record
    { to   = to xs ys
    ; from = from xs ys
    ; from∘to = from∘to xs ys
    ; to∘from = to∘from xs ys
    }
    where
    to : ∀ (xs ys : List a) → All P (xs ++ ys) → All P xs × All P ys
    to []       ys pys       = ([] , pys)
    to (x ∷ xs) ys (px ∷ ps) = let (pxs , pys) = to xs ys ps in (px ∷ pxs , pys)

    from : ∀ (xs ys : List a) → All P xs × All P ys → All P (xs ++ ys)
    from []       ys ([]       , pys) = pys
    from (x ∷ xs) ys (px ∷ pxs , pys) = px ∷ from xs ys (pxs , pys)

    from∘to : ∀ (xs ys : List a) (ps : All P (xs ++ ys))
        → from xs ys (to xs ys ps) ≡ ps
    from∘to []       ys ps                                 = refl
    from∘to (x ∷ xs) ys (px ∷ ps) rewrite from∘to xs ys ps = refl

    to∘from : ∀ (xs ys : List a) (ps : All P xs × All P ys)
        → to xs ys (from xs ys ps) ≡ ps
    to∘from []       ys ([]       , pys)                                   = refl
    to∘from (x ∷ xs) ys (px ∷ pxs , pys) rewrite to∘from xs ys (pxs , pys) = refl

Any-++-≃ : ∀ {a : Set} {P : a → Set} (xs ys : List a)
    → Any P (xs ++ ys) ≃ (Any P xs ⊎ Any P ys)
Any-++-≃ {a} {P} xs ys = record
    { to   = to xs ys
    ; from = from xs ys
    ; from∘to = from∘to xs ys
    ; to∘from = to∘from xs ys
    }
    where
    to : ∀ (xs ys : List a) → Any P (xs ++ ys) → Any P xs ⊎ Any P ys
    to []       ys p         = inj₂ p
    to (x ∷ xs) ys (here p)  = inj₁ (here p)
    to (x ∷ xs) ys (there p) with to xs ys p
    ...                         | inj₁ p' = inj₁ (there p')
    ...                         | inj₂ p' = inj₂ p'

    from : ∀ (xs ys : List a) → Any P xs ⊎ Any P ys → Any P (xs ++ ys)
    from []       ys (inj₂ p)         = p
    from (x ∷ xs) ys (inj₂ p)         = there (from xs ys (inj₂ p))
    from (x ∷ xs) ys (inj₁ (here p))  = here p
    from (x ∷ xs) ys (inj₁ (there p)) = there (from xs ys (inj₁ p))

    -- This isomorphism may or may not be possible.
    postulate
        from∘to : ∀ (xs ys : List a) (p : Any P (xs ++ ys))
            → from xs ys (to xs ys p) ≡ p
        --from∘to []       ys p        = refl
        --from∘to (x ∷ xs) ys (here p) = refl
        --from∘to (x ∷ xs) ys (there p) = ?

        to∘from : ∀ (xs ys : List a) (p : Any P xs ⊎ Any P ys)
            → to xs ys (from xs ys p) ≡ p

¬Any≃All¬ : ∀ {a : Set} {P : a → Set} (xs : List a)
    → ¬ (Any P xs) ≃ All (¬_ ∘ P) xs
¬Any≃All¬ {a} {P} xs = record
    { to   = to xs
    ; from = from xs
    ; from∘to = from∘to xs
    ; to∘from = to∘from xs
    }
    where
    to : ∀ (xs : List a) → ¬ (Any P xs) → All (¬_ ∘ P) xs
    to []       ¬any = []
    to (x ∷ xs) ¬any = (λ p → ¬any (here p)) ∷ to xs (λ x → ¬any (there x))

    from : ∀ (xs : List a) → All (¬_ ∘ P) xs → ¬ (Any P xs)
    from (x ∷ xs) (¬p ∷ ¬ps) = λ { (here p) → ¬p p ; (there p) → from xs ¬ps p }

    from∘to : ∀ (xs : List a) (¬any : ¬ (Any P xs)) → from xs (to xs ¬any) ≡ ¬any
    from∘to []       ¬any = extensionality λ ()
    from∘to (x ∷ xs) ¬any = extensionality λ any → helper any
        where
        helper : (any : Any P (x ∷ xs))
            → from (x ∷ xs) (to (x ∷ xs) ¬any) any ≡ ¬any any
        helper (here p)                                            = refl
        helper (there p) rewrite from∘to xs (λ x → ¬any (there x)) = refl

    to∘from : ∀ (xs : List a) (all¬ : All (¬_ ∘ P) xs) → to xs (from xs all¬) ≡ all¬
    to∘from []       []                                = refl
    to∘from (x ∷ xs) (¬p ∷ ¬ps) rewrite to∘from xs ¬ps = refl

{-
¬All≃Any¬ : ∀ {a : Set} {P : a → Set} (xs : List a)
    → ¬ (All P xs) ≃ Any (¬_ ∘ P) xs
¬All≃Any¬ {a} {P} xs = record
    { to   = to xs
    ; from = from xs
    ; from∘to = from∘to xs
    ; to∘from = to∘from xs
    }
    where
    to : ∀ (xs : List a) → ¬ All P xs → Any (¬_ ∘ P) xs
    to []       ¬all = ⊥-elim (¬all [])
    to (x ∷ xs) ¬all = there (to xs (λ all → ¬all (? ∷ all)))

    postulate
        from : ∀ (xs : List a) → Any (¬_ ∘ P) xs → ¬ All P xs
        from∘to : ∀ (xs : List a) (¬all : ¬ All P xs) → from xs (to xs ¬all) ≡ ¬all
        to∘from : ∀ (xs : List a) (any¬ : Any (¬_ ∘ P) xs) → to xs (from xs any¬) ≡ any¬
-}

All-∀ : ∀ {a : Set} {P : a → Set} (xs : List a)
    → All P xs ≃ (∀ (x : a) → x ∈ xs → P x)
All-∀ {a} {P} xs = record
    { to   = to xs
    ; from = from xs
    ; from∘to = from∘to xs
    ; to∘from = to∘from xs
    }
    where
    to : ∀ (xs : List a) → All P xs → ∀ (x : a) → x ∈ xs → P x
    to (x ∷ xs) (p ∷ ps) x (here refl) = p
    to (x ∷ xs) (p ∷ ps) y (there ∈)   = to xs ps y ∈

    from : ∀ (xs : List a) → (∀ (x : a) → x ∈ xs → P x) → All P xs
    from []       f = []
    from (x ∷ xs) f = f x (here refl) ∷ from xs (λ x ∈ → f x (there ∈))

    from∘to : ∀ (xs : List a) (all : All P xs) → from xs (to xs all) ≡ all
    from∘to []       []                             = refl
    from∘to (x ∷ xs) (p ∷ ps) rewrite from∘to xs ps = refl

    to∘from : ∀ (xs : List a) (f : (x : a) → x ∈ xs → P x) → to xs (from xs f) ≡ f
    to∘from []       f = ∀-extensionality λ x → extensionality λ ()
    to∘from (x ∷ xs) f = ∀-extensionality λ y → extensionality (helper y)
        where
        helper : ∀ (y : a) (∈ : y ∈ x ∷ xs)
            → to (x ∷ xs) (from (x ∷ xs) f) y ∈ ≡ f y ∈
        helper y (here refl) rewrite to∘from xs (λ x ∈ → f x (there ∈)) = refl
        helper y (there ∈)   rewrite to∘from xs (λ x ∈ → f x (there ∈)) = refl

Any-∃ : ∀ {a : Set} {P : a → Set} (xs : List a)
    → Any P xs ≃ ∃[ x ] (x ∈ xs × P x)
Any-∃ {a} {P} xs = record
    { to   = to xs
    ; from = from xs
    ; from∘to = from∘to xs
    ; to∘from = to∘from xs
    }
    where
    to : ∀ (xs : List a) → Any P xs → ∃[ x ] (x ∈ xs × P x)
    to (x ∷ xs) (here p)  = (x , here refl , p)
    to (x ∷ xs) (there p) = let (x , ∈ , p) = to xs p in (x , there ∈ , p)

    from : ∀ (xs : List a) → ∃[ x ] (x ∈ xs × P x) → Any P xs
    from (x ∷ xs) (x  , here refl , p) = here p
    from (x ∷ xs) (x' , there ∈   , p) = there (from xs (x' , ∈ , p))

    from∘to : ∀ (xs : List a) (any : Any P xs) → from xs (to xs any) ≡ any
    from∘to (x ∷ xs) (here p)                       = refl
    from∘to (x ∷ xs) (there p) rewrite from∘to xs p = refl

    to∘from : ∀ (xs : List a) (∃ : ∃[ x ] (x ∈ xs × P x)) → to xs (from xs ∃) ≡ ∃
    to∘from (x ∷ xs) (x  , here refl , p)                                 = refl
    to∘from (x ∷ xs) (x' , there ∈   , p) rewrite to∘from xs (x' , ∈ , p) = refl

all : ∀ {a : Set} → (a → Bool) → List a → Bool
all p = foldr _∧_ true ∘ map p

Decidable : ∀ {a : Set} → (a → Set) → Set
Decidable {a} P = ∀ (x : a) → Dec (P x)

All? : ∀ {a : Set} {P : a → Set} → Decidable P → Decidable (All P)
All? p? [] = yes []
All? p? (x ∷ xs) with p? x  | All? p? xs
...                 | yes p | yes ps = yes (p ∷ ps)
...                 | no ¬p | _      = no λ { (p ∷ ps) → ¬p p }
...                 | _     | no ¬ps = no λ { (p ∷ ps) → ¬ps ps }

any : ∀ {a : Set} → (a → Bool) → List a → Bool
any p = foldr _∨_ false ∘ map p

Any? : ∀ {a : Set} {P : a → Set} → Decidable P → Decidable (Any P)
Any? p? [] = no λ ()
Any? p? (x ∷ xs) with p? x  | Any? p? xs
...                 | yes p | _      = yes (here p)
...                 | _     | yes ps = yes (there ps)
...                 | no ¬p | no ¬ps = no λ { (here p) → ¬p p ; (there ps) → ¬ps ps }

data merge {a : Set} : (xs ys zs : List a) → Set where
    [] : merge [] [] []
    left-∷  : ∀ {x xs ys zs} → merge xs ys zs → merge (x ∷ xs) ys (x ∷ zs)
    right-∷ : ∀ {y xs ys zs} → merge xs ys zs → merge xs (y ∷ ys) (y ∷ zs)

split : ∀ {a : Set} {P : a → Set} (P? : Decidable P) (zs : List a)
    → ∃[ xs ] ∃[ ys ] (merge xs ys zs × All P xs × All (¬_ ∘ P) ys)
split p? []       = ([] , [] , [] , [] , [])
split p? (z ∷ zs) with p? z  | split p? zs
...                  | yes p | (xs , ys , m , ps , ¬ps) = (z ∷ xs , ys , left-∷ m , p ∷ ps , ¬ps)
...                  | no ¬p | (xs , ys , m , ps , ¬ps) = (xs , z ∷ ys , right-∷ m , ps , ¬p ∷ ¬ps)

data IsZero : ℕ → Set where
    zero : IsZero zero

zero? : ∀ (x : ℕ) → Dec (IsZero x)
zero? zero    = yes zero
zero? (suc n) = no λ ()

-- split zero? (1 ∷ 0 ∷ 0 ∷ 2 ∷ 5 ∷ [])