List.tail/List.dropLast + List.take

Stream: Is there code for X?

[Snir Broshi]

theorem tail_take {α : Type*} (l : List α) (n : ℕ) :
    (l.take n).tail = l.tail.take (n - 1) := by
  sorry

theorem dropLast_take {α : Type*} (l : List α) (n : ℕ) :
    (l.take n).dropLast = l.dropLast.take (n - 1) := by
  sorry

theorem tail_drop {α : Type*} (l : List α) (n : ℕ) :
    (l.drop n).tail = l.tail.drop n := by
  sorry

theorem dropLast_drop {α : Type*} (l : List α) (n : ℕ) :
    (l.drop n).dropLast = l.dropLast.drop n := by
  sorry

(docs#List.dropLast_take is close to the second one)

[Kim Morrison]

(Please remember to post #mwe's where possible!)

[Kim Morrison]

import Mathlib

theorem tail_take {α : Type*} (l : List α) (n : ℕ) :
    (l.take n).tail = l.tail.take (n - 1) := by
  apply List.ext_getElem <;>
  grind

theorem dropLast_take {α : Type*} (l : List α) (n : ℕ) :
    (l.take n).dropLast = l.dropLast.take (n - 1) := by
  apply List.ext_getElem <;>
  grind

[Kim Morrison]

But I agree these are missing, or at least should be doable with just grind.

[Snir Broshi]

Sorry, forgot the import :sweat_smile:

[Snir Broshi]

Thanks!

[Kim Morrison]

(If, for the sake of the #mwe, you don't want to import Mathlib, the better choice is to use Type _ instead of Type* and Nat instead of \nat.)

[Snir Broshi]

Do you think I should try to PR straight to core?

[Kim Morrison]

Yes, that would be good, but you can't use grind for the proofs there!

[Snir Broshi]

I'm confused as to how contributing to core works, but here are grind-free proofs:

theorem tail_take {α : Type _} (l : List α) (n : Nat) :
    (l.take n).tail = l.tail.take (n - 1) := by
  simp [← List.drop_one, List.drop_take]

theorem dropLast_take {α : Type _} (l : List α) (n : Nat) :
    (l.take n).dropLast = l.dropLast.take (n - 1) := by
  simp [List.dropLast_eq_take, List.take_take, Nat.sub_min_sub_right,
    Nat.le_trans (Nat.sub_le ..) (Nat.min_le_left ..)]

theorem tail_drop {α : Type _} (l : List α) (n : Nat) :
    (l.drop n).tail = l.tail.drop n := by
  simp

theorem dropLast_drop {α : Type _} (l : List α) (n : Nat) :
    (l.drop n).dropLast = l.dropLast.drop n := by
  simp [List.dropLast_eq_take, Nat.sub_right_comm, List.drop_take]

[Snir Broshi]

(it seems contributing to core requires building Lean first, which then requires me to install GMP and wait a lot, which is a strange hurdle to have to cross. I could've sworn I saw someone mentioning some cache/zip I can download to skip these?)