I have hypothesis list_max l<= nth 0 l 0 . Maximum value cannot less than any value of the list. Therefore it is false. Is there any situation where above relation can be true ? If length of l is 1 , then we can prove above is true?

it can be equal

I want to ask under what condition it can be equal? when one element exist in the list? How I can prove this?

forall a l : In a l -> a>=list_max l can be helpful in this case.

When is the maximum of a list smaller or equal to the first element in the list? It will never be strictly smaller as it is the maximum, but it can be equal as Gaëtan said. It could be that the first element of the list is also the greatest.

Thank you. It means maximum value of the list is present at the head of the list. It is not necessary that single element present in the list.More than one elements may exist in the list but all values are smaller than value present at head. From " list_max l<= nth 0 l 0 " we can prove that list_max l= nth 0 l 0 remaining elements are less than list_max l ?

Then I don't know what `list_max`

is. Are you assuming your lists are sorted?

list_max l function finds the greatest value of the list. No, I have not sorted the list. What ever the position of maximum value is

in the list.It is found by list_max function. Therefore I have two case maximum value at head or any where in the list.

Last updated: Jan 27 2023 at 01:03 UTC