chore: fix Array.modify lemmas

chore: more monadic simp lemmas (#5522 )
feat: Option.attach (#5532 )
2026-03-19 11:24:07 +00:00 · 2024-09-30 16:14:18 +10:00 · 2024-09-30 04:47:49 +00:00 · 2024-09-30 04:13:27 +00:00 · 2024-09-30 04:08:56 +00:00 · 2024-09-30 04:02:24 +00:00
39 changed files with 762 additions and 248 deletions
--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -133,6 +133,9 @@ theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y
  rw [← bind_pure_comp]
  simp only [bind_assoc, pure_bind]

+@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
+  simp [map]
+
 /--
 An alternative constructor for `LawfulMonad` which has more
 defaultable fields in the common case.
--- a/src/Init/Control/Lawful/Instances.lean
+++ b/src/Init/Control/Lawful/Instances.lean
@@ -84,6 +84,11 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
  pure_bind      := by intros; apply ext; simp [run_bind]
  bind_assoc     := by intros; apply ext; simp [run_bind]; apply bind_congr; intro a; cases a <;> simp

+@[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
+    f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
+  simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
+    pure_bind]
+
 end ExceptT

 /-! # Except -/
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -810,11 +810,27 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
  as.foldl (init := (#[], #[])) fun (as, bs) a =>
    if p a then (as.push a, bs) else (as, bs.push a)

-/-! ### Auxiliary functions used in metaprogramming.
+/-! ## Auxiliary functions used in metaprogramming.

 We do not intend to provide verification theorems for these functions.
 -/

+/-! ### eraseReps -/
+
+/--
+`O(|l|)`. Erase repeated adjacent elements. Keeps the first occurrence of each run.
+* `eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5]`
+-/
+def eraseReps {α} [BEq α] (as : Array α) : Array α :=
+  if h : 0 < as.size then
+    let ⟨last, r⟩ := as.foldl (init := (as[0], #[])) fun ⟨last, r⟩ a =>
+      if a == last then ⟨last, r⟩ else ⟨a, r.push last⟩
+    r.push last
+  else
+    #[]
+
+/-! ### allDiff -/
+
 private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
  | 0,   _ => true
  | i+1, h =>
@@ -832,6 +848,8 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def allDiff [BEq α] (as : Array α) : Bool :=
  allDiffAux as 0

+/-! ### getEvenElems -/
+
@[inline] def getEvenElems (as : Array α) : Array α :=
  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
    if even then
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -98,7 +98,7 @@ theorem toArray_concat {as : List α} {x : α} :
  simp

@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
-  apply Array.ext'
+  apply ext'
  simp

 /-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
@@ -136,10 +136,10 @@ attribute [simp] uset
@[deprecated toArray_toList (since := "2024-09-09")]
 abbrev toArray_data := @toArray_toList

-@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
+@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl

-@[deprecated toList_length (since := "2024-09-09")]
-abbrev data_length := @toList_length
+@[deprecated length_toList (since := "2024-09-09")]
+abbrev data_length := @length_toList

@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl

@@ -175,25 +175,25 @@ where
      mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
    unfold mapM.map; split
    · rw [← List.get_drop_eq_drop _ i ‹_›]
-      simp only [aux (i + 1), map_eq_pure_bind, toList_length, List.foldlM_cons, bind_assoc,
+      simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
        pure_bind]
      rfl
    · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
  termination_by arr.size - i
  decreasing_by decreasing_trivial_pre_omega

-@[simp] theorem map_toList (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
+@[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
  rw [map, mapM_eq_foldlM]
  apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
  have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
    induction l generalizing arr <;> simp [*]
  simp [H]

-@[deprecated map_toList (since := "2024-09-09")]
-abbrev map_data := @map_toList
+@[deprecated toList_map (since := "2024-09-09")]
+abbrev map_data := @toList_map

@[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
-  simp only [← toList_length]
+  simp only [← length_toList]
  simp

@[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@@ -201,6 +201,11 @@ abbrev map_data := @map_toList
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
    arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)

+@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
+    (arr ++ l).toList = arr.toList ++ l := by
+  cases arr
+  simp
+
 theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
    (F : Array β → α → Array β) (G : α → List β)
    (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
@@ -292,14 +297,14 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
@[simp] theorem set!_is_setD : @set! = @setD := rfl

@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
-  (Array.setD a index val).size = a.size := by
+    (Array.setD a index val).size = a.size := by
  if h : index < a.size  then
    simp [setD, h]
  else
    simp [setD, h]

@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-  (setD a i v)[i]'h = v := by
+    (setD a i v)[i]'h = v := by
  simp at h
  simp only [setD, h, dite_true, getElem_set, ite_true]

@@ -309,7 +314,7 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a

 /-- Simplifies a normal form from `get!` -/
@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
-  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
+    Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
  by_cases h : i < a.size <;>
    simp [setD, Nat.not_lt_of_le, h,  getD_get?]

@@ -424,12 +429,18 @@ theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList :
@[deprecated getElem_mem_toList (since := "2024-09-09")]
 abbrev getElem_mem_data := @getElem_mem_toList

+theorem getElem?_eq_toList_getElem? (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
+  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg]
+
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-30")]
 theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
  by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]

-@[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
+set_option linter.deprecated false in
+@[deprecated getElem?_eq_toList_getElem? (since := "2024-09-09")]
 abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?

+set_option linter.deprecated false in
 theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
  getElem?_eq_toList_get? ..

@@ -443,7 +454,7 @@ theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD
  simp [back, back?]

@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
-  simp [back?, getElem?_eq_toList_get?]
+  simp [back?, getElem?_eq_toList_getElem?]

 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp

@@ -501,7 +512,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
  simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]

 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
-  (setD a i v)[i] = v := by
+    (setD a i v)[i] = v := by
  simp at h
  simp only [setD, h, dite_true, get_set, ite_true]

@@ -603,11 +614,11 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
  simp [getElem_eq_getElem_toList]

 set_option linter.deprecated false in
-@[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
+@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
  let rec go (as : Array α) (i j hj)
      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
-      (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
+      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
+      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
    rw [reverse.loop]; dsimp; split <;> rename_i h₁
    · match j with | j+1 => ?_
      simp only [Nat.add_sub_cancel]
@@ -615,34 +626,37 @@ set_option linter.deprecated false in
      · rwa [Nat.add_right_comm i]
      · simp [size_swap, h₂]
      · intro k
-        rw [← getElem?_eq_toList_get?, get?_swap]
-        simp only [H, getElem_eq_toList_get, ← List.get?_eq_get, Nat.le_of_lt h₁,
-          getElem?_eq_toList_get?]
+        rw [← getElem?_eq_toList_getElem?, get?_swap]
+        simp only [H, getElem_eq_getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
+          getElem?_eq_toList_getElem?]
        split <;> rename_i h₂
        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
        split <;> rename_i h₃
        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.get?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
    · rw [H]; split <;> rename_i h₂
      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
        cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.get?_reverse' _ _ h).symm
+        exact (List.getElem?_reverse' _ _ h).symm
      · rfl
    termination_by j - i
  simp only [reverse]
  split
  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext_get? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
    split
    · rfl
    · rename_i h
      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
        true_and, Nat.not_lt] at h
-      rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.toList.length_reverse ▸ ‹_›)]
+      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
+
+@[deprecated toList_reverse (since := "2024-09-30")]
+abbrev reverse_toList := @toList_reverse

 /-! ### foldl / foldr -/

@@ -708,7 +722,7 @@ theorem foldr_induction
 /-! ### map -/

@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
-  simp only [mem_def, map_toList, List.mem_map]
+  simp only [mem_def, toList_map, List.mem_map]

 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
    arr.mapM f = return mk (← arr.toList.mapM f) := by
@@ -833,26 +847,26 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
  unfold modify modifyM Id.run
  split <;> simp

-theorem getElem_modify {as : Array α} {x i} (h : i < as.size) :
-    (as.modify x f)[i]'(by simp [h]) = if x = i then f as[i] else as[i] := by
+theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
+    (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h) := by
  simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]
  split
-  · simp only [Id.bind_eq, get_set _ _ _ h]; split <;> simp [*]
-  · rw [if_neg (mt (by rintro rfl; exact h) ‹_›)]
+  · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
+  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]

-theorem getElem_modify_self {as : Array α} {i : Nat} (h : i < as.size) (f : α → α) :
-    (as.modify i f)[i]'(by simp [h]) = f as[i] := by
+theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
+    (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
  simp [getElem_modify h]

-theorem getElem_modify_of_ne {as : Array α} {i : Nat} (hj : j < as.size)
-    (f : α → α) (h : i ≠ j) :
-    (as.modify i f)[j]'(by rwa [size_modify]) = as[j] := by
+theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
+    (f : α → α) (hj : j < (as.modify i f).size) :
+    (as.modify i f)[j] = as[j]'(by simpa using hj) := by
  simp [getElem_modify hj, h]

@[deprecated getElem_modify (since := "2024-08-08")]
-theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
-    (arr.modify x f).get ⟨i, by simp [h]⟩ =
-    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+theorem get_modify {arr : Array α} {x i} (h : i < (arr.modify x f).size) :
+    (arr.modify x f).get ⟨i, h⟩ =
+    if x = i then f (arr.get ⟨i, by simpa using h⟩) else arr.get ⟨i, by simpa using h⟩ := by
  simp [getElem_modify h]

 /-! ### filter -/
@@ -926,7 +940,7 @@ theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size :=
 theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
    (as ++ bs)[i] = as[i] := by
  simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
  conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
  apply List.get_of_eq; rw [append_toList]

@@ -934,7 +948,7 @@ theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.
    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
    (as ++ bs)[i] = bs[i - as.size] := by
  simp only [getElem_eq_getElem_toList]
-  have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
+  have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
  conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
  apply List.get_of_eq; rw [append_toList]

--- a/src/Init/Data/Array/QSort.lean
+++ b/src/Init/Data/Array/QSort.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
+import Init.Data.Ord

 namespace Array
 -- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget
@@ -44,4 +45,11 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
    else as
  sort as low high

+set_option linter.unusedVariables.funArgs false in
+/--
+Sort an array using `compare` to compare elements.
+-/
+def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
+  xs.qsort fun x y => compare x y |>.isLT
+
 end Array
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -59,6 +59,22 @@ def popFront (s : Subarray α) : Subarray α :=
  else
    s

+/--
+The empty subarray.
+-/
+protected def empty : Subarray α where
+  array := #[]
+  start := 0
+  stop := 0
+  start_le_stop := Nat.le_refl 0
+  stop_le_array_size := Nat.le_refl 0
+
+instance : EmptyCollection (Subarray α) :=
+  ⟨Subarray.empty⟩
+
+instance : Inhabited (Subarray α) :=
+  ⟨{}⟩
+
@[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
  let sz := USize.ofNat s.stop
  let rec @[specialize] loop (i : USize) (b : β) : m β := do
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -799,7 +799,6 @@ theorem umod_eq_divRec (hd : 0#w < d) :
  have := lawful_divRec this
  apply DivModState.umod_eq_of_lawful this (wn_divRec ..)

-@[simp]
 theorem divRec_succ' (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
    divRec (m+1) args qr =
    let wn := qr.wn - 1
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -72,21 +72,35 @@ instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
 instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b

@[extern "lean_float_to_string"] opaque Float.toString : Float → String
-
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt8, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt8 (including Inf), returns maximum value of UInt8
+(i.e. UInt8.size - 1).
+-/
@[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt16, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt16 (including Inf), returns maximum value of UInt16
+(i.e. UInt16.size - 1).
+-/
@[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt32, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt32 (including Inf), returns maximum value of UInt32
+(i.e. UInt32.size - 1).
+-/
@[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for UInt64, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for UInt64 (including Inf), returns maximum value of UInt64
+(i.e. UInt64.size - 1).
+-/
@[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64
-/-- If the given float is positive, truncates the value to the nearest positive integer.
-If negative or larger than the maximum value for USize, returns 0. -/
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns 0.
+If larger than the maximum value for USize (including Inf), returns maximum value of USize
+(i.e. USize.size - 1;  Note that this value is platform dependent).
+-/
@[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize

@[extern "lean_float_isnan"] opaque Float.isNaN : Float → Bool
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -43,7 +43,7 @@ The operations are organized as follow:
 * Logic: `any`, `all`, `or`, and `and`.
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
 * Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
-* Minima and maxima: `minimum?` and `maximum?`.
+* Minima and maxima: `min?` and `max?`.
 * Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
  `removeAll`
  (currently these functions are mostly only used in meta code,
@@ -1464,30 +1464,34 @@ def enum : List α → List (Nat × α) := enumFrom 0

 /-! ## Minima and maxima -/

-/-! ### minimum? -/
+/-! ### min? -/

 /--
 Returns the smallest element of the list, if it is not empty.
-* `[].minimum? = none`
-* `[4].minimum? = some 4`
-* `[1, 4, 2, 10, 6].minimum? = some 1`
+* `[].min? = none`
+* `[4].min? = some 4`
+* `[1, 4, 2, 10, 6].min? = some 1`
 -/
-def minimum? [Min α] : List α → Option α
+def min? [Min α] : List α → Option α
  | []    => none
  | a::as => some <| as.foldl min a

-/-! ### maximum? -/
+@[inherit_doc min?, deprecated min? (since := "2024-09-29")] abbrev minimum? := @min?
+
+/-! ### max? -/

 /--
 Returns the largest element of the list, if it is not empty.
-* `[].maximum? = none`
-* `[4].maximum? = some 4`
-* `[1, 4, 2, 10, 6].maximum? = some 10`
+* `[].max? = none`
+* `[4].max? = some 4`
+* `[1, 4, 2, 10, 6].max? = some 10`
 -/
-def maximum? [Max α] : List α → Option α
+def max? [Max α] : List α → Option α
  | []    => none
  | a::as => some <| as.foldl max a

+@[inherit_doc max?, deprecated max? (since := "2024-09-29")] abbrev maximum? := @max?
+
 /-! ## Other list operations

 The functions are currently mostly used in meta code,
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -31,7 +31,7 @@ The following operations are still missing `@[csimp]` replacements:
 The following operations are not recursive to begin with
 (or are defined in terms of recursive primitives):
 `isEmpty`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft`, `rotateRight`, `insert`, `zip`, `enum`,
-`minimum?`, `maximum?`, and `removeAll`.
+`min?`, `max?`, and `removeAll`.

 The following operations were already given `@[csimp]` replacements in `Init/Data/List/Basic.lean`:
 `length`, `map`, `filter`, `replicate`, `leftPad`, `unzip`, `range'`, `iota`, `intersperse`.
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -55,7 +55,7 @@ See also
 * `Init.Data.List.Erase` for lemmas about `List.eraseP` and `List.erase`.
 * `Init.Data.List.Find` for lemmas about `List.find?`, `List.findSome?`, `List.findIdx`,
  `List.findIdx?`, and `List.indexOf`
-* `Init.Data.List.MinMax` for lemmas about `List.minimum?` and `List.maximum?`.
+* `Init.Data.List.MinMax` for lemmas about `List.min?` and `List.max?`.
 * `Init.Data.List.Pairwise` for lemmas about `List.Pairwise` and `List.Nodup`.
 * `Init.Data.List.Sublist` for lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`,
  `List.IsSuffix`, and `List.IsInfix`.
@@ -203,6 +203,9 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=

@[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl

+theorem getElem?_eq_some {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i]'h = a := by
+  simpa using get?_eq_some
+
 /--
 If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
 `rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
@@ -489,7 +492,7 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
  let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩

-theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
+@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
  | _ :: _, 0, _ => .head ..
  | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)

@@ -878,6 +881,20 @@ theorem foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' :
  · simp
  · simp [*, h]

+theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] :
+    ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
+  | [], a₁, a₂ => rfl
+  | a :: l, a₁, a₂ => by
+    simp only [foldl_cons, ha.assoc]
+    rw [foldl_assoc]
+
+theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] :
+    ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂
+  | [], a₁, a₂ => rfl
+  | a :: l, a₁, a₂ => by
+    simp only [foldr_cons, ha.assoc]
+    rw [foldr_assoc]
+
 theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁)
    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
  induction l generalizing init <;> simp [*, H]
@@ -1004,7 +1021,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
 theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
  simp [getLast!, getLast_eq_getLastD]

-theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
+@[simp] theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
  | [], h => absurd rfl h
  | [_], _ => .head ..
  | _::a::l, _ => .tail _ <| getLast_mem (cons_ne_nil a l)
@@ -1102,7 +1119,7 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys
@[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
  cases l <;> simp

-theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
+@[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
  | [], h => absurd rfl h
  | _::_, _ => .head ..

@@ -2392,6 +2409,10 @@ theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
@[simp] theorem map_const (l : List α) (b : β) : map (Function.const α b) l = replicate l.length b :=
  map_eq_replicate_iff.mpr fun _ _ => rfl

+@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.length x) := by
+  funext l
+  simp
+
 /-- Variant of `map_const` using a lambda rather than `Function.const`. -/
 -- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
 theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.length b :=
--- a/src/Init/Data/List/MinMax.lean
+++ b/src/Init/Data/List/MinMax.lean
@@ -7,7 +7,7 @@ prelude
 import Init.Data.List.Lemmas

 /-!
-# Lemmas about `List.minimum?` and `List.maximum?.
+# Lemmas about `List.min?` and `List.max?.
 -/

 namespace List
@@ -16,24 +16,24 @@ open Nat

 /-! ## Minima and maxima -/

-/-! ### minimum? -/
+/-! ### min? -/

-@[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl
+@[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl

-- We don't put `@[simp]` on `minimum?_cons`,
+-- We don't put `@[simp]` on `min?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem minimum?_cons [Min α] {xs : List α} : (x :: xs).minimum? = foldl min x xs := rfl
+theorem min?_cons [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl

-@[simp] theorem minimum?_eq_none_iff {xs : List α} [Min α] : xs.minimum? = none ↔ xs = [] := by
-  cases xs <;> simp [minimum?]
+@[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = [] := by
+  cases xs <;> simp [min?]

-theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
-    {xs : List α} → xs.minimum? = some a → a ∈ xs := by
+theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
+    {xs : List α} → xs.min? = some a → a ∈ xs := by
  intro xs
  match xs with
  | nil => simp
  | x :: xs =>
-    simp only [minimum?_cons, Option.some.injEq, List.mem_cons]
+    simp only [min?_cons, Option.some.injEq, List.mem_cons]
    intro eq
    induction xs generalizing x with
    | nil =>
@@ -49,12 +49,12 @@ theorem minimum?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b

 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.

-theorem le_minimum?_iff [Min α] [LE α]
+theorem le_min?_iff [Min α] [LE α]
    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
-    {xs : List α} → xs.minimum? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
+    {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
  | nil => by simp
  | cons x xs => by
-    rw [minimum?]
+    rw [min?]
    intro eq y
    simp only [Option.some.injEq] at eq
    induction xs generalizing x with
@@ -67,46 +67,46 @@ theorem le_minimum?_iff [Min α] [LE α]

 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
    (le_refl : ∀ a : α, a ≤ a)
    (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
-    xs.minimum? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
-  refine ⟨fun h => ⟨minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
+    xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
+  refine ⟨fun h => ⟨min?_mem min_eq_or h, (le_min?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
  intro ⟨h₁, h₂⟩
  cases xs with
  | nil => simp at h₁
  | cons x xs =>
    exact congrArg some <| anti.1
-      ((le_minimum?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
-      (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
+      ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))

-theorem minimum?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
-    (replicate n a).minimum? = if n = 0 then none else some a := by
+theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
+    (replicate n a).min? = if n = 0 then none else some a := by
  induction n with
  | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, minimum?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons]

-@[simp] theorem minimum?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
-    (replicate n a).minimum? = some a := by
-  simp [minimum?_replicate, Nat.ne_of_gt h, w]
+@[simp] theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
+    (replicate n a).min? = some a := by
+  simp [min?_replicate, Nat.ne_of_gt h, w]

-/-! ### maximum? -/
+/-! ### max? -/

-@[simp] theorem maximum?_nil [Max α] : ([] : List α).maximum? = none := rfl
+@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl

-- We don't put `@[simp]` on `maximum?_cons`,
+-- We don't put `@[simp]` on `max?_cons`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem maximum?_cons [Max α] {xs : List α} : (x :: xs).maximum? = foldl max x xs := rfl
+theorem max?_cons [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl

-@[simp] theorem maximum?_eq_none_iff {xs : List α} [Max α] : xs.maximum? = none ↔ xs = [] := by
-  cases xs <;> simp [maximum?]
+@[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = [] := by
+  cases xs <;> simp [max?]

-theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
-    {xs : List α} → xs.maximum? = some a → a ∈ xs
+theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
+    {xs : List α} → xs.max? = some a → a ∈ xs
  | nil => by simp
  | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩
+    rw [max?]; rintro ⟨⟩
    induction xs generalizing x with simp at *
    | cons y xs ih =>
      rcases ih (max x y) with h | h <;> simp [h]
@@ -114,40 +114,57 @@ theorem maximum?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b

 -- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.

-theorem maximum?_le_iff [Max α] [LE α]
+theorem max?_le_iff [Max α] [LE α]
    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
-    {xs : List α} → xs.maximum? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
+    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
  | nil => by simp
  | cons x xs => by
-    rw [maximum?]; rintro ⟨⟩ y
+    rw [max?]; rintro ⟨⟩ y
    induction xs generalizing x with
    | nil => simp
    | cons y xs ih => simp [ih, max_le_iff, and_assoc]

 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
 -- and `le_min_iff`.
-theorem maximum?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
+theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
    (le_refl : ∀ a : α, a ≤ a)
    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
-    xs.maximum? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
-  refine ⟨fun h => ⟨maximum?_mem max_eq_or h, (maximum?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
+    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
+  refine ⟨fun h => ⟨max?_mem max_eq_or h, (max?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
  intro ⟨h₁, h₂⟩
  cases xs with
  | nil => simp at h₁
  | cons x xs =>
    exact congrArg some <| anti.1
-      (h₂ _ (maximum?_mem max_eq_or (xs := x::xs) rfl))
-      ((maximum?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
+      ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)

-theorem maximum?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
-    (replicate n a).maximum? = if n = 0 then none else some a := by
+theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
+    (replicate n a).max? = if n = 0 then none else some a := by
  induction n with
  | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, maximum?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons]

-@[simp] theorem maximum?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
-    (replicate n a).maximum? = some a := by
-  simp [maximum?_replicate, Nat.ne_of_gt h, w]
+@[simp] theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
+    (replicate n a).max? = some a := by
+  simp [max?_replicate, Nat.ne_of_gt h, w]
+
+@[deprecated min?_nil (since := "2024-09-29")] abbrev minimum?_nil := @min?_nil
+@[deprecated min?_cons (since := "2024-09-29")] abbrev minimum?_cons := @min?_cons
+@[deprecated min?_eq_none_iff (since := "2024-09-29")] abbrev mininmum?_eq_none_iff := @min?_eq_none_iff
+@[deprecated min?_mem (since := "2024-09-29")] abbrev minimum?_mem := @min?_mem
+@[deprecated le_min?_iff (since := "2024-09-29")] abbrev le_minimum?_iff := @le_min?_iff
+@[deprecated min?_eq_some_iff (since := "2024-09-29")] abbrev minimum?_eq_some_iff := @min?_eq_some_iff
+@[deprecated min?_replicate (since := "2024-09-29")] abbrev minimum?_replicate := @min?_replicate
+@[deprecated min?_replicate_of_pos (since := "2024-09-29")] abbrev minimum?_replicate_of_pos := @min?_replicate_of_pos
+@[deprecated max?_nil (since := "2024-09-29")] abbrev maximum?_nil := @max?_nil
+@[deprecated max?_cons (since := "2024-09-29")] abbrev maximum?_cons := @max?_cons
+@[deprecated max?_eq_none_iff (since := "2024-09-29")] abbrev maximum?_eq_none_iff := @max?_eq_none_iff
+@[deprecated max?_mem (since := "2024-09-29")] abbrev maximum?_mem := @max?_mem
+@[deprecated max?_le_iff (since := "2024-09-29")] abbrev maximum?_le_iff := @max?_le_iff
+@[deprecated max?_eq_some_iff (since := "2024-09-29")] abbrev maximum?_eq_some_iff := @max?_eq_some_iff
+@[deprecated max?_replicate (since := "2024-09-29")] abbrev maximum?_replicate := @max?_replicate
+@[deprecated max?_replicate_of_pos (since := "2024-09-29")] abbrev maximum?_replicate_of_pos := @max?_replicate_of_pos

 end List
--- a/src/Init/Data/List/Nat/Basic.lean
+++ b/src/Init/Data/List/Nat/Basic.lean
@@ -86,26 +86,26 @@ theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃
    obtain ⟨h', -⟩ := getElem?_eq_some_iff.1 h
    exact ⟨h', h⟩

-/-! ### minimum? -/
+/-! ### min? -/

-- A specialization of `minimum?_eq_some_iff` to Nat.
-theorem minimum?_eq_some_iff' {xs : List Nat} :
-    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  minimum?_eq_some_iff
+-- A specialization of `min?_eq_some_iff` to Nat.
+theorem min?_eq_some_iff' {xs : List Nat} :
+    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  min?_eq_some_iff
    (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => by omega)
-    (le_min_iff := fun _ _ _ => by omega)
+    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
+    (le_min_iff := fun _ _ _ => Nat.le_min)

 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem minimum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).minimum? = some (match l.minimum? with
+theorem min?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).min? = some (match l.min? with
    | none => a
    | some m => min a m) := by
-  rw [minimum?_eq_some_iff']
+  rw [min?_eq_some_iff']
  split <;> rename_i h m
  · simp_all
-  · rw [minimum?_eq_some_iff'] at m
+  · rw [min?_eq_some_iff'] at m
    obtain ⟨m, le⟩ := m
    rw [Nat.min_def]
    constructor
@@ -122,11 +122,11 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
 theorem foldl_min
    {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
    {l : List α} {a : α} :
-    l.foldl (init := a) min = min a (l.minimum?.getD a) := by
+    l.foldl (init := a) min = min a (l.min?.getD a) := by
  cases l with
  | nil => simp [Std.IdempotentOp.idempotent]
  | cons b l =>
-    simp only [minimum?]
+    simp only [min?]
    induction l generalizing a b with
    | nil => simp
    | cons c l ih => simp [ih, Std.Associative.assoc]
@@ -134,7 +134,7 @@ theorem foldl_min
 theorem foldl_min_right {α β : Type _}
    [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)]
    {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
+    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).min?.getD b) := by
  rw [← foldl_map, foldl_min]

 theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by
@@ -148,12 +148,12 @@ theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
    l.foldl (init := a) min ≤ b :=
  Nat.le_trans (foldl_min_le) h

-theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    l.minimum?.getD k ≤ a := by
+theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.min?.getD k ≤ a := by
  cases l with
  | nil => simp at h
  | cons b l =>
-    simp [minimum?_cons]
+    simp [min?_cons]
    simp at h
    rcases h with (rfl | h)
    · exact foldl_min_le
@@ -166,26 +166,26 @@ theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
        · exact foldl_min_min_of_le (Nat.min_le_right _ _)
        · exact ih _ h

-/-! ### maximum? -/
+/-! ### max? -/

-- A specialization of `maximum?_eq_some_iff` to Nat.
-theorem maximum?_eq_some_iff' {xs : List Nat} :
-    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
-  maximum?_eq_some_iff
+-- A specialization of `max?_eq_some_iff` to Nat.
+theorem max?_eq_some_iff' {xs : List Nat} :
+    xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
+  max?_eq_some_iff
    (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => by omega)
-    (max_le_iff := fun _ _ _ => by omega)
+    (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp)
+    (max_le_iff := fun _ _ _ => Nat.max_le)

 -- This could be generalized,
 -- but will first require further work on order typeclasses in the core repository.
-theorem maximum?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).maximum? = some (match l.maximum? with
+theorem max?_cons' {a : Nat} {l : List Nat} :
+    (a :: l).max? = some (match l.max? with
    | none => a
    | some m => max a m) := by
-  rw [maximum?_eq_some_iff']
+  rw [max?_eq_some_iff']
  split <;> rename_i h m
  · simp_all
-  · rw [maximum?_eq_some_iff'] at m
+  · rw [max?_eq_some_iff'] at m
    obtain ⟨m, le⟩ := m
    rw [Nat.max_def]
    constructor
@@ -202,11 +202,11 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
 theorem foldl_max
    {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
    {l : List α} {a : α} :
-    l.foldl (init := a) max = max a (l.maximum?.getD a) := by
+    l.foldl (init := a) max = max a (l.max?.getD a) := by
  cases l with
  | nil => simp [Std.IdempotentOp.idempotent]
  | cons b l =>
-    simp only [maximum?]
+    simp only [max?]
    induction l generalizing a b with
    | nil => simp
    | cons c l ih => simp [ih, Std.Associative.assoc]
@@ -214,7 +214,7 @@ theorem foldl_max
 theorem foldl_max_right {α β : Type _}
    [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)]
    {l : List α} {b : β} {f : α → β} :
-    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
+    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).max?.getD b) := by
  rw [← foldl_map, foldl_max]

 theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by
@@ -228,12 +228,12 @@ theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
    a ≤ l.foldl (init := b) max :=
  Nat.le_trans h (le_foldl_max)

-theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    a ≤ l.maximum?.getD k := by
+theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.max?.getD k := by
  cases l with
  | nil => simp at h
  | cons b l =>
-    simp [maximum?_cons]
+    simp [max?_cons]
    simp at h
    rcases h with (rfl | h)
    · exact le_foldl_max
@@ -246,4 +246,11 @@ theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
        · exact le_foldl_max_of_le (Nat.le_max_right b a)
        · exact ih _ h

+@[deprecated min?_eq_some_iff' (since := "2024-09-29")] abbrev minimum?_eq_some_iff' := @min?_eq_some_iff'
+@[deprecated min?_cons' (since := "2024-09-29")] abbrev minimum?_cons' := @min?_cons'
+@[deprecated min?_getD_le_of_mem (since := "2024-09-29")] abbrev minimum?_getD_le_of_mem := @min?_getD_le_of_mem
+@[deprecated max?_eq_some_iff' (since := "2024-09-29")] abbrev maximum?_eq_some_iff' := @max?_eq_some_iff'
+@[deprecated max?_cons' (since := "2024-09-29")] abbrev maximum?_cons' := @max?_cons'
+@[deprecated le_max?_getD_of_mem (since := "2024-09-29")] abbrev le_maximum?_getD_of_mem := @le_max?_getD_of_mem
+
 end List
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -42,7 +42,7 @@ theorem getElem_take' (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j)

 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
-theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
+@[simp] theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
    (L.take j)[i] =
    L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
  rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1]
@@ -52,7 +52,7 @@ length `> i`. Version designed to rewrite from the big list to the small list. -
@[deprecated getElem_take' (since := "2024-06-12")]
 theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
-  simp [getElem_take' _ hi hj]
+  simp

 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the small list to the big list. -/
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -248,6 +248,10 @@ theorem countP_eq_countP_filter_add (l : List α) (p q : α → Bool) :
 theorem Perm.count_eq [DecidableEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) :
    count a l₁ = count a l₂ := p.countP_eq _

+/-
+This theorem is a variant of `Perm.foldl_eq` defined in Mathlib which uses typeclasses rather
+than the explicit `comm` argument.
+-/
 theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f (f z x) y = f (f z y) x)
    (init) : foldl f init l₁ = foldl f init l₂ := by
@@ -264,6 +268,28 @@ theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~
    refine (IH₁ comm init).trans (IH₂ ?_ _)
    intros; apply comm <;> apply p₁.symm.subset <;> assumption

+/-
+This theorem is a variant of `Perm.foldr_eq` defined in Mathlib which uses typeclasses rather
+than the explicit `comm` argument.
+-/
+theorem Perm.foldr_eq' {f : α → β → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
+    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f y (f x z) = f x (f y z))
+    (init) : foldr f init l₁ = foldr f init l₂ := by
+  induction p using recOnSwap' generalizing init with
+  | nil => simp
+  | cons x _p IH =>
+    simp only [foldr]
+    congr 1
+    apply IH; intros; apply comm <;> exact .tail _ ‹_›
+  | swap' x y _p IH =>
+    simp only [foldr]
+    rw [comm x (.tail _ <| .head _) y (.head _)]
+    congr 2
+    apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›)
+  | trans p₁ _p₂ IH₁ IH₂ =>
+    refine (IH₁ comm init).trans (IH₂ ?_ _)
+    intros; apply comm <;> apply p₁.symm.subset <;> assumption
+
 theorem Perm.rec_heq {β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α}
    (hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b'))
    (f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :
--- a/src/Init/Data/Option.lean
+++ b/src/Init/Data/Option.lean
@@ -8,3 +8,5 @@ import Init.Data.Option.Basic
 import Init.Data.Option.BasicAux
 import Init.Data.Option.Instances
 import Init.Data.Option.Lemmas
+import Init.Data.Option.Attach
+import Init.Data.Option.List
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Option.Basic
+import Init.Data.Option.List
+import Init.Data.List.Attach
+import Init.BinderPredicates
+
+namespace Option
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`Option {x // P x}` is the same as the input `Option α`.
+-/
+@[inline] private unsafe def attachWithImpl
+    (o : Option α) (P : α → Prop) (_ : ∀ x ∈ o, P x) : Option {x // P x} := unsafeCast o
+
+/-- "Attach" a proof `P x` that holds for the element of `o`, if present,
+to produce a new option with the same element but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (xs : Option α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Option {x // P x} :=
+  match xs with
+  | none => none
+  | some x => some ⟨x, H x (mem_some_self x)⟩
+
+/-- "Attach" the proof that the element of `xs`, if present, is in `xs`
+to produce a new option with the same elements but in the type `{x // x ∈ xs}`. -/
+@[inline] def attach (xs : Option α) : Option {x // x ∈ xs} := xs.attachWith _ fun _ => id
+
+@[simp] theorem attach_none : (none : Option α).attach = none := rfl
+@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
+
+@[simp] theorem attach_some {x : α} :
+    (some x).attach = some ⟨x, rfl⟩ := rfl
+@[simp] theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) :
+    (some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl
+
+theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
+    o₁.attach = o₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
+  subst h
+  simp
+
+theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
+    o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
+  subst w
+  simp
+
+theorem attach_map_coe (o : Option α) (f : α → β) :
+    (o.attach.map fun (i : {i // i ∈ o}) => f i) = o.map f := by
+  cases o <;> simp
+
+theorem attach_map_val (o : Option α) (f : α → β) :
+    (o.attach.map fun i => f i.val) = o.map f :=
+  attach_map_coe _ _
+
+@[simp]
+theorem attach_map_subtype_val (o : Option α) :
+    o.attach.map Subtype.val = o :=
+  (attach_map_coe _ _).trans (congrFun Option.map_id _)
+
+theorem attachWith_map_coe {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
+    ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
+  cases o <;> simp [H]
+
+theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
+    ((o.attachWith p H).map fun i => f i.val) = o.map f :=
+  attachWith_map_coe _ _ _
+
+@[simp]
+theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).map Subtype.val = o :=
+  (attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
+
+@[simp] theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
+  | none, ⟨x, h⟩ => by simp at h
+  | some a, ⟨x, h⟩ => by simpa using h
+
+@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
+  cases o <;> simp
+
+@[simp] theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).isNone = o.isNone := by
+  cases o <;> simp
+
+@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
+  cases o <;> simp
+
+@[simp] theorem isSome_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    (o.attachWith p H).isSome = o.isSome := by
+  cases o <;> simp
+
+@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none ↔ o = none := by
+  cases o <;> simp
+
+@[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} :
+    o.attach = some x ↔ o = some x.val := by
+  cases o <;> cases x <;> simp
+
+@[simp] theorem attachWith_eq_none_iff {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
+    o.attachWith p H = none ↔ o = none := by
+  cases o <;> simp
+
+@[simp] theorem attachWith_eq_some_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) {x : {x // p x}} :
+    o.attachWith p H = some x ↔ o = some x.val := by
+  cases o <;> cases x <;> simp
+
+@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
+    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ := by
+  cases o
+  · simp at h
+  · simp [get_some]
+
+@[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) (h : (o.attachWith p H).isSome) :
+    (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
+  cases o
+  · simp at h
+  · simp [get_some]
+
+@[simp] theorem toList_attach (o : Option α) :
+    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  cases o <;> simp
+
+theorem attach_map {o : Option α} (f : α → β) :
+    (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
+  cases o <;> simp
+
+theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
+    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
+      fun ⟨x, h⟩ => ⟨f x, h⟩ := by
+  cases o <;> simp
+
+theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
+    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
+  cases o <;> simp
+
+theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}
+    (f : { x // P x } → β) :
+    (o.attachWith P H).map f =
+      o.pmap (fun a (h : a ∈ o ∧ P a) => f ⟨a, h.2⟩) (fun a h => ⟨h, H a h⟩) := by
+  cases o <;> simp
+
+theorem attach_bind {o : Option α} {f : α → Option β} :
+    (o.bind f).attach =
+      o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, mem_bind_iff.mpr ⟨x, h, h'⟩⟩ := by
+  cases o <;> simp
+
+theorem bind_attach {o : Option α} {f : {x // x ∈ o} → Option β} :
+    o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
+  cases o <;> simp
+
+theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → a ∈ o → Option β} :
+    o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
+  cases o <;> simp
+
+theorem attach_filter {o : Option α} {p : α → Bool} :
+    (o.filter p).attach =
+      o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp only [filter_some, attach_some]
+    ext
+    simp only [mem_def, attach_eq_some_iff, ite_none_right_eq_some, some.injEq, some_bind,
+      dite_none_right_eq_some]
+    constructor
+    · rintro ⟨h, w⟩
+      refine ⟨h, by ext; simpa using w⟩
+    · rintro ⟨h, rfl⟩
+      simp [h]
+
+theorem filter_attach {o : Option α} {p : {x // x ∈ o} → Bool} :
+    o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
+  cases o <;> simp [filter_some]
+
+end Option
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -138,6 +138,10 @@ theorem bind_eq_none' {o : Option α} {f : α → Option β} :
    o.bind f = none ↔ ∀ b a, a ∈ o → b ∉ f a := by
  simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]

+theorem mem_bind_iff {o : Option α} {f : α → Option β} :
+    b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
+  cases o <;> simp
+
 theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β) :
    (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
  cases a <;> cases b <;> rfl
@@ -232,9 +236,27 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
  cases o <;> simp at h ⊢

@[simp] theorem filter_eq_none {p : α → Bool} :
-    Option.filter p o = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
+    o.filter p = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
  cases o <;> simp [filter_some]

+@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} :
+    o.filter p = some a ↔ a ∈ o ∧ p a := by
+  cases o with
+  | none => simp
+  | some a =>
+    simp [filter_some]
+    split <;> rename_i h
+    · simp only [some.injEq, iff_self_and]
+      rintro rfl
+      exact h
+    · simp only [reduceCtorEq, false_iff, not_and, Bool.not_eq_true]
+      rintro rfl
+      simpa using h
+
+theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
+    a ∈ o.filter p ↔ a ∈ o ∧ p a := by
+  simp
+
@[simp] theorem all_guard (p : α → Prop) [DecidablePred p] (a : α) :
    Option.all q (guard p a) = (!p a || q a) := by
  simp only [guard]
@@ -350,6 +372,8 @@ end choice

@[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl

+-- See `Init.Data.Option.List` for lemmas about `toList`.
+
@[simp] theorem or_some : (some a).or o = some a := rfl
@[simp] theorem none_or : none.or o = o := rfl

--- a/src/Init/Data/Option/List.lean
+++ b/src/Init/Data/Option/List.lean
@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Lemmas
+
+namespace Option
+
+@[simp] theorem mem_toList (a : α) (o : Option α) : a ∈ o.toList ↔ a ∈ o := by
+  cases o <;> simp [eq_comm]
+
+end Option
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -733,7 +733,8 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
        throwError "invalid default value for field, it contains metavariables{indentExpr value}"
      /- The identity function is used as "marker". -/
      let value ← mkId value
-      discard <| mkAuxDefinition declName type value (zetaDelta := true)
+      -- No need to compile the definition, since it is only used during elaboration.
+      discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
      setReducibleAttribute declName

 /--
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -277,6 +277,7 @@ where
      | _ => mkAtomLinearCombo e
    | (``Min.min, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_min []) a b)
    | (``Max.max, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_max []) a b)
+    | (``Int.toNat, #[n]) => rewrite e (mkApp (.const ``Int.toNat_eq_max []) n)
    | (``HShiftLeft.hShiftLeft, #[_, _, _, _, a, b]) =>
      rewrite e (mkApp2 (.const ``Int.ofNat_shiftLeft_eq []) a b)
    | (``HShiftRight.hShiftRight, #[_, _, _, _, a, b]) =>
--- a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
+++ b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
@@ -29,12 +29,14 @@ The minimum non-zero entry in a list of natural numbers, or zero if all entries
 We completely characterize the function via
 `nonzeroMinimum_eq_zero_iff` and `nonzeroMinimum_eq_nonzero_iff` below.
 -/
-def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.minimum? |>.getD 0
+def nonzeroMinimum (xs : List Nat) : Nat := xs.filter (· ≠ 0) |>.min? |>.getD 0

 -- A specialization of `minimum?_eq_some_iff` to Nat.
-theorem minimum?_eq_some_iff' {xs : List Nat} :
-    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  minimum?_eq_some_iff
+-- This is a duplicate `min?_eq_some_iff'` proved in `Init.Data.List.Nat.Basic`,
+-- and could be deduplicated but the import hierarchy is awkward.
+theorem min?_eq_some_iff'' {xs : List Nat} :
+    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  min?_eq_some_iff
    (le_refl := Nat.le_refl)
    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
    (le_min_iff := fun _ _ _ => Nat.le_min)
@@ -42,27 +44,27 @@ theorem minimum?_eq_some_iff' {xs : List Nat} :
 open Classical in
@[simp] theorem nonzeroMinimum_eq_zero_iff {xs : List Nat} :
    xs.nonzeroMinimum = 0 ↔ ∀ x ∈ xs, x = 0 := by
-  simp [nonzeroMinimum, Option.getD_eq_iff, minimum?_eq_none_iff, minimum?_eq_some_iff',
+  simp [nonzeroMinimum, Option.getD_eq_iff, min?_eq_none_iff, min?_eq_some_iff'',
    filter_eq_nil_iff, mem_filter]

 theorem nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum ≠ 0) :
    xs.nonzeroMinimum ∈ xs := by
  dsimp [nonzeroMinimum] at *
-  generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m at *
+  generalize h : (xs.filter (· ≠ 0) |>.min?) = m at *
  match m, w with
-  | some (m+1), _ => simp_all [minimum?_eq_some_iff', mem_filter]
+  | some (m+1), _ => simp_all [min?_eq_some_iff'', mem_filter]

 theorem nonzeroMinimum_pos {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : 0 < xs.nonzeroMinimum :=
  Nat.pos_iff_ne_zero.mpr fun w => h (nonzeroMinimum_eq_zero_iff.mp w _ m)

 theorem nonzeroMinimum_le {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : xs.nonzeroMinimum ≤ a := by
-  have : (xs.filter (· ≠ 0) |>.minimum?) = some xs.nonzeroMinimum := by
+  have : (xs.filter (· ≠ 0) |>.min?) = some xs.nonzeroMinimum := by
    have w := nonzeroMinimum_pos m h
    dsimp [nonzeroMinimum] at *
-    generalize h : (xs.filter (· ≠ 0) |>.minimum?) = m? at *
+    generalize h : (xs.filter (· ≠ 0) |>.min?) = m? at *
    match m?, w with
    | some m?, _ => rfl
-  rw [minimum?_eq_some_iff'] at this
+  rw [min?_eq_some_iff''] at this
  apply this.2
  simp [List.mem_filter]
  exact ⟨m, h⟩
@@ -142,4 +144,4 @@ theorem minNatAbs_eq_nonzero_iff (xs : List Int) (w : z ≠ 0) :
@[simp] theorem minNatAbs_nil : ([] : List Int).minNatAbs = 0 := rfl

 /-- The maximum absolute value in a list of integers. -/
-def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.maximum? |>.getD 0
+def maxNatAbs (xs : List Int) : Nat := xs.map Int.natAbs |>.max? |>.getD 0
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -573,15 +573,33 @@ where
    catch _  =>
      return some mvarId

+/--
+Discharges assumptions of the form `∀ …, a = b` using `rfl`. This is particularly useful for higher
+order assumptions of the form `∀ …, e = ?g x y` to instaniate  a paramter `g` even if that does not
+appear on the lhs of the rule.
+-/
+def dischargeRfl (e : Expr) : SimpM (Option Expr) := do
+  forallTelescope e fun xs e => do
+    let some (t, a, b) := e.eq? | return .none
+    unless a.getAppFn.isMVar || b.getAppFn.isMVar do return .none
+    if (← withReducible <| isDefEq a b) then
+      trace[Meta.Tactic.simp.discharge] "Discharging with rfl: {e}"
+      let u ← getLevel t
+      let proof := mkApp2 (.const ``rfl [u]) t a
+      let proof ← mkLambdaFVars xs proof
+      return .some proof
+    return .none
+
+
 def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
  let e := e.cleanupAnnotations
  if isEqnThmHypothesis e then
-    if let some r ← dischargeUsingAssumption? e then
-      return some r
-    if let some r ← dischargeEqnThmHypothesis? e then
-      return some r
+    if let some r ← dischargeUsingAssumption? e then return some r
+    if let some r ← dischargeEqnThmHypothesis? e then return some r
  let r ← simp e
-  if r.expr.isTrue then
+  if let some p ← dischargeRfl r.expr then
+    return some (← mkEqMPR (← r.getProof) p)
+  else if r.expr.isTrue then
    return some (← mkOfEqTrue (← r.getProof))
  else
    return none
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -360,7 +360,8 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
    else
      -- stopped after `tk` => add space
-      push $ tk ++ " "
+      pushLine
+      push tk
      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
  else
    -- already separated => use `tk` as is
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -237,7 +237,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
    let _ := @lexOrd
    let _ := @leOfOrd.{0}
    let _ := @maxOfLe
-    results.map (·.1) |>.maximum?
+    results.map (·.1) |>.max?
  let res? := results.find? (·.1 == maxPrio?) |>.map (·.2)
  if let some i := res? then
    if let .ofTermInfo ti := i.info then
@@ -380,7 +380,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
              priority := if hoverPos.byteIdx == tailPos.byteIdx + trailSize then 0 else 1
            }]
    return gs
-  let maxPrio? := gs.map (·.priority) |>.maximum?
+  let maxPrio? := gs.map (·.priority) |>.max?
  gs.filter (some ·.priority == maxPrio?)
 where
  hasNestedTactic (pos tailPos) : InfoTree → Bool
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -186,7 +186,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
    have := (hg (l := []) (l' := [])).length_eq
    rw [List.length_append, List.append_nil] at this
    omega
-  rw [updateAllBuckets, toListModel, Array.map_toList, List.bind_eq_foldl, List.foldl_map,
+  rw [updateAllBuckets, toListModel, Array.toList_map, List.bind_eq_foldl, List.foldl_map,
    toListModel, List.bind_eq_foldl]
  suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
      Perm (g l'') l' →
--- a/src/Std/Sat/CNF/RelabelFin.lean
+++ b/src/Std/Sat/CNF/RelabelFin.lean
@@ -15,12 +15,12 @@ namespace CNF
 /--
 Obtain the literal with the largest identifier in `c`.
 -/
-def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.maximum?
+def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.max?

 theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) :
    ∀ lit, Mem lit c → lit ≤ maxLit := by
  intro lit hlit
-  simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
+  simp only [maxLiteral, List.max?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at h
  simp only [Mem] at hlit
  rcases h with ⟨_, hbar⟩
@@ -35,25 +35,25 @@ theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) :
  cases h <;> rename_i h
  all_goals
    have h1 := List.ne_nil_of_mem h
-    have h2 := not_congr <| @List.maximum?_eq_none_iff _ (c.map (·.1)) _
+    have h2 := not_congr <| @List.max?_eq_none_iff _ (c.map (·.1)) _
    simp [← Option.ne_none_iff_exists', h1, h2, maxLiteral]

 theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) :
    ∀ lit, ¬Mem lit c := by
  intro lit hlit
-  simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil_iff] at h
+  simp only [maxLiteral, List.max?_eq_none_iff, List.map_eq_nil_iff] at h
  simp only [h, not_mem_nil] at hlit

 /--
 Obtain the literal with the largest identifier in `f`.
 -/
 def maxLiteral (f : CNF Nat) : Option Nat :=
-  List.filterMap Clause.maxLiteral f |>.maximum?
+  List.filterMap Clause.maxLiteral f |>.max?

 theorem of_maxLiteral_eq_some' (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
    ∀ clause, clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit := by
  intro clause hclause1 hclause2
-  simp [maxLiteral, List.maximum?_eq_some_iff'] at h
+  simp [maxLiteral, List.max?_eq_some_iff'] at h
  rcases h with ⟨_, hclause3⟩
  apply hclause3 localMax clause hclause1 hclause2

@@ -70,7 +70,7 @@ theorem of_maxLiteral_eq_some (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
 theorem of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) :
    ∀ lit, ¬Mem lit f := by
  intro lit hlit
-  simp only [maxLiteral, List.maximum?_eq_none_iff] at h
+  simp only [maxLiteral, List.max?_eq_none_iff] at h
  dsimp [Mem] at hlit
  rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩
  have := Clause.of_maxLiteral_eq_none clause (List.forall_none_of_filterMap_eq_nil h clause hclause1) lit
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -136,12 +136,10 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
          exact ih.2 i b h
        | some (l, true) =>
          simp only [heq] at h
-          have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
-          have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
          rcases ih with ⟨hsize, ih⟩
          by_cases i = l.1
          · next i_eq_l =>
-            simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
+            simp only [i_eq_l, Array.getElem_modify_self] at h
            by_cases b
            · next b_eq_true =>
              rw [isUnit_iff, DefaultClause.toList] at heq
@@ -160,16 +158,14 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
              rw [b_eq_false, Subtype.ext i_eq_l]
              exact ih h
          · next i_ne_l =>
-            simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
+            simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
            exact ih i b h
        | some (l, false) =>
          simp only [heq] at h
-          have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
-          have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
          rcases ih with ⟨hsize, ih⟩
          by_cases i = l.1
          · next i_eq_l =>
-            simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
+            simp only [i_eq_l, Array.getElem_modify_self] at h
            by_cases b
            · next b_eq_true =>
              simp only [hasAssignment, b_eq_true, ite_true, hasPos_addNeg] at h
@@ -187,7 +183,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
              rw [c_def] at cOpt_in_arr
              exact cOpt_in_arr
          · next i_ne_l =>
-            simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
+            simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
            exact ih i b h
    rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
    intro i b h
@@ -281,7 +277,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
    intro i b hb
    have hf := f_readyForRupAdd.2.2 i b
    have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
-    have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
    simp only at hb
    by_cases (i, b) = (l, true)
    · next ib_eq_c =>
@@ -292,7 +287,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
      apply DefaultClause.ext
      simp only [unit, hc]
    · next ib_ne_c =>
-      have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
+      have hb' : hasAssignment b f.assignments[i.1] := by
        by_cases l.1 = i.1
        · next l_eq_i =>
          have b_eq_false : b = false := by
@@ -302,10 +297,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
            · next b_eq_false =>
              simp only [Bool.not_eq_true] at b_eq_false
              exact b_eq_false
-          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos, reduceCtorEq] at hb
+          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb
          simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq]
        · next l_ne_i =>
-          simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+          simp only [Array.getElem_modify_of_ne l_ne_i] at hb
          exact hb
      specialize hf hb'
      simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -322,7 +317,6 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
    intro i b hb
    have hf := f_readyForRupAdd.2.2 i b
    have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
-    have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
    simp only at hb
    by_cases (i, b) = (l, false)
    · next ib_eq_c =>
@@ -333,7 +327,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
      apply DefaultClause.ext
      simp only [unit, hc]
    · next ib_ne_c =>
-      have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
+      have hb' : hasAssignment b f.assignments[i.1] := by
        by_cases l.1 = i.1
        · next l_eq_i =>
          have b_eq_false : b = true := by
@@ -341,10 +335,10 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
            · assumption
            · next b_eq_false =>
              simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
-          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_true, hasPos_addNeg] at hb
+          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_true, hasPos_addNeg] at hb
          simp only [hasAssignment, b_eq_false, ite_true, hb]
        · next l_ne_i =>
-          simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+          simp only [Array.getElem_modify_of_ne l_ne_i] at hb
          exact hb
      specialize hf hb'
      simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -471,14 +465,14 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
      simp only [deleteOne, heq, hl] at hb
      by_cases l.1.1 = i.1
      · next l_eq_i =>
-        simp only [l_eq_i, Array.getElem_modify_self i_in_bounds] at hb
+        simp only [l_eq_i, Array.getElem_modify_self] at hb
        have l_ne_b : l.2 ≠ b := by
          intro l_eq_b
          rw [← l_eq_b] at hb
          have hb' := not_has_remove f.assignments[i.1] l.2
          simp [hb] at hb'
        replace l_ne_b := Bool.eq_not_of_ne l_ne_b
-        rw [l_ne_b] at hb
+        simp only [l_ne_b] at hb
        have hb := has_remove_irrelevant f.assignments[i.1] b hb
        specialize hf i b hb
        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@@ -502,7 +496,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
              have idx_in_bounds2 : idx < f.clauses.size := by
                conv => rhs; rw [Array.size_mk]
                exact hbound
-              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
              rw [hidx, hl] at heq
              simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
@@ -512,7 +506,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
          · exact hf
        · exact Or.inr hf
      · next l_ne_i =>
-        simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
+        simp only [Array.getElem_modify_of_ne l_ne_i] at hb
        specialize hf i b hb
        simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
          exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
@@ -535,7 +529,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
              have idx_in_bounds2 : idx < f.clauses.size := by
                conv => rhs; rw [Array.size_mk]
                exact hbound
-              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
              rw [hidx, hl] at heq
              simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
@@ -595,7 +589,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
              have idx_in_bounds2 : idx < f.clauses.size := by
                conv => rhs; rw [Array.size_mk]
                exact hbound
-              simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
+              simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
              rw [hidx] at heq
              simp only [Option.some.injEq] at heq
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -468,10 +468,10 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
  rcases List.get_of_mem h with ⟨j, h'⟩
  have j_in_bounds : j < ratHints.size := by
    have j_property := j.2
-    simp only [Array.map_toList, List.length_map] at j_property
+    simp only [Array.toList_map, List.length_map] at j_property
    dsimp at *
    omega
-  simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
+  simp only [List.get_eq_getElem, Array.toList_map, Array.length_toList, List.getElem_map] at h'
  rw [← Array.getElem_eq_getElem_toList] at h'
  rw [← Array.getElem_eq_getElem_toList] at c'_in_f
  exists ⟨j.1, j_in_bounds⟩
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -115,7 +115,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
        constructor
        · rfl
        · constructor
-          · rw [Array.getElem_modify_self l_in_bounds]
+          · rw [Array.getElem_modify_self]
            simp only [← i_eq_l, h1]
          · constructor
            · simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@@ -138,7 +138,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
      · next i_ne_l =>
        apply Or.inl
        simp only [insertUnit, h3, ite_false, reduceCtorEq]
-        rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)]
+        rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l)]
        constructor
        · exact h1
        · intro j
@@ -197,7 +197,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
              rfl
            · constructor
              · simp only [i_eq_l]
-                rw [Array.getElem_modify_self l_in_bounds]
+                rw [Array.getElem_modify_self]
                simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
                apply addNeg_addPos_eq_both
              · constructor
@@ -234,7 +234,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
            · rw [Array.get_push_lt units l j.1 j.2, h1]
            · constructor
              · simp only [i_eq_l]
-                rw [Array.getElem_modify_self l_in_bounds]
+                rw [Array.getElem_modify_self]
                simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
                apply addPos_addNeg_eq_both
              · constructor
@@ -277,7 +277,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
        constructor
        · rw [Array.get_push_lt units l j.1 j.2, h1]
        · constructor
-          · rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h2]
+          · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
          · constructor
            · exact h3
            · intro k k_ne_j
@@ -319,9 +319,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
            by_cases i.1 = l.1.1
            · next i_eq_l =>
              simp only [i_eq_l]
-              rw [Array.getElem_modify_self l_in_bounds]
+              rw [Array.getElem_modify_self]
              simp only [← i_eq_l, h3, add_both_eq_both]
-            · next i_ne_l => rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l), h3]
+            · next i_ne_l => rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h3]
        · constructor
          · exact h4
          · intro k k_ne_j1 k_ne_j2
@@ -535,7 +535,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
      have i_in_bounds : i.1 < assignments.size := by
        rw [hsize]
        exact i.2
-      have h := Array.getElem_modify_of_ne i_in_bounds (removeAssignment units[idx.val].2) ih2
+      have h := Array.getElem_modify_of_ne ih2 (removeAssignment units[idx.val].2) (by simpa using i_in_bounds)
      simp only [Fin.getElem_fin] at h
      rw [h]
      exact ih1
@@ -546,8 +546,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
      apply Or.inl
      constructor
      · simp only [clearUnit, idx_eq_j, Array.get_eq_getElem, ih1]
-        have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
-        rw [Array.getElem_modify_self i_in_bounds, ih2, remove_add_cancel]
+        rw [Array.getElem_modify_self, ih2, remove_add_cancel]
        exact ih3
      · intro k k_ge_idx_add_one
        have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one
@@ -568,8 +567,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
        · constructor
          · simp only [clearUnit, Array.get_eq_getElem]
            specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
-            have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
-            rw [Array.getElem_modify_of_ne i_in_bounds _ ih4]
+            rw [Array.getElem_modify_of_ne ih4]
            exact ih2
          · constructor
            · exact ih3
@@ -593,8 +591,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
          exact ih2
        · constructor
          · simp only [clearUnit, idx_eq_j1, Array.get_eq_getElem, ih1]
-            have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-            rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
+            rw [Array.getElem_modify_self, ih3, ih4]
            decide
          · constructor
            · simp [hasAssignment, hasNegAssignment, ih4]
@@ -630,8 +627,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
            exact ih1
          · constructor
            · simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2]
-              have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-              rw [Array.getElem_modify_self i_in_bounds, ih3, ih4]
+              rw [Array.getElem_modify_self, ih3, ih4]
              decide
            · constructor
              · simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true]
@@ -687,10 +683,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
                      simp only [Bool.not_eq_true] at h2
                      simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
                      exact h3 rfl
-                  have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by
-                    rw [hsize]; exact units[idx.1].1.2.2
-                  have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
-                  rw [Array.getElem_modify_of_ne i_in_bounds _ idx_res_ne_i]
+                  rw [Array.getElem_modify_of_ne idx_res_ne_i]
                  exact ih3
                · constructor
                  · exact ih4
@@ -796,7 +789,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
      constructor
      · simp only [List.get, l_eq_i]
      · constructor
-        · simp only [l_eq_i, Array.getElem_modify_self i_in_bounds, List.get, h1]
+        · simp only [l_eq_i, Array.getElem_modify_self, List.get, h1]
        · constructor
          · simp only [List.get, Bool.not_eq_true]
            simp only [getElem!, l_in_bounds, ↓reduceDIte, Array.get_eq_getElem,
@@ -826,7 +819,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
    · next l_ne_i =>
      apply Or.inl
      constructor
-      · rw [Array.getElem_modify_of_ne i_in_bounds (addAssignment l.2) l_ne_i]
+      · rw [Array.getElem_modify_of_ne l_ne_i]
        exact h1
      · intro l' l'_in_list
        simp only [List.find?, List.mem_cons] at l'_in_list
@@ -865,7 +858,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
            apply And.intro l_eq_true ∘ And.intro l'_eq_false
            constructor
            · simp only [l'] at l'_eq_false
-              simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
+              simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.getElem_modify_self, h1,
                l'_eq_false, ite_false]
              apply addPos_addNeg_eq_both
            · constructor
@@ -914,7 +907,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
            apply And.intro l'_eq_true ∘ And.intro l_eq_false
            constructor
            · simp only [l'] at l'_eq_true
-              simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self i_in_bounds, h1,
+              simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.getElem_modify_self, h1,
                l_eq_false, ite_false]
              apply addNeg_addPos_eq_both
            · constructor
@@ -950,7 +943,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
      constructor
      · exact j_eq_i
      · constructor
-        · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+        · rw [Array.getElem_modify_of_ne l_ne_i]
          exact h1
        · apply And.intro h2
          intro k k_ne_j_succ
@@ -1002,7 +995,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
      all_goals
        simp (config := {decide := true}) [getElem!, l_eq_i, i_in_bounds, h1, decidableGetElem?] at h
    constructor
-    · rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+    · rw [Array.getElem_modify_of_ne l_ne_i]
      exact h1
    · constructor
      · exact h2
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
@@ -39,27 +39,26 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
    rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
    · simp only [insertUnit, hl, ite_false]
      rcases h foundContradiction_eq_true with ⟨i, h⟩
-      have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
      apply Exists.intro i
      by_cases l.1.1 = i.1
      · next l_eq_i =>
-        simp [l_eq_i, Array.getElem_modify_self i_in_bounds, h]
+        simp [l_eq_i, Array.getElem_modify_self, h]
        exact add_both_eq_both l.2
      · next l_ne_i =>
-        simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
+        simp [Array.getElem_modify_of_ne l_ne_i]
        exact h
    · apply Exists.intro l.1
-      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq]
+      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq]
      simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
      by_cases l.2
      · next l_eq_true =>
-        rw [l_eq_true]
+        simp only [l_eq_true]
        simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
          Bool.not_eq_true, decidableGetElem?] at hl
        split at hl <;> simp_all (config := { decide := true })
      · next l_eq_false =>
        simp only [Bool.not_eq_true] at l_eq_false
-        rw [l_eq_false]
+        simp only [l_eq_false]
        simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, decidableGetElem?] at hl
        split at hl <;> simp_all (config := { decide := true })

@@ -681,7 +680,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
          by_cases l.1 = i.1
          · next l_eq_i =>
            simp only [getElem!, Array.size_modify, i_in_bounds, ↓ reduceDIte,
-              Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self i_in_bounds (addAssignment b), decidableGetElem?]
+              Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self (addAssignment b), decidableGetElem?]
            simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc
            by_cases pi : p i
            · simp only [pi, decide_False]
@@ -705,7 +704,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
                exact pacc
          · next l_ne_i =>
            simp only [getElem!, Array.size_modify, i_in_bounds,
-              Array.getElem_modify_of_ne i_in_bounds _ l_ne_i, dite_true,
+              Array.getElem_modify_of_ne l_ne_i, dite_true,
              Array.get_eq_getElem, decidableGetElem?]
            simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc
            exact pacc
--- a/tests/compiler/float.lean
+++ b/tests/compiler/float.lean
@@ -19,12 +19,29 @@ def tst1 : IO Unit := do
  IO.println (0 / 0 : Float).toUInt16
  IO.println (0 / 0 : Float).toUInt32
  IO.println (0 / 0 : Float).toUInt64
+  IO.println (0 / 0 : Float).toUSize
+
  IO.println (-1 : Float).toUInt8
  IO.println (256 : Float).toUInt8
  IO.println (1 / 0 : Float).toUInt8
+
+  IO.println (-1 : Float).toUInt16
+  IO.println (2^16 : Float).toUInt16
+  IO.println (1 / 0 : Float).toUInt16
+
+  IO.println (-1 : Float).toUInt32
+  IO.println (2^32 : Float).toUInt32
+  IO.println (1 / 0 : Float).toUInt32
+
  IO.println (-1 : Float).toUInt64
  IO.println (2^64 : Float).toUInt64
  IO.println (1 / 0 : Float).toUInt64
+
+  let platBits := USize.size.log2.toFloat
+  IO.println (-1 : Float).toUSize
+  IO.println ((2^platBits).toUSize.toNat == (USize.size - 1))
+  IO.println ((1 / 0 : Float).toUSize.toNat == (USize.size - 1))
+
  IO.println (let x : Float := 1.4; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
  IO.println (let x : Float := 0 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
  IO.println (let x : Float := -0 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
--- a/tests/compiler/float.lean.expected.out
+++ b/tests/compiler/float.lean.expected.out
@@ -18,11 +18,21 @@ true
 0
 0
 0
+0
 255
 255
 0
+65535
+65535
+0
+4294967295
+4294967295
+0
 18446744073709551615
 18446744073709551615
+0
+true
+true
 (1.400000, (false, (false, (true, (0.700000, 1)))))
 (NaN, (true, (false, (false, (NaN, 0)))))
 (NaN, (true, (false, (false, (NaN, 0)))))
--- a/tests/lean/run/2710.lean
+++ b/tests/lean/run/2710.lean
@@ -0,0 +1,8 @@
+/-!
+# Structure field default values can be noncomputable
+-/
+
+noncomputable def ohno := 1
+
+structure OhNo where
+  x := ohno
--- a/tests/lean/run/5424.lean
+++ b/tests/lean/run/5424.lean
@@ -0,0 +1,21 @@
+/-!
+# Long runs of identifiers should include line breaks
+-/
+
+set_option linter.unusedVariables false
+
+def foo (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20
+         a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 a32 a33 a34 a35 a36 a37 a38 a39 a40
+         a41 a42 a43 a44 a45 a46 a47 a48 a49 a50 a51 a52 a53 a54 a55 a56 a57 a58 a59 a60
+         a61 a62 a63 a64 a65 a66 a67 a68 a69 a70 a71 a72 a73 a74 a75 a76 a77 a78 a79 a80
+         a81 a82 a83 a84 a85 a86 a87 a88 a89 a90 a91 a92 a93 a94 a95 a96 a97 a98 a99 : Nat) : Nat := 0
+
+/--
+info: foo
+  (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31
+    a32 a33 a34 a35 a36 a37 a38 a39 a40 a41 a42 a43 a44 a45 a46 a47 a48 a49 a50 a51 a52 a53 a54 a55 a56 a57 a58 a59 a60
+    a61 a62 a63 a64 a65 a66 a67 a68 a69 a70 a71 a72 a73 a74 a75 a76 a77 a78 a79 a80 a81 a82 a83 a84 a85 a86 a87 a88 a89
+    a90 a91 a92 a93 a94 a95 a96 a97 a98 a99 : Nat) :
+  Nat
+-/
+#guard_msgs(whitespace := exact) in #check foo
--- a/tests/lean/run/eraseReps.lean
+++ b/tests/lean/run/eraseReps.lean
@@ -0,0 +1,2 @@
+example : Array.eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5] := rfl
+example : List.eraseReps   [1, 3, 2, 2, 2, 3, 5] =  [1, 3, 2, 3, 5] := rfl
--- a/tests/lean/run/list_simp.lean
+++ b/tests/lean/run/list_simp.lean
@@ -336,21 +336,21 @@ variable (h : n ≤ m) in
 -- unzip
 #check_simp unzip (replicate n (x, y)) ~> (replicate n x, replicate n y)

-- minimum?
+-- min?

 -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma
-#check_simp (replicate (n+1) 7).minimum? ~> some 7
+#check_simp (replicate (n+1) 7).min? ~> some 7

 variable (h : 0 < n) in
-#check_tactic (replicate n 7).minimum? ~> some 7 by simp [h]
+#check_tactic (replicate n 7).min? ~> some 7 by simp [h]

-- maximum?
+-- max?

 -- Note this relies on the fact that we do not have `replicate_succ` as a `@[simp]` lemma
-#check_simp (replicate (n+1) 7).maximum? ~> some 7
+#check_simp (replicate (n+1) 7).max? ~> some 7

 variable (h : 0 < n) in
-#check_tactic (replicate n 7).maximum? ~> some 7 by simp [h]
+#check_tactic (replicate n 7).max? ~> some 7 by simp [h]

 end

@@ -456,9 +456,9 @@ end Pairwise

 /-! ### enumFrom -/

-/-! ### minimum? -/
+/-! ### min? -/

-/-! ### maximum? -/
+/-! ### max? -/

 /-! ## Monadic operations -/

--- a/tests/lean/run/omega.lean
+++ b/tests/lean/run/omega.lean
@@ -458,6 +458,14 @@ example (a : Nat) :
    (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by
  omega

+/-! ### Int.toNat -/
+
+example (z : Int) : z.toNat = 0 ↔ z ≤ 0 := by
+  omega
+
+example (z : Int) (a : Fin z.toNat) (h : 0 ≤ z) : ↑↑a ≤ z := by
+  omega
+
 /-! ### BitVec -/
 open BitVec

--- a/tests/lean/run/simpHigherOrder.lean
+++ b/tests/lean/run/simpHigherOrder.lean
@@ -0,0 +1,69 @@
+/-!
+This test checks that simp is able to instantiate the parameter `g` below. It does not
+appear on the lhs of the rule, but solving `hf` fully determines it.
+-/
+
+theorem List.foldl_subtype (p : α → Prop) (l : List (Subtype p)) (f : β → Subtype p → β)
+  (g : β → α → β) (b : β)
+  (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
+    l.foldl f b = (l.map (·.val)).foldl g b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => simp [hf, ih]
+
+example (l : List Nat)  :
+  l.attach.foldl (fun acc t => max acc (t.val)) 0 = l.foldl (fun acc t => max acc t) 0 := by
+  simp [List.foldl_subtype]
+
+example (l : List Nat)  :
+  l.attach.foldl (fun acc ⟨t, _⟩ => max acc t) 0 = l.foldl (fun acc t => max acc t) 0 := by
+  simp [List.foldl_subtype]
+
+
+theorem foldr_to_sum (l : List Nat) (f : Nat → Nat → Nat) (g : Nat → Nat)
+  (h : ∀ acc x, f x acc = g x + acc) :
+  l.foldr f 0 = Nat.sum (l.map g) := by
+  rw [Nat.sum, List.foldr_map]
+  congr
+  funext x acc
+  apply h
+
+-- this works:
+example (l : List Nat) :
+  l.foldr (fun x a => x*x + a) 0 = Nat.sum (l.map (fun x => x * x)) := by
+  simp [foldr_to_sum]
+
+-- this does not, so such a pattern is still quite fragile
+
+/-- error: simp made no progress -/
+#guard_msgs in
+example (l : List Nat) :
+  l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
+  simp [foldr_to_sum]
+
+-- but with stronger simp normal forms, it would work:
+
+@[simp]
+theorem add_eq_add_cancel (a x y : Nat) : (a + x = y + a) ↔  (x = y) := by omega
+
+example (l : List Nat) :
+  l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
+  simp [foldr_to_sum]
+
+
+-- An example with zipWith
+
+theorem zipWith_ignores_right
+  (l₁ : List α) (l₂ : List β) (f : α → β → γ) (g : α → γ)
+  (h : ∀ a b, f a b = g a) :
+  List.zipWith f l₁ l₂ = List.map g (l₁.take l₂.length) := by
+  induction l₁ generalizing l₂ with
+  | nil => simp
+  | cons x xs ih =>
+    cases l₂
+    · simp
+    · simp [List.zipWith, h, ih]
+
+example (l₁ l₂ : List Nat) (hlen: l₁.length = l₂.length):
+  List.zipWith (fun x y => x*x) l₁ l₂ = l₁.map (fun x => x * x) := by
+  simp only [zipWith_ignores_right, hlen.symm, List.take_length]
Author	SHA1	Message	Date
Kim Morrison	822dc5ba3d	chore: fix Array.modify lemmas	2024-09-30 16:14:18 +10:00
Kim Morrison	56ba39d68a	chore: more monadic simp lemmas (#5522 )	2024-09-30 04:47:49 +00:00
Kim Morrison	1fca66b8c9	feat: Option.attach (#5532 )	2024-09-30 04:13:27 +00:00
Kim Morrison	36c29bee31	chore: fix name of Array.length_toList (#5526 )	2024-09-30 04:08:56 +00:00
Kyle Miller	cf14178929	fix: default values for structure fields can be noncomputable (#5531 ) Closes #2710	2024-09-30 04:02:24 +00:00
Kim Morrison	a4dfa83af5	chore: reduce use of deprecated lemmas in Array (#5527 )	2024-09-30 02:59:15 +00:00
Kim Morrison	c5fd652765	feat: support Int.toNat in omega (#5523 ) Trivial to add and works nicely.	2024-09-29 22:23:29 +00:00
Kim Morrison	4cd4bcc9be	chore: List simp fixes (#5521 )	2024-09-29 13:28:19 +00:00
Kim Morrison	7d26a1604f	chore: restore @[simp] on List.getElem_mem et al (#5520 )	2024-09-29 13:28:13 +00:00
Kim Morrison	3a46fd0fde	chore: unsimp BitVec.divRec_succ' (#5505 ) @bollu, it would be good to have confirmation from you, but presumably this was not meant to be `@[simp]`? It competes with `divRec_succ`, and has a terrible RHS.	2024-09-29 11:38:54 +00:00
TomasPuverle	994cfa4c74	doc: update documentation and tests for `toUIntX` functions (#5497 ) Update documentation on functions to reflect actual behavior. Add tests to ensure said behavior is as documented. Closes #5483	2024-09-29 08:11:04 +00:00
Joachim Breitner	cf3e7de143	feat: let simp apply rules with higher-order patterns (#5479 ) after this change, `simp` will be able to discharge side-goals that, after simplification, are of the form `∀ …, a = b` with `a =?= b`. Usually these side-goals are solved by simplification using `eq_self`, but that does not work when there are metavariables involved. This enables us to have rewrite rules like ``` theorem List.foldl_subtype (p : α → Prop) (l : List (Subtype p)) (f : β → Subtype p → β) (g : β → α → β) (b : β) (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) : l.foldl f b = (l.map (·.val)).foldl g b := by ``` where the parameter `g` does not appear on the lhs, but can be solved for using the `hf` equation. See `tests/lean/run/simpHigherOrder.lean` for more examples. The motivating use-case is that `simp` should be able to clean up the usual ``` l.attach.map (fun <x, _> => x) ``` idiom often seen in well-founded recursive functions with nested recursion. Care needs to be taken with adding such rules to the default simp set if the lhs is very general, and thus causes them to be tried everywhere. Performance impact of just this PR (no additional simp rules) on mathlib is unsuspicious: http://speed.lean-fro.org/mathlib4/compare/b5bc44c7-e53c-4b6c-9184-bbfea54c4f80/to/ae1d769b-2ff2-4894-940c-042d5a698353 I tried a few alternatives, e.g. letting `simp` apply `eq_self` without bumping the mvar depth, or just solve equalities directly, but that broke too much things, and adding code to the default discharger seemed simpler.	2024-09-29 07:26:48 +00:00
Kim Morrison	2ace579438	chore: upstream List.fold lemmas (#5519 )	2024-09-29 07:21:32 +00:00
Kyle Miller	40d6a6def0	fix: use breakable instead of unbreakable whitespace when formatting tokens (#5513 ) The formatter was using `tk ++ " "` to separate tokens from tokens they would merge with, but `" "` is not whitespace that could merge. This affected large binder lists, which wouldn't pretty print with any line breaks. Now they can be flowed across multiple lines. Closes #5424	2024-09-29 06:33:39 +00:00
Kim Morrison	d96b7a7d98	chore: rename List.maximum? to max? (#5518 ) More consistent with other API.	2024-09-29 06:23:24 +00:00
Kim Morrison	40e97bd566	chore: upstream Subarray.empty (#5516 )	2024-09-29 05:53:12 +00:00
Kim Morrison	3bd01de384	feat: upstream Array.qsortOrd (#5515 )	2024-09-29 05:50:25 +00:00
Kim Morrison	8835ab46ad	feat: Array.eraseReps (#5514 ) Just an `Array` version of `List.eraseReps`. These functions are for now outside of scope for verification, so there's just a simple `example` in the tests.	2024-09-29 05:44:14 +00:00