From ba2c0563da31dae1a6467876a8672bda921e56bf Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Sun, 6 Jun 2021 03:28:06 +0000
Subject: [PATCH] feat(data/list/nodup): nodup.pairwise_of_forall_ne (#7587)

---
 src/data/list/nodup.lean    | 14 +++++++++++
 src/data/list/pairwise.lean | 48 +++++++++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+)

diff --git a/src/data/list/nodup.lean b/src/data/list/nodup.lean
index 8d3730a93baeb..e22c041c112dc 100644
--- a/src/data/list/nodup.lean
+++ b/src/data/list/nodup.lean
@@ -322,6 +322,20 @@ begin
   { simp [ne.symm H, H, update_nth, ← apply_ite (cons (f hd))] }
 end
 
+lemma 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 :=
+begin
+  classical,
+  refine pairwise_of_reflexive_on_dupl_of_forall_ne _ h,
+  intros x hx,
+  rw nodup_iff_count_le_one at hl,
+  exact absurd (hl x) hx.not_le
+end
+
+lemma nodup.pairwise_of_set_pairwise_on {l : list α} {r : α → α → Prop}
+  (hl : l.nodup) (h : {x | x ∈ l}.pairwise_on r) : l.pairwise r :=
+hl.pairwise_of_forall_ne h
+
 end list
 
 theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup
diff --git a/src/data/list/pairwise.lean b/src/data/list/pairwise.lean
index 8da6fc7b178a0..44ebe3e0197c6 100644
--- a/src/data/list/pairwise.lean
+++ b/src/data/list/pairwise.lean
@@ -227,6 +227,54 @@ from λ R l, ⟨λ p, reverse_reverse l ▸ this p, this⟩,
     pairwise_cons, forall_prop_of_false (not_mem_nil _), forall_true_iff,
     pairwise.nil, mem_reverse, mem_singleton, forall_eq, true_and] using h]
 
+lemma pairwise.set_pairwise_on {l : list α} (h : pairwise R l) (hr : symmetric R) :
+  set.pairwise_on {x | x ∈ l} R :=
+begin
+  induction h with hd tl imp h IH,
+  { simp },
+  { intros x hx y hy hxy,
+    simp only [mem_cons_iff, set.mem_set_of_eq] at hx hy,
+    rcases hx with rfl|hx;
+    rcases hy with rfl|hy,
+    { contradiction },
+    { exact imp y hy },
+    { exact hr (imp x hx) },
+    { exact IH x hx y hy hxy } }
+end
+
+lemma pairwise_of_reflexive_on_dupl_of_forall_ne [decidable_eq α] {l : list α} {r : α → α → Prop}
+  (hr : ∀ a, 1 < count a l → r a a)
+  (h : ∀ (a ∈ l) (b ∈ l), a ≠ b → r a b) : l.pairwise r :=
+begin
+  induction l with hd tl IH,
+  { simp },
+  { rw list.pairwise_cons,
+    split,
+    { intros x hx,
+      by_cases H : hd = x,
+      { rw H,
+        refine hr _ _,
+        simpa [count_cons, H, nat.succ_lt_succ_iff, count_pos] using hx },
+      { exact h hd (mem_cons_self _ _) x (mem_cons_of_mem _ hx) H } },
+    { refine IH _ _,
+      { intros x hx,
+        refine hr _ _,
+        rw count_cons,
+        split_ifs,
+        { exact hx.trans (nat.lt_succ_self _) },
+        { exact hx } },
+      { intros x hx y hy,
+        exact h x (mem_cons_of_mem _ hx) y (mem_cons_of_mem _ hy) } } }
+end
+
+lemma pairwise_of_reflexive_of_forall_ne {l : list α} {r : α → α → Prop}
+  (hr : reflexive r) (h : ∀ (a ∈ l) (b ∈ l), a ≠ b → r a b) : l.pairwise r :=
+begin
+  classical,
+  refine pairwise_of_reflexive_on_dupl_of_forall_ne _ h,
+  exact λ _ _, hr _
+end
+
 theorem pairwise_iff_nth_le {R} : ∀ {l : list α},
   pairwise R l ↔ ∀ i j (h₁ : j < length l) (h₂ : i < j),
     R (nth_le l i (lt_trans h₂ h₁)) (nth_le l j h₁)