zohaze (Nov 09 2021 at 15:01): zohaze (Nov 09 2021 at 15:01):I have these three hypothesis . These are contradictory statements, we can prove it ?
H1 : a > nth 0 l 0
H2 : max a (list_max l) <= a
Laurent Théry (Nov 12 2021 at 13:14):If I that a = 2 and l = 1 :: nil, we have both a > nth 0 l 0 and max a (list_max l) <= a
sara lee (Nov 13 2021 at 08:40):When we say list is not empty, then we should write a::l instead of writing l in the hypothesis?(which shows at least one element a is present in the list)
zohaze (Nov 13 2021 at 08:42):I forget to write H3: a <= max a (list_max l). From H2 & H3 it is clear that max a (list_max l) = a. Now it is possible to prove contradiction among two(H1 : a > nth 0 l 0 & H2 : max a (list_max l) <= a)?
Christian Doczkal (Nov 13 2021 at 12:09):Even with H3, if you have l = nil, then list_max l = 0 so for any a > 0, all three assumptions are true, and there is no contradiction. Do you also have l <> nil?
zohaze (Nov 14 2021 at 17:36):Yes,l have non empty list and max a (list_max l) <>0 . From S (length l) >0 we can derive length l >0 ? Would you like to answer sara's question also? Is there any problem if we say list is non empty then use l instead of a::l in the code?
Last updated: Apr 19 2024 at 09:01 UTC