Stream: Coq users

Topic: One less than other

zohaze (Sep 08 2022 at 15:50):

Could we convert a = S b into a <= b by le_S command?

Emilio Jesús Gallego Arias (Sep 08 2022 at 15:55):

not likely, as if you replace a by S b in a <= b you get S b <= b

zohaze (Sep 08 2022 at 17:35):

What about this relation

S b > 0 ->
x = S a ->
a <= S b->
x <=b.

a b x are nat

zohaze (Sep 09 2022 at 14:59):

Is above relation between two variables correct?

Mukesh Tiwari (Sep 09 2022 at 15:57):

@zohaze I am assuming you are working with natural numbers. We can assume b = 0 (S b = 1 > 0 holds), assume a = 0 (x = 1), a <= S b (0 <= 1 holds) but your goal x <= b (1 <= 0) does not hold and therefore, it's not provable.

Mukesh Tiwari (Sep 09 2022 at 15:59):

Another way to think: you have assumed a <= S b and then you are trying to prove S a <= b (replace x by S a in the goal).

zohaze (Sep 09 2022 at 17:19):

Ok, thank you.

zohaze (Sep 10 2022 at 04:27):

@Emilio Jesús Gallego Arias . Its means we can prove whole relation is false because S b <= b is wrong.

zohaze (Sep 10 2022 at 04:55):

1) From ( a<=S b) could we prove (a<=b) ? (Reverse of le_S.)
2) From ( a<=S b) could we prove (S a<= b) ?

Last updated: Sep 23 2023 at 08:01 UTC