zohaze (Nov 07 2021 at 17:52): zohaze (Nov 07 2021 at 17:52):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?
Gaëtan Gilbert (Nov 07 2021 at 18:06):it can be equal
zohaze (Nov 08 2021 at 03:18):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.
Théo Winterhalter (Nov 08 2021 at 07:47):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.
zohaze (Nov 08 2021 at 17:52):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 ?
Théo Winterhalter (Nov 08 2021 at 19:02):Then I don't know what list_max is. Are you assuming your lists are sorted?
zohaze (Nov 09 2021 at 17:34):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: Oct 03 2023 at 20:01 UTC