pianke (Jun 28 2022 at 05:07): 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)
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 ).
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
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.
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.
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?
pianke (Jun 30 2022 at 18:08):Proof of above is possible?
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: Oct 13 2024 at 01:02 UTC