List.agda

module List where

open import Core

infixr 10 _∷_

data List : Set where
  [] : List
  _∷_ : ℕ → List → List

infix 5 _∈_

data _∈_ : ℕ → List → Set where
  here : ∀ {x xs} → x ∈ x ∷ xs
  there : ∀ {x y xs} → x ∈ xs → x ∈ y ∷ xs

_∈?_ : (x : ℕ) (xs : List) → Decidable (x ∈ xs)
x ∈? [] = no λ ()
x ∈? (y ∷ xs) with x ≟ y
... | yes x=y = yes (subst x=y (here {x} {xs}))
... | no ¬x=y with x ∈? xs
... | yes x∈xs = yes (there x∈xs)
... | no ¬x∈xs = no λ
  { here → ¬x=y refl
  ; (there x∈yxs) → ¬x∈xs x∈yxs
  }

_++_ : List → List → List
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data all : (ℕ → Set) → List → Set where
  [] : ∀ {F} → all F []
  _∷_ : ∀ {F x xs} → F x → all F xs → all F (x ∷ xs)

all-pop : ∀ {F x xs} → all F (x ∷ xs) → all F xs
all-pop (x ∷ xs) = xs

each : ∀ {x xs} {F : ℕ → Set} → all F xs → x ∈ xs → F x
each (x ∷ allxs) here = x
each (x ∷ allxs) (there x∈xs) = each allxs x∈xs

all-subst : {F G : ℕ → Set} → (∀ {x} → F x → G x) → ∀ {xs} → all F xs → all G xs
all-subst F⇒G [] = []
all-subst F⇒G (x ∷ xs) = F⇒G x ∷ all-subst F⇒G xs

++-all : ∀ {xs ys F} → all F xs → all F ys → all F (xs ++ ys)
++-all [] ys = ys
++-all (x ∷ xs) ys = x ∷ (++-all xs ys)

_<∈_ : ℕ → List → Set
x <∈ xs = all (λ y → x < y) xs

_≤∈_ : ℕ → List → Set
x ≤∈ xs = all (λ y → x ≤ y) xs

_>∈_ : ℕ → List → Set
x >∈ xs = all (λ y → x > y) xs

_≥∈_ : ℕ → List → Set
x ≥∈ xs = all (λ y → x ≥ y) xs

<∈-suc : ∀ {x y xs} → x < y → y <∈ xs → x <∈ (y ∷ xs)
<∈-suc {x} x<y y<xs = x<y ∷ all-subst (<-trans x<y) y<xs

data Sorted : List → Set where
  [] : Sorted []
  singleton : ∀ x → Sorted (x ∷ [])
  _∷_ : ∀ {x y xs} → x < y → Sorted (y ∷ xs) → Sorted (x ∷ y ∷ xs)

sorted-pop : ∀ {x xs} → Sorted (x ∷ xs) → Sorted xs
sorted-pop (singleton _) = []
sorted-pop (x ∷ xxs<) = xxs<

xmin : ∀ {x xs} → Sorted (x ∷ xs) → x <∈ xs
xmin .{x} .{[]} (singleton x) = []
xmin {x} {y ∷ ys} (x<y ∷ xs<) = <∈-suc x<y (xmin xs<)

SList = Σ List Sorted

open Σ

s-insert-lower : ∀ x {xs} → x <∈ xs → Sorted xs → Sorted (x ∷ xs)
s-insert-lower x x< [] = singleton x
s-insert-lower x (x<y ∷ _) (singleton y) = x<y ∷ singleton y
s-insert-lower x (x<y ∷ _) (y ∷ xs<) = x<y ∷ y ∷ xs<

