max/min of list

Stream: general

[Kenny Lau]

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]

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

[Chris Hughes]

@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]

aha