# Zulip Chat Archive

## 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

#### Eric Wieser (Feb 03 2021 at 18:00):

#### 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`

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

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,
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 (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,
apply nat.lt_add_right,
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