## Stream: Coq users

### Topic: how to prove false

#### pianke (May 29 2022 at 03:53):

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?

#### Pierre Castéran (May 29 2022 at 05:48):

`````` Goal nth 0  0 > nth 1  0.
Proof.  cbn; auto.  Qed.
``````

#### pianke (May 29 2022 at 06:25):

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.

#### Pierre Castéran (May 29 2022 at 06:34):

You forgot the role of the `default`argument of `nth`
https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html
`nth 1  x` is equal to `x`, whichever `x`.

You should consider adding hypotheses like `a1 < length l`, which reduces to `a1=0`(id. for `a2`)

#### pianke (May 31 2022 at 00:58):

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