Mathlib.Data.List.Duplicate

List.Duplicate inductive

(x : α) : List α → Prop

Full source

/-- Property that an element `x : α` of `l : List α` can be found in the list more than once. -/
inductive Duplicate (x : α) : List α → Prop
  | cons_mem {l : List α} : x ∈ l → Duplicate x (x :: l)
  | cons_duplicate {y : α} {l : List α} : Duplicate x l → Duplicate x (y :: l)

Duplicate element in a list

Informal description

The inductive property `List.Duplicate x l` holds when the element `x` appears more than once in the list `l`.

List.Mem.duplicate_cons_self theorem

(h : x ∈ l) : x ∈+ x :: l

Full source

theorem Mem.duplicate_cons_self (h : x ∈ l) : x ∈+ x :: l :=
  Duplicate.cons_mem h

Prepending an existing element creates a duplicate

Informal description

For any element $x$ in a list $l$, the element $x$ is a duplicate in the list obtained by prepending $x$ to $l$, i.e., $x \in x :: l$ implies $x$ is a duplicate in $x :: l$.

List.Duplicate.duplicate_cons theorem

(h : x ∈+ l) (y : α) : x ∈+ y :: l

Full source

theorem Duplicate.duplicate_cons (h : x ∈+ l) (y : α) : x ∈+ y :: l :=
  Duplicate.cons_duplicate h

Duplicates persist under list cons operation

Informal description

If an element $x$ is a duplicate in a list $l$, then for any element $y$, $x$ remains a duplicate in the list obtained by prepending $y$ to $l$, i.e., $x \in^+ l$ implies $x \in^+ y :: l$ for any $y$.

List.Duplicate.mem theorem

(h : x ∈+ l) : x ∈ l

Full source

theorem Duplicate.mem (h : x ∈+ l) : x ∈ l := by
  induction h with
  | cons_mem => exact mem_cons_self
  | cons_duplicate _ hm => exact mem_cons_of_mem _ hm

Duplicate implies membership in list

Informal description

If an element $x$ is a duplicate in a list $l$, then $x$ is an element of $l$, i.e., $x \in l$.

List.Duplicate.mem_cons_self theorem

(h : x ∈+ x :: l) : x ∈ l

Full source

theorem Duplicate.mem_cons_self (h : x ∈+ x :: l) : x ∈ l := by
  obtain h | h := h
  · exact h
  · exact h.mem

Duplicate in cons implies membership in tail

Informal description

If an element $x$ is a duplicate in the list obtained by prepending $x$ to $l$ (i.e., $x \in^+ x :: l$), then $x$ must be an element of $l$ (i.e., $x \in l$).

List.duplicate_cons_self_iff theorem

: x ∈+ x :: l ↔ x ∈ l

Full source

@[simp]
theorem duplicate_cons_self_iff : x ∈+ x :: lx ∈+ x :: l ↔ x ∈ l :=
  ⟨Duplicate.mem_cons_self, Mem.duplicate_cons_self⟩

Duplicate in prepended list iff element in original list

Informal description

For any element $x$ and list $l$, the element $x$ is a duplicate in the list $x :: l$ if and only if $x$ is an element of $l$. In other words, $x$ appears more than once in $x :: l$ precisely when $x$ was already present in $l$.

List.Duplicate.ne_nil theorem

(h : x ∈+ l) : l ≠ []

Full source

theorem Duplicate.ne_nil (h : x ∈+ l) : l ≠ [] := fun H => (mem_nil_iff x).mp (H ▸ h.mem)

Non-empty list contains duplicates

Informal description

If an element $x$ is a duplicate in a list $l$ (i.e., $x$ appears more than once in $l$), then $l$ cannot be the empty list.

List.not_duplicate_nil theorem

(x : α) : ¬x ∈+ []

Full source

@[simp]
theorem not_duplicate_nil (x : α) : ¬x ∈+ [] := fun H => H.ne_nil rfl

No Duplicates in Empty List

Informal description

For any element $x$ of type $\alpha$, the empty list $[]$ does not contain any duplicates of $x$.

List.Duplicate.ne_singleton theorem

(h : x ∈+ l) (y : α) : l ≠ [y]

Full source

theorem Duplicate.ne_singleton (h : x ∈+ l) (y : α) : l ≠ [y] := by
  induction h with
  | cons_mem h => simp [ne_nil_of_mem h]
  | cons_duplicate h => simp [ne_nil_of_mem h.mem]

