sara lee (Jul 30 2022 at 07:17): 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?
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 := []).
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: Oct 13 2024 at 01:02 UTC