Merge and sorted lists and agda

SortedList.agda

open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming (sym to psym ; trans to ptrans)

module SortedList
  (A : Set)
  (_≤_ : A -> A -> Set)
  (isDecTotalOrder : IsDecTotalOrder _≡_ _≤_)
where

open import Data.Nat hiding (_≤_  ; _≤?_)
open import Data.List hiding ([_])
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Data.Nat.Properties as NP
open import Algebra.Structures
open import Relation.Nullary
open import Relation.Unary
open import Function

open IsDecTotalOrder isDecTotalOrder
module TO = IsDecTotalOrder isDecTotalOrder

module NC = IsCommutativeSemiring NP.isCommutativeSemiring

mutual
  data SVec : ℕ -> Set where
    [] : SVec 0
    [_] : A -> SVec 1
    _∷_Witness_ : ∀ {n} -> (x : A) -> (xs : SVec (suc n)) -> (p : x ≤ min xs) -> SVec (suc (suc n))

  min : ∀ {n} -> SVec (suc n) -> A
  min [ x ] = x
  min (x ∷ xs Witness _) = x

max : ∀ {n} -> SVec (suc n) -> A
max [ x ] = x
max (x ∷ xs Witness _) = max xs

rest : ∀ {n} -> SVec (suc n) -> SVec n
rest [ _ ] = []
rest (x ∷ xs Witness p) = xs

min-is-min : {n m : ℕ} (eq : suc n ≡ suc m) (xs : SVec (suc n)) -> min xs ≡ min (subst SVec eq xs)
min-is-min eq xs with eq
min-is-min eq [ y ] | _≡_.refl = _≡_.refl
min-is-min eq (x ∷ xs Witness p) | _≡_.refl = _≡_.refl

data All (P : A -> Set) : {n : ℕ} (xs : SVec n) -> Set where
  []-All : All P []
  _:All_∷_ : ∀ {n} (xs : SVec (suc n)) -> P (min xs) -> All P (rest xs) -> All P {suc n} xs

map-all : {P Q : A -> Set} {n : ℕ} {xs : SVec n} -> P ⊆ Q -> All P xs -> All Q xs
map-all f []-All = []-All
map-all {xs = xs} f (.xs :All p ∷ ps) = xs :All f p ∷ map-all f ps

min≤rest : ∀ {n} (xs : SVec (suc n)) -> All (_≤_ (min xs)) (rest xs)
min≤rest [ x ] = []-All
min≤rest (x ∷ xs Witness p) = xs :All p ∷ map-all (TO.trans p) (min≤rest xs)

lview : ∀ {n} -> SVec (suc n) -> A × SVec n
lview [ x ] = x , []
lview (x ∷ xs Witness _) = x , xs

toList : ∀ {n} -> SVec n -> List A
toList [] = []
toList [ x ] = x ∷ []
toList (x ∷ xs Witness _) = x ∷ toList xs

≤-sym : {x y : A} -> ¬ (x ≤ y) -> y ≤ x
≤-sym {x} {y} p with total x y
≤-sym p | inj₁ a = ⊥-elim (p a)
≤-sym p | inj₂ b = b

mutual
  insert : ∀ {n} -> A -> SVec n -> SVec (suc n)
  insert x [] = [ x ]
  insert x [ y ] with total x y
  insert x [ y ] | inj₁ p = x ∷ [ y ] Witness p
  insert x [ y ] | inj₂ p = y ∷ [ x ] Witness p
  insert x (y ∷ ys Witness p) with total x y
  insert x (y ∷ ys Witness p) | inj₁ q = x ∷ y ∷ ys Witness p Witness q
  insert x (y ∷ ys Witness p) | inj₂ q = y ∷ insert x ys Witness y≤min-insert y x ys p q

  y≤min-insert : ∀ {n} -> (v x : A)(ys : SVec (suc n)) -> v ≤ min ys -> v ≤ x -> v ≤ min (insert x ys)
  y≤min-insert v x [ y ] s t with total x y
  y≤min-insert v x [ y ] s t | inj₁ p = t
  y≤min-insert v x [ y ] s t | inj₂ p = s
  y≤min-insert v x (y ∷ ys Witness p) s t with total x y
  y≤min-insert v x (y ∷ ys Witness p) s t | inj₁ q = t
  y≤min-insert v x (y ∷ ys Witness p) s t | inj₂ q = s

fromList : (xs : List A) -> SVec (length xs)
fromList [] = []
fromList (x ∷ xs) = insert x (fromList xs)

mutual
  merge : ∀ {n} {m} -> SVec n -> SVec m -> SVec (n + m)
  merge [] ys = ys
  merge {n} xs [] = subst SVec (NC.+-comm 0 n) xs
  merge [ x ] ys = insert x ys
  merge {n} xs [ y ] = subst SVec (NC.+-comm 1 n) (insert y xs)
  merge {suc (suc n)} {suc (suc m)} (x ∷ xs Witness p) (y ∷ ys Witness q)
    with total x y | merge xs (y ∷ ys Witness q) | merge ys (x ∷ xs Witness p)
  ... | inj₁ r | m1 | m2 = x ∷ m1 Witness {!x≤min-merge x y xs ys p q r!}
  ... | inj₂ r | m1 | m2 = subst SVec (NC.+-comm (2 + m) (2 + n))
                 (y ∷ m2 Witness {!x≤min-merge y x ys xs q p r!})

  x≤min-merge : ∀ {n m} -> (x y : A)(xs : SVec (suc n))(ys : SVec (suc m))(p : x ≤ min xs)(q : y ≤ min ys) -> x ≤ y -> x ≤ min (merge xs (y ∷ ys Witness q))
  x≤min-merge x y [ a ] ys p q r = y≤min-insert x a (y ∷ ys Witness q) r p
  x≤min-merge {suc n} {m} x y (xx ∷ xss Witness pa) ys p q r with total xx y
  ... | inj₁ s = p
  ... | inj₂ s = subst (_≤_ x)
                   (min-is-min (NC.+-comm (2 + m) (2 + n))
                    (y ∷ merge ys (xx ∷ xss Witness pa) Witness
                     x≤min-merge y xx ys xss q pa s))
                   r


{-  merge {suc n} {suc m} xs ys with total (min xs) (min ys)
  ... | inj₁ p = merge-rest xs ys p
  ... | inj₂ p = subst SVec (NC.+-comm (suc m) (suc n)) (merge-rest ys xs p)-}

{-  merge-rest : ∀ {n m} (x : SVec (suc n)) (y : SVec (suc m)) -> min x ≤ min y -> SVec (suc n + suc m)
  merge-rest {n} {m} x y p = subst SVec (cong suc (NC.+-comm (suc m) n)) (min x ∷ merge y (rest x) Witness {!!})-}