zohaze (Jun 08 2022 at 11:35): 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 ?
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).
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.
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.
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: Oct 05 2023 at 02:01 UTC