English
If the elements of a list are pairwise related by an antisymmetric relation r, then destutter by ≠ equals dedup.
Русский
Если элементы списка пары связаны отношением противосимметричным r, то применяя destutter по ≠ получаем то же, что и dedup.
LaTeX
$$$\\text{List.Pairwise } r \\; l \\Rightarrow \\mathrm{destutter}_{\\neq}(l) = l.Dedup$$$
Lean4
/-- If the elements of a list `l` are related pairwise by an antisymmetric relation `r`, then
destuttering `l` by disequality produces the same result as deduplicating `l`.
This is most useful when `r` is a strict or weak ordering.
-/
theorem destutter_eq_dedup [DecidableEq α] {r : α → α → Prop} [IsAntisymm α r] :
∀ {l : List α}, l.Pairwise r → l.destutter (· ≠ ·) = l.dedup
| [], h => by simp
| [x], h => by simp
| x :: y :: xs, h => by
rw [pairwise_cons] at h
rw [destutter_cons_cons, ← destutter_cons', ← destutter_cons', h.2.destutter_eq_dedup]
obtain rfl | hxy := eq_or_ne x y
· simpa using h.2.destutter_eq_dedup
· simp only [mem_cons, forall_eq_or_imp, pairwise_cons] at h
have : x ∉ xs := fun hx ↦ hxy (antisymm h.1.1 (h.2.1 x hx))
rw [if_pos hxy, dedup_cons_of_notMem (a := x) (by simp [*])]
