Split

Split.agda

module Split where

open import Data.Bool
open import Data.Nat
open import Data.Nat.Properties
open import Data.List hiding ([_])
open import Data.Product

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Induction.WellFounded as WF
import Induction.Nat as NI

-- If this is in Dummy, I get a weird error
open Subrelation {_<₁_ = λ i j → i < j} ≤⇒≤′ renaming (well-founded to <-well-founded)

module Split {A} where
  open Inverse-image {A = List A} {ℕ} {_<_ = _<_} length
  open WF.All (well-founded (<-well-founded NI.<-well-founded)) renaming (wfRec to <-rec)

  open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)

  break-< : (p : A → Bool) (xs : List A) → length (proj₂ (break p xs)) ≤ length xs
  break-< p [] = z≤n
  break-< p (x ∷ xs) with p x
  break-< p (x ∷ xs) | true = ≤-refl
  break-< p (x ∷ xs) | false = ≤-trans (break-< p xs) (n≤1+n _)

  split : (A → Bool) → List A → List (List A)
  split p xs = <-rec _ helper xs
    where
    helper : (xs : List A) (f : (ys : List A) → length ys < length xs → List (List A)) → List (List A)
    helper xs f with break p xs | inspect (break p) xs 
    helper xs f | h , [] | _ = h ∷ []
    helper xs f | h , t ∷ ts | [ eq ] = h ∷ f ts (subst (λ q → length (proj₂ q) ≤ length xs) eq (break-< p xs))

open Split