list.sorted with list.map?

Stream: Is there code for X?

[Jake Levinson]

Do we have these lemmas or equivalent, for applying a monotone function to a sorted list?

lemma list.sorted_of_map_of_mono {α β : Type} [preorder α] [preorder β]
  {f : α → β} (hf : monotone f) {s : list α} (hs : s.sorted (≤)) : (list.map f s).sorted (≤) := sorry

lemma list.sorted_of_map_of_anti {α β : Type} [preorder α] [preorder β]
  {f : α → β} (hf : antitone f) {s : list α} (hs : s.sorted (≤)) : (list.map f s).sorted (≥) := sorry

My actual use case was for a list of the form list.map f (list.range n) for n : ℕ, so there would also be a need for

lemma list.sorted_range (n : ℕ) : (list.range n).sorted (≤) := sorry

These aren't too bad to prove, I was just wondering if I was overlooking them in the library. The list.sorted API seems pretty short. My solution below (which can maybe be golfed):

lemma list.sorted_of_map_of_mono {α β : Type} [preorder α] [preorder β]
  {f : α → β} (hf : monotone f) {s : list α} (hs : s.sorted (≤)) : (list.map f s).sorted (≤) :=
begin
  induction s with hd tl ih, simp,
  rw list.map, rw list.sorted_cons at ⊢ hs,
  simp only [list.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂],
  exact ⟨λ b hb, hf (hs.1 _ hb), ih hs.2⟩,
end

lemma list.sorted_of_map_of_anti {α β : Type} [preorder α] [preorder β]
  {f : α → β} (hf : antitone f) {s : list α} (hs : s.sorted (≤)) : (list.map f s).sorted (≥) :=
begin
  induction s with hd tl ih, simp,
  rw list.map, rw list.sorted_cons at ⊢ hs,
  simp only [list.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂],
  exact ⟨λ b hb, hf (hs.1 _ hb), ih hs.2⟩,
end

lemma list.sorted_range (n : ℕ) : (list.range n).sorted (≤) :=
begin
  induction n with n ih, simp,
  rw [list.range_succ_eq_map, list.sorted_cons],
  simp only [zero_le, implies_true_iff, true_and],
  exact list.sorted_of_map_of_mono (by apply nat.succ_le_succ) ih,
end

[Yaël Dillies]

docs#list.pairwise.map