Sublists.idr

module UniqueList

import Data.List

%default total

data UniqueListProof : List a -> Type where
    UNil : UniqueListProof []
    UCons : {xs : List a}
        -> (x : a)
        -> Not (Elem x xs)
        -> UniqueListProof xs
        -> UniqueListProof (x::xs)

data UniqueList : Type -> Type where
    MkUniqueList : (l : List a) -> UniqueListProof l -> UniqueList a

addUnique : DecEq a => (x : a) -> UniqueList a -> UniqueList a
addUnique x (MkUniqueList [] UNil) = MkUniqueList [x] (UCons x uninhabited UNil)
addUnique x (MkUniqueList (y::ys) rest) with (isElem x (y::ys))
    | Yes _   = MkUniqueList (y::ys)    rest
    | No  prf = MkUniqueList (x::y::ys) (UCons x prf rest)

||| Proof that S is the sublist of all distinct elements from L.
||| This interpretation is substantiated by the functions below.
data UniqueSublistProof : (s : List a) -> (l : List a) -> Type where
    USNil : UniqueSublistProof [] []

    AddLeftRight : {s,l : List a}
        -> (x : a)
        -> Not (Elem x s)
        -> UniqueSublistProof s l
        -> UniqueSublistProof (x::s) (x::l)

    AddRight : {s,l : List a}
        -> (x : a)
        -> Elem x s
        -> UniqueSublistProof s l
        -> UniqueSublistProof s (x::l)

data UniqueSublistOf : (l : List a) -> Type where
    MkUniqueSublistOf : (s : List a) -> UniqueSublistProof s l -> UniqueSublistOf l

||| Proof that a UniqueSublistProof S L does not leave out any elements of L in S.
uniqueSublistOk : UniqueSublistProof s l -> Elem x l -> Elem x s
uniqueSublistOk USNil                     elemPrf      = absurd elemPrf
uniqueSublistOk (AddLeftRight _ _ _)      Here         = Here
uniqueSublistOk (AddLeftRight _ _ rest)   (There more) = There (uniqueSublistOk rest more)
uniqueSublistOk (AddRight _ elemPrf _)    Here         = elemPrf
uniqueSublistOk (AddRight _ elemPrf rest) (There more) = uniqueSublistOk rest more

||| Proof that S appearing in UniqueSublistProof S L is in fact a list of distinct elements.
uniqueSublistIsUnique : UniqueSublistProof s l -> UniqueListProof s
uniqueSublistIsUnique USNil                   = UNil
uniqueSublistIsUnique (AddRight     _ _ rest) = uniqueSublistIsUnique rest
uniqueSublistIsUnique (AddLeftRight x p rest) = UCons x p (uniqueSublistIsUnique rest)

addUniqueSublist : DecEq a => (x : a) -> UniqueSublistOf xs -> UniqueSublistOf (x::xs)
addUniqueSublist x (MkUniqueSublistOf s usProof) with (isElem x s)
    | Yes prf = MkUniqueSublistOf _      (AddRight     x prf usProof)
    | No  prf = MkUniqueSublistOf (x::_) (AddLeftRight x prf usProof)

toUniqueSublist : DecEq a => (l : List a) -> UniqueSublistOf l
toUniqueSublist []      = MkUniqueSublistOf [] USNil
toUniqueSublist (x::xs) = addUniqueSublist x (toUniqueSublist xs)

fromUniqueSublist : {l : List a} -> UniqueSublistOf l -> List a
fromUniqueSublist (MkUniqueSublistOf s _) = s

verifiedUniqueSublist : DecEq a => List a -> List a
verifiedUniqueSublist l = fromUniqueSublist (toUniqueSublist l)