chore: adjust List.replicate simp lemmas (#4687)

src/Init/Data/List/TakeDrop.lean

@@ -383,6 +383,29 @@ theorem minimum?_eq_some_iff' {xs : List Nat} :
     (min_eq_or := fun _ _ => by omega)
     (le_min_iff := fun _ _ _ => by omega)
 
+-- 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
+    | none => a
+    | some m => min a m) := by
+  rw [minimum?_eq_some_iff']
+  split <;> rename_i h m
+  · simp_all
+  · rw [minimum?_eq_some_iff'] at m
+    obtain ⟨m, le⟩ := m
+    rw [Nat.min_def]
+    constructor
+    · split
+      · exact mem_cons_self a l
+      · exact mem_cons_of_mem a m
+    · intro b m
+      cases List.mem_cons.1 m with
+      | inl => split <;> omega
+      | inr h =>
+        specialize le b h
+        split <;> omega
+
 /-! ### maximum? -/
 
 -- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -393,4 +416,27 @@ theorem maximum?_eq_some_iff' {xs : List Nat} :
     (max_eq_or := fun _ _ => by omega)
     (max_le_iff := fun _ _ _ => by omega)
 
+-- 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
+    | none => a
+    | some m => max a m) := by
+  rw [maximum?_eq_some_iff']
+  split <;> rename_i h m
+  · simp_all
+  · rw [maximum?_eq_some_iff'] at m
+    obtain ⟨m, le⟩ := m
+    rw [Nat.max_def]
+    constructor
+    · split
+      · exact mem_cons_of_mem a m
+      · exact mem_cons_self a l
+    · intro b m
+      cases List.mem_cons.1 m with
+      | inl => split <;> omega
+      | inr h =>
+        specialize le b h
+        split <;> omega
+
 end List

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -12,3 +12,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.lean

@@ -0,0 +1,21 @@
+/-
+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 Lean.Meta.LitValues
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace List
+open Lean Meta Simp
+
+/-- Simplification procedure for `List.replicate` applied to a `Nat` literal. -/
+-- We don't always want `List.replicate_succ` as a `simp` lemma,
+-- so we use this `dsimproc` to unfold `List.replicate` applied to literals.
+builtin_dsimproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
+  let_expr replicate α n x ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
+  return .done <| (← mkListLit α (List.replicate n x))
+
+end List

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -438,19 +438,19 @@ private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fu
     return .continue e
 
 /--
-Auliliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
+Auxiliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
 This is the `dsimp` equivalent of the approach used at `visitApp`.
 Recall that we fold orphan raw Nat literals.
 -/
 private def doNotVisitOfNat : DSimproc := doNotVisit isOfNatNatLit ``OfNat.ofNat
 
 /--
-Auliliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms.
+Auxiliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms.
 -/
 private def doNotVisitOfScientific : DSimproc := doNotVisit isOfScientificLit ``OfScientific.ofScientific
 
 /--
-Auliliary `dsimproc` for not visiting `Char` literal subterms.
+Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
 private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
 

tests/lean/run/list_simp.lean

@@ -1,3 +1,5 @@
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
+
 open List
 
 variable {α : Type _}
@@ -120,6 +122,7 @@ variable (p : β → Option γ) in
 
 #check_simp replicate 0 x ~> []
 #check_simp replicate 1 x ~> [x]
+#check_simp replicate 5 x ~> [x, x, x, x, x]
 
 -- `∈` and `contains
 
@@ -316,6 +319,7 @@ variable (h : n ≤ m) in
 
 -- minimum?
 
+-- 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
 
 variable (h : 0 < n) in
@@ -323,6 +327,7 @@ variable (h : 0 < n) in
 
 -- maximum?
 
+-- 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
 
 variable (h : 0 < n) in