Lessness (Oct 15 2022 at 18:04): 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.
Lessness has marked this topic as resolved.
Last updated: Oct 12 2024 at 12:01 UTC