Stream: Coq users

Topic: Is wrong statement?


view this post on Zulip pianke (Jun 28 2022 at 05:07):

H1 : length (x :: l) > 0
n : (x <? S (list_max (x :: l) + m)) = true
H2 : list_max (x :: l) <= x

Is above contra statement? We can prove it false ? (l= list nat , x m are nat)

view this post on Zulip Pierre Castéran (Jun 28 2022 at 05:21):

No, your context is not contradictory. Take for instance x=3 and l=[3]. Note that H1and n aren't truly hypotheses (because they are provable for any xand l ).

view this post on Zulip pianke (Jun 29 2022 at 13:37):

You have given example in which one element present in the list. If I add H3 then it become contra statement?
H3 : nth 0 (a :: l) 0 > nth (S k2) (a :: l) 0

view this post on Zulip James Wood (Jun 29 2022 at 13:55):

H3 is x > nth k2 l 0 (assuming you meant x rather than a), so x=3; l=[2]; k2=0 should be an example. H2 says that x is the maximal element of x :: l (because it's as big as anything in the list, and also itself in the list), so saying that x is bigger than some other element in the list doesn't tell you that much.

view this post on Zulip James Wood (Jun 29 2022 at 14:02):

You could also have k2 be out of bounds, in which case the type of H3 simplifies to x > 0, which again doesn't tell you that much. That suggests that a hypothesis of the form _ > nth k2 l 0 should come with another hypothesis that k2 < length l.

view this post on Zulip pianke (Jun 29 2022 at 17:49):

I have k2< length l. Now x is at zero index then k2=0 is not possible.Because two indexes can not be same.Should i add hypothesis that two indexes are not same Or by default it consider that two indexed are not same. What more information i required to prove above is wrong?

view this post on Zulip pianke (Jun 30 2022 at 18:08):

Proof of above is possible?

view this post on Zulip James Wood (Jun 30 2022 at 20:25):

It's hard to know what's reasonable in your setting, but I guess the following would be contradictory:

list_max l <= x
nth i l 0 > x

(And it happens that you don't have to worry about i being out of bounds for this one, because 0 is not strictly greater than anything.)

You should eventually establish the standard characterisation of list_max, namely that list_max l is greater than or equal to everything in l, and that for any x greater than or equal to everything in l, x >= list_max l too. This probably goes a long way towards proving whatever you want to prove about list_max.


Last updated: Jan 31 2023 at 13:02 UTC