```
a < S b
b2 = S b
b <= S a
```

a b b2 are nat. What information i can extract among the variables from above? Or existing relation may be prove wrong?

You can show `a <= b <= a+1`

- the relation to b2 should be obvious.

Sorry, I have (<=) relation between a and b . In this case below is possible

```
a <= S b
b < c
c = S a
```

What could be possible relation between a & c or false

Just chaining things together, you get `a <= S b < S c = S (S a)`

. From `S b < S (S a)`

you can get `b <= a`

, so `S b`

is either `a`

or `S a`

, similar to what you had before.

@sara lee : if you are unsure about such facts, you can easily test them with:

```
Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a <= b+1 <= a+1.
intros; lia.
```

You can check if this are the tightest bounds by increasing the left / decreasing the right bound and see if lia can still solve them.

If you are in the middle of a proof you can do

```
assert( a <= b+1 <= a+1 ) by lia.
```

`lia`

is a decision procedure for the domain it can handle (addition, multiplication with constants, relational operators in N and Z).

Thanks to all of you. I have asserted above relation in hypothesis. At the end i need (a=S c). Now how to extract this?

`a = S c`

is obviously wrong since you have `c = S a`

.

If it would be true, you could do:

```
Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a = S c.
intros; lia.
```

Indeed you can do:

```
Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a = S c -> False.
intros; lia.
```

which proves that `a = S c`

together with the other premises is incompatible.

Addition of a <= b in above three will change the result in any way? May i get some contra statement? I m in need of contra from these 4 relations.

@sara lee : I think I explained now in quite some detail how to ask `lia`

such questions rather than us. You should also be able to figure this out pencil and paper. It is not a good idea to try to prove things you don't understand on pencil and paper.

My last example on this: adding `a <= b`

does not lead to a contradiction:

```
Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a <= b -> False.
intros; lia.
```

The above fails. If the 4 statements would be contradicting, `lia`

could derive `False`

from it.

In some (true and false) proposition, lia command works (it reply). But some time gives message" cannot not find witness".

It means some information is required in decision making .e.g have single hypothesis H:= a<=b and want to prove S a <= b (which is incorrect).

To prove it wrong i have asserted (a <= S b due to H). Having correct relation and on its inverse basis could i prove it wrong ? Or what is the missing relation to do this?

Uh, what?

Well, to prove that the implication is wrong, you could indeed prove

`(a <= b -> S a <= b) -> False`

.

What do you even mean by "correct relation and inverse basis"? Also why are you even looking for missing relation?

EDIT: ouch, I forgot `forall.`

, it won't work without it.

I would prefer not to talk about goals with undeclared free variables or, more generally, without enough information about the context (as presented in this stream and a few others).

What we can prove is:

```
Goal (forall a b, a <= b -> S a <= b) -> False.
intro H; specialize (H 42 42); lia.
Qed.
```

But not:

```
Variables a b: nat.
Goal (a <= b -> S a <= b) -> False.
Fail lia.
Abort.
```

When asking questions, it's important to give all the necessary information about the context (preferably a syntactically correct script we could replay). Otherwise, we can't help.

A last remark: we are just talking about the implication `a <= b -> a < b`

!

```
Goal (forall a b, a <= b -> S a <= b) -> False.
intros;lia.
```

With specialize case it works but intros ; lia without specialize case it does not work (does not find witness).Why lia is not helpful here? Why we are giving particular case here? Want to prove it in this form

```
Theorem ab : forall a b :nat, a <= b -> S a <= b -> False.
```

The statement of `ab`

would mean "the proposition `(a <= b /\ a < b) `

never holds ".

It's clearly false.

In https://coq.inria.fr/distrib/current/refman/addendum/micromega.html#coq:tacn.lia, there is a description of the kind of formulas `lia`

and a few other similar tactics are supposed to solve. The considered goal (with an inner quantification) is not in that domain of application.

Thanks. First i import Lia, then copy lemma ab. Still i am unable to run code because of error "cannot find witness".

You are trying to prove a false statement. Take for example `a=1`

and `b=3`

.

(deleted)

Last updated: Dec 05 2023 at 12:01 UTC