Stream: Is there code for X?

Topic: Halves of a sorted list are related

Eric Wieser (Feb 03 2021 at 17:32):

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 (Feb 03 2021 at 17:54):

docs#list.nth_le_of_sorted_of_le is close

#6027

Eric Wieser (Feb 03 2021 at 18:12):

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 (Feb 03 2021 at 18:16):

Maybe mem_take_iff and mem_drop_iff as well (or instead)?

Mario Carneiro (Feb 03 2021 at 18:19):

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

Eric Wieser (Feb 03 2021 at 18:20):

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

Mario Carneiro (Feb 03 2021 at 18:20):

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

yes

Eric Wieser (Feb 03 2021 at 18:21):

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 (Feb 03 2021 at 18:22):

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

Mario Carneiro (Feb 03 2021 at 18:22):

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

Bhavik Mehta (Feb 03 2021 at 18:23):

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 (Feb 03 2021 at 18:23):

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

Bhavik Mehta (Feb 03 2021 at 18:23):

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

Eric Wieser (Feb 03 2021 at 18:24):

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 (Feb 03 2021 at 18:24):

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 (Feb 03 2021 at 18:24):

plus that version needs decidable eq

Bhavik Mehta (Feb 03 2021 at 18:27):

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 (Feb 03 2021 at 18:30):

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

Bhavik Mehta (Feb 03 2021 at 18:32):

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 (Feb 03 2021 at 18:33):

maybe there's a nicer way?

Eric Wieser (Feb 03 2021 at 18:33):

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

Bhavik Mehta (Feb 03 2021 at 18:36):

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

Eric Wieser (Feb 03 2021 at 18:39):

I'll PR your first proof I think Bhavik

Bhavik Mehta (Feb 03 2021 at 18:39):

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,
end


for the other one

Mario Carneiro (Feb 03 2021 at 18:40):

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 (Feb 03 2021 at 18:41):

I feel like k should be implicit in exists_i_lt_of_mem_take as well

Eric Wieser (Feb 03 2021 at 18:41):

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

Mario Carneiro (Feb 03 2021 at 18:42):

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 (Feb 03 2021 at 18:43):

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 (Feb 03 2021 at 18:43):

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 (Feb 03 2021 at 18:43):

To complement the existing nth_le_of_mem

Mario Carneiro (Feb 03 2021 at 18:44):

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

Eric Wieser (Feb 03 2021 at 18:44):

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

Mario Carneiro (Feb 03 2021 at 18:45):

yes, I think mem_take_nth is a nice lemma

Mario Carneiro (Feb 03 2021 at 18:45):

the one for drop is a bit more complicated

Bhavik Mehta (Feb 03 2021 at 18:45):

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 (Feb 03 2021 at 18:46):

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 (Feb 03 2021 at 18:46):

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

Mario Carneiro (Feb 03 2021 at 18:47):

it doesn't even have an le in it

Eric Wieser (Feb 03 2021 at 18:47):

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

Mario Carneiro (Feb 03 2021 at 18:47):

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

Mario Carneiro (Feb 03 2021 at 18:48):

same thing with list.filter_map

Eric Wieser (Feb 03 2021 at 18:48):

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

Mario Carneiro (Feb 03 2021 at 18:49):

no, something in one word like pnth or something

Mario Carneiro (Feb 03 2021 at 18:49):

or nth'

Mario Carneiro (Feb 03 2021 at 18:50):

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 (Feb 03 2021 at 19:06):

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,
simp at hix,
exact hix.left
end


Yakov Pechersky (Feb 03 2021 at 19:07):

I guess that is golfed if list.exists_i_lt_of_mem_take exists.

Mario Carneiro (Feb 03 2021 at 19:08):

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

Eric Wieser (Feb 03 2021 at 19:14):

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.

Last updated: May 07 2021 at 19:12 UTC