merge master

src/Init/Data/List/Lemmas.lean

@@ -2376,7 +2376,7 @@ instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
 
 /-! ## Pairwise and Nodup -/
 
-/-! ### pairwise -/
+/-! ### Pairwise -/
 
 theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R
   | .slnil, h => h
@@ -2397,6 +2397,28 @@ theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by
   induction l <;> simp [*, pairwise_append, and_comm]
 
+@[simp] theorem pairwise_replicate {n : Nat} {a : α} :
+    (replicate n a).Pairwise R ↔ n ≤ 1 ∨ R a a := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp only [replicate_succ, pairwise_cons, mem_replicate, ne_eq, and_imp,
+      forall_eq_apply_imp_iff, ih]
+    constructor
+    · rintro ⟨h, h' | h'⟩
+      · by_cases w : n = 0
+        · left
+          subst w
+          simp
+        · right
+          exact h w
+      · right
+        exact h'
+    · rintro (h | h)
+      · obtain rfl := eq_zero_of_le_zero (le_of_lt_succ h)
+        simp
+      · exact ⟨fun _ => h, Or.inr h⟩
+
 theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) :
     ∀ {l : List α}, l.Pairwise R → l.Pairwise S
   | _, .nil => .nil
@@ -2440,6 +2462,9 @@ theorem getElem?_inj {xs : List α}
       simp only [get?_eq_getElem?]
     exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
 
+@[simp] theorem nodup_replicate {n : Nat} {a : α} :
+    (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/

tests/lean/run/list_simp.lean

@@ -363,6 +363,36 @@ variable [BEq α] in
 
 /-! ### rotateRight -/
 
+
+/-! ## Pairwise and Nodup -/
+
+/-! ### Pairwise -/
+section Pairwise
+variable (R : α → α → Prop)
+#check_simp Pairwise R [] ~> True
+#check_simp Pairwise R (x :: l) ~> (∀ (a' : α), a' ∈ l → R x a') ∧ Pairwise R l
+#check_simp Pairwise R [x, y, z] ~> (R x y ∧ R x z) ∧ R y z
+
+#check_simp Pairwise R (replicate n x) ~> n ≤ 1 ∨ R x x
+#check_simp Pairwise R (replicate 1 x) ~> True
+#check_simp Pairwise R (replicate (n+2) x) ~> R x x
+#check_simp Pairwise (· < ·) (replicate 2 m) ~> False
+#check_simp Pairwise (· < ·) (replicate n m) ~> n ≤ 1
+#check_simp Pairwise (· < ·) (replicate (n + 2) m) ~> False
+#check_simp Pairwise (· = ·) (replicate 2 m) ~> True
+#check_simp Pairwise (· = ·) (replicate n m) ~> True
+
+end Pairwise
+
+/-! ### Nodup -/
+
+#check_simp Nodup [] ~> True
+#check_simp Nodup (x :: l) ~> ¬x ∈ l ∧ l.Nodup
+#check_simp Nodup [x, y, z] ~> (¬x = y ∧ ¬x = z) ∧ ¬y = z
+
+#check_simp Nodup (replicate (n+2) x) ~> False
+#check_simp Nodup (replicate 2 x) ~> False
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/