Stream: new members

Topic: nth append

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


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

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


Scott Morrison (Nov 09 2019 at 04:49):

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

Scott Morrison (Nov 09 2019 at 04:58):

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

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


Scott Morrison (Nov 09 2019 at 05:20):

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

Eamon Barrett (Nov 10 2019 at 23:01):

Thank you Scott!

Last updated: May 14 2021 at 02:15 UTC