## Stream: Coq users

### Topic: derive contra statement

#### zohaze (Oct 24 2022 at 14:10):

H: a < b-> S (S a) < S b .
I have above hypothesis ,which is wrong (correct is a < b-> S (S a) <= S b . )
From H ,i want to derive contra statement. Is it possible?

#### James Wood (Oct 24 2022 at 14:24):

Where do `a` and `b` come into scope? If they're already in scope before `H` is introduced, then this is not a contradictory context, as `(a, b)` could be `(0, 0)` and `H` could be by ex falso quodlibet.

#### James Wood (Oct 24 2022 at 14:33):

``````a : nat
b : nat
H : a < b -> S (S a) < S b
``````

then it's equivalent to the type `{ a : nat { b : nat & a < b -> S (S a) < S b } }`, which can be inhabited:

``````Require Import Lia.

Goal { a : nat { b : nat & a < b -> S (S a) < S b } }.
exists 0.
exists 0.
lia.
Defined.
``````

#### zohaze (Oct 25 2022 at 04:37):

Yes, a & b :nat already in scope before H is introduced. Secondly, S a < S b exist in hypothesis and i have reduced them into a < b to make them simpl. Now i can say (0,0 ) could not be happen, a < b -> S (S a) < S b is not f alse statement and it could occur.

#### Pierre Castéran (Oct 25 2022 at 04:55):

It’s difficult to help you if we don’t have a self-contained copy/pastable Coq script.
Coq is a formalism, and looking at an interactive proof attempt is more helpful than interpreting semi-formal statements like "happen", "occur".

#### zohaze (Oct 26 2022 at 07:15):

Ok.

``````a : nat
b : nat
H : S a < S b -> S (S a) < S b
``````

I want to ask that H statement may be prove False? (because correct is S a < S b -> S (S a) <= S b). Secondly,addition of another hypothesis a<=b may helpful. When run Lia command,i get message does not find witness. I just want to know , under what conditions H statement can be prove right or wrong ?

#### James Wood (Oct 26 2022 at 08:44):

It's still equivalent to what you had before.

``````Require Import Lia.

Goal { a : nat { b : nat & S a < S b -> S (S a) < S b } }.
exists 0.
exists 0.
lia.
Defined.
``````

#### James Wood (Oct 26 2022 at 08:47):

It doesn't make sense to call `H` "right" or "wrong". It is what it is, and true for certain values of `a` and `b`, and false for others. As an analogy, `a <= b` is true for some values of `a` and `b`, and false for others. It's not "right" or "wrong".

#### James Wood (Oct 26 2022 at 08:48):

If `H` were true for all values of `a` and `b`, it'd be a useless hypothesis.

Last updated: Sep 30 2023 at 16:01 UTC