Documentation

BasicLeanDatastructures.List.EraseDupsKeepRight

eraseDupsKeepRight #

In this file, we define the eraseDupsKeepRight convenience function that removes duplicates from a given list while keeping the rightmost occurrence. This function assumes DecidableEq on the list elements. As one would expect, the resulting list is free of duplicates and still contains the same members as the original list, which is shown in theorems below.

source
def List.eraseDupsKeepRight {α : Type u_1} [DecidableEq α] :
List α → List α

Remove duplicates from a list, keeping the rightmost occurrense.

Equations
Instances For
    source
    @[simp]
    theorem List.mem_eraseDupsKeepRight {α : Type u_1} [DecidableEq α] (l : List α) (e : α) :
    e ∈ l.eraseDupsKeepRight ↔ e ∈ l

    The deduplicated list contains the same elements as the original list.

    source
    theorem List.length_eraseDupsKeepRight_le {α : Type u_1} [DecidableEq α] (l : List α) :
    l.eraseDupsKeepRight.length ≤ l.length

    eraseDupsKeepRight can only make the list shorter.

    source
    theorem List.nodup_eraseDupsKeepRight {α : Type u_1} [DecidableEq α] (l : List α) :
    l.eraseDupsKeepRight.Nodup

    The deduplicated list indeed has no duplicates.

    source
    @[simp]
    theorem List.eraseDupsKeepRight_eq_self_of_nodup {α : Type u_1} [DecidableEq α] (l : List α) (nodup : l.Nodup) :
    l.eraseDupsKeepRight = l

    Erasing dups from a list without duplicates does not change anything.

    source
    theorem List.nodup_of_length_eraseDupsKeepRight_same {α : Type u_1} [DecidableEq α] (l : List α) (length_eq : l.eraseDupsKeepRight.length = l.length) :
    l.Nodup

    If the length after erasing duplicates remains the same, then the list contains no duplicates.

    source
    @[simp]
    theorem List.eraseDupsKeepRight_idempotent {α : Type u_1} [DecidableEq α] (l : List α) :
    l.eraseDupsKeepRight.eraseDupsKeepRight = l.eraseDupsKeepRight

    Calling eraseDupsKeepRight a second time does not change anything anymore.

    source
    theorem List.length_eraseDupsKeepRight_eq_of_same_elements {α : Type u_1} [DecidableEq α] (l1 l2 : List α) :
    (∀ (e : α), e ∈ l1 ↔ e ∈ l2) → l1.eraseDupsKeepRight.length = l2.eraseDupsKeepRight.length

    If two lists contain the same elements, then calling eraseDupsKeepRight on both ends up with lists of equal length. Again the lists might not be equal as they could differ in their order of elements.