Halves of a sorted list are related

Stream: Is there code for X?

[Eric Wieser]

Does this exist?

example {α : Type u_1} (k : ℕ)
  (r : α → α → Prop)
  [decidable_rel r]
  [is_trans α r]
  [is_antisymm α r]
  [is_total α r]
  (l : list α)
  (ls : list.sorted r l) : ∀ (x ∈ list.take k l) (y ∈ list.drop k l), r x y :=
begin
  intros x hx y hy,
  sorry,
end

[Eric Wieser]

docs#list.nth_le_of_sorted_of_le is close

[Eric Wieser]

#6027

[Eric Wieser]

Two related lemmas that also seem missing:

lemma list.exists_i_lt_of_mem_take {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.take k l) :
  ∃ i (h : i < k), x = l.nth_le i sorry :=
begin
  sorry
end

lemma list.exists_le_i_of_mem_drop {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.drop k l) :
  ∃ i (h : k ≤ i), x = l.nth_le i sorry :=
begin
  sorry
end

[Kevin Buzzard]

Maybe mem_take_iff and mem_drop_iff as well (or instead)?

[Mario Carneiro]

To avoid the sorry in the statement, use x \in l.nth i

[Eric Wieser]

Is there a lemma to convert from x ∈ l.nth i to the nth_le version?

[Mario Carneiro]

and I think that the better way to expose this is i < k -> (l.take k).nth i = l.nth i

[Mario Carneiro]

yes

[Eric Wieser]

The statement I have above is the one I actually need if I want to reuse
docs#list.nth_le_of_sorted_of_le in #6027 instead of working from scratch

[Mario Carneiro]

It's not hard to go back and forth from nth to nth_le

[Mario Carneiro]

it might be worth making an nth version of that lemma though

[Bhavik Mehta]

lemma mem_take_iff (x : α) (k : ℕ) (l : list α) [decidable_eq α] (hx : x ∈ list.take k l) :
  list.index_of x l ≤ k :=
begin

[Mario Carneiro]

that's a bit different, that's about searching in a list

[Bhavik Mehta]

I think some combination of nth_le_of_mem with nth_le_take' gives things close to mem_take_iff as well

[Eric Wieser]

Here's the proof I came up with using nth_le:

lemma list.exists_i_lt_of_mem_take {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.take k l) :
  ∃ i (h : i < k) (h₂ : i < l.length), x = l.nth_le i h₂ :=
begin
  induction l generalizing k,
  { simpa using hx, },
  cases k,
  { simpa using hx, },
  rw [list.take, list.mem_cons_iff] at hx,
  obtain (rfl | hx) := hx,
  { exact ⟨0, k.zero_lt_succ, l_tl.length.zero_lt_succ, rfl⟩, },
  { obtain ⟨i, h, h₂, rfl⟩ := l_ih _ hx,
    exact ⟨i.succ, nat.succ_lt_succ h, nat.succ_lt_succ h₂, rfl⟩, }
end

[Bhavik Mehta]

Mario Carneiro said:

that's a bit different, that's about searching in a list

I realise that, but we also have lemmas to convert between searching and nth, so it's an alternate approach to the original question

[Mario Carneiro]

plus that version needs decidable eq

[Bhavik Mehta]

Eric Wieser said:

Here's the proof I came up with using nth_le:

lemma list.exists_i_lt_of_mem_take {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.take k l) :
  ∃ i (h : i < k) (h₂ : i < l.length), x = l.nth_le i h₂ :=
begin
  induction l generalizing k,
  { simpa using hx, },
  cases k,
  { simpa using hx, },
  rw [list.take, list.mem_cons_iff] at hx,
  obtain (rfl | hx) := hx,
  { exact ⟨0, k.zero_lt_succ, l_tl.length.zero_lt_succ, rfl⟩, },
  { obtain ⟨i, h, h₂, rfl⟩ := l_ih _ hx,
    exact ⟨i.succ, nat.succ_lt_succ h, nat.succ_lt_succ h₂, rfl⟩, }
end

lemma list.exists_i_lt_of_mem_take {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.take k l) :
  ∃ i (h : i < k) (h₂ : i < l.length), x = l.nth_le i h₂ :=
begin
  rcases nth_le_of_mem hx with ⟨m, hm, rfl⟩,
  simp only [lt_min_iff, length_take] at hm,
  refine ⟨m, hm.1, hm.2, nth_le_take' _ _⟩,
end

an alternate, shorter proof

[Eric Wieser]

What does the proof for the l.nth version look like?

[Bhavik Mehta]

lemma list.exists_i_lt_of_mem_take' {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.take k l) :
  ∃ i (h : i < k) (h₂ : i < l.length), ↑x = l.nth i :=
begin
  rcases nth_le_of_mem hx with ⟨m, hm, rfl⟩,
  simp only [lt_min_iff, length_take] at hm,
  refine ⟨m, hm.1, hm.2, _⟩,
  rw nth_le_take',
  apply (nth_le_nth _).symm,
end

this is what I get

[Bhavik Mehta]

maybe there's a nicer way?

[Eric Wieser]

Which of ↑x = l.nth i, some x = l.nth i and x ∈ l.nth i is simp-normal?

[Bhavik Mehta]

For me the last one isn't, and the other two don't simplify?

[Eric Wieser]

I'll PR your first proof I think Bhavik

[Bhavik Mehta]

lemma list.exists_i_lt_of_mem_drop {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.drop k l) :
  ∃ i (h : k ≤ i) (h₂ : i < l.length), x = l.nth_le i h₂ :=
