feat: adjust grind annotations for List.drop (#12170)

This PR adjusts the grind annotations for List.take/drop, and adds two
theorems.

This resolves problems @datokrat encountered while working on
https://github.com/leanprover/human-eval-lean/blob/master/HumanEvalLean/HumanEval114.lean.

src/Init/Data/List/Nat/TakeDrop.lean

@@ -141,6 +141,10 @@ theorem take_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁
     (l₁ ++ l₂).take i = l₁.take i := by
   simp [take_append, Nat.sub_eq_zero_of_le h]
 
+@[grind =]
+theorem take_append_length {l₁ l₂ : List α} : (l₁ ++ l₂).take l₁.length = l₁ := by
+  simp
+
 /-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
 `i` elements of `l₂` to `l₁`. -/
 theorem take_length_add_append {l₁ l₂ : List α} (i : Nat) :
@@ -304,7 +308,6 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
 
 /-- Dropping the elements up to `i` in `l₁ ++ l₂` is the same as dropping the elements up to `i`
 in `l₁`, dropping the elements up to `i - l₁.length` in `l₂`, and appending them. -/
-@[grind =]
 theorem drop_append {l₁ l₂ : List α} {i : Nat} :
     drop i (l₁ ++ l₂) = drop i l₁ ++ drop (i - l₁.length) l₂ := by
   induction l₁ generalizing i
@@ -315,10 +318,15 @@ theorem drop_append {l₁ l₂ : List α} {i : Nat} :
       congr 1
       omega
 
+@[grind =]
 theorem drop_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) :
     (l₁ ++ l₂).drop i = l₁.drop i ++ l₂ := by
   simp [drop_append, Nat.sub_eq_zero_of_le h]
 
+@[grind =]
+theorem drop_append_length {l₁ l₂ : List α} : (l₁ ++ l₂).drop l₁.length = l₂ := by
+  simp [List.drop_append_of_le_length (Nat.le_refl _)]
+
 /-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
 up to `i` in `l₂`. -/
 @[simp]

src/Lean/Elab/Tactic/Grind/LintExceptions.lean

@@ -20,6 +20,7 @@ import Std
 #grind_lint skip List.getLast_attach
 #grind_lint skip List.getLast_attachWith
 #grind_lint skip List.head_attachWith
+#grind_lint skip List.drop_append_length
 #grind_lint skip Array.back_singleton
 #grind_lint skip Array.count_singleton
 #grind_lint skip Array.foldl_empty

tests/lean/run/grind_human_eval_114.lean

@@ -0,0 +1,5 @@
+example (xs : List Nat) (x : Nat)
+    (i : Nat) (hi : i < (xs ++ [x]).length)
+    (h : 1 ≤ (List.drop i xs).sum + x) :
+    1 ≤ (List.drop i (List.take (xs ++ [x]).length (xs ++ [x]))).sum := by
+  grind

tests/lean/run/grind_lint_list.lean

@@ -35,6 +35,10 @@ import Lean.Elab.Tactic.Grind.LintExceptions
 #guard_msgs in
 #grind_lint inspect (min := 25) List.head_attachWith
 
+-- `List.drop_append_length` is reasonable at 25.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.drop_append_length
+
 /-! Check List namespace: -/
 
 #guard_msgs in