nth append

Stream: new members

[Eamon Barrett]

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

[Kevin Buzzard]

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

[Scott Morrison]

@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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Eamon Barrett]

Thank you Scott!