merge

src/Init/Data/List/Attach.lean

@@ -328,7 +328,7 @@ Unfortunately this can't be applied by `simp` because of the higher order unific
 and even when rewriting we need to specify the function explicitly.
 -/
 theorem foldl_attach (l : List α) (f : β → α → β) (b : β) :
-    l.attach.foldl (fun acc t => f acc t.val) b = l.foldl (fun acc a => f acc a) b := by
+    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
   induction l generalizing b with
   | nil => simp
   | cons a l ih => rw [foldl_cons, attach_cons, foldl_cons, foldl_map, ih]
@@ -343,7 +343,7 @@ Unfortunately this can't be applied by `simp` because of the higher order unific
 and even when rewriting we need to specify the function explicitly.
 -/
 theorem foldr_attach (l : List α) (f : α → β → β) (b : β) :
-    l.attach.foldr (fun t acc => f t.val acc) b = l.foldr (fun a acc => f a acc) b := by
+    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
   induction l generalizing b with
   | nil => simp
   | cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]

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

@@ -119,6 +119,53 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
         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.minimum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [minimum?]
+    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).minimum?.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 minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.minimum?.getD k ≤ a := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [minimum?_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
+
 /-! ### maximum? -/
 
 -- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -152,4 +199,51 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
         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.maximum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [maximum?]
+    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).maximum?.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_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.maximum?.getD k := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [maximum?_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
+
 end List