Module docstring
{"# Lists with no duplicates
List.Nodup is defined in Data/List/Basic. In this file we prove various properties of this
predicate.
"}
List.Pairwise.nodup
theorem
{l : List α} {r : α → α → Prop} [IsIrrefl α r] (h : Pairwise r l) : Nodup l
Full source
protected theorem Pairwise.nodup {l : List α} {r : α → α → Prop} [IsIrrefl α r] (h : Pairwise r l) :
Nodup l :=
h.imp ne_of_irreflInformal description
For any list $l$ of elements of type $\alpha$ and any irreflexive binary relation $r$ on $\alpha$, if the elements of $l$ are pairwise related under $r$ (i.e., `Pairwise r l` holds), then $l$ has no duplicate elements (i.e., `Nodup l` holds).
List.rel_nodup
theorem
{r : α → β → Prop} (hr : Relator.BiUnique r) : (Forall₂ r ⇒ (· ↔ ·)) Nodup Nodup
Full source
theorem rel_nodup {r : α → β → Prop} (hr : Relator.BiUnique r) : (Forall₂Forall₂ r ⇒ (· ↔ ·)) Nodup Nodup
| _, _, Forall₂.nil => by simp only [nodup_nil]
| _, _, Forall₂.cons hab h => by
simpa only [nodup_cons] using
Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)Informal description
For any bi-unique relation $r$ between types $\alpha$ and $\beta$, and for any two lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$ that are pairwise related under $r$ (i.e., $\text{Forall}_2(r)(l_1, l_2)$ holds), the list $l_1$ has no duplicate elements if and only if the list $l_2$ has no duplicate elements.
List.Nodup.cons
theorem
(ha : a ∉ l) (hl : Nodup l) : Nodup (a :: l)
Full source
protected theorem Nodup.cons (ha : a ∉ l) (hl : Nodup l) : Nodup (a :: l) :=
nodup_cons.2 ⟨ha, hl⟩Informal description
For any element $a$ and list $l$, if $a$ is not in $l$ and $l$ has no duplicate elements, then the list obtained by prepending $a$ to $l$ (denoted $a :: l$) also has no duplicate elements.
List.nodup_singleton
theorem
(a : α) : Nodup [a]
Full source
theorem nodup_singleton (a : α) : Nodup [a] :=
pairwise_singleton _ _Informal description
For any element $a$ of type $\alpha$, the singleton list $[a]$ has no duplicate elements.
List.Nodup.of_cons
theorem
(h : Nodup (a :: l)) : Nodup l
Full source
theorem Nodup.of_cons (h : Nodup (a :: l)) : Nodup l :=
(nodup_cons.1 h).2Informal description
If a list `a :: l` has no duplicate elements, then the tail `l` also has no duplicate elements.
List.Nodup.not_mem
theorem
(h : (a :: l).Nodup) : a ∉ l
Full source
theorem Nodup.not_mem (h : (a :: l).Nodup) : a ∉ l :=
(nodup_cons.1 h).1Informal description
If a list `a :: l` has no duplicate elements, then the element `a` does not appear in the list `l`.
List.not_nodup_cons_of_mem
theorem
: a ∈ l → ¬Nodup (a :: l)
Full source
theorem not_nodup_cons_of_mem : a ∈ l → ¬Nodup (a :: l) :=
imp_not_comm.1 Nodup.not_memInformal description
If an element $a$ is in a list $l$, then the list $a :: l$ (obtained by prepending $a$ to $l$) contains duplicates. In other words, $\neg \text{Nodup}(a :: l)$.
List.not_nodup_pair
theorem
(a : α) : ¬Nodup [a, a]
Full source
theorem not_nodup_pair (a : α) : ¬Nodup [a, a] :=
not_nodup_cons_of_mem <| mem_singleton_self _Informal description
For any element $a$ of type $\alpha$, the list $[a, a]$ contains duplicates. In other words, $\neg \text{Nodup}([a, a])$.
List.nodup_iff_sublist
theorem
{l : List α} : Nodup l ↔ ∀ a, ¬[a, a] <+ l
Full source
theorem nodup_iff_sublist {l : List α} : NodupNodup l ↔ ∀ a, ¬[a, a] <+ l :=
⟨fun d a h => not_nodup_pair a (d.sublist h),
by
induction l <;> intro h; · exact nodup_nil
case cons a l IH =>
exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons
fun al => h a <| (singleton_sublist.2 al).cons_cons _⟩Informal description
A list $l$ of elements of type $\alpha$ has no duplicate elements if and only if for every element $a$ of type $\alpha$, the list $[a, a]$ is not a sublist of $l$.
List.nodup_mergeSort
theorem
{l : List α} {le : α → α → Bool} : (l.mergeSort le).Nodup ↔ l.Nodup
Full source
@[simp]
theorem nodup_mergeSort {l : List α} {le : α → α → Bool} : (l.mergeSort le).Nodup ↔ l.Nodup :=
(mergeSort_perm l le).nodup_iffInformal description
For any list $l$ of elements of type $\alpha$ and any boolean-valued comparison function $\mathrm{le} : \alpha \to \alpha \to \mathrm{Bool}$, the merge-sorted version of $l$ has no duplicate elements if and only if the original list $l$ has no duplicate elements.
List.nodup_iff_injective_getElem
theorem
{l : List α} : Nodup l ↔ Function.Injective (fun i : Fin l.length => l[i.1])
Full source
theorem nodup_iff_injective_getElem {l : List α} :
NodupNodup l ↔ Function.Injective (fun i : Fin l.length => l[i.1]) :=
pairwise_iff_getElem.trans
⟨fun h i j hg => by
obtain ⟨i, hi⟩ := i; obtain ⟨j, hj⟩ := j
rcases lt_trichotomy i j with (hij | rfl | hji)
· exact (h i j hi hj hij hg).elim
· rfl
· exact (h j i hj hi hji hg.symm).elim,
fun hinj i j hi hj hij h => Nat.ne_of_lt hij (Fin.val_eq_of_eq (@hinj ⟨i, hi⟩ ⟨j, hj⟩ h))⟩Informal description
A list $l$ of elements of type $\alpha$ has no duplicates if and only if the function that maps each index $i$ in the finite set $\{0, \dots, \text{length}(l) - 1\}$ to the element $l[i]$ is injective.
List.nodup_iff_injective_get
theorem
{l : List α} : Nodup l ↔ Function.Injective l.get
Full source
theorem nodup_iff_injective_get {l : List α} :
NodupNodup l ↔ Function.Injective l.get := by
rw [nodup_iff_injective_getElem]
change _ ↔ Injective (fun i => l.get i)
simpInformal description
A list $l$ of elements of type $\alpha$ has no duplicates if and only if the function that maps each index $i$ in the finite set $\{0, \dots, \text{length}(l) - 1\}$ to the element $l[i]$ is injective.
List.Nodup.get_inj_iff
theorem
{l : List α} (h : Nodup l) {i j : Fin l.length} : l.get i = l.get j ↔ i = j
Full source
theorem Nodup.get_inj_iff {l : List α} (h : Nodup l) {i j : Fin l.length} :
l.get i = l.get j ↔ i = j :=
(nodup_iff_injective_get.1 h).eq_iffInformal description
For a duplicate-free list $l$ of elements of type $\alpha$, and for any two indices $i$ and $j$ within the bounds of $l$, the elements $l[i]$ and $l[j]$ are equal if and only if the indices $i$ and $j$ are equal.
List.Nodup.getElem_inj_iff
theorem
{l : List α} (h : Nodup l) {i : Nat} {hi : i < l.length} {j : Nat} {hj : j < l.length} : l[i] = l[j] ↔ i = j
Full source
theorem Nodup.getElem_inj_iff {l : List α} (h : Nodup l)
{i : Nat} {hi : i < l.length} {j : Nat} {hj : j < l.length} :
l[i]l[i] = l[j] ↔ i = j := by
have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩
simpaInformal description
For a duplicate-free list $l$ of elements of type $\alpha$, and for any two indices $i$ and $j$ within the bounds of $l$ (i.e., $i < \text{length}(l)$ and $j < \text{length}(l)$), the elements $l[i]$ and $l[j]$ are equal if and only if the indices $i$ and $j$ are equal.
List.nodup_iff_getElem?_ne_getElem?
theorem
{l : List α} : l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l[i]? ≠ l[j]?
Full source
theorem nodup_iff_getElem?_ne_getElem? {l : List α} :
l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l[i]? ≠ l[j]? := by
rw [Nodup, pairwise_iff_getElem]
constructor
· intro h i j hij hj
rw [getElem?_eq_getElem (lt_trans hij hj), getElem?_eq_getElem hj, Ne, Option.some_inj]
exact h _ _ (by omega) hj hij
· intro h i j hi hj hij
rw [Ne, ← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem]
exact h i j hij hjInformal description
A list $l$ of elements of type $\alpha$ has no duplicates if and only if for any two natural numbers $i$ and $j$ such that $i < j$ and $j < \text{length}(l)$, the elements $l[i]?$ and $l[j]?$ are distinct.
List.nodup_iff_get?_ne_get?
theorem
{l : List α} : l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l.get? i ≠ l.get? j
Full source
@[deprecated nodup_iff_getElem?_ne_getElem? (since := "2025-02-17")]
theorem nodup_iff_get?_ne_get? {l : List α} :
l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l.get? i ≠ l.get? j := by
simp [nodup_iff_getElem?_ne_getElem?]Informal description
A list $l$ of elements of type $\alpha$ has no duplicates if and only if for any two natural numbers $i$ and $j$ such that $i < j$ and $j$ is less than the length of $l$, the $i$-th and $j$-th elements of $l$ (accessed via `List.get?`) are distinct. In other words, $l$ is duplicate-free precisely when all its elements at distinct positions are different.
List.Nodup.ne_singleton_iff
theorem
{l : List α} (h : Nodup l) (x : α) : l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x
Full source
theorem Nodup.ne_singleton_iff {l : List α} (h : Nodup l) (x : α) :
l ≠ [x]l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x := by
induction l with
| nil => simp
| cons hd tl hl =>
specialize hl h.of_cons
by_cases hx : tl = [x]
· simpa [hx, and_comm, and_or_left] using h
· rw [← Ne, hl] at hx
rcases hx with (rfl | ⟨y, hy, hx⟩)
· simp
· suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
exact ⟨y, mem_cons_of_mem _ hy, hx⟩Informal description
For a duplicate-free list $l$ of elements of type $\alpha$ and an element $x \in \alpha$, the list $l$ is not equal to the singleton list $[x]$ if and only if either $l$ is empty or there exists an element $y \in l$ such that $y \neq x$.
List.not_nodup_of_get_eq_of_ne
theorem
(xs : List α) (n m : Fin xs.length) (h : xs.get n = xs.get m) (hne : n ≠ m) : ¬Nodup xs
Full source
theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length)
(h : xs.get n = xs.get m) (hne : n ≠ m) : ¬Nodup xs := by
rw [nodup_iff_injective_get]
exact fun hinj => hne (hinj h)Informal description
For any list $xs$ of elements of type $\alpha$, if there exist two distinct indices $n$ and $m$ (with $n \neq m$) within the bounds of $xs$ such that the elements at these indices are equal (i.e., $xs[n] = xs[m]$), then the list $xs$ cannot be duplicate-free.
List.idxOf_getElem
theorem
[DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) : idxOf l[i] l = i
Full source
theorem idxOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) :
idxOf l[i] l = i :=
suffices (⟨idxOf l[i] l, idxOf_lt_length_iff.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩
from Fin.val_eq_of_eq this
nodup_iff_injective_get.1 H (by simp)Informal description
For any type $\alpha$ with decidable equality and any duplicate-free list $l$ of elements of type $\alpha$, if $i$ is a natural number such that $i < \text{length}(l)$, then the index of the element $l[i]$ in $l$ is equal to $i$.
List.get_idxOf
theorem
[DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) : idxOf (get l i) l = i
Full source
theorem get_idxOf [DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) :
idxOf (get l i) l = i := by
simp [idxOf_getElem, H]Informal description
For any type $\alpha$ with decidable equality and any duplicate-free list $l$ of elements of type $\alpha$, if $i$ is a valid index of $l$ (i.e., $i < \text{length}(l)$), then the index of the element $l[i]$ in $l$ is equal to $i$.
List.nodup_iff_count_le_one
theorem
[DecidableEq α] {l : List α} : Nodup l ↔ ∀ a, count a l ≤ 1
Full source
theorem nodup_iff_count_le_one [DecidableEq α] {l : List α} : NodupNodup l ↔ ∀ a, count a l ≤ 1 :=
nodup_iff_sublist.trans <|
forall_congr' fun a =>
have : replicatereplicate 2 a <+ lreplicate 2 a <+ l ↔ 1 < count a l := (le_count_iff_replicate_sublist ..).symm
(not_congr this).trans not_ltInformal description
For a list $l$ of elements of type $\alpha$ with decidable equality, $l$ has no duplicate elements if and only if for every element $a$ of type $\alpha$, the count of $a$ in $l$ is at most 1.
List.nodup_iff_count_eq_one
theorem
[DecidableEq α] : Nodup l ↔ ∀ a ∈ l, count a l = 1
Informal description
For a list $l$ of elements of type $\alpha$ with decidable equality, $l$ has no duplicate elements if and only if every element $a$ in $l$ appears exactly once in $l$.
List.count_eq_one_of_mem
theorem
[DecidableEq α] {a : α} {l : List α} (d : Nodup l) (h : a ∈ l) : count a l = 1
Full source
@[simp]
theorem count_eq_one_of_mem [DecidableEq α] {a : α} {l : List α} (d : Nodup l) (h : a ∈ l) :
count a l = 1 :=
_root_.le_antisymm (nodup_iff_count_le_one.1 d a) (Nat.succ_le_of_lt (count_pos_iff.2 h))Informal description
For any list $l$ of elements of type $\alpha$ with decidable equality, if $l$ has no duplicate elements ($\text{Nodup}(l)$) and an element $a$ is in $l$ ($a \in l$), then the count of $a$ in $l$ is exactly 1, i.e., $\text{count}(a, l) = 1$.
List.count_eq_of_nodup
theorem
[DecidableEq α] {a : α} {l : List α} (d : Nodup l) : count a l = if a ∈ l then 1 else 0
Full source
theorem count_eq_of_nodup [DecidableEq α] {a : α} {l : List α} (d : Nodup l) :
count a l = if a ∈ l then 1 else 0 := by
split_ifs with h
· exact count_eq_one_of_mem d h
· exact count_eq_zero_of_not_mem hInformal description
For any list $l$ of elements of type $\alpha$ with decidable equality, if $l$ has no duplicate elements ($\text{Nodup}(l)$), then the count of any element $a$ in $l$ is $1$ if $a$ is in $l$ and $0$ otherwise, i.e., $\text{count}(a, l) = \begin{cases} 1 & \text{if } a \in l \\ 0 & \text{otherwise} \end{cases}$.
List.Nodup.of_append_left
theorem
: Nodup (l₁ ++ l₂) → Nodup l₁
Full source
theorem Nodup.of_append_left : Nodup (l₁ ++ l₂) → Nodup l₁ :=
Nodup.sublist (sublist_append_left l₁ l₂)Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, if the concatenated list $l₁ ++ l₂$ has no duplicate elements, then $l₁$ also has no duplicate elements.
List.Nodup.of_append_right
theorem
: Nodup (l₁ ++ l₂) → Nodup l₂
Full source
theorem Nodup.of_append_right : Nodup (l₁ ++ l₂) → Nodup l₂ :=
Nodup.sublist (sublist_append_right l₁ l₂)Informal description
If the concatenation of two lists $l_1$ and $l_2$ has no duplicate elements, then the list $l_2$ has no duplicate elements.
List.nodup_append
theorem
{l₁ l₂ : List α} : Nodup (l₁ ++ l₂) ↔ Nodup l₁ ∧ Nodup l₂ ∧ Disjoint l₁ l₂
Full source
theorem nodup_append {l₁ l₂ : List α} :
NodupNodup (l₁ ++ l₂) ↔ Nodup l₁ ∧ Nodup l₂ ∧ Disjoint l₁ l₂ := by
simp only [Nodup, pairwise_append, disjoint_iff_ne]Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the concatenated list $l₁ ++ l₂$ has no duplicate elements if and only if $l₁$ has no duplicates, $l₂$ has no duplicates, and $l₁$ and $l₂$ are disjoint (i.e., they share no common elements).
List.disjoint_of_nodup_append
theorem
{l₁ l₂ : List α} (d : Nodup (l₁ ++ l₂)) : Disjoint l₁ l₂
Full source
theorem disjoint_of_nodup_append {l₁ l₂ : List α} (d : Nodup (l₁ ++ l₂)) : Disjoint l₁ l₂ :=
(nodup_append.1 d).2.2Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if the concatenated list $l_1 ++ l_2$ has no duplicate elements, then $l_1$ and $l_2$ are disjoint (i.e., they share no common elements).
List.Nodup.append
theorem
(d₁ : Nodup l₁) (d₂ : Nodup l₂) (dj : Disjoint l₁ l₂) : Nodup (l₁ ++ l₂)
Full source
theorem Nodup.append (d₁ : Nodup l₁) (d₂ : Nodup l₂) (dj : Disjoint l₁ l₂) : Nodup (l₁ ++ l₂) :=
nodup_append.2 ⟨d₁, d₂, dj⟩Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ has no duplicate elements, $l_2$ has no duplicate elements, and $l_1$ and $l_2$ are disjoint (i.e., they share no common elements), then the concatenated list $l_1 ++ l_2$ also has no duplicate elements.
List.nodup_append_comm
theorem
{l₁ l₂ : List α} : Nodup (l₁ ++ l₂) ↔ Nodup (l₂ ++ l₁)
Full source
theorem nodup_append_comm {l₁ l₂ : List α} : NodupNodup (l₁ ++ l₂) ↔ Nodup (l₂ ++ l₁) := by
simp only [nodup_append, and_left_comm, disjoint_comm]Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the concatenation $l₁ ++ l₂$ has no duplicate elements if and only if the concatenation $l₂ ++ l₁$ has no duplicate elements.
List.nodup_middle
theorem
{a : α} {l₁ l₂ : List α} : Nodup (l₁ ++ a :: l₂) ↔ Nodup (a :: (l₁ ++ l₂))
Full source
theorem nodup_middle {a : α} {l₁ l₂ : List α} :
NodupNodup (l₁ ++ a :: l₂) ↔ Nodup (a :: (l₁ ++ l₂)) := by
simp only [nodup_append, not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
disjoint_cons_right]Informal description
For any element $a$ and lists $l₁$, $l₂$ of type $\alpha$, the concatenated list $l₁ ++ [a] ++ l₂$ has no duplicates if and only if the list $a :: (l₁ ++ l₂)$ has no duplicates.
List.Nodup.of_map
theorem
(f : α → β) {l : List α} : Nodup (map f l) → Nodup l
Full source
theorem Nodup.of_map (f : α → β) {l : List α} : Nodup (map f l) → Nodup l :=
(Pairwise.of_map f) fun _ _ => mt <| congr_arg fInformal description
For any function $f : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, if the mapped list $\mathrm{map}\,f\,l$ has no duplicate elements, then the original list $l$ also has no duplicate elements.
List.Nodup.map_on
theorem
{f : α → β} (H : ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) (d : Nodup l) : (map f l).Nodup
Full source
theorem Nodup.map_on {f : α → β} (H : ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) (d : Nodup l) :
(map f l).Nodup :=
Pairwise.map _ (fun a b ⟨ma, mb, n⟩ e => n (H a ma b mb e)) (Pairwise.and_mem.1 d)Informal description
Let $f : \alpha \to \beta$ be a function and $l$ be a list of elements of type $\alpha$. If $f$ is injective on $l$ (i.e., for any $x, y \in l$, $f(x) = f(y)$ implies $x = y$) and $l$ has no duplicate elements, then the mapped list $\mathrm{map}\,f\,l$ also has no duplicate elements.
List.inj_on_of_nodup_map
theorem
{f : α → β} {l : List α} (d : Nodup (map f l)) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = y
Full source
theorem inj_on_of_nodup_map {f : α → β} {l : List α} (d : Nodup (map f l)) :
∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = y := by
induction l with
| nil => simp
| cons hd tl ih =>
simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
simp only [mem_cons]
rintro _ (rfl | h₁) _ (rfl | h₂) h₃
· rfl
· apply (d.1 _ h₂ h₃.symm).elim
· apply (d.1 _ h₁ h₃).elim
· apply ih d.2 h₁ h₂ h₃Informal description
For any function $f : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, if the mapped list $\mathrm{map}\,f\,l$ has no duplicate elements, then $f$ is injective on $l$, i.e., for any $x, y \in l$, $f(x) = f(y)$ implies $x = y$.
List.nodup_map_iff_inj_on
theorem
{f : α → β} {l : List α} (d : Nodup l) : Nodup (map f l) ↔ ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y
Full source
theorem nodup_map_iff_inj_on {f : α → β} {l : List α} (d : Nodup l) :
NodupNodup (map f l) ↔ ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y :=
⟨inj_on_of_nodup_map, fun h => d.map_on h⟩Informal description
For any function $f : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$ with no duplicates, the mapped list $\mathrm{map}\,f\,l$ has no duplicates if and only if $f$ is injective on $l$, i.e., for any $x, y \in l$, $f(x) = f(y)$ implies $x = y$.
List.Nodup.map
theorem
{f : α → β} (hf : Injective f) : Nodup l → Nodup (map f l)
Informal description
Let $f : \alpha \to \beta$ be an injective function and $l$ be a list of elements of type $\alpha$. If $l$ has no duplicate elements, then the list obtained by applying $f$ to each element of $l$ (denoted $\mathrm{map}\,f\,l$) also has no duplicate elements.
List.nodup_map_iff
theorem
{f : α → β} {l : List α} (hf : Injective f) : Nodup (map f l) ↔ Nodup l
Full source
theorem nodup_map_iff {f : α → β} {l : List α} (hf : Injective f) : NodupNodup (map f l) ↔ Nodup l :=
⟨Nodup.of_map _, Nodup.map hf⟩Informal description
For an injective function $f : \alpha \to \beta$ and a list $l$ of elements of type $\alpha$, the mapped list $\mathrm{map}\,f\,l$ has no duplicate elements if and only if the original list $l$ has no duplicate elements.
List.nodup_attach
theorem
{l : List α} : Nodup (attach l) ↔ Nodup l
Informal description
For any list $l$ of elements of type $\alpha$, the list `attach l` (which pairs each element with its index) has no duplicate elements if and only if the original list $l$ has no duplicate elements.
List.Nodup.pmap
theorem
{p : α → Prop} {f : ∀ a, p a → β} {l : List α} {H} (hf : ∀ a ha b hb, f a ha = f b hb → a = b) (h : Nodup l) :
Nodup (pmap f l H)
Full source
theorem Nodup.pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} {H}
(hf : ∀ a ha b hb, f a ha = f b hb → a = b) (h : Nodup l) : Nodup (pmap f l H) := by
rw [pmap_eq_map_attach]
exact h.attach.map fun ⟨a, ha⟩ ⟨b, hb⟩ h => by congr; exact hf a (H _ ha) b (H _ hb) hInformal description
Let $p : \alpha \to \mathrm{Prop}$ be a predicate, $f : \forall a, p(a) \to \beta$ be a dependent function, and $l$ be a list of elements of type $\alpha$ with no duplicates. If for any $a, b \in \alpha$ and any proofs $h_a : p(a)$, $h_b : p(b)$, the equality $f(a, h_a) = f(b, h_b)$ implies $a = b$, then the list obtained by mapping $f$ over $l$ (denoted $\mathrm{pmap}\,f\,l\,H$) also has no duplicates.
List.Nodup.filter
theorem
(p : α → Bool) {l} : Nodup l → Nodup (filter p l)
Full source
theorem Nodup.filter (p : α → Bool) {l} : Nodup l → Nodup (filter p l) := by
simpa using Pairwise.filter pInformal description
For any predicate `p : α → Bool` and any list `l : List α`, if `l` has no duplicate elements, then the filtered list `filter p l` also has no duplicate elements.
List.nodup_reverse
theorem
{l : List α} : Nodup (reverse l) ↔ Nodup l
Full source
@[simp]
theorem nodup_reverse {l : List α} : NodupNodup (reverse l) ↔ Nodup l :=
pairwise_reverse.trans <| by simp only [Nodup, Ne, eq_comm]Informal description
For any list $l$ of elements of type $\alpha$, the reversed list $\mathrm{reverse}(l)$ has no duplicate elements if and only if the original list $l$ has no duplicate elements.
List.nodup_tail_reverse
theorem
(l : List α) (h : l[0]? = l.getLast?) : Nodup l.reverse.tail ↔ Nodup l.tail
Full source
lemma nodup_tail_reverse (l : List α) (h : l[0]? = l.getLast?) :
NodupNodup l.reverse.tail ↔ Nodup l.tail := by
induction l with
| nil => simp
| cons a l ih =>
by_cases hl : l = []
· aesop
· simp_all only [List.tail_reverse, List.nodup_reverse,
List.dropLast_cons_of_ne_nil hl, List.tail_cons]
simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem, getElem_cons_zero,
Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
rw [h,
show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
simp [List.dropLast_eq_take],
List.nodup_append_comm]
simp [List.getLast_eq_getElem]Informal description
For any list $l$ of elements of type $\alpha$ such that the first element of $l$ (if it exists) is equal to the last element of $l$ (if it exists), the tail of the reversed list $\mathrm{reverse}(l)$ has no duplicate elements if and only if the tail of $l$ has no duplicate elements.
List.Nodup.erase_getElem
theorem
[DecidableEq α] {l : List α} (hl : l.Nodup) (i : Nat) (h : i < l.length) : l.erase l[i] = l.eraseIdx ↑i
Full source
theorem Nodup.erase_getElem [DecidableEq α] {l : List α} (hl : l.Nodup)
(i : Nat) (h : i < l.length) : l.erase l[i] = l.eraseIdx ↑i := by
induction l generalizing i with
| nil => simp
| cons a l IH =>
cases i with
| zero => simp
| succ i =>
rw [nodup_cons] at hl
rw [erase_cons_tail]
· simp [IH hl.2]
· rw [beq_iff_eq]
simp only [getElem_cons_succ]
simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at h
exact mt (· ▸ getElem_mem h) hl.1Informal description
Let $\alpha$ be a type with decidable equality, and let $l$ be a list of elements of type $\alpha$ with no duplicates. For any natural number $i$ such that $i < \text{length}(l)$, the result of erasing the element at index $i$ from $l$ is equal to the result of removing the element at position $i$ from $l$.
List.Nodup.erase_get
theorem
[DecidableEq α] {l : List α} (hl : l.Nodup) (i : Fin l.length) : l.erase (l.get i) = l.eraseIdx ↑i
Full source
theorem Nodup.erase_get [DecidableEq α] {l : List α} (hl : l.Nodup) (i : Fin l.length) :
l.erase (l.get i) = l.eraseIdx ↑i := by
simp [erase_getElem, hl]Informal description
Let $\alpha$ be a type with decidable equality, and let $l$ be a list of elements of type $\alpha$ with no duplicates. For any index $i$ within the bounds of $l$, the result of erasing the element at position $i$ from $l$ is equal to the result of removing the element at index $i$ from $l$.
List.Nodup.diff
theorem
[DecidableEq α] : l₁.Nodup → (l₁.diff l₂).Nodup
Full source
theorem Nodup.diff [DecidableEq α] : l₁.Nodup → (l₁.diff l₂).Nodup :=
Nodup.sublist <| diff_sublist _ _Informal description
For any two lists `l₁` and `l₂` of elements of type `α` with a decidable equality, if `l₁` has no duplicate elements, then the list difference `l₁.diff l₂` also has no duplicate elements.
List.nodup_flatten
theorem
{L : List (List α)} : Nodup (flatten L) ↔ (∀ l ∈ L, Nodup l) ∧ Pairwise Disjoint L
Full source
theorem nodup_flatten {L : List (List α)} :
NodupNodup (flatten L) ↔ (∀ l ∈ L, Nodup l) ∧ Pairwise Disjoint L := by
simp only [Nodup, pairwise_flatten, disjoint_left.symm, forall_mem_ne]Informal description
For a list of lists $L$ of elements of type $\alpha$, the concatenation (flattening) of $L$ has no duplicate elements if and only if every list in $L$ has no duplicates and all pairs of lists in $L$ are disjoint (i.e., they share no common elements).
List.nodup_flatMap
theorem
{l₁ : List α} {f : α → List β} : Nodup (l₁.flatMap f) ↔ (∀ x ∈ l₁, Nodup (f x)) ∧ Pairwise (Disjoint on f) l₁
Full source
theorem nodup_flatMap {l₁ : List α} {f : α → List β} :
NodupNodup (l₁.flatMap f) ↔
(∀ x ∈ l₁, Nodup (f x)) ∧ Pairwise (Disjoint on f) l₁ := by
simp only [List.flatMap, nodup_flatten, pairwise_map, and_comm, and_left_comm, mem_map,
exists_imp, and_imp]
rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
from forall_swap.trans <| forall_congr' fun _ => forall_eq']Informal description
For a list $l_1$ of elements of type $\alpha$ and a function $f \colon \alpha \to \text{List } \beta$, the concatenation of the lists obtained by applying $f$ to each element of $l_1$ (denoted $l_1.\text{flatMap } f$) has no duplicate elements if and only if:
1. For every element $x$ in $l_1$, the list $f(x)$ has no duplicates, and
2. The images of $f$ on distinct elements of $l_1$ are pairwise disjoint (i.e., $f(x) \cap f(y) = \emptyset$ for any distinct $x, y \in l_1$).
List.Nodup.product
theorem
{l₂ : List β} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : (l₁ ×ˢ l₂).Nodup
Full source
protected theorem Nodup.product {l₂ : List β} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) :
(l₁ ×ˢ l₂).Nodup :=
nodup_flatMap.2
⟨fun a _ => d₂.map <| LeftInverse.injective fun b => (rfl : (a, b).2 = b),
d₁.imp fun {a₁ a₂} n x h₁ h₂ => by
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
exact n rfl⟩Informal description
For any lists $l_1$ of elements of type $\alpha$ and $l_2$ of elements of type $\beta$, if both $l_1$ and $l_2$ have no duplicate elements, then their Cartesian product list $l_1 \times l_2$ also has no duplicate elements.
List.Nodup.sigma
theorem
{σ : α → Type*} {l₂ : ∀ a, List (σ a)} (d₁ : Nodup l₁) (d₂ : ∀ a, Nodup (l₂ a)) : (l₁.sigma l₂).Nodup
Full source
theorem Nodup.sigma {σ : α → Type*} {l₂ : ∀ a, List (σ a)} (d₁ : Nodup l₁)
(d₂ : ∀ a, Nodup (l₂ a)) : (l₁.sigma l₂).Nodup :=
nodup_flatMap.2
⟨fun a _ => (d₂ a).map fun b b' h => by injection h with _ h,
d₁.imp fun {a₁ a₂} n x h₁ h₂ => by
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
exact n rfl⟩Informal description
Let $l_1$ be a list of elements of type $\alpha$ with no duplicates, and for each $a \in \alpha$, let $l_2(a)$ be a list of elements of type $\sigma(a)$ with no duplicates. Then the list formed by taking the dependent product (sigma type) of $l_1$ and $l_2$, denoted $l_1.\mathrm{sigma}\,l_2$, also has no duplicates.
List.Nodup.filterMap
theorem
{f : α → Option β} (h : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') : Nodup l → Nodup (filterMap f l)
Full source
protected theorem Nodup.filterMap {f : α → Option β} (h : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
Nodup l → Nodup (filterMap f l) :=
(Pairwise.filterMap f) @fun a a' n b bm b' bm' e => n <| h a a' b' (by rw [← e]; exact bm) bm'Informal description
Let $f : \alpha \to \text{Option } \beta$ be a function such that for any $a, a' \in \alpha$ and $b \in \beta$, if $b$ is in both $f(a)$ and $f(a')$, then $a = a'$. If a list $l$ has no duplicate elements, then the list obtained by applying `filterMap` with $f$ to $l$ also has no duplicate elements.
List.Nodup.concat
theorem
(h : a ∉ l) (h' : l.Nodup) : (l.concat a).Nodup
Full source
protected theorem Nodup.concat (h : a ∉ l) (h' : l.Nodup) : (l.concat a).Nodup := by
rw [concat_eq_append]; exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, if $a$ is not in $l$ and $l$ has no duplicate elements, then the list obtained by appending $a$ to $l$ (denoted $l \concat [a]$) also has no duplicate elements.
List.Nodup.insert
theorem
[DecidableEq α] (h : l.Nodup) : (l.insert a).Nodup
Full source
protected theorem Nodup.insert [DecidableEq α] (h : l.Nodup) : (l.insert a).Nodup :=
if h' : a ∈ l then by rw [insert_of_mem h']; exact h
else by rw [insert_of_not_mem h', nodup_cons]; constructor <;> assumptionInformal description
For any list $l$ of elements of type $\alpha$ with no duplicates (i.e., $\text{Nodup}(l)$), and for any element $a$ of type $\alpha$, the list obtained by inserting $a$ into $l$ (denoted as $l.\text{insert}(a)$) also has no duplicates.
List.Nodup.union
theorem
[DecidableEq α] (l₁ : List α) (h : Nodup l₂) : (l₁ ∪ l₂).Nodup
Full source
theorem Nodup.union [DecidableEq α] (l₁ : List α) (h : Nodup l₂) : (l₁ ∪ l₂).Nodup := by
induction l₁ generalizing l₂ with
| nil => exact h
| cons a l₁ ih => exact (ih h).insertInformal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₂$ has no duplicates (i.e., $\text{Nodup}(l₂)$), then the union of $l₁$ and $l₂$ (denoted as $l₁ ∪ l₂$) also has no duplicates.
List.Nodup.inter
theorem
[DecidableEq α] (l₂ : List α) : Nodup l₁ → Nodup (l₁ ∩ l₂)
Full source
theorem Nodup.inter [DecidableEq α] (l₂ : List α) : Nodup l₁ → Nodup (l₁ ∩ l₂) :=
Nodup.filter _Informal description
For any list $l_2$ of elements of type $\alpha$ with a decidable equality, if $l_1$ has no duplicate elements, then the intersection list $l_1 \cap l_2$ also has no duplicate elements.
List.Nodup.diff_eq_filter
theorem
[BEq α] [LawfulBEq α] : ∀ {l₁ l₂ : List α} (_ : l₁.Nodup), l₁.diff l₂ = l₁.filter (· ∉ l₂)
Full source
theorem Nodup.diff_eq_filter [BEq α] [LawfulBEq α] :
∀ {l₁ l₂ : List α} (_ : l₁.Nodup), l₁.diff l₂ = l₁.filter (· ∉ l₂)
| l₁, [], _ => by simp
| l₁, a :: l₂, hl₁ => by
rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]
simp only [decide_not, bne, Bool.and_comm, mem_cons, not_or, decide_mem_cons, Bool.not_or]Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$ with decidable equality, if $l₁$ has no duplicates, then the difference of $l₁$ and $l₂$ is equal to filtering $l₁$ by elements not in $l₂$, i.e.,
\[ l₁ \setminus l₂ = \text{filter } (\lambda x, x \notin l₂) \, l₁. \]
List.Nodup.mem_diff_iff
theorem
[DecidableEq α] (hl₁ : l₁.Nodup) : a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂
Full source
theorem Nodup.mem_diff_iff [DecidableEq α] (hl₁ : l₁.Nodup) : a ∈ l₁.diff l₂a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂ := by
rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$ with decidable equality, if $l₁$ has no duplicates, then an element $a$ belongs to the difference list $l₁ \setminus l₂$ if and only if $a$ belongs to $l₁$ and does not belong to $l₂$, i.e.,
\[ a \in l₁ \setminus l₂ \leftrightarrow a \in l₁ \land a \notin l₂. \]
List.Nodup.set
theorem
: ∀ {l : List α} {n : ℕ} {a : α} (_ : l.Nodup) (_ : a ∉ l), (l.set n a).Nodup
Full source
protected theorem Nodup.set :
∀ {l : List α} {n : ℕ} {a : α} (_ : l.Nodup) (_ : a ∉ l), (l.set n a).Nodup
| [], _, _, _, _ => nodup_nil
| _ :: _, 0, _, hl, ha => nodup_cons.2 ⟨mt (mem_cons_of_mem _) ha, (nodup_cons.1 hl).2⟩
| _ :: _, _ + 1, _, hl, ha =>
nodup_cons.2
⟨fun h =>
(mem_or_eq_of_mem_set h).elim (nodup_cons.1 hl).1 fun hba => ha (hba ▸ mem_cons_self),
hl.of_cons.set (mt (mem_cons_of_mem _) ha)⟩Informal description
For any list $l$ of type $\alpha$ with no duplicate elements, any natural number $n$, and any element $a$ of type $\alpha$ that is not in $l$, the list obtained by setting the $n$-th element of $l$ to $a$ also has no duplicate elements.
List.Nodup.map_update
theorem
[DecidableEq α] {l : List α} (hl : l.Nodup) (f : α → β) (x : α) (y : β) :
l.map (Function.update f x y) = if x ∈ l then (l.map f).set (l.idxOf x) y else l.map f
Full source
theorem Nodup.map_update [DecidableEq α] {l : List α} (hl : l.Nodup) (f : α → β) (x : α) (y : β) :
l.map (Function.update f x y) =
if x ∈ l then (l.map f).set (l.idxOf x) y else l.map f := by
induction l with | nil => simp | cons hd tl ihl => ?_
rw [nodup_cons] at hl
simp only [mem_cons, map, ihl hl.2]
by_cases H : hd = x
· subst hd
simp [set, hl.1]
· simp [Ne.symm H, H, set, ← apply_ite (cons (f hd))]Informal description
Let $l$ be a list of elements of type $\alpha$ with no duplicates, and let $f : \alpha \to \beta$ be a function. For any $x \in \alpha$ and $y \in \beta$, the map of the updated function $\text{update } f \, x \, y$ over $l$ is equal to:
\[
\begin{cases}
(l.map \, f).\text{set } (\text{idxOf } x \, l) \, y & \text{if } x \in l, \\
l.map \, f & \text{otherwise.}
\end{cases}
\]
Here, $\text{update } f \, x \, y$ denotes the function that is equal to $f$ everywhere except at $x$, where it takes the value $y$, and $\text{idxOf } x \, l$ is the index of $x$ in $l$.
List.Nodup.pairwise_of_forall_ne
theorem
{l : List α} {r : α → α → Prop} (hl : l.Nodup) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r
Full source
theorem Nodup.pairwise_of_forall_ne {l : List α} {r : α → α → Prop} (hl : l.Nodup)
(h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by
rw [pairwise_iff_forall_sublist]
intro a b hab
if heq : a = b then
cases heq; have := nodup_iff_sublist.mp hl _ hab; contradiction
else
apply h <;> try (apply hab.subset; simp)
exact heqInformal description
For any list $l$ of elements of type $\alpha$ with no duplicates, and for any binary relation $r$ on $\alpha$, if for every pair of distinct elements $a$ and $b$ in $l$ the relation $r(a, b)$ holds, then the list $l$ satisfies the pairwise property with respect to $r$.
List.Nodup.take_eq_filter_mem
theorem
[DecidableEq α] : ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (l.take n).elem
Full source
theorem Nodup.take_eq_filter_mem [DecidableEq α] :
∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (l.take n).elem
| [], n, _ => by simp
| b::l, 0, _ => by simp
| b::l, n+1, hl => by
rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]
congr 1
refine List.filter_congr ?_
intro x hx
have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
simp +contextual [List.mem_filter, this, hx]Informal description
For any list $l$ of elements of type $\alpha$ with no duplicates, and for any natural number $n$, the first $n$ elements of $l$ are equal to the sublist of $l$ consisting of elements that appear in the first $n$ elements, i.e.,
\[ \text{take } n \, l = \text{filter } (\lambda x, x \in \text{take } n \, l) \, l. \]
Option.toList_nodup
theorem
: ∀ o : Option α, o.toList.Nodup
Informal description
For any option type $o$ of type $\text{Option } \alpha$, the list obtained by converting $o$ to a list has no duplicate elements.