begin
  rcases nth_le_of_mem hx with ⟨m, hm, rfl⟩,
  simp only [length_drop] at hm,
  exact ⟨k+m, nat.le_add_right k m, nat.add_lt_of_lt_sub_left hm, nth_le_drop' _ _⟩,
end

for the other one

[Mario Carneiro]

import data.list.basic

variables {α : Type*}

lemma list.nth_lt_length {l : list α} {i : ℕ} {x : α} (h : x ∈ l.nth i) : i < l.length :=
(list.nth_eq_some.1 h).fst

lemma list.mem_take_nth {l : list α} {k i : ℕ} {x : α} :
  x ∈ (list.take k l).nth i ↔ i < k ∧ x ∈ l.nth i :=
begin
  split,
  { intro h,
    have : i < k := (list.nth_lt_length h).trans_le (list.length_take_le _ _),
    refine ⟨this, by rwa [← list.nth_take this]⟩ },
  { rintro ⟨h, h'⟩, rwa [list.nth_take h] }
end

lemma list.mem_take_iff_nth {l : list α} {k : ℕ} {x : α} :
  x ∈ list.take k l ↔ ∃ i, i < k ∧ x ∈ l.nth i :=
list.mem_iff_nth.trans (exists_congr (λ i, list.mem_take_nth))

lemma list.exists_i_lt_of_mem_take {l : list α} (k : ℕ) {x : α} (hx : x ∈ list.take k l) :
  ∃ i (h : i < k) h', x = l.nth_le i h' :=
begin
  rcases list.mem_take_iff_nth.1 hx with ⟨i, hi, h⟩,
  rcases list.nth_eq_some.1 h with ⟨h₁, h₂⟩,
  exact ⟨i, hi, h₁, h₂.symm⟩,
end

[Bhavik Mehta]

I feel like k should be implicit in exists_i_lt_of_mem_take as well

[Eric Wieser]

@Mario Carneiro, at this point could you PR it?

[Mario Carneiro]

I don't think that one should be PR'd actually, it's just there to show how the other lemmas come together

[Mario Carneiro]

the proof is kind of uninteresting, it's just unpacking the other existentials and putting them back together. That can be done in a user proof

[Eric Wieser]

My original plan was to PR @Bhavik Mehta's two lemmas as nth_le_of_mem_drop and nth_le_of_mem_take

[Eric Wieser]

To complement the existing nth_le_of_mem

[Mario Carneiro]

The simp normal form is o = some a, although I prefer a \in o

[Eric Wieser]

If you don't think those lemmas should be PR'd, are you saying your auxiliary ones should?

[Mario Carneiro]

yes, I think mem_take_nth is a nice lemma

[Mario Carneiro]

the one for drop is a bit more complicated

[Bhavik Mehta]

example {α : Type u} (k : ℕ) (r : α → α → Prop) (l : list α)
  (ls : list.sorted r l) : ∀ (x ∈ list.take k l) (y ∈ list.drop k l), r x y :=
begin
  intros x hx y hy,
  rcases list.exists_i_lt_of_mem_take hx with ⟨m, hm₁, hm₂, rfl⟩,
  rcases list.exists_i_lt_of_mem_drop hy with ⟨n, hn₁, hn₂, rfl⟩,
  exact pairwise_iff_nth_le.mp ls m n hn₂ (lt_of_lt_of_le hm₁ hn₁),
end

we don't need the transitivity assumption in your original lemma

[Eric Wieser]

list.nth_lt_length seems like a confusing name given it looks like it contains nth_lt, perhaps list.lt_length_of_mem_nth?

[Mario Carneiro]

Actually I would argue that nth_le is the one with the bad name

[Mario Carneiro]

it doesn't even have an le in it

[Eric Wieser]

@Bhavik, I copy-pasted those from the definition for sorted I thought, but I guess I screwed up

[Mario Carneiro]

having a definition be named the same as two other definitions separated by _ leads to a whole lot of name clashes

[Mario Carneiro]

same thing with list.filter_map

[Eric Wieser]

Are you advocating a rename nth_le to nth_lt or even nth_of_lt?

[Mario Carneiro]

no, something in one word like pnth or something

[Mario Carneiro]

or nth'

[Mario Carneiro]

nth_of_lt would be much worse, because then you will be super confused reading things like nth_of_lt_eq_self_of_lt

[Yakov Pechersky]

What's wrong with this?

lemma nth_le_of_sorted_of_lt {l : list α}
  (h : l.sorted r) {a b : ℕ} {ha : a < l.length} {hb : b < l.length} (hab : a < b) :
  r (l.nth_le a ha) (l.nth_le b hb) :=
list.pairwise_iff_nth_le.1 h a b hb hab

lemma sorted.rel_of_mem_take_of_mem_drop {l : list α} (h : list.sorted r l)
  (k : ℕ) {x y : α} (hx : x ∈ list.take k l) (hy : y ∈ list.drop k l) :
  r x y :=
begin
  obtain ⟨iy, hiy, rfl⟩ := nth_le_of_mem hy,
  obtain ⟨ix, hix, rfl⟩ := nth_le_of_mem hx,
  rw [nth_le_take', nth_le_drop'],
  apply nth_le_of_sorted_of_lt h,
  apply nat.lt_add_right,
  simp at hix,
  exact hix.left
end

[Yakov Pechersky]

I guess that is golfed if list.exists_i_lt_of_mem_take exists.

[Mario Carneiro]

that looks good to me, I was answering the Y instead of the X in eric's #xy question

[Eric Wieser]

I've updated the PR to use @Yakov Pechersky's approach. Feel free to edit the PR description to include a Co-authored-by line.