## Stream: Coq users

### Topic: is statement true?

#### 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=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.

#### 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: Jun 15 2024 at 05:01 UTC