Stream: Coq users

Topic: is statement true?


view this post on Zulip zohaze (Jun 08 2022 at 11:35):

I have non empty list(n::t) and list_max (n::l)<>0 . I have hypothesis H:= list_max (n::l)<= n. list_max=n is possible but list_max<n is not possible. Is statement is correct ?

view this post on Zulip Pierre Castéran (Jun 08 2022 at 16:56):

For any n and l, you have n <= list_max (n :: l). From your hypothesis H, you infer n = list_max (n :: l) (by antisymmetry).

In your post, you wrote incorrect propositions like list_max<n (without any argument to list_max). We cannot be sure to answer such imprecise questions (it could have been list_max l < n).

view this post on Zulip zohaze (Jun 09 2022 at 13:53):

Sorry , list_max (n:: l) = n is possible but list_max (n::l) < n is not possible. I want to ask may i prove H:= list_max (n::l)<= n is wrong and it gives False. I want to use fact that for all a b n l , In a (n:: l) -> b <= list_max(n::l) -> list_max (n::l)<= n -> False.

view this post on Zulip Pierre Castéran (Jun 09 2022 at 14:40):

zohaze said:

Sorry , list_max (n:: l) = n is possible but list_max (n::l) < n is not possible. I want to ask may i prove H:= list_max (n::l)<= n is wrong and it gives False. I want to use fact that for all a b n l , In a (n:: l) -> b <= list_max(n::l) -> list_max (n::l)<= n -> False.

Take n=5and l=[3;2]. list_max (n::l)<= n holds. In your lemma, which role do aand b play ? As it is stated, you cannot prove it.

view this post on Zulip zohaze (Jun 09 2022 at 16:48):

a is the element whose presence in the list want to check .b is the any element which we take from list . n=first element of list. In above example l=[3;2] n=3 .Therefore list_max l=3 but 3<3 is not possible. Then why we cannot prove list_max (n::l)<= n -> False is false. Any element of list cannot be greater than list maximum value.


Last updated: Jan 28 2023 at 05:02 UTC