## Stream: new members

### Topic: index_of_erase_lt

#### Marcus Rossel (Mar 02 2021 at 20:22):

I'm trying to prove that if the index of one element x in a list l is smaller than that of another element x', then this also holds if we remove an element from l (which is neither x nor x'):

So far I've been able to prove this for the case that l = hd :: tl, such that we remove hd:

lemma list.mem_nmem_ne {α : Type*} {l : list α} {x x' : α} (h : x ∈ l) (h' : x' ∉ l) :
x ≠ x' :=
begin
rintro rfl,
exact h' h
end

lemma list.index_of_cons_lt {α : Type*} [decidable_eq α] {hd : α} {tl : list α} {x x' : α} (h : (hd :: tl).index_of x < (hd :: tl).index_of x') (hₘ : x ∈ tl) (hₘ' : x' ∈ tl) (hₙ : (hd :: tl).nodup) :
tl.index_of x < tl.index_of x' :=
begin
have hₕ, from list.not_mem_of_nodup_cons hₙ,
have hₓ, from list.mem_nmem_ne hₘ hₕ,
have hₓ', from list.mem_nmem_ne hₘ' hₕ,
have hₛ, from list.index_of_cons_ne tl hₓ,
have hₛ', from list.index_of_cons_ne tl hₓ',
rw [hₛ, hₛ'] at h,
exact nat.succ_lt_succ_iff.mp h
end


The key step for me was list.index_of_cons_ne.
Unfortunately such a lemma does not exist for list.erase, so I'm stuck at:

lemma list.index_of_erase_lt {α : Type*} [decidable_eq α] {l : list α} {e x x' : α} (h : l.index_of x < l.index_of x') (hₘ : x ∈ l.erase e) (hₘ' : x' ∈ l.erase e) (hₙ : l.nodup) :
(l.erase e).index_of x < (l.erase e).index_of x' :=
begin
have hₕ : e ∉ l.erase e, from list.mem_erase_of_nodup hₙ,
have hₓ, from list.mem_nmem_ne hₘ hₕ,
have hₓ', from list.mem_nmem_ne hₘ' hₕ,
-- ?
end


Are there any useful lemmas that could help complete this proof?
Thanks :)

#### Yakov Pechersky (Mar 02 2021 at 20:29):

Can you prove list.index_of_cons_lt for arbitrary list.sublist?

#### Yakov Pechersky (Mar 03 2021 at 03:02):

@Marcus Rossel

lemma list.mem_nmem_ne {α : Type*} {l : list α} {x x' : α} (h : x ∈ l) (h' : x' ∉ l) :
x ≠ x' :=
begin
rintro rfl,
exact h' h
end

@[simp] lemma list.sublist_nil {α : Type*} {l : list α} : l <+ [] ↔ l = [] :=
begin
split,
{ rintro ⟨⟩,
refl },
{ rintro rfl,
refl }
end

lemma list.mem_of_mem_sublist {α : Type*} {l l' : list α} {x : α} (h : x ∈ l) (hl : l <+ l') :
x ∈ l' :=
begin
induction hl with _ tl hd hl IH tl tl' hd hl IH,
{ simpa using h },
{ exact list.mem_cons_of_mem _ (IH h) },
{ rw [list.mem_cons_iff] at h ⊢,
rcases h with h | h,
{ exact or.inl h },
{ exact or.inr (IH h) } }
end

lemma list.index_of_lt_of_sublist {α : Type*} [decidable_eq α] {l l' : list α} {x x' : α}
(h : l.index_of x < l.index_of x') (hl : l' <+ l)
(hₘ : x ∈ l') (hₘ' : x' ∈ l') (hₙ : l.nodup) :
l'.index_of x < l'.index_of x' :=
begin
induction hl with _ tl hd hl IH tl tl' hd hl IH,
{ simpa using hₘ },
{ refine IH _ hₘ hₘ' _,
{ have hne : ∀ z ∈ hl_l₁, z ≠ hd,
{ rintro z hz rfl,
have : z ∈ tl := list.mem_of_mem_sublist hz hl,
simpa [this] using hₙ },
rwa [list.index_of_cons_ne _ (hne _ hₘ), list.index_of_cons_ne _ (hne _ hₘ'),
nat.succ_lt_succ_iff] at h },
{ rw list.nodup_cons at hₙ,
exact hₙ.right } },
{ rw list.mem_cons_iff at hₘ hₘ',
rw list.nodup_cons at hₙ,
rcases hₘ with rfl|hₘ;
rcases hₘ' with rfl|hₘ',
{ simpa using h },
{ have hx' : x' ∈ tl' := list.mem_of_mem_sublist hₘ' hl,
replace hx' : x' ≠ x := list.mem_nmem_ne hx' hₙ.left,
simp [hx'] },
{ have hx : x ∈ tl' := list.mem_of_mem_sublist hₘ hl,
replace hx : x ≠ x' := list.mem_nmem_ne hx hₙ.left,
simpa [hx] using h },
{ have hx : x ∈ tl' := list.mem_of_mem_sublist hₘ hl,
replace hx : x ≠ hd := list.mem_nmem_ne hx hₙ.left,
have hx' : x' ∈ tl' := list.mem_of_mem_sublist hₘ' hl,
replace hx' : x' ≠ hd := list.mem_nmem_ne hx' hₙ.left,
rw [list.index_of_cons_ne _ hx, list.index_of_cons_ne _ hx', nat.succ_lt_succ_iff] at h ⊢,
exact IH h hₘ hₘ' hₙ.right } }
end

lemma list.index_of_erase_lt {α : Type*} [decidable_eq α] {l : list α} {e x x' : α}
(h : l.index_of x < l.index_of x') (hₘ : x ∈ l.erase e) (hₘ' : x' ∈ l.erase e) (hₙ : l.nodup) :
(l.erase e).index_of x < (l.erase e).index_of x' :=
list.index_of_lt_of_sublist h (l.erase_sublist e) hₘ hₘ' hₙ


#### Yakov Pechersky (Mar 03 2021 at 03:02):

Feel free to PR any of this

#### Eric Wieser (Mar 03 2021 at 07:13):

First lemma is docs#ne_of_mem_of_not_mem

Last updated: Dec 20 2023 at 11:08 UTC