From f0b367d7aa5b02b87ab0b644231299805d23b82f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Mar 2026 01:45:15 -0700 Subject: [PATCH] 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 --- src/Init/Data/Array/Find.lean | 6 +++--- src/Init/Data/List/Find.lean | 2 +- src/Init/Data/List/Nat/TakeDrop.lean | 2 +- src/Init/Data/List/Sort/Impl.lean | 1 - src/Init/Data/Vector/Find.lean | 4 ++-- src/Init/Data/Vector/Monadic.lean | 2 +- src/Init/Prelude.lean | 2 +- tests/elab/Reparen.lean.out.expected | 2 +- tests/elab/implicit_reducible_list_length.lean | 13 +++++++++++++ ...implicit_reducible_list_length.lean.out.expected | 1 + 10 files changed, 24 insertions(+), 11 deletions(-) create mode 100644 tests/elab/implicit_reducible_list_length.lean create mode 100644 tests/elab/implicit_reducible_list_length.lean.out.expected diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index eb29c3359a..302eb7bc98 100644 --- a/src/Init/Data/Array/Find.lean +++ b/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 diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 276b3adb8b..73cce3d26c 100644 --- a/src/Init/Data/List/Find.lean +++ b/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 diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index e9b13e7f66..e9946c31da 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/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₁] diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index e0044cf21d..ee6ad1af34 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/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 diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean index 8d0a866a85..564706c19b 100644 --- a/src/Init/Data/Vector/Find.lean +++ b/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 diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index de23d28ff4..4f1e5f7e12 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/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'} : diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index d1b270aa06..6b33e68b82 100644 --- a/src/Init/Prelude.lean +++ b/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 diff --git a/tests/elab/Reparen.lean.out.expected b/tests/elab/Reparen.lean.out.expected index 685597b22d..f3feac0b4c 100644 --- a/tests/elab/Reparen.lean.out.expected +++ b/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 diff --git a/tests/elab/implicit_reducible_list_length.lean b/tests/elab/implicit_reducible_list_length.lean new file mode 100644 index 0000000000..e8dcdbccb9 --- /dev/null +++ b/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] diff --git a/tests/elab/implicit_reducible_list_length.lean.out.expected b/tests/elab/implicit_reducible_list_length.lean.out.expected new file mode 100644 index 0000000000..bdbe0cb04f --- /dev/null +++ b/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`