index_of_erase_lt

Stream: new members

[Marcus Rossel]

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]

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

[Yakov Pechersky]

@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]

Feel free to PR any of this

[Eric Wieser]

First lemma is docs#ne_of_mem_of_not_mem