Non-singleton list contains duplicates

Informal description

If an element $x$ is a duplicate in a list $l$ (i.e., $x$ appears more than once in $l$), then $l$ cannot be a singleton list $[y]$ for any element $y$.

List.not_duplicate_singleton theorem

(x y : α) : ¬x ∈+ [y]

Full source

@[simp]
theorem not_duplicate_singleton (x y : α) : ¬x ∈+ [y] := fun H => H.ne_singleton _ rfl

No Duplicates in Singleton Lists

Informal description

For any elements $x$ and $y$ of type $\alpha$, the singleton list $[y]$ does not contain any duplicates of $x$ (i.e., $x$ cannot appear more than once in $[y]$).

List.Duplicate.elim_nil theorem

(h : x ∈+ []) : False

Full source

theorem Duplicate.elim_nil (h : x ∈+ []) : False :=
  not_duplicate_nil x h

No Duplicates in Empty List Leads to Contradiction

Informal description

For any element $x$ of type $\alpha$, the statement that $x$ is a duplicate in the empty list $[]$ leads to a contradiction (i.e., is false).

List.Duplicate.elim_singleton theorem

{y : α} (h : x ∈+ [y]) : False

Full source

theorem Duplicate.elim_singleton {y : α} (h : x ∈+ [y]) : False :=
  not_duplicate_singleton x y h

No Duplicates in Singleton Lists

Informal description

For any element $y$ of type $\alpha$, the statement that $x$ is a duplicate in the singleton list $[y]$ (i.e., $x$ appears more than once in $[y]$) leads to a contradiction (is false).

List.duplicate_cons_iff theorem

{y : α} : x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l

Full source

theorem duplicate_cons_iff {y : α} : x ∈+ y :: lx ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · obtain hm | hm := h
    · exact Or.inl ⟨rfl, hm⟩
    · exact Or.inr hm
  · rcases h with (⟨rfl | h⟩ | h)
    · simpa
    · exact h.cons_duplicate

Characterization of Duplicates in Cons List: $x \in^+ y :: l \leftrightarrow (y = x \land x \in l) \lor x \in^+ l$

Informal description

For any element $y$ of type $\alpha$ and list $l$ of type $\alpha$, the element $x$ is a duplicate in the list $y :: l$ (i.e., $x$ appears more than once in $y :: l$) if and only if either $y = x$ and $x$ appears in $l$, or $x$ is already a duplicate in $l$.

List.Duplicate.of_duplicate_cons theorem

{y : α} (h : x ∈+ y :: l) (hx : x ≠ y) : x ∈+ l

Full source

theorem Duplicate.of_duplicate_cons {y : α} (h : x ∈+ y :: l) (hx : x ≠ y) : x ∈+ l := by
  simpa [duplicate_cons_iff, hx.symm] using h

Duplicate in Cons List Implies Duplicate in Tail When Not Equal

Informal description

For any element $y$ of type $\alpha$ and list $l$ of type $\alpha$, if $x$ is a duplicate in the list $y :: l$ (i.e., $x$ appears more than once in $y :: l$) and $x \neq y$, then $x$ is a duplicate in $l$.

List.duplicate_cons_iff_of_ne theorem

{y : α} (hne : x ≠ y) : x ∈+ y :: l ↔ x ∈+ l

Full source

theorem duplicate_cons_iff_of_ne {y : α} (hne : x ≠ y) : x ∈+ y :: lx ∈+ y :: l ↔ x ∈+ l := by
  simp [duplicate_cons_iff, hne.symm]

Duplicate Preservation Under Cons with Distinct Element

Informal description

For any element $y$ in a type $\alpha$ such that $x \neq y$, the element $x$ is a duplicate in the list $y :: l$ (i.e., $x \in^+ y :: l$) if and only if $x$ is a duplicate in the list $l$ (i.e., $x \in^+ l$).

List.Duplicate.mono_sublist theorem

{l' : List α} (hx : x ∈+ l) (h : l <+ l') : x ∈+ l'

Full source

theorem Duplicate.mono_sublist {l' : List α} (hx : x ∈+ l) (h : l <+ l') : x ∈+ l' := by
  induction h with
  | slnil => exact hx
  | cons y _ IH => exact (IH hx).duplicate_cons _
  | cons₂ y h IH =>
    rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]

Duplicate Preservation Under Sublist Inclusion: $x \in^+ l \land l <+ l' \to x \in^+ l'$

