## Stream: general

### Topic: max/min of list

#### Kenny Lau (May 01 2018 at 10:09):

maybe you'll find this useful:

def list.max : α :=
list.foldr max (inhabited.default _) L

def list.min : α :=
list.foldr min (inhabited.default _) L

theorem list.le_max : ∀ x ∈ L, x ≤ L.max :=
list.rec_on L (λ _, false.elim) $λ hd tl ih x hx, or.cases_on hx (assume H : x = hd, H.symm ▸ le_max_left hd tl.max) (assume H : x ∈ tl, le_trans (ih x H) (le_max_right hd tl.max)) theorem list.min_le : ∀ x ∈ L, L.min ≤ x := list.rec_on L (λ _, false.elim)$ λ hd tl ih x hx,
or.cases_on hx
(assume H : x = hd, H.symm ▸ min_le_left hd tl.min)
(assume H : x ∈ tl, le_trans (min_le_right hd tl.min) (ih x H))


#### Johan Commelin (May 01 2018 at 10:11):

I'll take look. First it's lunch time...

#### Chris Hughes (May 02 2018 at 17:06):

@Kenny Lau That doesn't take the max, it takes the max of the list and the default value. You won't be able to prove L.max \in L You should define it as default for nil, and then list.foldr max L.head otherwise.

#### Kenny Lau (May 02 2018 at 17:08):

aha

Last updated: Aug 03 2023 at 10:10 UTC