List lemma for mathlib

Stream: mathlib4

[Yves Jäckle]

Hey, would you like to add the following to Data.List.DropRight ?

lemma List.rdrop_append.{u} {α : Type u} {l₁ l₂ : List α} (i : ℕ) : List.rdrop (l₁ ++ l₂) (List.length l₂ + i)  = List.rdrop l₁ i:=
  by
  simp_rw [List.rdrop_eq_reverse_drop_reverse, List.reverse_append]
  congr 1
  rw [← List.length_reverse]
  apply List.drop_append

[Michael Rothgang]

I don't know that corner of mathlib very well. That said: it seems your lemma decomposes into two pieces; I'd rather have just these.

• rdroping first n and then m elements is the same as rdropping n+m
• rdrop (l₁ ++ l₂) (length l₂) = l₁ (is that easier to prove?)

BTW - not the point of your question, but since I guess you may be interested, let me mention it: I would tweak the code slightly:

import Mathlib
open List
lemma rdrop_append {α : Type*} {l₁ l₂ : List α} (i : ℕ) :
    rdrop (l₁ ++ l₂) (length l₂ + i)  = rdrop l₁ i := by
  simp_rw [rdrop_eq_reverse_drop_reverse, reverse_append]
  congr 1
  rw [← length_reverse]
  apply drop_append

[Michael Rothgang]

Congratulations, you nerd-sniped me :-) Here's your proof refactored to use the two above lemmas. In particular,

• the second lemma seems "obviously" missing
• your initial lemma is probably not worth including separately

import Mathlib
set_option autoImplicit false

open List
variable {α : Type*} {l l₁ l₂ : List α}

lemma foo : rdrop (l₁ ++ l₂) (length l₂) = l₁ := by
  rw [rdrop_eq_reverse_drop_reverse, reverse_eq_iff, reverse_append, ← length_reverse, drop_left]

lemma rdrop_add {n m : ℕ} : rdrop l (n + m) = rdrop (rdrop l n) m := by
  repeat rw [rdrop_eq_reverse_drop_reverse]
  rw [reverse_eq_iff]
  repeat rw [reverse_reverse, reverse_reverse]
  rw [← drop_add, Nat.add_comm]

lemma rdrop_append {i : ℕ} : rdrop (l₁ ++ l₂) (length l₂ + i)  = rdrop l₁ i := by
  calc
    _ = rdrop (rdrop (l₁ ++ l₂) (length l₂)) i := by rw [← rdrop_add]
    _ = rdrop l₁ i := by rw [foo]

[Bolton Bailey]

import Mathlib

lemma List.rdrop_add.{u} {α : Type u} {l : List α} (i j : ℕ) : l.rdrop (i + j)  = (l.rdrop i).rdrop j  :=
  by
  simp_rw [List.rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop, add_comm]

@[simp]
lemma List.rdrop_append_length.{u} {α : Type u} {l₁ l₂ : List α} :
    List.rdrop (l₁ ++ l₂) (List.length l₂) = l₁:= by
  rw [List.rdrop_eq_reverse_drop_reverse, ← length_reverse l₂, reverse_append, drop_left, reverse_reverse]

@[simp]
lemma List.rdrop_append.{u} {α : Type u} {l₁ l₂ : List α} (i : ℕ) : List.rdrop (l₁ ++ l₂) (List.length l₂ + i)  = List.rdrop l₁ i:=
  by
  rw [rdrop_add, rdrop_append_length]

Edit: Now golfed to one-liners

[Michael Rothgang]

You beat me to it :-)

[Michael Rothgang]

I don't think my solution is necessarily better. But I like that just rw can solve this :-)

[Michael Rothgang]

Actually, I think using simp_rw is slightly nicer, because you avoid the repetition.

[Yves Jäckle]

:+1: so you'll add these ?

[Yves Jäckle]

Made the PR:
https://github.com/leanprover-community/mathlib4/pull/12468
:tada:

[Johan Commelin]

Thanks, I left some comments.

[Yves Jäckle]

:+1: Thanks for the advice