Stream: Coq users

Topic: how to prove false


view this post on Zulip 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?

view this post on Zulip Pierre Castéran (May 29 2022 at 05:48):

You cannot prove that your hypotheses lead to a contradiction. Here's a simple example:

 Goal nth 0 [2] 0 > nth 1 [2] 0.
  Proof.  cbn; auto.  Qed.

view this post on Zulip pianke (May 29 2022 at 06:25):

How it possibel? nth 0 [2] 0 means value at 0 index and nth 1[2] 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.

view this post on Zulip Pierre Castéran (May 29 2022 at 06:34):

You forgot the role of the defaultargument of nth
https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html
nth 1 [2] x is equal to x, whichever x.

You should consider adding hypotheses like a1 < length l, which implies a1=0 under your hypotheses (same thing for a2)

view this post on Zulip pianke (May 31 2022 at 00:58):

Ok ,thank you.I I have to consider that both indexes are less than length l. If max -list l=0 & nth a1 l 0 > nth a2 l 0 then it is contra statement?


Last updated: Jun 20 2024 at 12:02 UTC