Stream: Coq users

Topic: contra statement ?

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: May 19 2024 at 16:02 UTC