From 9b9ce0c2acda58b0b95c624534caef1a9fc58ca2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 29 Jan 2026 11:27:46 +1100
Subject: [PATCH] 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           | 10 +++++++++-
 src/Lean/Elab/Tactic/Grind/LintExceptions.lean |  1 +
 tests/lean/run/grind_human_eval_114.lean       |  5 +++++
 tests/lean/run/grind_lint_list.lean            |  4 ++++
 4 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_human_eval_114.lean

diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index a68a71b38d..94aa3ea5f8 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/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]
diff --git a/src/Lean/Elab/Tactic/Grind/LintExceptions.lean b/src/Lean/Elab/Tactic/Grind/LintExceptions.lean
index de94d2e2af..92f9200587 100644
--- a/src/Lean/Elab/Tactic/Grind/LintExceptions.lean
+++ b/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
diff --git a/tests/lean/run/grind_human_eval_114.lean b/tests/lean/run/grind_human_eval_114.lean
new file mode 100644
index 0000000000..be78b3938c
--- /dev/null
+++ b/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
diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean
index 9fc5320a99..d5193e6a5e 100644
--- a/tests/lean/run/grind_lint_list.lean
+++ b/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