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

``````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).

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

#### zohaze (Feb 20 2024 at 16:39):

I have non empty list(k::t) and two hypothesis. H1: k <= list_max (k::t) & H2: list_max (k::t) <=k.
From these H1 and H2 , is it possible list_max (k::t) =k?

#### Michael Soegtrop (Feb 20 2024 at 16:57):

The `lia` tactic should be able to do this (assuming the type of k is some well known integer data type). E.g. `assert(list_max (k::t) =k) by lia.` should work.

#### Michael Soegtrop (Feb 20 2024 at 17:43):

@zohaze : btw: you can ask all of your above questions to lia. As long as you stay in the domain of linear integer arithmetic (+, -, S, <, <=, > >=, =, multiplication with constants) you can expect lia to give the right answer (prove provable things, fail on unprovable things). Here are a few examples:

``````Require Import Lia.

a = S b -> a <= b.
Proof.
intros.
Fail lia.
Abort.

(* the above is abviously wrong (a=4, b=3 is an example, but we can prove the opposite: *)

a = S b -> ~ (a <= b).
Proof.
intros.
lia.
Qed.

Example AskLia3: forall a b x,
S b > 0 ->
x = S a ->
a <= S b->
x <=b.
Proof.
intros.
Fail lia.
Abort.

Example AskLia4: forall a b x,
(* S b > 0 -> this is always true so useless - see below *)
x = S a ->
a <= S b->
x <= S (S b).
Proof.
intros.
lia.
Qed.