Skip to content

Commit c9ed7ae

Browse files
ecyrbeecyrbe
committed
feat: add min and max list operations
1 parent 3e86729 commit c9ed7ae

File tree

5 files changed

+204
-2
lines changed

5 files changed

+204
-2
lines changed

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2086,6 +2086,18 @@ def min? [Min α] : List α → Option α
20862086
| [] => none
20872087
| a::as => some <| as.foldl min a
20882088

2089+
/-! ### min -/
2090+
2091+
/--
2092+
Returns the smallest element of a non empty list.
2093+
2094+
Examples:
2095+
* `[4].min (by decide) = 4`
2096+
* `[1, 4, 2, 10, 6].min (by decide) = 1`
2097+
-/
2098+
protected def min [Min α] : (l: List α) → (h: l ≠ []) → α
2099+
| a::as, _ => as.foldl min a
2100+
20892101
/-! ### max? -/
20902102

20912103
/--
@@ -2100,6 +2112,17 @@ def max? [Max α] : List α → Option α
21002112
| [] => none
21012113
| a::as => some <| as.foldl max a
21022114

2115+
/-! ### max -/
2116+
2117+
/--
2118+
Returns the largest element of a non empty list.
2119+
Examples:
2120+
* `[4].max (by decide) = 4`
2121+
* `[1, 4, 2, 10, 6].max (by decide) = 10`
2122+
-/
2123+
protected def max [Max α] : (l: List α) → (h: l ≠ []) → α
2124+
| a::as, _ => as.foldl max a
2125+
21032126
/-! ## Other list operations
21042127
21052128
The functions are currently mostly used in meta code,

‎src/Init/Data/List/Impl.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ The following operations are still missing `@[csimp]` replacements:
3838
The following operations are not recursive to begin with
3939
(or are defined in terms of recursive primitives):
4040
`isEmpty`, `isSuffixOf`, `isSuffixOf?`, `rotateLeft`, `rotateRight`, `insert`, `zip`, `enum`,
41-
`min?`, `max?`, and `removeAll`.
41+
`min?`, `max?`, `min`, `max` and `removeAll`.
4242
4343
The following operations were already given `@[csimp]` replacements in `Init/Data/List/Basic.lean`:
4444
`length`, `map`, `filter`, `replicate`, `leftPad`, `unzip`, `range'`, `iota`, `intersperse`.