++-sorted-bounded : ∀ {xs ys m} → m >∈ xs → m ≤∈ ys → Sorted xs → Sorted ys → Sorted (xs ++ ys)
++-sorted-bounded {[]} {ys} {m} m>xs m≤ys xs< ys< = ys<
++-sorted-bounded {x ∷ xs} {ys} {m} m>xs m≤ys xs< ys< =
  s-insert-lower x (++-all (xmin xs<) x<∈ys) xs++ys<
  where
    xs++ys< : Sorted (xs ++ ys)
    xs++ys< = ++-sorted-bounded (all-pop m>xs) m≤ys (sorted-pop xs<) ys<
    x<∈ys : x <∈ ys
    x<∈ys = all-subst (λ m≤z → <-≤-trans (each m>xs here) m≤z) m≤ys

-- x∉xs : ∀ {x xs} → Sorted (x 

{-
s-insert-m : ℕ → ℕ → SList → SList
s-insert-m zero _ xs = xs
s-insert-m (suc m) x (.[] , []) = x ∷ [] , singleton x
s-insert-m (suc m) x (.(y ∷ []) , singleton y) with x <?> y
... | le x<y = x ∷ y ∷ [] , x<y ∷ singleton y
... | eq x=y = y ∷ [] , singleton y
... | gt x>y = y ∷ x ∷ [] , x>y ∷ singleton x
s-insert-m (suc m) x (y ∷ z ∷ xs , y<z ∷ zxs<) with x <?> y
... | le x<y = x ∷ y ∷ z ∷ xs , x<y ∷ y<z ∷ zxs<
... | eq x=y = y ∷ z ∷ xs , y<z ∷ zxs<
... | gt x>y
  with s-insert-m m x (z ∷ xs , zxs<)
... | [] , xzxs< = y ∷ [] , singleton y
... | w ∷ xzxs , xzxs<
  with y <?> w
... | le y<w = y ∷ w ∷ xzxs , y<w ∷ xzxs<
... | eq refl = {!!}
... | gt y>w = {!!}
-- y ∷ w ∷ xzxs , {!!}
-}

{-
s-insert : ℕ → SList → SList
s-insert x (.[] , []) = x ∷ [] , singleton x
s-insert x (.(y ∷ []) , singleton y) with x <?> y
... | le x<y = x ∷ y ∷ [] , x<y ∷ singleton y
... | eq x=y = y ∷ [] , singleton y
... | gt x>y = y ∷ x ∷ [] , x>y ∷ singleton x
s-insert x (y ∷ z ∷ xs , y<z ∷ zxs<) with x <?> y
... | le x<y = x ∷ y ∷ z ∷ xs , x<y ∷ y<z ∷ zxs<
... | eq x=y = y ∷ z ∷ xs , y<z ∷ zxs<
... | gt x>y with s-insert x (z ∷ xs , zxs<)
... | (xzxs , xzxs<) = {!!}
-}

{-
-- helper: for termination checking we have m always decreasing
s-insert-with-length : ℕ → ℕ → SList → SList
s-insert-with-length zero x xs = xs
s-insert-with-length (suc m) x ([] , []) = x ∷ [] , [] ∷ []
s-insert-with-length (suc m) x (y ∷ xs , y< ∷ xs<)
  with x <?> y
... | le x<y = x ∷ y ∷ xs , <∈-suc x<y y< ∷ y< ∷ xs<
... | eq x=y = y ∷ xs , y< ∷ xs<
... | gt x>y
  with s-insert-with-length m x (xs , xs<)
... | xxs , xxs< = y ∷ xxs , {!!} ∷ xxs<
-}

{-
s-insert : ℕ → SList → SList
s-insert x ([] , []) = x ∷ [] , [] ∷ []
s-insert x (y ∷ xs , y< ∷ sorted) with x <?> y
... | le x<y = x ∷ y ∷ xs , <∈-suc x<y y< ∷ y< ∷ sorted
... | eq x=y = y ∷ xs , y< ∷ sorted
... | gt x>y with s-insert x (xs , sorted)
... | xxs = {!!}
-}

{-
i-sort : List → SList
i-sort [] = [] , []
i-sort (x ∷ xs) = {!!}
-}