module Data.List.Membership where

# Membership in listsð

We can inductively define a notion of membership between elements
$a:A$
and lists
$as:List(A);$
we write
$aâ_{l}as.$
However, note that this notion of membership is **not** a
proposition! The type
$aâ_{l}as$
has at least as many inhabitants as there are occurrences of
$a$
in
$as;$
and if the type
$A$
is not a set, then each proof of
$aâas$
can be acted on by a loop on
$a$
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)

instance Membership-List : â {â} {A : Type â} â Membership A (List A) â Membership-List = record { _â_ = _ââ_ }

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
$i:[length(xs)],$
living in the standard finite
set with as many elements as the list has positions, together with a
proof that
$xs!i=x.$

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 $aâ_{l}as$ 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 $A.$

!-fibreâelementâfibre : â {x : A} {xs} (f : fibre (xs !_) x) â elementâ!-fibre (!-fibreâelement f) â¡ f !-fibreâelementâfibre {A = A} {x = x} (ix , p) = go ix p where go : â {xs} (ix : Fin (length xs)) (p : xs ! ix â¡ x) â elementâ!-fibre (!-fibreâelement.go {xs = xs} ix p) â¡ (ix , p) go {xs = x â· xs} fzero p = refl go {xs = x â· xs} (fsuc ix) p = Î£-pathp (ap fsuc (ap fst p')) (ap snd p') where p' = go {xs = xs} ix p elementâ!-fibreâelement : {x : A} {xs : List A} (p : x â xs) â p â¡ !-fibreâelement (elementâ!-fibre p) elementâ!-fibreâelement (here p) = refl elementâ!-fibreâelement (there p) = ap there (elementâ!-fibreâelement p) elementâ!-fibre : â {x : A} {xs} â (x ââ xs) â fibre (xs !_) x elementâ!-fibre .fst = elementâ!-fibre elementâ!-fibre .snd = is-isoâis-equiv Î» where .is-iso.inv p â !-fibreâelement p .is-iso.rinv p â !-fibreâelementâfibre p .is-iso.linv p â sym (elementâ!-fibreâelement p)

Despite the potential complexity of $aâ_{l}as,$ we do note that if $A$ is a set, then all that matters is the index; If $A$ is moreover discrete, then $aâ_{l}as$ 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 }

instance Dec-ââ : âŠ _ : Discrete A âŠ {x : A} {xs : List A} â Dec (x â xs) Dec-ââ {x = x} {xs} = elem? x xs

## 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
$O(n_{2}),$
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 `nub`

bing 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.

member-nub-is-prop : â âŠ _ : Discrete A âŠ {x : A} (xs : List A) â is-prop (x â nub xs) memberâmember-nub : â âŠ _ : 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 _ââ_.here (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 Î±)

!-tabulate : â {n} (f : Fin n â A) i â tabulate f ! i â¡ f (cast (length-tabulate f) i) !-tabulate {n = suc n} f fzero = refl !-tabulate {n = suc n} f (fsuc i) = !-tabulate (f â fsuc) i !-tabulate-fibre : â {n} (f : Fin n â A) x â fibre (tabulate f !_) x â fibre f x !-tabulate-fibre f x = Î£-ap (cast (length-tabulate f) , cast-is-equiv _) Î» i â pathâequiv (ap (_â¡ x) (!-tabulate f i)) member-tabulate : â {n} (f : Fin n â A) x â (x â tabulate f) â fibre f x member-tabulate f x = elementâ!-fibre âe !-tabulate-fibre f x

map-member : â {A : Type â} {B : Type â'} (f : A â B) {x : A} {xs : List A} â x â xs â f x â map f xs map-member f (here p) = here (ap f p) map-member f (there x) = there (map-member f x) ++-memberâ : x ââ xs â x ââ (xs ++ ys) ++-memberâ (here p) = here p ++-memberâ (there p) = there (++-memberâ p) ++-memberáµ£ : x ââ ys â x ââ (xs ++ ys) ++-memberáµ£ {xs = []} p = p ++-memberáµ£ {xs = x â· xs} p = there (++-memberáµ£ p)

any-one-of : â {â} {A : Type â} â (f : A â Bool) (x : A) (xs : List A) â x â xs â f x â¡ true â any-of f xs â¡ true any-one-of f x (y â· xs) (here x=y) x-true = apâ or (subst (Î» e â f e â¡ true) x=y x-true) refl any-one-of f x (y â· xs) (there xâxs) x-true = apâ or refl (any-one-of f x xs xâxs x-true) â or-truer _