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 ?

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`

).

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.

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=5`

and `l=[3;2]`

. `list_max (n::l)<= n`

holds. In your lemma, which role do `a`

and `b`

play ? As it is stated, you cannot prove it.

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