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.

theorem List.length_eq_of_nodup_of_same_elements {α : Type u_1} [DecidableEq α] (l1 l2 : List α) (nodup1 : l1.Nodup) (nodup2 : l2.Nodup) (same_elems : ∀ (e : α), e ∈ l1 ↔ e ∈ l2) : l1.length = l2.length

If two lists have no duplicates and have the same elements, then their length is the same. Note that the lists are not necessarily equal since the order of elements may differ.

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

Remove duplicates from a list, keeping the rightmost occurrense.

Equations

• [].eraseDupsKeepRight = []
• (hd :: tl).eraseDupsKeepRight = if hd ∈ tl then tl.eraseDupsKeepRight else hd :: tl.eraseDupsKeepRight

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.

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

The deduplicated list indeed has no duplicates.

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.

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.