Informal description

For any lists $l$ and $l'$ of type $\alpha$, if $x$ is a duplicate in $l$ (i.e., $x$ appears more than once in $l$) and $l$ is a sublist of $l'$ (denoted $l <+ l'$), then $x$ is also a duplicate in $l'$.

List.duplicate_iff_sublist theorem

: x ∈+ l ↔ [x, x] <+ l

Full source

/-- The contrapositive of `List.nodup_iff_sublist`. -/
theorem duplicate_iff_sublist : x ∈+ lx ∈+ l ↔ [x, x] <+ l := by
  induction' l with y l IH
  · simp
  · by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction

Characterization of List Duplicates via Sublist: $x \in^+ l \leftrightarrow [x, x] <+ l$

Informal description

An element $x$ is a duplicate in a list $l$ (i.e., $x \in^+ l$) if and only if the sublist $[x, x]$ is a sublist of $l$ (i.e., $[x, x] <+ l$).

List.nodup_iff_forall_not_duplicate theorem

: Nodup l ↔ ∀ x : α, ¬x ∈+ l

Full source

theorem nodup_iff_forall_not_duplicate : NodupNodup l ↔ ∀ x : α, ¬x ∈+ l := by
  simp_rw [nodup_iff_sublist, duplicate_iff_sublist]

Characterization of Duplicate-Free Lists: $\text{Nodup}(l) \leftrightarrow \forall x, \neg (x \in^+ l)$

Informal description

A list $l$ has no duplicate elements if and only if for every element $x$ in the type $\alpha$, $x$ does not appear more than once in $l$.

List.exists_duplicate_iff_not_nodup theorem

: (∃ x : α, x ∈+ l) ↔ ¬Nodup l

Full source

theorem exists_duplicate_iff_not_nodup : (∃ x : α, x ∈+ l) ↔ ¬Nodup l := by
  simp [nodup_iff_forall_not_duplicate]

Existence of Duplicate Element Equivalent to Non-Duplicate-Free List

Informal description

There exists an element $x$ that is duplicated in the list $l$ if and only if $l$ is not a list without duplicates (i.e., $l$ contains at least one duplicate).

List.Duplicate.not_nodup theorem

(h : x ∈+ l) : ¬Nodup l

Full source

theorem Duplicate.not_nodup (h : x ∈+ l) : ¬Nodup l := fun H =>
  nodup_iff_forall_not_duplicate.mp H _ h

Presence of Duplicate Implies Non-Duplicate-Free List

Informal description

If an element $x$ is duplicated in a list $l$ (i.e., $x \in^+ l$), then $l$ is not duplicate-free (i.e., $\neg \text{Nodup}(l)$).

List.duplicate_iff_two_le_count theorem

[DecidableEq α] : x ∈+ l ↔ 2 ≤ count x l

Full source

theorem duplicate_iff_two_le_count [DecidableEq α] : x ∈+ lx ∈+ l ↔ 2 ≤ count x l := by
  simp [replicate_succ, duplicate_iff_sublist, le_count_iff_replicate_sublist]

Characterization of Duplicate Elements in a List via Count

Informal description

For a list $l$ with elements of type $\alpha$ (where equality is decidable), an element $x$ is a duplicate in $l$ if and only if $x$ appears at least twice in $l$, i.e., the count of $x$ in $l$ is at least 2.

List.decidableDuplicate instance

[DecidableEq α] (x : α) : ∀ l : List α, Decidable (x ∈+ l)

Full source

instance decidableDuplicate [DecidableEq α] (x : α) : ∀ l : List α, Decidable (x ∈+ l)
  | [] => isFalse (not_duplicate_nil x)
  | y :: l =>
    match decidableDuplicate x l with
    | isTrue h => isTrue (h.duplicate_cons y)
    | isFalse h =>
      if hx : y = x ∧ x ∈ l then isTrue (hx.left.symm ▸ List.Mem.duplicate_cons_self hx.right)
      else isFalse (by simpa [duplicate_cons_iff, h] using hx)

Decidability of List Duplicates

Informal description

For any type $\alpha$ with decidable equality, given an element $x$ of type $\alpha$ and a list $l$ of elements of type $\alpha$, it is decidable whether $x$ is a duplicate in $l$ (i.e., whether $x$ appears more than once in $l$).

Mathlib.Data.List.Duplicate

Main definitions

Implementation details