From 26590e97adf86f75a17393a6e7f6a7ce0bcee0cb Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Wed, 18 Aug 2021 18:52:46 +0000
Subject: [PATCH] feat(data/list/min_max): maximum is a fold, bounded prod
 (#8543)

Also provide the same lemmas for multiset.
---
 src/algebra/big_operators/order.lean | 10 ++++++
 src/data/list/basic.lean             | 11 +++++++
 src/data/list/min_max.lean           | 48 ++++++++++++++++++++++++++++
 src/data/multiset/basic.lean         |  8 +++++
 src/data/multiset/fold.lean          | 17 ++++++++++
 5 files changed, 94 insertions(+)

diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean
index febe9381bffc0..2cc7dd2b6bc0f 100644
--- a/src/algebra/big_operators/order.lean
+++ b/src/algebra/big_operators/order.lean
@@ -219,6 +219,16 @@ theorem mul_card_image_le_card {f : α → β} (s : finset α)
   n * (s.image f).card ≤ s.card :=
 mul_card_image_le_card_of_maps_to (λ x, mem_image_of_mem _) n hn
 
+@[to_additive]
+lemma prod_le_of_forall_le {α β : Type*} [ordered_comm_monoid β] (s : finset α) (f : α → β)
+  (n : β) (h : ∀ (x ∈ s), f x ≤ n) :
+  s.prod f ≤ n ^ s.card :=
+begin
+  refine (multiset.prod_le_of_forall_le (s.val.map f) n _).trans _,
+  { simpa using h },
+  { simpa }
+end
+
 end pigeonhole
 
 section canonically_ordered_monoid
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 1b05761995639..6d4ce5097e77e 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -2657,6 +2657,17 @@ begin
     exact lt_of_add_lt_add_left (lt_of_le_of_lt h $ add_lt_add_right (lt_of_not_ge h') _) }
 end
 
+@[to_additive]
+lemma prod_le_of_forall_le [ordered_comm_monoid α] (l : list α) (n : α) (h : ∀ (x ∈ l), x ≤ n) :
+  l.prod ≤ n ^ l.length :=
+begin
+  induction l with y l IH,
+  { simp },
+  { specialize IH (λ x hx, h x (mem_cons_of_mem _ hx)),
+    have hy : y ≤ n := h y (mem_cons_self _ _),
+    simpa [pow_succ] using mul_le_mul' hy IH }
+end
+
 -- Several lemmas about sum/head/tail for `list ℕ`.
 -- These are hard to generalize well, as they rely on the fact that `default ℕ = 0`.
 
diff --git a/src/data/list/min_max.lean b/src/data/list/min_max.lean
index ef7c049fe774f..aa32f32936993 100644
--- a/src/data/list/min_max.lean
+++ b/src/data/list/min_max.lean
@@ -271,4 +271,52 @@ theorem minimum_eq_coe_iff {m : α} {l : list α} :
   minimum l = m ↔ m ∈ l ∧ (∀ a ∈ l, m ≤ a) :=
 @maximum_eq_coe_iff (order_dual α) _ _ _
 
+section fold
+
+variables {M : Type*} [canonically_linear_ordered_add_monoid M]
+
+/-! Note: since there is no typeclass for both `linear_order` and `has_top`, nor a typeclass dual
+to `canonically_linear_ordered_add_monoid α` we cannot express these lemmas generally for
+`minimum`; instead we are limited to doing so on `order_dual α`. -/
+
+lemma maximum_eq_coe_foldr_max_of_ne_nil (l : list M) (h : l ≠ []) :
+  l.maximum = (l.foldr max ⊥ : M) :=
+begin
+  induction l with hd tl IH,
+  { contradiction },
+  { rw [maximum_cons, foldr, with_bot.coe_max],
+    by_cases h : tl = [],
+    { simp [h, -with_top.coe_zero] },
+    { simp [IH h] } }
+end
+
+lemma minimum_eq_coe_foldr_min_of_ne_nil (l : list (order_dual M)) (h : l ≠ []) :
+  l.minimum = (l.foldr min ⊤ : order_dual M) :=
+maximum_eq_coe_foldr_max_of_ne_nil l h
+
+lemma maximum_nat_eq_coe_foldr_max_of_ne_nil (l : list ℕ) (h : l ≠ []) :
+  l.maximum = (l.foldr max 0 : ℕ) :=
+maximum_eq_coe_foldr_max_of_ne_nil l h
+
+lemma max_le_of_forall_le (l : list M) (n : M) (h : ∀ (x ∈ l), x ≤ n) :
+  l.foldr max ⊥ ≤ n :=
+begin
+  induction l with y l IH,
+  { simp },
+  { specialize IH (λ x hx, h x (mem_cons_of_mem _ hx)),
+    have hy : y ≤ n := h y (mem_cons_self _ _),
+    simpa [hy] using IH }
+end
+
+lemma le_min_of_le_forall (l : list (order_dual M)) (n : (order_dual M))
+  (h : ∀ (x ∈ l), n ≤ x) :
+  n ≤ l.foldr min ⊤ :=
+max_le_of_forall_le l n h
+
+lemma max_nat_le_of_forall_le (l : list ℕ) (n : ℕ) (h : ∀ (x ∈ l), x ≤ n) :
+  l.foldr max 0 ≤ n :=
+max_le_of_forall_le l n h
+
+end fold
+
 end list
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
index fb901e765ede1..1945b15130836 100644
--- a/src/data/multiset/basic.lean
+++ b/src/data/multiset/basic.lean
@@ -985,6 +985,14 @@ lemma single_le_prod [ordered_comm_monoid α] {m : multiset α} :
   (∀ x ∈ m, (1 : α) ≤ x) → ∀ x ∈ m, x ≤ m.prod :=
 quotient.induction_on m $ λ l hl x hx, by simpa using list.single_le_prod hl x hx
 
+@[to_additive]
+lemma prod_le_of_forall_le [ordered_comm_monoid α] (l : multiset α) (n : α) (h : ∀ (x ∈ l), x ≤ n) :
+  l.prod ≤ n ^ l.card :=
+begin
+  induction l using quotient.induction_on,
+  simpa using list.prod_le_of_forall_le _ _ h
+end
+
 @[to_additive all_zero_of_le_zero_le_of_sum_eq_zero]
 lemma all_one_of_le_one_le_of_prod_eq_one [ordered_comm_monoid α] {m : multiset α} :
   (∀ x ∈ m, (1 : α) ≤ x) → m.prod = 1 → (∀ x ∈ m, x = (1 : α)) :=
diff --git a/src/data/multiset/fold.lean b/src/data/multiset/fold.lean
index 5a9261828485f..fdd74592c4d0a 100644
--- a/src/data/multiset/fold.lean
+++ b/src/data/multiset/fold.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.multiset.erase_dup
+import data.list.min_max
 
 /-!
 # The fold operation for a commutative associative operation over a multiset.
@@ -80,6 +81,22 @@ end
 
 end fold
 
+section order
+
+lemma max_le_of_forall_le {α : Type*} [canonically_linear_ordered_add_monoid α]
+  (l : multiset α) (n : α) (h : ∀ (x ∈ l), x ≤ n) :
+  l.fold max ⊥ ≤ n :=
+begin
+  induction l using quotient.induction_on,
+  simpa using list.max_le_of_forall_le _ _ h
+end
+
+lemma max_nat_le_of_forall_le (l : multiset ℕ) (n : ℕ) (h : ∀ (x ∈ l), x ≤ n) :
+  l.fold max 0 ≤ n :=
+max_le_of_forall_le l n h
+
+end order
+
 open nat
 
 theorem le_smul_erase_dup [decidable_eq α] (s : multiset α) :