## Stream: Coq users

### Topic: ✔ Searching for tactic

#### Lessness (Oct 15 2022 at 18:04):

How can one prove that set of linear inequalities in real numbers has no solution, using Coq? Is there some tactic that can do that?

#### Karl Palmskog (Oct 15 2022 at 18:06):

this may be the closest: https://github.com/validsdp/validsdp

#### Lessness (Oct 15 2022 at 18:31):

It seems that `lra` tactic can do that too, if one is careful.

``````Require Import Reals Psatz.
Open Scope R.

Theorem T01 x1 x2 mu1 mu2 mu3:
3 * x1 + 2 * x2 <= 18 + mu1 ->
-3 * x1 + x2 <= 6 + mu2 ->
4 * x1 - 3 * x2 <= 12 + mu3 ->
18 + mu1 < 0 ->
x1 >= 0 ->
x2 >= 0 ->
False.
Proof.
lra.
Qed.

Theorem T02 x1 x2 mu1 mu2 mu3:
3 * x1 + 2 * x2 <= 18 + mu1 ->
-3 * x1 + x2 <= 6 + mu2 ->
4 * x1 - 3 * x2 <= 12 + mu3 ->
18 + mu1 >= 0 ->
6 + mu2 >= 0 ->
12 + mu3 < 0 ->
9 + mu1 / 2 < -4 - mu3 / 3 ->
x1 >= 0 ->
x2 >= 0 ->
False.
Proof.
lra.
Qed.
``````

#### Notification Bot (Oct 16 2022 at 11:40):

Lessness has marked this topic as resolved.

Last updated: Sep 23 2023 at 07:01 UTC