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)?

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`

?

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: Jan 29 2023 at 06:02 UTC