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):

Formally, if your context is:

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: Apr 16 2024 at 07:02 UTC