‎src/Init/Data/List/Lemmas.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ See also
6060
* `Init.Data.List.Erase` for lemmas about `List.eraseP` and `List.erase`.
6161
* `Init.Data.List.Find` for lemmas about `List.find?`, `List.findSome?`, `List.findIdx`,
6262
`List.findIdx?`, and `List.indexOf`
63-
* `Init.Data.List.MinMax` for lemmas about `List.min?` and `List.max?`.
63+
* `Init.Data.List.MinMax` for lemmas about `List.min?`, `List.min`, `List.max?` and `List.max`.
6464
* `Init.Data.List.Pairwise` for lemmas about `List.Pairwise` and `List.Nodup`.
6565
* `Init.Data.List.Sublist` for lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`,
6666
`List.IsSuffix`, and `List.IsInfix`.

‎src/Init/Data/List/MinMax.lean‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,51 @@ theorem foldl_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Asso
155155
{l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a) := by
156156
cases l <;> simp [min?, foldl_assoc, Std.IdempotentOp.idempotent]
157157

158+
/-! ### min -/
159+
160+
theorem min?_eq_some_min [Min α] : {l : List α} → (hl : l ≠ []) →
161+
l.min? = some (l.min hl)
162+
| a::as, _ => by simp [List.min, List.min?_cons']
163+
164+
theorem min_eq_head {α : Type u} [Min α] {l : List α}
165+
(hl : l ≠ [])
166+
(h : l.Pairwise (fun a b => min a b = a)) : l.min hl = l.head hl := by
167+
apply Option.some.inj
168+
rw [← min?_eq_some_min, ←head?_eq_some_head]
169+
exact min?_eq_head? h
170+
171+
theorem min_mem [Min α] [MinEqOr α] {l : List α} {hl : l ≠ []} :
172+
l.min hl ∈ l := by
173+
exact min?_mem (min?_eq_some_min hl)
174+
175+
protected theorem le_min_iff [Min α] [LE α] [LawfulOrderInf α]
176+
{l : List α} {hl : l ≠ []} : ∀ {x}, x ≤ l.min hl ↔ ∀ b, b ∈ l → x ≤ b := by
177+
exact le_min?_iff (min?_eq_some_min hl)
178+
179+
theorem min_iff [Min α] [LE α] {l : List α} [IsLinearOrder α] [LawfulOrderMin α] {hl : l ≠ []} :
180+
l.min hl = a ↔ a ∈ l ∧ ∀ b, b ∈ l → a ≤ b := by
181+
simpa [min?_eq_some_min hl] using (min?_eq_some_iff (xs := l))
182+
183+
theorem min_eq_min_attach [Min α] [MinEqOr α] {l : List α} {hl : l ≠ []} :
184+
l.min hl = Subtype.val (l.attach.min (List.attach_ne_nil_iff.mpr hl)) := by
185+
simpa [min?_eq_some_min hl, min?_eq_some_min (List.attach_ne_nil_iff.mpr hl)]
186+
using (min?_eq_min?_attach (xs := l))
187+
188+
theorem min_iff_subtype [Min α] [LE α] {l : List α} {hl : l ≠ []}
189+
[MinEqOr α] [IsLinearOrder (Subtype (· ∈ l))] [LawfulOrderMin (Subtype (· ∈ l))] :
190+
l.min hl = a ↔ a ∈ l ∧ ∀ b, b ∈ l → a ≤ b := by
191+
simpa [min?_eq_some_min hl] using (min?_eq_some_iff_subtype (xs := l))
192+
193+
theorem min_replicate [Min α] [MinEqOr α] {n : Nat} {a : α} (h: replicate n a ≠ []) :
194+
(replicate n a).min h = a := by
195+
have n_pos : 0 < n := Nat.pos_of_ne_zero (fun hn => by simp [hn] at h)
196+
simpa [min?_eq_some_min h] using (min?_replicate_of_pos (a:=a) n_pos)
197+
198+
theorem foldl_min_eq_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
199+
{l : List α} {hl : l ≠ []} {a : α}:
200+
l.foldl min a = min a (l.min hl) := by
201+
simpa [min?_eq_some_min hl] using foldl_min (l := l)
202+
158203
/-! ### max? -/
159204

160205
@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
@@ -296,4 +341,49 @@ theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Asso
296341
{l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a) := by
297342
cases l <;> simp [max?, foldl_assoc, Std.IdempotentOp.idempotent]
298343

344+
/-! ### max -/
345+
346+
theorem max?_eq_some_max [Max α] : {l : List α} → (hl : l ≠ []) →
347+
l.max? = some (l.max hl)
348+
| a::as, _ => by simp [List.max, List.max?_cons']
349+
350+
theorem max_eq_head {α : Type u} [Max α] {l : List α}
351+
(hl : l ≠ [])
352+
(h : l.Pairwise (fun a b => max a b = a)) : l.max hl = l.head hl := by
353+
apply Option.some.inj
354+
rw [← max?_eq_some_max, ←head?_eq_some_head]
355+
exact max?_eq_head? h
356+
357+
theorem max_mem [Max α] [MaxEqOr α] {l : List α} {hl : l ≠ []} :
358+
l.max hl ∈ l := by
359+
exact max?_mem (max?_eq_some_max hl)
360+
361+
protected theorem max_le_iff [Max α] [LE α] [LawfulOrderSup α]
362+
{l : List α} {hl : l ≠ []} : ∀ {x}, l.max hl ≤ x ↔ ∀ b, b ∈ l → b ≤ x := by
363+
exact max?_le_iff (max?_eq_some_max hl)
364+
365+
theorem max_iff [Max α] [LE α] {l : List α} [IsLinearOrder α] [LawfulOrderMax α] {hl : l ≠ []} :
366+
l.max hl = a ↔ a ∈ l ∧ ∀ b, b ∈ l → b ≤ a := by
367+
simpa [max?_eq_some_max hl] using (max?_eq_some_iff (xs := l))
368+
369+
theorem max_eq_max_attach [Max α] [MaxEqOr α] {l : List α} {hl : l ≠ []} :
370+
l.max hl = Subtype.val (l.attach.max (List.attach_ne_nil_iff.mpr hl)) := by
371+
simpa [max?_eq_some_max hl, max?_eq_some_max (List.attach_ne_nil_iff.mpr hl)]
372+
using (max?_eq_max?_attach (xs := l))
373+
374+
theorem max_iff_subtype [Max α] [LE α] {l : List α} {hl : l ≠ []}
375+
[MaxEqOr α] [IsLinearOrder (Subtype (· ∈ l))] [LawfulOrderMax (Subtype (· ∈ l))] :
376+
l.max hl = a ↔ a ∈ l ∧ ∀ b, b ∈ l → b ≤ a := by
377+
simpa [max?_eq_some_max hl] using (max?_eq_some_iff_subtype (xs := l))
378+
379+
theorem max_replicate [Max α] [MaxEqOr α] {n : Nat} {a : α} (h: replicate n a ≠ []) :
380+
(replicate n a).max h = a := by
381+
have n_pos : 0 < n := Nat.pos_of_ne_zero (fun hn => by simp [hn] at h)
382+
simpa [max?_eq_some_max h] using (max?_replicate_of_pos (a:=a) n_pos)
383+
384+
theorem foldl_max_eq_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
385+
{l : List α} {hl : l ≠ []} {a : α}:
386+
l.foldl max a = max a (l.max hl) := by
387+
simpa [max?_eq_some_max hl] using foldl_max (l := l)
388+
299389
end List

‎tests/lean/run/list_minmax.lean‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
/-! ### min? -/
2+
3+
/--
4+
info: none
5+
-/
6+
#guard_msgs(info) in #eval ([]: List Nat).min?
7+
8+
/--
9+
info: some 1
10+
-/
11+
#guard_msgs(info) in #eval [1].min?
12+
13+
/--
14+
info: some 1
15+
-/
16+
#guard_msgs(info) in #eval [1, 4, 2, 10, 6].min?
17+
18+
/--
19+
info: some (-10)
20+
-/
21+
#guard_msgs(info) in #eval [-1, -4, -2, -10, -6].min?
22+
23+
/-! ### min -/
24+
25+
/--
26+
error: unsolved goals
27+
⊢ False
28+
-/
29+
#guard_msgs(error) in #eval [].min (by simp)
30+
31+
/--
32+
info: 1
33+
-/
34+
#guard_msgs(info) in #eval [1].min (by decide)
35+
36+
/--
37+
info: 1
38+
-/
39+
#guard_msgs(info) in #eval [1, 4, 2, 10, 6].min (by decide)
40+
41+
/--
42+
info: -10
43+
-/
44+
#guard_msgs(info) in #eval [-1, -4, -2, -10, -6].min (by decide)
45+
46+
/-! ### max? -/
47+
48+
/--
49+
info: none
50+
-/
51+
#guard_msgs(info) in #eval ([]: List Nat).max?
52+
53+
/--
54+
info: some 4
55+
-/
56+
#guard_msgs(info) in #eval [4].max?
57+
58+
/--
59+
info: some 10
60+
-/
61+
#guard_msgs(info) in #eval [1, 4, 2, 10, 6].max?
62+
63+
/--
64+
info: some (-1)
65+
-/
66+
#guard_msgs(info) in #eval [-1, -4, -2, -10, -6].max?
67+
68+
/-! ### max -/
69+
70+
/--
71+
error: unsolved goals
72+
⊢ False
73+
-/
74+
#guard_msgs(error) in #eval [].max (by simp)
75+
76+
/--
77+
info: 4
78+
-/
79+
#guard_msgs(info) in #eval [4].max (by decide)
80+
81+
/--
82+
info: 10
83+
-/
84+
#guard_msgs(info) in #eval [1, 4, 2, 10, 6].max (by decide)
85+
86+
/--
87+
info: -1
88+
-/
89+
#guard_msgs(info) in #eval [-1, -4, -2, -10, -6].max (by decide)

0 commit comments

Comments
 (0)