Zulip Chat Archive

Stream: general

Topic: max/min of list


view this post on Zulip 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))

view this post on Zulip Johan Commelin (May 01 2018 at 10:11):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 02 2018 at 17:08):

aha


Last updated: May 18 2021 at 16:25 UTC