Stream: Coq users

Topic: contra statement ?


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)?

view this post on Zulip 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?

view this post on Zulip 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: Jan 29 2023 at 06:02 UTC