chore(data/list/pairwise): add list.pairwise_pmap and `list.pairwis…

…e.pmap` (#5273)

Also add `list.pairwise.tail` and use it in the proof of `list.sorted.tail`.

src/data/list/pairwise.lean

@@ -27,6 +27,10 @@ theorem pairwise_of_pairwise_cons {a : α} {l : list α}
   (p : pairwise R (a::l)) : pairwise R l :=
 (pairwise_cons.1 p).2
 
+theorem pairwise.tail : ∀ {l : list α} (p : pairwise R l), pairwise R l.tail
+| [] h := h
+| (a :: l) h := pairwise_of_pairwise_cons h
+
 theorem pairwise.imp_of_mem {S : α → α → Prop} {l : list α}
   (H : ∀ {a b}, a ∈ l → b ∈ l → R a b → S a b) (p : pairwise R l) : pairwise S l :=
 begin
@@ -180,6 +184,27 @@ theorem pairwise_filter_of_pairwise (p : α → Prop) [decidable_pred p] {l : li
   : pairwise R l → pairwise R (filter p l) :=
 pairwise_of_sublist (filter_sublist _)
 
+theorem pairwise_pmap {p : β → Prop} {f : Π b, p b → α} {l : list β} (h : ∀ x ∈ l, p x) :
+  pairwise R (l.pmap f h) ↔
+    pairwise (λ b₁ b₂, ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l :=
+begin
+  induction l with a l ihl, { simp },
+  obtain ⟨ha, hl⟩ : p a ∧ ∀ b, b ∈ l → p b, by simpa using h,
+  simp only [ihl hl, pairwise_cons, bex_imp_distrib, pmap, and.congr_left_iff, mem_pmap],
+  refine λ _, ⟨λ H b hb hpa hpb, H _ _ hb rfl, _⟩,
+  rintro H _ b hb rfl,
+  exact H b hb _ _
+end
+
+theorem pairwise.pmap {l : list α} (hl : pairwise R l)
+  {p : α → Prop} {f : Π a, p a → β} (h : ∀ x ∈ l, p x) {S : β → β → Prop}
+  (hS : ∀ ⦃x⦄ (hx : p x) ⦃y⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
+  pairwise S (l.pmap f h) :=
+begin
+  refine (pairwise_pmap h).2 (pairwise.imp_of_mem _ hl),
+  intros, apply hS, assumption
+end
+
 theorem pairwise_join {L : list (list α)} : pairwise R (join L) ↔
   (∀ l ∈ L, pairwise R l) ∧ pairwise (λ l₁ l₂, ∀ (x ∈ l₁) (y ∈ l₂), R x y) L :=
 begin

src/data/list/sort.lean

@@ -26,9 +26,8 @@ list.decidable_pairwise _
 theorem sorted_of_sorted_cons {a : α} {l : list α} : sorted r (a :: l) → sorted r l :=
 pairwise_of_pairwise_cons
 
-theorem sorted.tail {r : α → α → Prop} : Π {l : list α}, sorted r l → sorted r l.tail
-| [] h := h
-| (hd :: tl) h := sorted_of_sorted_cons h
+theorem sorted.tail {r : α → α → Prop} {l : list α} (h : sorted r l) : sorted r l.tail :=
+h.tail
 
 theorem rel_of_sorted_cons {a : α} {l : list α} : sorted r (a :: l) →
   ∀ b ∈ l, r a b :=