Zulip Chat Archive

Stream: new members

Topic: nth append


view this post on Zulip Eamon Barrett (Nov 08 2019 at 04:59):

Is there was a lemma like this in mathlib or any ideas for a simple proof?

lemma nth_gt_append_right {α : Type}  (L M : list α) (k : ℕ) (h₁) (h₂) :
  (L ++ M).nth_le k h₁ = M.nth_le (k - L.length) h₂ := sorry

view this post on Zulip Kevin Buzzard (Nov 08 2019 at 09:40):

I can't see it in data.list.basic; nth_le_append only deals with the n'th element of L equalling the n'th element of L++M

view this post on Zulip Scott Morrison (Nov 09 2019 at 04:48):

@Eamon Barrett

import data.nat.basic

lemma nth_le_append_right {α : Type} : Π (L M : list α) (k : ℕ) (h₀ : L.length ≤ k) (h₁) (h₂),
  (L ++ M).nth_le k h₁ = M.nth_le (k - L.length) h₂
| [] M k h₀ h₁ h₂ := rfl
| (l :: L) M (k+1) h₀ h₁ h₂ :=
  begin
    dsimp,
    conv { to_rhs, congr, skip, rw [←nat.sub_sub, nat.sub.right_comm, nat.add_sub_cancel], },
    rw nth_le_append_right L M k (nat.lt_succ_iff.mp h₀),
  end

view this post on Zulip Scott Morrison (Nov 09 2019 at 04:49):

(This isn't exactly what you asked for, which I think wasn't true.)

view this post on Zulip Scott Morrison (Nov 09 2019 at 04:58):

You can eliminate h2 here, which is a consequence of h0 and h1.

view this post on Zulip Scott Morrison (Nov 09 2019 at 05:10):

import data.nat.basic

lemma nth_le_append_right_aux {α : Type} {L M : list α} {k : }
  (h₁ : list.length L  k) (h₂ : k < list.length (L ++ M)) : k - list.length L < list.length M :=
begin
  rw list.length_append at h₂,
  convert (nat.sub_lt_sub_right_iff h₁).mpr h₂,
  simp,
end

lemma nth_le_append_right {α : Type} :  {l₁ l₂ : list α} {n : } (h₁ : l₁.length  n) (h₂),
  (l₁ ++ l₂).nth_le n h₂ = l₂.nth_le (n - l₁.length) (nth_le_append_right_aux h₁ h₂)
| []       _ n     h₁ h₂ := rfl
| (a :: l) _ (n+1) h₁ h₂ :=
  begin
    dsimp,
    conv { to_rhs, congr, skip, rw [nat.sub_sub, nat.sub.right_comm, nat.add_sub_cancel], },
    rw nth_le_append_right (nat.lt_succ_iff.mp h₁),
  end

view this post on Zulip Scott Morrison (Nov 09 2019 at 05:20):

https://github.com/leanprover-community/mathlib/pull/1662

view this post on Zulip Eamon Barrett (Nov 10 2019 at 23:01):

Thank you Scott!


Last updated: May 14 2021 at 02:15 UTC