module Data.List.Membership where

Membership in listsπŸ”—

We can inductively define a notion of membership between elements and lists we write However, note that this notion of membership is not a proposition! The type has at least as many inhabitants as there are occurrences of in and if the type is not a set, then each proof of can be acted on by a loop on to give a new proof.

data _βˆˆβ‚—_ {β„“} {A : Type β„“} (x : A) : List A β†’ Type β„“ where
  here  : βˆ€ {x'} (p : x ≑ x') β†’ x βˆˆβ‚— (x' ∷ xs)
  there : (p : x βˆˆβ‚— xs)       β†’ x βˆˆβ‚— (y ∷ xs)

There is a more (homotopically) straightforward characterisation of membership in lists: the fibres of the lookup function xs ! i. These are given by an index living in the standard finite set with as many elements as the list has positions, together with a proof that

The inverse equivalences between these notions is defined below; the proof that they are are inverses is a straightforward induction in both cases, so it’s omitted for space.

elementβ†’!-fibre : βˆ€ {x : A} {xs} β†’ x ∈ xs β†’ fibre (xs !_) x
element→!-fibre (here p) = fzero , sym p
element→!-fibre (there prf) with element→!-fibre prf
... | ix , p = fsuc ix , p

!-fibreβ†’element : βˆ€ {x : A} {xs} β†’ fibre (xs !_) x β†’ x ∈ xs
!-fibre→element {A = A} {x = x} = λ (ix , p) → go ix p module !-fibre→element where
  go : βˆ€ {xs} (ix : Fin (length xs)) β†’ xs ! ix ≑ x β†’ x ∈ xs
  go {xs = x ∷ xs} fzero p     = here  (sym p)
  go {xs = x ∷ xs} (fsuc ix) p = there (go ix p)

The equivalence between these definitions explains why can be so complicated. First, it’s at least a set, since it stores the index. Second, it stores a path, which can be arbitrarily complicated depending on the type

Despite the potential complexity of we do note that if is a set, then all that matters is the index; If is moreover discrete, then is decidable.

elem? : ⦃ _ : Discrete A ⦄ (x : A) (xs : List A) β†’ Dec (x ∈ xs)
elem? x [] = no Ξ» ()
elem? x (y ∷ xs) with x ≑ᡒ? y
... | yes reflα΅’ = yes (here refl)
... | no Β¬p with elem? x xs
... | yes p = yes (there p)
... | no Β¬q = no Ξ» { (here p) β†’ Β¬p (Id≃path.from p) ; (there q) β†’ Β¬q q }

Removing duplicatesπŸ”—

Still working with a discrete type, we can define a function nub which removes duplicates from a list. It is constructed by inductively deciding whether or not to keep the head of the list, discarding those which already appear further down. This has terrible the terrible time complexity but it works for an arbitrary discrete type, which is the best possible generality.

nub-cons : (x : A) (xs : List A) β†’ Dec (x ∈ xs) β†’ List A
nub-cons x xs (yes _) = xs
nub-cons x xs (no _)  = x ∷ xs

nub : ⦃ _ : Discrete A ⦄ β†’ List A β†’ List A
nub []       = []
nub (x ∷ xs) = nub-cons x (nub xs) (elem? x (nub xs))

The function nub is characterised by the following two facts. First, membership in nub is a proposition β€” each element appears at most once. Second, membership is (logically) preserved when nubbing a list β€” note that the function mapping old indices to new indices is not injective, since all occurrences of an element will be mapped to the same (first) occurrence in the deduplicated list.

  : βˆ€ ⦃ _ : Discrete A ⦄ {x : A} (xs : List A) β†’ is-prop (x ∈ nub xs)
  : βˆ€ ⦃ _ : Discrete A ⦄ {x : A} {xs : List A} β†’ x ∈ xs β†’ x ∈ nub xs
The proofs here are also straightforward inductive arguments.
member-nub-is-prop (x ∷ xs) p1 p2 with elem? x (nub xs) | p1 | p2
... | yes p | p1 | p2 = member-nub-is-prop xs p1 p2
... | no Β¬p | here  p1 | here  p2 = ap _βˆˆβ‚— (Discreteβ†’is-set auto _ _ p1 p2)
... | no ¬p | here  p1 | there p2 = absurd (¬p (subst (_∈ nub xs) p1 p2))
... | no ¬p | there p1 | here  p2 = absurd (¬p (subst (_∈ nub xs) p2 p1))
... | no Β¬p | there p1 | there p2 = ap there (member-nub-is-prop xs p1 p2)

memberβ†’member-nub {xs = x ∷ xs} (here p) with elem? x (nub xs)
... | yes x∈nub = subst (_∈ nub xs) (sym p) x∈nub
... | no ¬x∈nub = here p
memberβ†’member-nub {xs = x ∷ xs} (there Ξ±) with elem? x (nub xs)
... | yes x∈nub = memberβ†’member-nub Ξ±
... | no Β¬x∈nub = there (memberβ†’member-nub Ξ±)