I have two contra statements in hypothesis length l=1 and nth a1 l 0 > nth a2 l 0 . It should be solve by lia.But it is not not solving. What could be the reason?
You cannot prove that your hypotheses lead to a contradiction. Here's a simple example:
Goal nth 0  0 > nth 1  0. Proof. cbn; auto. Qed.
How it possibel? nth 0  0 means value at 0 index and nth 1 0 means value at 1 index. From this i conclude that two different indexes (0& 1) are present in the list. It means two elements are present in the list and its length is 2. In hypothesis i have length 1. Therefore it is contra statement.
You forgot the role of the
nth 1  x is equal to
You should consider adding hypotheses like
a1 < length l, which reduces to
Ok ,thank you.If i consider that both indexes are less than length then it can be prove that above is contra statement?
Last updated: Jan 27 2023 at 01:03 UTC