Zulip Chat Archive

Stream: Is there code for X?

Topic: Halves of a sorted list are related


view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 03 2021 at 17:54):

docs#list.nth_le_of_sorted_of_le is close

view this post on Zulip Eric Wieser (Feb 03 2021 at 18:00):

#6027

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 03 2021 at 18:16):

Maybe mem_take_iff and mem_drop_iff as well (or instead)?

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:19):

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

view this post on Zulip Eric Wieser (Feb 03 2021 at 18:20):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:20):

yes

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:22):

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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:22):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:24):

plus that version needs decidable eq

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 03 2021 at 18:30):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Feb 03 2021 at 18:33):

maybe there's a nicer way?

view this post on Zulip 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?

view this post on Zulip Bhavik Mehta (Feb 03 2021 at 18:36):

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

view this post on Zulip Eric Wieser (Feb 03 2021 at 18:39):

I'll PR your first proof I think Bhavik

view this post on Zulip 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,
  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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Feb 03 2021 at 18:41):

I feel like k should be implicit in exists_i_lt_of_mem_take as well

view this post on Zulip Eric Wieser (Feb 03 2021 at 18:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 03 2021 at 18:43):

To complement the existing nth_le_of_mem

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:44):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:45):

yes, I think mem_take_nth is a nice lemma

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:45):

the one for drop is a bit more complicated

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:46):

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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:47):

it doesn't even have an le in it

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:48):

same thing with list.filter_map

view this post on Zulip Eric Wieser (Feb 03 2021 at 18:48):

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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:49):

no, something in one word like pnth or something

view this post on Zulip Mario Carneiro (Feb 03 2021 at 18:49):

or nth'

view this post on Zulip 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

view this post on Zulip 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,
  apply nat.lt_add_right,
  simp at hix,
  exact hix.left
end

view this post on Zulip Yakov Pechersky (Feb 03 2021 at 19:07):

I guess that is golfed if list.exists_i_lt_of_mem_take exists.

view this post on Zulip 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

view this post on Zulip 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