fix: mark List.length as @[implicit_reducible] (#12924)

This PR fixes a regression introduced in Lean 4.29.0-rc2 where `simp` no
longer simplifies inside type class instance arguments due to the
`backward.isDefEq.respectTransparency` change. This breaks proofs where
a term like `(a :: l).length` appears both in the main expression and
inside implicit instance arguments (e.g., determining a `BitVec` width).

**The problem:** After `simp only [List.length_cons]`, the main
expression has `l.length + 1` but instances still have `(a ::
l).length`. Since `simp` no longer simplifies inside instances, and
`isDefEq` won't unfold `List.length` at the default transparency,
subsequent lemma applications fail.

**Reproducer** (from Son Ho, reported by Sebastian Ullrich):
```lean
theorem BitVec.getElem!_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) :
     x[i]! = x.toNat.testBit i := by sorry

example (l : List Nat) (a : Nat) (j : Nat) :
  (0#((a :: l).length))[j]! = (0#((a :: l).length)).toNat.testBit j := by
  simp only [List.length_cons]
  simp only [BitVec.getElem!_eq_testBit_toNat] -- works in 4.28.0-rc1, fails in 4.29.0-rc6
```

**The fix:** Mark `List.length` as `@[implicit_reducible]`, allowing
`isDefEq` to unfold it when checking implicit arguments. Several proofs
that previously needed a trailing `rfl` after `simp` now close directly,
since `simp` can see through `List.length` in more positions.

**Longer term:** The root cause is that `GetElem` carries complex proof
obligations in its type class instances, making implicit arguments
sensitive to definitional equality of collection sizes. We are
considering a redesign with a noncomputable `GetElemV` variant based on
`Nonempty` that avoids these casts entirely, but that is a larger change
planned for a future release.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/Data/Array/Find.lean

@@ -622,12 +622,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp; rfl
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp; rfl
+  simp
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -801,7 +801,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?]
 
-@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl
+@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
 
 @[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by

src/Init/Data/List/Find.lean

@@ -1050,7 +1050,7 @@ theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
 
 @[simp, grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp [findFinIdx?_cons, findFinIdx?_nil]; rfl
+  simp [findFinIdx?_cons, findFinIdx?_nil]
 
 @[simp, grind =] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
     l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by

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

@@ -311,7 +311,7 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
   | nil =>
     cases h rfl
   | cons y l ih =>
-    simp only [drop, length]
+    simp only [drop]
     by_cases h₁ : l = []
     · simp [h₁]
     rw [getLast_cons h₁]

src/Init/Data/List/Sort/Impl.lean

@@ -182,7 +182,6 @@ private theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α
     simp only [mergeSortTR.run, mergeSortTR.run, mergeSort]
     rw [merge_eq_mergeTR]
     rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort]
-    rfl
 
 -- We don't make this a `@[csimp]` lemma because `mergeSort_eq_mergeSortTR₂` is faster.
 theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by

src/Init/Data/Vector/Find.lean

@@ -303,12 +303,12 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp; rfl
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp; rfl
+  simp
 
 @[congr] theorem findFinIdx?_congr {p : α → Bool} {xs : Vector α n} {ys : Vector α n} (w : xs = ys) :
     findFinIdx? p xs = findFinIdx? p ys := by

src/Init/Data/Vector/Monadic.lean

@@ -53,7 +53,7 @@ theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
     (mk #[] rfl).mapM f = pure #v[] := by
   unfold mapM
   unfold mapM.go
-  simp; rfl
+  simp
 
 @[simp, grind =] theorem mapM_append [Monad m] [LawfulMonad m]
     {f : α → m β} {xs : Vector α n} {ys : Vector α n'} :

src/Init/Prelude.lean

@@ -3004,7 +3004,7 @@ Examples:
  * `([] : List String).length = 0`
  * `["green", "brown"].length = 2`
 -/
-def List.length : List α → Nat
+@[implicit_reducible] def List.length : List α → Nat
   | nil       => 0
   | cons _ as => HAdd.hAdd (length as) 1
 

tests/elab/Reparen.lean.out.expected

@@ -2983,7 +2983,7 @@ Examples:
  * `([] : List String).length = 0`
  * `["green", "brown"].length = 2`
 -/
-def List.length : List α → Nat
+@[implicit_reducible] def List.length : List α → Nat
   | nil       => 0
   | cons _ as => HAdd.hAdd (  length as)1
 

tests/elab/implicit_reducible_list_length.lean

@@ -0,0 +1,13 @@
+/-!
+Regression test: `simp` should be able to apply lemmas that depend on `List.length`
+even when `List.length` appears inside implicit type class instance arguments.
+See https://github.com/leanprover/lean4/pull/12924
+-/
+
+theorem BitVec.getElem!_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) :
+    x[i]! = x.toNat.testBit i := by sorry
+
+example (l : List Nat) (a : Nat) (j : Nat) :
+    (0#((a :: l).length))[j]! = (0#((a :: l).length)).toNat.testBit j := by
+  simp only [List.length_cons]
+  simp only [BitVec.getElem!_eq_testBit_toNat]

tests/elab/implicit_reducible_list_length.lean.out.expected

@@ -0,0 +1 @@
+implicit_reducible_list_length.lean:7:8-7:40: warning: declaration uses `sorry`