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?

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

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

Lessness has marked this topic as resolved.

Last updated: May 19 2024 at 16:02 UTC