Stream: Coq users

Topic: Is wrong statement ?


view this post on Zulip sara lee (Jul 30 2022 at 07:17):

Lemma m_c0  c0  l  :
list_max (c0 :: l) <= c0 -> False.

Lemma max_value k l: In k l -> k <= list_max l. This lemma may be helpful in proving above?

view this post on Zulip James Wood (Aug 03 2022 at 08:29):

You can prove list_max (c0 :: l) < c0 -> False, but with <= there are many counterexamples (take l := []).

view this post on Zulip James Wood (Aug 03 2022 at 08:34):

I think you would prove the < version by showing c0 <= list_max (c0 :: l) and then using some standard lemma to turn <= into >. Indeed, max_value (or_introl eq_refl) should be enough.


Last updated: Jan 28 2023 at 07:30 UTC