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
If I that
a = 2 and
l = 1 :: nil, we have both
a > nth 0 l 0 and
max a (list_max l) <= a
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)
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)?
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?
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: Dec 07 2023 at 06:38 UTC