Unique.agda

module Unique where

-- I deal with naturals instead of integers. with a bit more effort, I could
-- probably have parameterized this over any type with decidable equality.
open import Data.Nat
open import Data.Product
open import Data.List hiding (any)
open import Data.List.Any
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open Membership-≡
open import Function

member? : (x : ℕ) (l : List ℕ) → Dec (x ∈ l)
member? x l = any (_≟_ x) l

data Unique : List ℕ → Set where
  [] : Unique []
  _∷_ : {x : ℕ} {l : List ℕ} → x ∉ l → Unique l → Unique (x ∷ l)

nub : (l : List ℕ) → Σ[ v ∈ List ℕ ] Unique v × l ⊆ v × v ⊆ l
nub [] = [] , [] , (λ ()) , (λ ())
nub (x ∷ l) with nub l
... | v , uv , l⊆v , v⊆l with member? x v
... | yes p = v , uv , (λ { (here refl) → p ; (there x∈l) → l⊆v x∈l }) , there ∘ v⊆l
... | no ¬p = x ∷ v , ¬p ∷ uv
            , (λ { (here refl) → here refl ; (there x∈l) → there (l⊆v x∈l) })
            , (λ { (here refl) → here refl ; (there x∈v) → there (v⊆l x∈v) })