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

not likely, as if you replace `a`

by `S b`

in `a <= b`

you get `S b <= b`

What about this relation

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

a b x are nat

Is above relation between two variables correct?

@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.

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.

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

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

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?

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.

@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.
Example AskLia1: forall a b,
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: *)
Example AskLia2: forall a b,
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.
Example AskLia5: forall b,
S b > 0.
Proof.
intros.
lia.
Qed.
```

Last updated: Jun 14 2024 at 20:01 UTC