Stream: Coq users

Topic: compare two value


view this post on Zulip pianke (Jun 08 2022 at 11:18):

I have a list of natural numbers (b::l) and want to compare two values at two different indexes. Only available information is that both indexes are less than length l. How i should proceed? To find length of list might be helpful? Secondly, what more information i should have to perform comparision?

view this post on Zulip Li-yao (Jun 08 2022 at 12:17):

You can use the nth function to get the two values.

view this post on Zulip pianke (Jun 09 2022 at 14:09):

I am also using nth function. I have two indexes k1 k2 both are less than length l. maximum of list is not equal zero. Want to prove nth 0 l d > nth (S k2) l d . How i can prove this? What more hypothesis i should add?

view this post on Zulip Julin S (Jun 10 2022 at 06:10):

If you've already got that theorem stated in Coq, it might make the question clearer if you include it here as well.


Last updated: Jan 31 2023 at 14:03 UTC