chore: induction-friendly List.min?_cons

src/Init/Data/List/MinMax.lean

@@ -20,20 +20,28 @@ open Nat
 
 @[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
 
--- We don't put `@[simp]` on `min?_cons`,
+-- We don't put `@[simp]` on `min?_cons'`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem min?_cons [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
+theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
+
+@[simp] theorem min?_cons [Min α] [Std.Associative (min : α → α → α)] {xs : List α} :
+    (x :: xs).min? = some (xs.min?.elim x (min x)) := by
+  cases xs <;> simp [min?_cons', foldl_assoc]
 
 @[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = [] := by
   cases xs <;> simp [min?]
 
+theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a ∈ l) :
+    l.min?.isSome := by
+  cases l <;> simp_all [List.min?_cons']
+
 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 [min?_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 =>
@@ -85,7 +93,7 @@ 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, min?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons']
 
 @[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
@@ -95,13 +103,21 @@ theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
 
 @[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
 
--- We don't put `@[simp]` on `max?_cons`,
+-- We don't put `@[simp]` on `max?_cons'`,
 -- because the definition in terms of `foldl` is not useful for proofs.
-theorem max?_cons [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
+theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
+
+@[simp] theorem max?_cons [Max α] [Std.Associative (max : α → α → α)] {xs : List α} :
+    (x :: xs).max? = some (xs.max?.elim x (max x)) := by
+  cases xs <;> simp [max?_cons', foldl_assoc]
 
 @[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = [] := by
   cases xs <;> simp [max?]
 
+theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a ∈ l) :
+    l.max?.isSome := by
+  cases l <;> simp_all [List.max?_cons']
+
 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
@@ -144,7 +160,7 @@ 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, max?_cons]
+  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons']
 
 @[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

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

@@ -96,75 +96,22 @@ theorem min?_eq_some_iff' {xs : List Nat} :
     (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 min?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).min? = some (match l.min? with
-    | none => a
-    | some m => min a m) := by
-  rw [min?_eq_some_iff']
-  split <;> rename_i h m
-  · simp_all
-  · rw [min?_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
-
-theorem foldl_min
-    {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
-    {l : List α} {a : α} :
-    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 [min?]
-    induction l generalizing a b with
-    | nil => simp
-    | cons c l ih => simp [ih, Std.Associative.assoc]
-
-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).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
-  induction l generalizing a with
-  | nil => simp
-  | cons c l ih =>
-    simp only [foldl_cons]
-    exact Nat.le_trans ih (Nat.min_le_left _ _)
-
-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 min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
-    l.min?.getD k ≤ a := by
-  cases l with
+theorem min?_get_le_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
+    l.min?.get (isSome_min?_of_mem h) ≤ a := by
+  induction l with
   | nil => simp at h
-  | cons b l =>
-    simp [min?_cons]
-    simp at h
-    rcases h with (rfl | h)
-    · exact foldl_min_le
-    · induction l generalizing b with
-      | nil => simp_all
-      | cons c l ih =>
-        simp only [foldl_cons]
-        simp at h
-        rcases h with (rfl | h)
-        · exact foldl_min_min_of_le (Nat.min_le_right _ _)
-        · exact ih _ h
+  | cons b t ih =>
+    simp only [min?_cons, Option.get_some] at ih ⊢
+    rcases mem_cons.1 h with (rfl|h)
+    · cases t.min? with
+      | none => simp
+      | some b => simpa using Nat.min_le_left _ _
+    · obtain ⟨q, hq⟩ := Option.isSome_iff_exists.1 (isSome_min?_of_mem h)
+      simp only [hq, Option.elim_some] at ih ⊢
+      exact Nat.le_trans (Nat.min_le_right _ _) (ih h)
+
+theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : l.min?.getD k ≤ a :=
+  Option.get_eq_getD _ ▸ min?_get_le_of_mem h
 
 /-! ### max? -/
 
@@ -176,75 +123,23 @@ theorem max?_eq_some_iff' {xs : List Nat} :
     (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 max?_cons' {a : Nat} {l : List Nat} :
-    (a :: l).max? = some (match l.max? with
-    | none => a
-    | some m => max a m) := by
-  rw [max?_eq_some_iff']
-  split <;> rename_i h m
-  · simp_all
-  · rw [max?_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
-
-theorem foldl_max
-    {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
-    {l : List α} {a : α} :
-    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 [max?]
-    induction l generalizing a b with
-    | nil => simp
-    | cons c l ih => simp [ih, Std.Associative.assoc]
-
-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).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
-  induction l generalizing a with
-  | nil => simp
-  | cons c l ih =>
-    simp only [foldl_cons]
-    exact Nat.le_trans (Nat.le_max_left _ _) ih
-
-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_max?_get_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
+    a ≤ l.max?.get (isSome_max?_of_mem h) := by
+  induction l with
+  | nil => simp at h
+  | cons b t ih =>
+    simp only [max?_cons, Option.get_some] at ih ⊢
+    rcases mem_cons.1 h with (rfl|h)
+    · cases t.max? with
+      | none => simp
+      | some b => simpa using Nat.le_max_left _ _
+    · obtain ⟨q, hq⟩ := Option.isSome_iff_exists.1 (isSome_max?_of_mem h)
+      simp only [hq, Option.elim_some] at ih ⊢
+      exact Nat.le_trans (ih h) (Nat.le_max_right _ _)
 
 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 [max?_cons]
-    simp at h
-    rcases h with (rfl | h)
-    · exact le_foldl_max
-    · induction l generalizing b with
-      | nil => simp_all
-      | cons c l ih =>
-        simp only [foldl_cons]
-        simp at h
-        rcases h with (rfl | h)
-        · exact le_foldl_max_of_le (Nat.le_max_right b a)
-        · exact ih _ h
+    a ≤ l.max?.getD k :=
+  Option.get_eq_getD _ ▸ le_max?_get_of_mem 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'