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)
No, your context is not contradictory. Take for instance
l=. Note that
n aren't truly hypotheses (because they are provable for any
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
x > nth k2 l 0 (assuming you meant
x rather than
x=3; l=; 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.
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.
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?
Proof of above is possible?
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
x >= list_max l too. This probably goes a long way towards proving whatever you want to prove about
Last updated: Jan 31 2023 at 13:02 UTC